summaryrefslogtreecommitdiff
path: root/theories/Arith
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Arith')
-rw-r--r--theories/Arith/Arith_base.v4
-rw-r--r--theories/Arith/Compare_dec.v6
-rw-r--r--theories/Arith/Div.v64
-rw-r--r--theories/Arith/Div2.v6
-rw-r--r--theories/Arith/EqNat.v12
-rw-r--r--theories/Arith/Even.v4
-rw-r--r--theories/Arith/Max.v11
-rw-r--r--theories/Arith/Min.v19
-rw-r--r--theories/Arith/Minus.v53
-rw-r--r--theories/Arith/Mult.v41
-rw-r--r--theories/Arith/Peano_dec.v2
-rw-r--r--theories/Arith/Plus.v12
-rw-r--r--theories/Arith/Wf_nat.v76
13 files changed, 203 insertions, 107 deletions
diff --git a/theories/Arith/Arith_base.v b/theories/Arith/Arith_base.v
index b076de2a..fbdf2a41 100644
--- a/theories/Arith/Arith_base.v
+++ b/theories/Arith/Arith_base.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Arith_base.v 11072 2008-06-08 16:13:37Z herbelin $ i*)
Require Export Le.
Require Export Lt.
@@ -18,3 +18,5 @@ Require Export Between.
Require Export Peano_dec.
Require Export Compare_dec.
Require Export Factorial.
+Require Export EqNat.
+Require Export Wf_nat.
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index b431fd05..e6cb5be4 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Compare_dec.v 9941 2007-07-05 12:42:35Z letouzey $ i*)
+(*i $Id: Compare_dec.v 10295 2007-11-06 22:46:21Z letouzey $ i*)
Require Import Le.
Require Import Lt.
@@ -170,7 +170,7 @@ Proof.
exact (lt_irrefl n).
intros.
apply not_gt.
- swap H.
+ contradict H.
destruct (nat_compare_gt n m); auto.
Qed.
@@ -184,7 +184,7 @@ Proof.
exact (lt_irrefl m).
intros.
apply not_lt.
- swap H.
+ contradict H.
destruct (nat_compare_lt n m); auto.
Qed.
diff --git a/theories/Arith/Div.v b/theories/Arith/Div.v
deleted file mode 100644
index 1dec34e2..00000000
--- a/theories/Arith/Div.v
+++ /dev/null
@@ -1,64 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(*i $Id: Div.v 9245 2006-10-17 12:53:34Z notin $ i*)
-
-(** Euclidean division *)
-
-V7only [Import nat_scope.].
-Open Local Scope nat_scope.
-
-Require Le.
-Require Euclid_def.
-Require Compare_dec.
-
-Implicit Variables Type n,a,b,q,r:nat.
-
-Fixpoint inf_dec [n:nat] : nat->bool :=
- [m:nat] Cases n m of
- O _ => true
- | (S n') O => false
- | (S n') (S m') => (inf_dec n' m')
- end.
-
-Theorem div1 : (b:nat)(gt b O)->(a:nat)(diveucl a b).
- Realizer Fix div1 {div1/2: nat->nat->diveucl :=
- [b,a]Cases a of
- O => (O,O)
- | (S n) =>
- let (q,r) = (div1 b n) in
- if (le_gt_dec b (S r)) then ((S q),O)
- else (q,(S r))
- end}.
- Program_all.
- Rewrite e.
- Replace b with (S r).
- Simpl.
- Elim plus_n_O; Auto with arith.
- Apply le_antisym; Auto with arith.
- Elim plus_n_Sm; Auto with arith.
-Qed.
-
-Theorem div2 : (b:nat)(gt b O)->(a:nat)(diveucl a b).
- Realizer Fix div1 {div1/2: nat->nat->diveucl :=
- [b,a]Cases a of
- O => (O,O)
- | (S n) =>
- let (q,r) = (div1 b n) in
- if (inf_dec b (S r)) :: :: { {(le b (S r))}+{(gt b (S r))} }
- then ((S q),O)
- else (q,(S r))
- end}.
- Program_all.
- Rewrite e.
- Replace b with (S r).
- Simpl.
- Elim plus_n_O; Auto with arith.
- Apply le_antisym; Auto with arith.
- Elim plus_n_Sm; Auto with arith.
-Qed.
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index c32759b2..1216a545 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Div2.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Div2.v 10625 2008-03-06 11:21:01Z notin $ i*)
Require Import Lt.
Require Import Plus.
@@ -169,12 +169,12 @@ Hint Resolve even_double double_even odd_double double_odd: arith.
Lemma even_2n : forall n, even n -> {p : nat | n = double p}.
Proof.
intros n H. exists (div2 n). auto with arith.
-Qed.
+Defined.
Lemma odd_S2n : forall n, odd n -> {p : nat | n = S (double p)}.
Proof.
intros n H. exists (div2 n). auto with arith.
-Qed.
+Defined.
(** Doubling before dividing by two brings back to the initial number. *)
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index 82d05e2c..a9244455 100644
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: EqNat.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: EqNat.v 9966 2007-07-10 23:54:53Z letouzey $ i*)
(** Equality on natural numbers *)
@@ -89,3 +89,13 @@ Proof.
intros n H1 H2. discriminate H2.
intros n H1 z H2 H3. case (H2 _ H3). reflexivity.
Defined.
+
+Lemma beq_nat_true : forall x y, beq_nat x y = true -> x=y.
+Proof.
+ induction x; destruct y; simpl; auto; intros; discriminate.
+Qed.
+
+Lemma beq_nat_false : forall x y, beq_nat x y = false -> x<>y.
+Proof.
+ induction x; destruct y; simpl; auto; intros; discriminate.
+Qed.
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index 83c0ce17..1484666b 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Even.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Even.v 10410 2007-12-31 13:11:55Z msozeau $ i*)
(** Here we define the predicates [even] and [odd] by mutual induction
and we prove the decidability and the exclusion of those predicates.
@@ -40,7 +40,7 @@ Proof.
induction n.
auto with arith.
elim IHn; auto with arith.
-Qed.
+Defined.
Lemma not_even_and_odd : forall n, even n -> odd n -> False.
Proof.
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index e0222e41..95af67f8 100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -6,9 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Max.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Max.v 9883 2007-06-07 18:44:59Z letouzey $ i*)
-Require Import Arith.
+Require Import Le.
Open Local Scope nat_scope.
@@ -30,6 +30,13 @@ Proof.
auto with arith.
Qed.
+Theorem max_assoc : forall m n p : nat, max m (max n p) = max (max m n) p.
+Proof.
+ induction m; destruct n; destruct p; trivial.
+ simpl.
+ auto using IHm.
+Qed.
+
Lemma max_comm : forall n m, max n m = max m n.
Proof.
induction n; induction m; simpl in |- *; auto with arith.
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
index db14e74b..aa009963 100644
--- a/theories/Arith/Min.v
+++ b/theories/Arith/Min.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Min.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Min.v 9660 2007-02-19 11:36:30Z notin $ i*)
Require Import Le.
@@ -25,11 +25,28 @@ Fixpoint min n m {struct n} : nat :=
(** * Simplifications of [min] *)
+Lemma min_0_l : forall n : nat, min 0 n = 0.
+Proof.
+ trivial.
+Qed.
+
+Lemma min_0_r : forall n : nat, min n 0 = 0.
+Proof.
+ destruct n; trivial.
+Qed.
+
Lemma min_SS : forall n m, S (min n m) = min (S n) (S m).
Proof.
auto with arith.
Qed.
+Lemma min_assoc : forall m n p : nat, min m (min n p) = min (min m n) p.
+Proof.
+ induction m; destruct n; destruct p; trivial.
+ simpl.
+ auto using (IHm n p).
+Qed.
+
Lemma min_comm : forall n m, min n m = min m n.
Proof.
induction n; induction m; simpl in |- *; auto with arith.
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index 2380c2de..b961886d 100644
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -6,13 +6,13 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Minus.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Minus.v 11072 2008-06-08 16:13:37Z herbelin $ i*)
(** [minus] (difference between two natural numbers) is defined in [Init/Peano.v] as:
<<
Fixpoint minus (n m:nat) {struct n} : nat :=
match n, m with
- | O, _ => 0
+ | O, _ => n
| S k, O => S k
| S k, S l => k - l
end
@@ -51,11 +51,18 @@ Qed.
(** * Diagonal *)
-Lemma minus_n_n : forall n, 0 = n - n.
+Lemma minus_diag : forall n, n - n = 0.
Proof.
induction n; simpl in |- *; auto with arith.
Qed.
-Hint Resolve minus_n_n: arith v62.
+
+Lemma minus_diag_reverse : forall n, 0 = n - n.
+Proof.
+ auto using minus_diag.
+Qed.
+Hint Resolve minus_diag_reverse: arith v62.
+
+Notation minus_n_n := minus_diag_reverse.
(** * Simplification *)
@@ -97,23 +104,39 @@ Hint Resolve le_plus_minus_r: arith v62.
(** * Relation with order *)
-Theorem le_minus : forall n m, n - m <= n.
+Theorem minus_le_compat_r : forall n m p : nat, n <= m -> n - p <= m - p.
Proof.
- intros i h; pattern i, h in |- *; apply nat_double_ind;
- [ auto
- | auto
- | intros m n H; simpl in |- *; apply le_trans with (m := m); auto ].
+ intros n m p; generalize n m; clear n m; induction p as [|p HI].
+ intros n m; rewrite <- (minus_n_O n); rewrite <- (minus_n_O m); trivial.
+
+ intros n m Hnm; apply le_elim_rel with (n:=n) (m:=m); auto with arith.
+ intros q r H _. simpl. auto using HI.
+Qed.
+
+Theorem minus_le_compat_l : forall n m p : nat, n <= m -> p - m <= p - n.
+Proof.
+ intros n m p; generalize n m; clear n m; induction p as [|p HI].
+ trivial.
+
+ intros n m Hnm; apply le_elim_rel with (n:=n) (m:=m); trivial.
+ intros q; destruct q; auto with arith.
+ simpl.
+ apply le_trans with (m := p - 0); [apply HI | rewrite <- minus_n_O];
+ auto with arith.
+
+ intros q r Hqr _. simpl. auto using HI.
+Qed.
+
+Corollary le_minus : forall n m, n - m <= n.
+Proof.
+ intros n m; rewrite minus_n_O; auto using minus_le_compat_l with arith.
Qed.
Lemma lt_minus : forall n m, m <= n -> 0 < m -> n - m < n.
Proof.
intros n m Le; pattern m, n in |- *; apply le_elim_rel; simpl in |- *;
- auto with arith.
- intros; absurd (0 < 0); auto with arith.
- intros p q lepq Hp gtp.
- elim (le_lt_or_eq 0 p); auto with arith.
- auto with arith.
- induction 1; elim minus_n_O; auto with arith.
+ auto using le_minus with arith.
+ intros; absurd (0 < 0); auto with arith.
Qed.
Hint Resolve lt_minus: arith v62.
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 2315e12c..a43579f9 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Mult.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Mult.v 11015 2008-05-28 20:06:42Z herbelin $ i*)
Require Export Plus.
Require Export Minus.
@@ -104,6 +104,43 @@ Proof.
Qed.
Hint Resolve mult_assoc: arith v62.
+(** ** Inversion lemmas *)
+
+Lemma mult_is_O : forall n m, n * m = 0 -> n = 0 \/ m = 0.
+Proof.
+ destruct n as [| n].
+ intros; left; trivial.
+
+ simpl; intros m H; right.
+ assert (H':m = 0 /\ n * m = 0) by apply (plus_is_O _ _ H).
+ destruct H'; trivial.
+Qed.
+
+Lemma mult_is_one : forall n m, n * m = 1 -> n = 1 /\ m = 1.
+Proof.
+ destruct n as [|n].
+ simpl; intros m H; elim (O_S _ H).
+
+ simpl; intros m H.
+ destruct (plus_is_one _ _ H) as [[Hm Hnm] | [Hm Hnm]].
+ rewrite Hm in H; simpl in H; rewrite mult_0_r in H; elim (O_S _ H).
+ rewrite Hm in Hnm; rewrite mult_1_r in Hnm; auto.
+Qed.
+
+(** ** Multiplication and successor *)
+
+Lemma mult_succ_l : forall n m:nat, S n * m = n * m + m.
+Proof.
+ intros; simpl. rewrite plus_comm. reflexivity.
+Qed.
+
+Lemma mult_succ_r : forall n m:nat, n * S m = n * m + n.
+Proof.
+ induction n as [| p H]; intro m; simpl.
+ reflexivity.
+ rewrite H, <- plus_n_Sm; apply f_equal; rewrite plus_assoc; reflexivity.
+Qed.
+
(** * Compatibility with orders *)
Lemma mult_O_le : forall n m, m = 0 \/ n <= m * n.
@@ -223,4 +260,4 @@ Qed.
Ltac tail_simpl :=
repeat rewrite <- plus_tail_plus; repeat rewrite <- mult_tail_mult;
- simpl in |- *. \ No newline at end of file
+ simpl in |- *.
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index 9ae80d79..cc970ae4 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Peano_dec.v 9941 2007-07-05 12:42:35Z letouzey $ i*)
+(*i $Id: Peano_dec.v 9698 2007-03-12 17:11:32Z letouzey $ i*)
Require Import Decidable.
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 74d0dc93..6d510447 100644
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Plus.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Plus.v 9750 2007-04-06 00:58:14Z letouzey $ i*)
(** Properties of addition. [add] is defined in [Init/Peano.v] as:
<<
@@ -198,16 +198,14 @@ Qed.
tail-recursive, whereas [plus] is not. This can be useful
when extracting programs. *)
-Fixpoint plus_acc q n {struct n} : nat :=
+Fixpoint tail_plus n m {struct n} : nat :=
match n with
- | O => q
- | S p => plus_acc (S q) p
+ | O => m
+ | S n => tail_plus n (S m)
end.
-Definition tail_plus n m := plus_acc m n.
-
Lemma plus_tail_plus : forall n m, n + m = tail_plus n m.
-unfold tail_plus in |- *; induction n as [| n IHn]; simpl in |- *; auto.
+induction n as [| n IHn]; simpl in |- *; auto.
intro m; rewrite <- IHn; simpl in |- *; auto.
Qed.
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index 11fcd161..6ad640eb 100644
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Wf_nat.v 9341 2006-11-06 13:08:10Z notin $ i*)
+(*i $Id: Wf_nat.v 11072 2008-06-08 16:13:37Z herbelin $ i*)
(** Well-founded relations and natural numbers *)
@@ -50,10 +50,12 @@ Defined.
the ML-like program for [induction_ltof1] is :
[[
- let induction_ltof1 F a = indrec ((f a)+1) a
- where rec indrec =
- function 0 -> (function a -> error)
- |(S m) -> (function a -> (F a (function y -> indrec y m)));;
+let induction_ltof1 f F a =
+ let rec indrec n k =
+ match n with
+ | O -> error
+ | S m -> F k (indrec m)
+ in indrec (f a + 1) a
]]
the ML-like program for [induction_ltof2] is :
@@ -210,3 +212,67 @@ Lemma well_founded_inv_rel_inv_lt_rel :
forall (A:Set) (F:A -> nat -> Prop), well_founded (inv_lt_rel A F).
intros; apply (well_founded_inv_lt_rel_compat A (inv_lt_rel A F) F); trivial.
Qed.
+
+(** A constructive proof that any non empty decidable subset of
+ natural numbers has a least element *)
+
+Set Implicit Arguments.
+
+Require Import Le.
+Require Import Compare_dec.
+Require Import Decidable.
+
+Definition has_unique_least_element (A:Type) (R:A->A->Prop) (P:A->Prop) :=
+ exists! x, P x /\ forall x', P x' -> R x x'.
+
+Lemma dec_inh_nat_subset_has_unique_least_element :
+ forall P:nat->Prop, (forall n, P n \/ ~ P n) ->
+ (exists n, P n) -> has_unique_least_element le P.
+Proof.
+ intros P Pdec (n0,HPn0).
+ assert
+ (forall n, (exists n', n'<n /\ P n' /\ forall n'', P n'' -> n'<=n'')
+ \/(forall n', P n' -> n<=n')).
+ induction n.
+ right.
+ intros n' Hn'.
+ apply le_O_n.
+ destruct IHn.
+ left; destruct H as (n', (Hlt', HPn')).
+ exists n'; split.
+ apply lt_S; assumption.
+ assumption.
+ destruct (Pdec n).
+ left; exists n; split.
+ apply lt_n_Sn.
+ split; assumption.
+ right.
+ intros n' Hltn'.
+ destruct (le_lt_eq_dec n n') as [Hltn|Heqn].
+ apply H; assumption.
+ assumption.
+ destruct H0.
+ rewrite Heqn; assumption.
+ destruct (H n0) as [(n,(Hltn,(Hmin,Huniqn)))|]; [exists n | exists n0];
+ repeat split;
+ assumption || intros n' (HPn',Hminn'); apply le_antisym; auto.
+Qed.
+
+Unset Implicit Arguments.
+
+(** [n]th iteration of the function [f] *)
+
+Fixpoint iter_nat (n:nat) (A:Type) (f:A -> A) (x:A) {struct n} : A :=
+ match n with
+ | O => x
+ | S n' => f (iter_nat n' A f x)
+ end.
+
+Theorem iter_nat_plus :
+ forall (n m:nat) (A:Type) (f:A -> A) (x:A),
+ iter_nat (n + m) A f x = iter_nat n A f (iter_nat m A f x).
+Proof.
+ simple induction n;
+ [ simpl in |- *; auto with arith
+ | intros; simpl in |- *; apply f_equal with (f := f); apply H ].
+Qed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 03:42:40 +0000