summaryrefslogtreecommitdiff
path: root/theories7/Arith
diff options
context:
space:
mode:
Diffstat (limited to 'theories7/Arith')
-rwxr-xr-xtheories7/Arith/Arith.v21
-rwxr-xr-xtheories7/Arith/Between.v185
-rw-r--r--theories7/Arith/Bool_nat.v43
-rwxr-xr-xtheories7/Arith/Compare.v60
-rwxr-xr-xtheories7/Arith/Compare_dec.v109
-rwxr-xr-xtheories7/Arith/Div.v64
-rw-r--r--theories7/Arith/Div2.v174
-rwxr-xr-xtheories7/Arith/EqNat.v78
-rw-r--r--theories7/Arith/Euclid.v65
-rw-r--r--theories7/Arith/Even.v310
-rw-r--r--theories7/Arith/Factorial.v51
-rwxr-xr-xtheories7/Arith/Gt.v149
-rwxr-xr-xtheories7/Arith/Le.v122
-rwxr-xr-xtheories7/Arith/Lt.v176
-rwxr-xr-xtheories7/Arith/Max.v87
-rwxr-xr-xtheories7/Arith/Min.v84
-rwxr-xr-xtheories7/Arith/Minus.v120
-rwxr-xr-xtheories7/Arith/Mult.v224
-rwxr-xr-xtheories7/Arith/Peano_dec.v36
-rwxr-xr-xtheories7/Arith/Plus.v223
-rwxr-xr-xtheories7/Arith/Wf_nat.v200
21 files changed, 0 insertions, 2581 deletions
diff --git a/theories7/Arith/Arith.v b/theories7/Arith/Arith.v
deleted file mode 100755
index 181fadbc..00000000
--- a/theories7/Arith/Arith.v
+++ /dev/null
@@ -1,21 +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: Arith.v,v 1.1.2.1 2004/07/16 19:31:23 herbelin Exp $ i*)
-
-Require Export Le.
-Require Export Lt.
-Require Export Plus.
-Require Export Gt.
-Require Export Minus.
-Require Export Mult.
-Require Export Between.
-Require Export Minus.
-Require Export Peano_dec.
-Require Export Compare_dec.
-Require Export Factorial.
diff --git a/theories7/Arith/Between.v b/theories7/Arith/Between.v
deleted file mode 100755
index b3fef325..00000000
--- a/theories7/Arith/Between.v
+++ /dev/null
@@ -1,185 +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: Between.v,v 1.1.2.1 2004/07/16 19:31:23 herbelin Exp $ i*)
-
-Require Le.
-Require Lt.
-
-V7only [Import nat_scope.].
-Open Local Scope nat_scope.
-
-Implicit Variables Type k,l,p,q,r:nat.
-
-Section Between.
-Variables P,Q : nat -> Prop.
-
-Inductive between [k:nat] : nat -> Prop
- := bet_emp : (between k k)
- | bet_S : (l:nat)(between k l)->(P l)->(between k (S l)).
-
-Hint constr_between : arith v62 := Constructors between.
-
-Lemma bet_eq : (k,l:nat)(l=k)->(between k l).
-Proof.
-NewInduction 1; Auto with arith.
-Qed.
-
-Hints Resolve bet_eq : arith v62.
-
-Lemma between_le : (k,l:nat)(between k l)->(le k l).
-Proof.
-NewInduction 1; Auto with arith.
-Qed.
-Hints Immediate between_le : arith v62.
-
-Lemma between_Sk_l : (k,l:nat)(between k l)->(le (S k) l)->(between (S k) l).
-Proof.
-NewInduction 1.
-Intros; Absurd (le (S k) k); Auto with arith.
-NewDestruct H; Auto with arith.
-Qed.
-Hints Resolve between_Sk_l : arith v62.
-
-Lemma between_restr :
- (k,l,m:nat)(le k l)->(le l m)->(between k m)->(between l m).
-Proof.
-NewInduction 1; Auto with arith.
-Qed.
-
-Inductive exists [k:nat] : nat -> Prop
- := exists_S : (l:nat)(exists k l)->(exists k (S l))
- | exists_le: (l:nat)(le k l)->(Q l)->(exists k (S l)).
-
-Hint constr_exists : arith v62 := Constructors exists.
-
-Lemma exists_le_S : (k,l:nat)(exists k l)->(le (S k) l).
-Proof.
-NewInduction 1; Auto with arith.
-Qed.
-
-Lemma exists_lt : (k,l:nat)(exists k l)->(lt k l).
-Proof exists_le_S.
-Hints Immediate exists_le_S exists_lt : arith v62.
-
-Lemma exists_S_le : (k,l:nat)(exists k (S l))->(le k l).
-Proof.
-Intros; Apply le_S_n; Auto with arith.
-Qed.
-Hints Immediate exists_S_le : arith v62.
-
-Definition in_int := [p,q,r:nat](le p r)/\(lt r q).
-
-Lemma in_int_intro : (p,q,r:nat)(le p r)->(lt r q)->(in_int p q r).
-Proof.
-Red; Auto with arith.
-Qed.
-Hints Resolve in_int_intro : arith v62.
-
-Lemma in_int_lt : (p,q,r:nat)(in_int p q r)->(lt p q).
-Proof.
-NewInduction 1; Intros.
-Apply le_lt_trans with r; Auto with arith.
-Qed.
-
-Lemma in_int_p_Sq :
- (p,q,r:nat)(in_int p (S q) r)->((in_int p q r) \/ <nat>r=q).
-Proof.
-NewInduction 1; Intros.
-Elim (le_lt_or_eq r q); Auto with arith.
-Qed.
-
-Lemma in_int_S : (p,q,r:nat)(in_int p q r)->(in_int p (S q) r).
-Proof.
-NewInduction 1;Auto with arith.
-Qed.
-Hints Resolve in_int_S : arith v62.
-
-Lemma in_int_Sp_q : (p,q,r:nat)(in_int (S p) q r)->(in_int p q r).
-Proof.
-NewInduction 1; Auto with arith.
-Qed.
-Hints Immediate in_int_Sp_q : arith v62.
-
-Lemma between_in_int : (k,l:nat)(between k l)->(r:nat)(in_int k l r)->(P r).
-Proof.
-NewInduction 1; Intros.
-Absurd (lt k k); Auto with arith.
-Apply in_int_lt with r; Auto with arith.
-Elim (in_int_p_Sq k l r); Intros; Auto with arith.
-Rewrite H2; Trivial with arith.
-Qed.
-
-Lemma in_int_between :
- (k,l:nat)(le k l)->((r:nat)(in_int k l r)->(P r))->(between k l).
-Proof.
-NewInduction 1; Auto with arith.
-Qed.
-
-Lemma exists_in_int :
- (k,l:nat)(exists k l)->(EX m:nat | (in_int k l m) & (Q m)).
-Proof.
-NewInduction 1.
-Case IHexists; Intros p inp Qp; Exists p; Auto with arith.
-Exists l; Auto with arith.
-Qed.
-
-Lemma in_int_exists : (k,l,r:nat)(in_int k l r)->(Q r)->(exists k l).
-Proof.
-NewDestruct 1; Intros.
-Elim H0; Auto with arith.
-Qed.
-
-Lemma between_or_exists :
- (k,l:nat)(le k l)->((n:nat)(in_int k l n)->((P n)\/(Q n)))
- ->((between k l)\/(exists k l)).
-Proof.
-NewInduction 1; Intros; Auto with arith.
-Elim IHle; Intro; Auto with arith.
-Elim (H0 m); Auto with arith.
-Qed.
-
-Lemma between_not_exists : (k,l:nat)(between k l)->
- ((n:nat)(in_int k l n) -> (P n) -> ~(Q n))
- -> ~(exists k l).
-Proof.
-NewInduction 1; Red; Intros.
-Absurd (lt k k); Auto with arith.
-Absurd (Q l); Auto with arith.
-Elim (exists_in_int k (S l)); Auto with arith; Intros l' inl' Ql'.
-Replace l with l'; Auto with arith.
-Elim inl'; Intros.
-Elim (le_lt_or_eq l' l); Auto with arith; Intros.
-Absurd (exists k l); Auto with arith.
-Apply in_int_exists with l'; Auto with arith.
-Qed.
-
-Inductive P_nth [init:nat] : nat->nat->Prop
- := nth_O : (P_nth init init O)
- | nth_S : (k,l:nat)(n:nat)(P_nth init k n)->(between (S k) l)
- ->(Q l)->(P_nth init l (S n)).
-
-Lemma nth_le : (init,l,n:nat)(P_nth init l n)->(le init l).
-Proof.
-NewInduction 1; Intros; Auto with arith.
-Apply le_trans with (S k); Auto with arith.
-Qed.
-
-Definition eventually := [n:nat](EX k:nat | (le k n) & (Q k)).
-
-Lemma event_O : (eventually O)->(Q O).
-Proof.
-NewInduction 1; Intros.
-Replace O with x; Auto with arith.
-Qed.
-
-End Between.
-
-Hints Resolve nth_O bet_S bet_emp bet_eq between_Sk_l exists_S exists_le
- in_int_S in_int_intro : arith v62.
-Hints Immediate in_int_Sp_q exists_le_S exists_S_le : arith v62.
diff --git a/theories7/Arith/Bool_nat.v b/theories7/Arith/Bool_nat.v
deleted file mode 100644
index c36f8f15..00000000
--- a/theories7/Arith/Bool_nat.v
+++ /dev/null
@@ -1,43 +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 *)
-(************************************************************************)
-
-(* $Id: Bool_nat.v,v 1.1.2.1 2004/07/16 19:31:23 herbelin Exp $ *)
-
-Require Export Compare_dec.
-Require Export Peano_dec.
-Require Sumbool.
-
-V7only [Import nat_scope.].
-Open Local Scope nat_scope.
-
-Implicit Variables Type m,n,x,y:nat.
-
-(** The decidability of equality and order relations over
- type [nat] give some boolean functions with the adequate specification. *)
-
-Definition notzerop := [n:nat] (sumbool_not ? ? (zerop n)).
-Definition lt_ge_dec : (x,y:nat){(lt x y)}+{(ge x y)} :=
- [n,m:nat] (sumbool_not ? ? (le_lt_dec m n)).
-
-Definition nat_lt_ge_bool :=
- [x,y:nat](bool_of_sumbool (lt_ge_dec x y)).
-Definition nat_ge_lt_bool :=
- [x,y:nat](bool_of_sumbool (sumbool_not ? ? (lt_ge_dec x y))).
-
-Definition nat_le_gt_bool :=
- [x,y:nat](bool_of_sumbool (le_gt_dec x y)).
-Definition nat_gt_le_bool :=
- [x,y:nat](bool_of_sumbool (sumbool_not ? ? (le_gt_dec x y))).
-
-Definition nat_eq_bool :=
- [x,y:nat](bool_of_sumbool (eq_nat_dec x y)).
-Definition nat_noteq_bool :=
- [x,y:nat](bool_of_sumbool (sumbool_not ? ? (eq_nat_dec x y))).
-
-Definition zerop_bool := [x:nat](bool_of_sumbool (zerop x)).
-Definition notzerop_bool := [x:nat](bool_of_sumbool (notzerop x)).
diff --git a/theories7/Arith/Compare.v b/theories7/Arith/Compare.v
deleted file mode 100755
index 1bca3fbe..00000000
--- a/theories7/Arith/Compare.v
+++ /dev/null
@@ -1,60 +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: Compare.v,v 1.1.2.1 2004/07/16 19:31:23 herbelin Exp $ i*)
-
-(** Equality is decidable on [nat] *)
-V7only [Import nat_scope.].
-Open Local Scope nat_scope.
-
-(*
-Lemma not_eq_sym : (A:Set)(p,q:A)(~p=q) -> ~(q=p).
-Proof sym_not_eq.
-Hints Immediate not_eq_sym : arith.
-*)
-Notation not_eq_sym := sym_not_eq.
-
-Implicit Variables Type m,n,p,q:nat.
-
-Require Arith.
-Require Peano_dec.
-Require Compare_dec.
-
-Definition le_or_le_S := le_le_S_dec.
-
-Definition compare := gt_eq_gt_dec.
-
-Lemma le_dec : (n,m:nat) {le n m} + {le m n}.
-Proof le_ge_dec.
-
-Definition lt_or_eq := [n,m:nat]{(gt m n)}+{n=m}.
-
-Lemma le_decide : (n,m:nat)(le n m)->(lt_or_eq n m).
-Proof le_lt_eq_dec.
-
-Lemma le_le_S_eq : (p,q:nat)(le p q)->((le (S p) q)\/(p=q)).
-Proof le_lt_or_eq.
-
-(* By special request of G. Kahn - Used in Group Theory *)
-Lemma discrete_nat : (m, n: nat) (lt m n) ->
- (S m) = n \/ (EX r: nat | n = (S (S (plus m r)))).
-Proof.
-Intros m n H.
-LApply (lt_le_S m n); Auto with arith.
-Intro H'; LApply (le_lt_or_eq (S m) n); Auto with arith.
-NewInduction 1; Auto with arith.
-Right; Exists (minus n (S (S m))); Simpl.
-Rewrite (plus_sym m (minus n (S (S m)))).
-Rewrite (plus_n_Sm (minus n (S (S m))) m).
-Rewrite (plus_n_Sm (minus n (S (S m))) (S m)).
-Rewrite (plus_sym (minus n (S (S m))) (S (S m))); Auto with arith.
-Qed.
-
-Require Export Wf_nat.
-
-Require Export Min.
diff --git a/theories7/Arith/Compare_dec.v b/theories7/Arith/Compare_dec.v
deleted file mode 100755
index 504c0562..00000000
--- a/theories7/Arith/Compare_dec.v
+++ /dev/null
@@ -1,109 +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: Compare_dec.v,v 1.1.2.1 2004/07/16 19:31:23 herbelin Exp $ i*)
-
-Require Le.
-Require Lt.
-Require Gt.
-Require Decidable.
-
-V7only [Import nat_scope.].
-Open Local Scope nat_scope.
-
-Implicit Variables Type m,n,x,y:nat.
-
-Definition zerop : (n:nat){n=O}+{lt O n}.
-NewDestruct n; Auto with arith.
-Defined.
-
-Definition lt_eq_lt_dec : (n,m:nat){(lt n m)}+{n=m}+{(lt m n)}.
-Proof.
-NewInduction n; Destruct m; Auto with arith.
-Intros m0; Elim (IHn m0); Auto with arith.
-NewInduction 1; Auto with arith.
-Defined.
-
-Lemma gt_eq_gt_dec : (n,m:nat)({(gt m n)}+{n=m})+{(gt n m)}.
-Proof lt_eq_lt_dec.
-
-Lemma le_lt_dec : (n,m:nat) {le n m} + {lt m n}.
-Proof.
-NewInduction n.
-Auto with arith.
-NewInduction m.
-Auto with arith.
-Elim (IHn m); Auto with arith.
-Defined.
-
-Definition le_le_S_dec : (n,m:nat) {le n m} + {le (S m) n}.
-Proof.
-Exact le_lt_dec.
-Defined.
-
-Definition le_ge_dec : (n,m:nat) {le n m} + {ge n m}.
-Proof.
-Intros; Elim (le_lt_dec n m); Auto with arith.
-Defined.
-
-Definition le_gt_dec : (n,m:nat){(le n m)}+{(gt n m)}.
-Proof.
-Exact le_lt_dec.
-Defined.
-
-Definition le_lt_eq_dec : (n,m:nat)(le n m)->({(lt n m)}+{n=m}).
-Proof.
-Intros; Elim (lt_eq_lt_dec n m); Auto with arith.
-Intros; Absurd (lt m n); Auto with arith.
-Defined.
-
-(** Proofs of decidability *)
-
-Theorem dec_le:(x,y:nat)(decidable (le x y)).
-Intros x y; Unfold decidable ; Elim (le_gt_dec x y); [
- Auto with arith
-| Intro; Right; Apply gt_not_le; Assumption].
-Qed.
-
-Theorem dec_lt:(x,y:nat)(decidable (lt x y)).
-Intros x y; Unfold lt; Apply dec_le.
-Qed.
-
-Theorem dec_gt:(x,y:nat)(decidable (gt x y)).
-Intros x y; Unfold gt; Apply dec_lt.
-Qed.
-
-Theorem dec_ge:(x,y:nat)(decidable (ge x y)).
-Intros x y; Unfold ge; Apply dec_le.
-Qed.
-
-Theorem not_eq : (x,y:nat) ~ x=y -> (lt x y) \/ (lt y x).
-Intros x y H; Elim (lt_eq_lt_dec x y); [
- Intros H1; Elim H1; [ Auto with arith | Intros H2; Absurd x=y; Assumption]
-| Auto with arith].
-Qed.
-
-
-Theorem not_le : (x,y:nat) ~(le x y) -> (gt x y).
-Intros x y H; Elim (le_gt_dec x y);
- [ Intros H1; Absurd (le x y); Assumption | Trivial with arith ].
-Qed.
-
-Theorem not_gt : (x,y:nat) ~(gt x y) -> (le x y).
-Intros x y H; Elim (le_gt_dec x y);
- [ Trivial with arith | Intros H1; Absurd (gt x y); Assumption].
-Qed.
-
-Theorem not_ge : (x,y:nat) ~(ge x y) -> (lt x y).
-Intros x y H; Exact (not_le y x H).
-Qed.
-
-Theorem not_lt : (x,y:nat) ~(lt x y) -> (ge x y).
-Intros x y H; Exact (not_gt y x H).
-Qed.
-
diff --git a/theories7/Arith/Div.v b/theories7/Arith/Div.v
deleted file mode 100755
index 59694628..00000000
--- a/theories7/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,v 1.1.2.1 2004/07/16 19:31:23 herbelin Exp $ 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/theories7/Arith/Div2.v b/theories7/Arith/Div2.v
deleted file mode 100644
index 8bd0160f..00000000
--- a/theories7/Arith/Div2.v
+++ /dev/null
@@ -1,174 +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: Div2.v,v 1.1.2.1 2004/07/16 19:31:24 herbelin Exp $ i*)
-
-Require Lt.
-Require Plus.
-Require Compare_dec.
-Require Even.
-
-V7only [Import nat_scope.].
-Open Local Scope nat_scope.
-
-Implicit Variables Type n:nat.
-
-(** Here we define [n/2] and prove some of its properties *)
-
-Fixpoint div2 [n:nat] : nat :=
- Cases n of
- O => O
- | (S O) => O
- | (S (S n')) => (S (div2 n'))
- end.
-
-(** Since [div2] is recursively defined on [0], [1] and [(S (S n))], it is
- useful to prove the corresponding induction principle *)
-
-Lemma ind_0_1_SS : (P:nat->Prop)
- (P O) -> (P (S O)) -> ((n:nat)(P n)->(P (S (S n)))) -> (n:nat)(P n).
-Proof.
-Intros.
-Cut (n:nat)(P n)/\(P (S n)).
-Intros. Elim (H2 n). Auto with arith.
-
-NewInduction n0. Auto with arith.
-Intros. Elim IHn0; Auto with arith.
-Qed.
-
-(** [0 <n => n/2 < n] *)
-
-Lemma lt_div2 : (n:nat) (lt O n) -> (lt (div2 n) n).
-Proof.
-Intro n. Pattern n. Apply ind_0_1_SS.
-Intro. Inversion H.
-Auto with arith.
-Intros. Simpl.
-Case (zerop n0).
-Intro. Rewrite e. Auto with arith.
-Auto with arith.
-Qed.
-
-Hints Resolve lt_div2 : arith.
-
-(** Properties related to the parity *)
-
-Lemma even_odd_div2 : (n:nat)
- ((even n)<->(div2 n)=(div2 (S n))) /\ ((odd n)<->(S (div2 n))=(div2 (S n))).
-Proof.
-Intro n. Pattern n. Apply ind_0_1_SS.
-(* n = 0 *)
-Split. Split; Auto with arith.
-Split. Intro H. Inversion H.
-Intro H. Absurd (S (div2 O))=(div2 (S O)); Auto with arith.
-(* n = 1 *)
-Split. Split. Intro. Inversion H. Inversion H1.
-Intro H. Absurd (div2 (S O))=(div2 (S (S O))).
-Simpl. Discriminate. Assumption.
-Split; Auto with arith.
-(* n = (S (S n')) *)
-Intros. Decompose [and] H. Unfold iff in H0 H1.
-Decompose [and] H0. Decompose [and] H1. Clear H H0 H1.
-Split; Split; Auto with arith.
-Intro H. Inversion H. Inversion H1.
-Change (S (div2 n0))=(S (div2 (S n0))). Auto with arith.
-Intro H. Inversion H. Inversion H1.
-Change (S (S (div2 n0)))=(S (div2 (S n0))). Auto with arith.
-Qed.
-
-(** Specializations *)
-
-Lemma even_div2 : (n:nat) (even n) -> (div2 n)=(div2 (S n)).
-Proof [n:nat](proj1 ? ? (proj1 ? ? (even_odd_div2 n))).
-
-Lemma div2_even : (n:nat) (div2 n)=(div2 (S n)) -> (even n).
-Proof [n:nat](proj2 ? ? (proj1 ? ? (even_odd_div2 n))).
-
-Lemma odd_div2 : (n:nat) (odd n) -> (S (div2 n))=(div2 (S n)).
-Proof [n:nat](proj1 ? ? (proj2 ? ? (even_odd_div2 n))).
-
-Lemma div2_odd : (n:nat) (S (div2 n))=(div2 (S n)) -> (odd n).
-Proof [n:nat](proj2 ? ? (proj2 ? ? (even_odd_div2 n))).
-
-Hints Resolve even_div2 div2_even odd_div2 div2_odd : arith.
-
-(** Properties related to the double ([2n]) *)
-
-Definition double := [n:nat](plus n n).
-
-Hints Unfold double : arith.
-
-Lemma double_S : (n:nat) (double (S n))=(S (S (double n))).
-Proof.
-Intro. Unfold double. Simpl. Auto with arith.
-Qed.
-
-Lemma double_plus : (m,n:nat) (double (plus m n))=(plus (double m) (double n)).
-Proof.
-Intros m n. Unfold double.
-Do 2 Rewrite -> plus_assoc_r. Rewrite -> (plus_permute n).
-Reflexivity.
-Qed.
-
-Hints Resolve double_S : arith.
-
-Lemma even_odd_double : (n:nat)
- ((even n)<->n=(double (div2 n))) /\ ((odd n)<->n=(S (double (div2 n)))).
-Proof.
-Intro n. Pattern n. Apply ind_0_1_SS.
-(* n = 0 *)
-Split; Split; Auto with arith.
-Intro H. Inversion H.
-(* n = 1 *)
-Split; Split; Auto with arith.
-Intro H. Inversion H. Inversion H1.
-(* n = (S (S n')) *)
-Intros. Decompose [and] H. Unfold iff in H0 H1.
-Decompose [and] H0. Decompose [and] H1. Clear H H0 H1.
-Split; Split.
-Intro H. Inversion H. Inversion H1.
-Simpl. Rewrite (double_S (div2 n0)). Auto with arith.
-Simpl. Rewrite (double_S (div2 n0)). Intro H. Injection H. Auto with arith.
-Intro H. Inversion H. Inversion H1.
-Simpl. Rewrite (double_S (div2 n0)). Auto with arith.
-Simpl. Rewrite (double_S (div2 n0)). Intro H. Injection H. Auto with arith.
-Qed.
-
-
-(** Specializations *)
-
-Lemma even_double : (n:nat) (even n) -> n=(double (div2 n)).
-Proof [n:nat](proj1 ? ? (proj1 ? ? (even_odd_double n))).
-
-Lemma double_even : (n:nat) n=(double (div2 n)) -> (even n).
-Proof [n:nat](proj2 ? ? (proj1 ? ? (even_odd_double n))).
-
-Lemma odd_double : (n:nat) (odd n) -> n=(S (double (div2 n))).
-Proof [n:nat](proj1 ? ? (proj2 ? ? (even_odd_double n))).
-
-Lemma double_odd : (n:nat) n=(S (double (div2 n))) -> (odd n).
-Proof [n:nat](proj2 ? ? (proj2 ? ? (even_odd_double n))).
-
-Hints Resolve even_double double_even odd_double double_odd : arith.
-
-(** Application:
- - if [n] is even then there is a [p] such that [n = 2p]
- - if [n] is odd then there is a [p] such that [n = 2p+1]
-
- (Immediate: it is [n/2]) *)
-
-Lemma even_2n : (n:nat) (even n) -> { p:nat | n=(double p) }.
-Proof.
-Intros n H. Exists (div2 n). Auto with arith.
-Qed.
-
-Lemma odd_S2n : (n:nat) (odd n) -> { p:nat | n=(S (double p)) }.
-Proof.
-Intros n H. Exists (div2 n). Auto with arith.
-Qed.
-
diff --git a/theories7/Arith/EqNat.v b/theories7/Arith/EqNat.v
deleted file mode 100755
index 9f5ee7ee..00000000
--- a/theories7/Arith/EqNat.v
+++ /dev/null
@@ -1,78 +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: EqNat.v,v 1.1.2.1 2004/07/16 19:31:24 herbelin Exp $ i*)
-
-(** Equality on natural numbers *)
-
-V7only [Import nat_scope.].
-Open Local Scope nat_scope.
-
-Implicit Variables Type m,n,x,y:nat.
-
-Fixpoint eq_nat [n:nat] : nat -> Prop :=
- [m:nat]Cases n m of
- O O => True
- | O (S _) => False
- | (S _) O => False
- | (S n1) (S m1) => (eq_nat n1 m1)
- end.
-
-Theorem eq_nat_refl : (n:nat)(eq_nat n n).
-NewInduction n; Simpl; Auto.
-Qed.
-Hints Resolve eq_nat_refl : arith v62.
-
-Theorem eq_eq_nat : (n,m:nat)(n=m)->(eq_nat n m).
-NewInduction 1; Trivial with arith.
-Qed.
-Hints Immediate eq_eq_nat : arith v62.
-
-Theorem eq_nat_eq : (n,m:nat)(eq_nat n m)->(n=m).
-NewInduction n; NewInduction m; Simpl; Contradiction Orelse Auto with arith.
-Qed.
-Hints Immediate eq_nat_eq : arith v62.
-
-Theorem eq_nat_elim : (n:nat)(P:nat->Prop)(P n)->(m:nat)(eq_nat n m)->(P m).
-Intros; Replace m with n; Auto with arith.
-Qed.
-
-Theorem eq_nat_decide : (n,m:nat){(eq_nat n m)}+{~(eq_nat n m)}.
-NewInduction n.
-NewDestruct m.
-Auto with arith.
-Intros; Right; Red; Trivial with arith.
-NewDestruct m.
-Right; Red; Auto with arith.
-Intros.
-Simpl.
-Apply IHn.
-Defined.
-
-Fixpoint beq_nat [n:nat] : nat -> bool :=
- [m:nat]Cases n m of
- O O => true
- | O (S _) => false
- | (S _) O => false
- | (S n1) (S m1) => (beq_nat n1 m1)
- end.
-
-Lemma beq_nat_refl : (x:nat)true=(beq_nat x x).
-Proof.
- Intro x; NewInduction x; Simpl; Auto.
-Qed.
-
-Definition beq_nat_eq : (x,y:nat)true=(beq_nat x y)->x=y.
-Proof.
- Double Induction x y; Simpl.
- Reflexivity.
- Intros; Discriminate H0.
- Intros; Discriminate H0.
- Intros; Case (H0 ? H1); Reflexivity.
-Defined.
-
diff --git a/theories7/Arith/Euclid.v b/theories7/Arith/Euclid.v
deleted file mode 100644
index adeaf713..00000000
--- a/theories7/Arith/Euclid.v
+++ /dev/null
@@ -1,65 +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: Euclid.v,v 1.1.2.1 2004/07/16 19:31:24 herbelin Exp $ i*)
-
-Require Mult.
-Require Compare_dec.
-Require Wf_nat.
-
-V7only [Import nat_scope.].
-Open Local Scope nat_scope.
-
-Implicit Variables Type a,b,n,q,r:nat.
-
-Inductive diveucl [a,b:nat] : Set
- := divex : (q,r:nat)(gt b r)->(a=(plus (mult q b) r))->(diveucl a b).
-
-
-Lemma eucl_dev : (b:nat)(gt b O)->(a:nat)(diveucl a b).
-Intros b H a; Pattern a; Apply gt_wf_rec; Intros n H0.
-Elim (le_gt_dec b n).
-Intro lebn.
-Elim (H0 (minus n b)); Auto with arith.
-Intros q r g e.
-Apply divex with (S q) r; Simpl; Auto with arith.
-Elim plus_assoc_l.
-Elim e; Auto with arith.
-Intros gtbn.
-Apply divex with O n; Simpl; Auto with arith.
-Qed.
-
-Lemma quotient : (b:nat)(gt b O)->
- (a:nat){q:nat|(EX r:nat | (a=(plus (mult q b) r))/\(gt b r))}.
-Intros b H a; Pattern a; Apply gt_wf_rec; Intros n H0.
-Elim (le_gt_dec b n).
-Intro lebn.
-Elim (H0 (minus n b)); Auto with arith.
-Intros q Hq; Exists (S q).
-Elim Hq; Intros r Hr.
-Exists r; Simpl; Elim Hr; Intros.
-Elim plus_assoc_l.
-Elim H1; Auto with arith.
-Intros gtbn.
-Exists O; Exists n; Simpl; Auto with arith.
-Qed.
-
-Lemma modulo : (b:nat)(gt b O)->
- (a:nat){r:nat|(EX q:nat | (a=(plus (mult q b) r))/\(gt b r))}.
-Intros b H a; Pattern a; Apply gt_wf_rec; Intros n H0.
-Elim (le_gt_dec b n).
-Intro lebn.
-Elim (H0 (minus n b)); Auto with arith.
-Intros r Hr; Exists r.
-Elim Hr; Intros q Hq.
-Elim Hq; Intros; Exists (S q); Simpl.
-Elim plus_assoc_l.
-Elim H1; Auto with arith.
-Intros gtbn.
-Exists n; Exists O; Simpl; Auto with arith.
-Qed.
diff --git a/theories7/Arith/Even.v b/theories7/Arith/Even.v
deleted file mode 100644
index bcc413f5..00000000
--- a/theories7/Arith/Even.v
+++ /dev/null
@@ -1,310 +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: Even.v,v 1.1.2.1 2004/07/16 19:31:24 herbelin Exp $ i*)
-
-(** Here we define the predicates [even] and [odd] by mutual induction
- and we prove the decidability and the exclusion of those predicates.
- The main results about parity are proved in the module Div2. *)
-
-V7only [Import nat_scope.].
-Open Local Scope nat_scope.
-
-Implicit Variables Type m,n:nat.
-
-Inductive even : nat->Prop :=
- even_O : (even O)
- | even_S : (n:nat)(odd n)->(even (S n))
-with odd : nat->Prop :=
- odd_S : (n:nat)(even n)->(odd (S n)).
-
-Hint constr_even : arith := Constructors even.
-Hint constr_odd : arith := Constructors odd.
-
-Lemma even_or_odd : (n:nat) (even n)\/(odd n).
-Proof.
-NewInduction n.
-Auto with arith.
-Elim IHn; Auto with arith.
-Qed.
-
-Lemma even_odd_dec : (n:nat) { (even n) }+{ (odd n) }.
-Proof.
-NewInduction n.
-Auto with arith.
-Elim IHn; Auto with arith.
-Qed.
-
-Lemma not_even_and_odd : (n:nat) (even n) -> (odd n) -> False.
-Proof.
-NewInduction n.
-Intros. Inversion H0.
-Intros. Inversion H. Inversion H0. Auto with arith.
-Qed.
-
-Lemma even_plus_aux:
- (n,m:nat)
- (iff (odd (plus n m)) (odd n) /\ (even m) \/ (even n) /\ (odd m)) /\
- (iff (even (plus n m)) (even n) /\ (even m) \/ (odd n) /\ (odd m)).
-Proof.
-Intros n; Elim n; Simpl; Auto with arith.
-Intros m; Split; Auto.
-Split.
-Intros H; Right; Split; Auto with arith.
-Intros H'; Case H'; Auto with arith.
-Intros H'0; Elim H'0; Intros H'1 H'2; Inversion H'1.
-Intros H; Elim H; Auto.
-Split; Auto with arith.
-Intros H'; Elim H'; Auto with arith.
-Intros H; Elim H; Auto.
-Intros H'0; Elim H'0; Intros H'1 H'2; Inversion H'1.
-Intros n0 H' m; Elim (H' m); Intros H'1 H'2; Elim H'1; Intros E1 E2; Elim H'2;
- Intros E3 E4; Clear H'1 H'2.
-Split; Split.
-Intros H'0; Case E3.
-Inversion H'0; Auto.
-Intros H; Elim H; Intros H0 H1; Clear H; Auto with arith.
-Intros H; Elim H; Intros H0 H1; Clear H; Auto with arith.
-Intros H'0; Case H'0; Intros C0; Case C0; Intros C1 C2.
-Apply odd_S.
-Apply E4; Left; Split; Auto with arith.
-Inversion C1; Auto.
-Apply odd_S.
-Apply E4; Right; Split; Auto with arith.
-Inversion C1; Auto.
-Intros H'0.
-Case E1.
-Inversion H'0; Auto.
-Intros H; Elim H; Intros H0 H1; Clear H; Auto with arith.
-Intros H; Elim H; Intros H0 H1; Clear H; Auto with arith.
-Intros H'0; Case H'0; Intros C0; Case C0; Intros C1 C2.
-Apply even_S.
-Apply E2; Left; Split; Auto with arith.
-Inversion C1; Auto.
-Apply even_S.
-Apply E2; Right; Split; Auto with arith.
-Inversion C1; Auto.
-Qed.
-
-Lemma even_even_plus : (n,m:nat) (even n) -> (even m) -> (even (plus n m)).
-Proof.
-Intros n m; Case (even_plus_aux n m).
-Intros H H0; Case H0; Auto.
-Qed.
-
-Lemma odd_even_plus : (n,m:nat) (odd n) -> (odd m) -> (even (plus n m)).
-Proof.
-Intros n m; Case (even_plus_aux n m).
-Intros H H0; Case H0; Auto.
-Qed.
-
-Lemma even_plus_even_inv_r :
- (n,m:nat) (even (plus n m)) -> (even n) -> (even m).
-Proof.
-Intros n m H; Case (even_plus_aux n m).
-Intros H' H'0; Elim H'0.
-Intros H'1; Case H'1; Auto.
-Intros H0; Elim H0; Auto.
-Intros H0 H1 H2; Case (not_even_and_odd n); Auto.
-Case H0; Auto.
-Qed.
-
-Lemma even_plus_even_inv_l :
- (n,m:nat) (even (plus n m)) -> (even m) -> (even n).
-Proof.
-Intros n m H; Case (even_plus_aux n m).
-Intros H' H'0; Elim H'0.
-Intros H'1; Case H'1; Auto.
-Intros H0; Elim H0; Auto.
-Intros H0 H1 H2; Case (not_even_and_odd m); Auto.
-Case H0; Auto.
-Qed.
-
-Lemma even_plus_odd_inv_r : (n,m:nat) (even (plus n m)) -> (odd n) -> (odd m).
-Proof.
-Intros n m H; Case (even_plus_aux n m).
-Intros H' H'0; Elim H'0.
-Intros H'1; Case H'1; Auto.
-Intros H0 H1 H2; Case (not_even_and_odd n); Auto.
-Case H0; Auto.
-Intros H0; Case H0; Auto.
-Qed.
-
-Lemma even_plus_odd_inv_l : (n,m:nat) (even (plus n m)) -> (odd m) -> (odd n).
-Proof.
-Intros n m H; Case (even_plus_aux n m).
-Intros H' H'0; Elim H'0.
-Intros H'1; Case H'1; Auto.
-Intros H0 H1 H2; Case (not_even_and_odd m); Auto.
-Case H0; Auto.
-Intros H0; Case H0; Auto.
-Qed.
-Hints Resolve even_even_plus odd_even_plus :arith.
-
-Lemma odd_plus_l : (n,m:nat) (odd n) -> (even m) -> (odd (plus n m)).
-Proof.
-Intros n m; Case (even_plus_aux n m).
-Intros H; Case H; Auto.
-Qed.
-
-Lemma odd_plus_r : (n,m:nat) (even n) -> (odd m) -> (odd (plus n m)).
-Proof.
-Intros n m; Case (even_plus_aux n m).
-Intros H; Case H; Auto.
-Qed.
-
-Lemma odd_plus_even_inv_l : (n,m:nat) (odd (plus n m)) -> (odd m) -> (even n).
-Proof.
-Intros n m H; Case (even_plus_aux n m).
-Intros H' H'0; Elim H'.
-Intros H'1; Case H'1; Auto.
-Intros H0 H1 H2; Case (not_even_and_odd m); Auto.
-Case H0; Auto.
-Intros H0; Case H0; Auto.
-Qed.
-
-Lemma odd_plus_even_inv_r : (n,m:nat) (odd (plus n m)) -> (odd n) -> (even m).
-Proof.
-Intros n m H; Case (even_plus_aux n m).
-Intros H' H'0; Elim H'.
-Intros H'1; Case H'1; Auto.
-Intros H0; Case H0; Auto.
-Intros H0 H1 H2; Case (not_even_and_odd n); Auto.
-Case H0; Auto.
-Qed.
-
-Lemma odd_plus_odd_inv_l : (n,m:nat) (odd (plus n m)) -> (even m) -> (odd n).
-Proof.
-Intros n m H; Case (even_plus_aux n m).
-Intros H' H'0; Elim H'.
-Intros H'1; Case H'1; Auto.
-Intros H0; Case H0; Auto.
-Intros H0 H1 H2; Case (not_even_and_odd m); Auto.
-Case H0; Auto.
-Qed.
-
-Lemma odd_plus_odd_inv_r : (n,m:nat) (odd (plus n m)) -> (even n) -> (odd m).
-Proof.
-Intros n m H; Case (even_plus_aux n m).
-Intros H' H'0; Elim H'.
-Intros H'1; Case H'1; Auto.
-Intros H0 H1 H2; Case (not_even_and_odd n); Auto.
-Case H0; Auto.
-Intros H0; Case H0; Auto.
-Qed.
-Hints Resolve odd_plus_l odd_plus_r :arith.
-
-Lemma even_mult_aux :
- (n,m:nat)
- (iff (odd (mult n m)) (odd n) /\ (odd m)) /\
- (iff (even (mult n m)) (even n) \/ (even m)).
-Proof.
-Intros n; Elim n; Simpl; Auto with arith.
-Intros m; Split; Split; Auto with arith.
-Intros H'; Inversion H'.
-Intros H'; Elim H'; Auto.
-Intros n0 H' m; Split; Split; Auto with arith.
-Intros H'0.
-Elim (even_plus_aux m (mult n0 m)); Intros H'3 H'4; Case H'3; Intros H'1 H'2;
- Case H'1; Auto.
-Intros H'5; Elim H'5; Intros H'6 H'7; Auto with arith.
-Split; Auto with arith.
-Case (H' m).
-Intros H'8 H'9; Case H'9.
-Intros H'10; Case H'10; Auto with arith.
-Intros H'11 H'12; Case (not_even_and_odd m); Auto with arith.
-Intros H'5; Elim H'5; Intros H'6 H'7; Case (not_even_and_odd (mult n0 m)); Auto.
-Case (H' m).
-Intros H'8 H'9; Case H'9; Auto.
-Intros H'0; Elim H'0; Intros H'1 H'2; Clear H'0.
-Elim (even_plus_aux m (mult n0 m)); Auto.
-Intros H'0 H'3.
-Elim H'0.
-Intros H'4 H'5; Apply H'5; Auto.
-Left; Split; Auto with arith.
-Case (H' m).
-Intros H'6 H'7; Elim H'7.
-Intros H'8 H'9; Apply H'9.
-Left.
-Inversion H'1; Auto.
-Intros H'0.
-Elim (even_plus_aux m (mult n0 m)); Intros H'3 H'4; Case H'4.
-Intros H'1 H'2.
-Elim H'1; Auto.
-Intros H; Case H; Auto.
-Intros H'5; Elim H'5; Intros H'6 H'7; Auto with arith.
-Left.
-Case (H' m).
-Intros H'8; Elim H'8.
-Intros H'9; Elim H'9; Auto with arith.
-Intros H'0; Elim H'0; Intros H'1.
-Case (even_or_odd m); Intros H'2.
-Apply even_even_plus; Auto.
-Case (H' m).
-Intros H H0; Case H0; Auto.
-Apply odd_even_plus; Auto.
-Inversion H'1; Case (H' m); Auto.
-Intros H1; Case H1; Auto.
-Apply even_even_plus; Auto.
-Case (H' m).
-Intros H H0; Case H0; Auto.
-Qed.
-
-Lemma even_mult_l : (n,m:nat) (even n) -> (even (mult n m)).
-Proof.
-Intros n m; Case (even_mult_aux n m); Auto.
-Intros H H0; Case H0; Auto.
-Qed.
-
-Lemma even_mult_r: (n,m:nat) (even m) -> (even (mult n m)).
-Proof.
-Intros n m; Case (even_mult_aux n m); Auto.
-Intros H H0; Case H0; Auto.
-Qed.
-Hints Resolve even_mult_l even_mult_r :arith.
-
-Lemma even_mult_inv_r: (n,m:nat) (even (mult n m)) -> (odd n) -> (even m).
-Proof.
-Intros n m H' H'0.
-Case (even_mult_aux n m).
-Intros H'1 H'2; Elim H'2.
-Intros H'3; Elim H'3; Auto.
-Intros H; Case (not_even_and_odd n); Auto.
-Qed.
-
-Lemma even_mult_inv_l : (n,m:nat) (even (mult n m)) -> (odd m) -> (even n).
-Proof.
-Intros n m H' H'0.
-Case (even_mult_aux n m).
-Intros H'1 H'2; Elim H'2.
-Intros H'3; Elim H'3; Auto.
-Intros H; Case (not_even_and_odd m); Auto.
-Qed.
-
-Lemma odd_mult : (n,m:nat) (odd n) -> (odd m) -> (odd (mult n m)).
-Proof.
-Intros n m; Case (even_mult_aux n m); Intros H; Case H; Auto.
-Qed.
-Hints Resolve even_mult_l even_mult_r odd_mult :arith.
-
-Lemma odd_mult_inv_l : (n,m:nat) (odd (mult n m)) -> (odd n).
-Proof.
-Intros n m H'.
-Case (even_mult_aux n m).
-Intros H'1 H'2; Elim H'1.
-Intros H'3; Elim H'3; Auto.
-Qed.
-
-Lemma odd_mult_inv_r : (n,m:nat) (odd (mult n m)) -> (odd m).
-Proof.
-Intros n m H'.
-Case (even_mult_aux n m).
-Intros H'1 H'2; Elim H'1.
-Intros H'3; Elim H'3; Auto.
-Qed.
-
diff --git a/theories7/Arith/Factorial.v b/theories7/Arith/Factorial.v
deleted file mode 100644
index a8a60c98..00000000
--- a/theories7/Arith/Factorial.v
+++ /dev/null
@@ -1,51 +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: Factorial.v,v 1.1.2.1 2004/07/16 19:31:24 herbelin Exp $ i*)
-
-Require Plus.
-Require Mult.
-Require Lt.
-V7only [Import nat_scope.].
-Open Local Scope nat_scope.
-
-(** Factorial *)
-
-Fixpoint fact [n:nat]:nat:=
- Cases n of
- O => (S O)
- |(S n) => (mult (S n) (fact n))
- end.
-
-Arguments Scope fact [ nat_scope ].
-
-Lemma lt_O_fact : (n:nat)(lt O (fact n)).
-Proof.
-Induction n; Unfold lt; Simpl; Auto with arith.
-Qed.
-
-Lemma fact_neq_0:(n:nat)~(fact n)=O.
-Proof.
-Intro.
-Apply sym_not_eq.
-Apply lt_O_neq.
-Apply lt_O_fact.
-Qed.
-
-Lemma fact_growing : (n,m:nat) (le n m) -> (le (fact n) (fact m)).
-Proof.
-NewInduction 1.
-Apply le_n.
-Assert (le (mult (S O) (fact n)) (mult (S m) (fact m))).
-Apply le_mult_mult.
-Apply lt_le_S; Apply lt_O_Sn.
-Assumption.
-Simpl (mult (S O) (fact n)) in H0.
-Rewrite <- plus_n_O in H0.
-Assumption.
-Qed.
diff --git a/theories7/Arith/Gt.v b/theories7/Arith/Gt.v
deleted file mode 100755
index 16b6f203..00000000
--- a/theories7/Arith/Gt.v
+++ /dev/null
@@ -1,149 +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: Gt.v,v 1.1.2.1 2004/07/16 19:31:24 herbelin Exp $ i*)
-
-Require Le.
-Require Lt.
-Require Plus.
-V7only [Import nat_scope.].
-Open Local Scope nat_scope.
-
-Implicit Variables Type m,n,p:nat.
-
-(** Order and successor *)
-
-Theorem gt_Sn_O : (n:nat)(gt (S n) O).
-Proof.
- Auto with arith.
-Qed.
-Hints Resolve gt_Sn_O : arith v62.
-
-Theorem gt_Sn_n : (n:nat)(gt (S n) n).
-Proof.
- Auto with arith.
-Qed.
-Hints Resolve gt_Sn_n : arith v62.
-
-Theorem gt_n_S : (n,m:nat)(gt n m)->(gt (S n) (S m)).
-Proof.
- Auto with arith.
-Qed.
-Hints Resolve gt_n_S : arith v62.
-
-Lemma gt_S_n : (n,p:nat)(gt (S p) (S n))->(gt p n).
-Proof.
- Auto with arith.
-Qed.
-Hints Immediate gt_S_n : arith v62.
-
-Theorem gt_S : (n,m:nat)(gt (S n) m)->((gt n m)\/(m=n)).
-Proof.
- Intros n m H; Unfold gt; Apply le_lt_or_eq; Auto with arith.
-Qed.
-
-Lemma gt_pred : (n,p:nat)(gt p (S n))->(gt (pred p) n).
-Proof.
- Auto with arith.
-Qed.
-Hints Immediate gt_pred : arith v62.
-
-(** Irreflexivity *)
-
-Lemma gt_antirefl : (n:nat)~(gt n n).
-Proof lt_n_n.
-Hints Resolve gt_antirefl : arith v62.
-
-(** Asymmetry *)
-
-Lemma gt_not_sym : (n,m:nat)(gt n m) -> ~(gt m n).
-Proof [n,m:nat](lt_not_sym m n).
-
-Hints Resolve gt_not_sym : arith v62.
-
-(** Relating strict and large orders *)
-
-Lemma le_not_gt : (n,m:nat)(le n m) -> ~(gt n m).
-Proof le_not_lt.
-Hints Resolve le_not_gt : arith v62.
-
-Lemma gt_not_le : (n,m:nat)(gt n m) -> ~(le n m).
-Proof.
-Auto with arith.
-Qed.
-
-Hints Resolve gt_not_le : arith v62.
-
-Theorem le_S_gt : (n,m:nat)(le (S n) m)->(gt m n).
-Proof.
- Auto with arith.
-Qed.
-Hints Immediate le_S_gt : arith v62.
-
-Lemma gt_S_le : (n,p:nat)(gt (S p) n)->(le n p).
-Proof.
- Intros n p; Exact (lt_n_Sm_le n p).
-Qed.
-Hints Immediate gt_S_le : arith v62.
-
-Lemma gt_le_S : (n,p:nat)(gt p n)->(le (S n) p).
-Proof.
- Auto with arith.
-Qed.
-Hints Resolve gt_le_S : arith v62.
-
-Lemma le_gt_S : (n,p:nat)(le n p)->(gt (S p) n).
-Proof.
- Auto with arith.
-Qed.
-Hints Resolve le_gt_S : arith v62.
-
-(** Transitivity *)
-
-Theorem le_gt_trans : (n,m,p:nat)(le m n)->(gt m p)->(gt n p).
-Proof.
- Red; Intros; Apply lt_le_trans with m; Auto with arith.
-Qed.
-
-Theorem gt_le_trans : (n,m,p:nat)(gt n m)->(le p m)->(gt n p).
-Proof.
- Red; Intros; Apply le_lt_trans with m; Auto with arith.
-Qed.
-
-Lemma gt_trans : (n,m,p:nat)(gt n m)->(gt m p)->(gt n p).
-Proof.
- Red; Intros n m p H1 H2.
- Apply lt_trans with m; Auto with arith.
-Qed.
-
-Theorem gt_trans_S : (n,m,p:nat)(gt (S n) m)->(gt m p)->(gt n p).
-Proof.
- Red; Intros; Apply lt_le_trans with m; Auto with arith.
-Qed.
-
-Hints Resolve gt_trans_S le_gt_trans gt_le_trans : arith v62.
-
-(** Comparison to 0 *)
-
-Theorem gt_O_eq : (n:nat)((gt n O)\/(O=n)).
-Proof.
- Intro n ; Apply gt_S ; Auto with arith.
-Qed.
-
-(** Simplification and compatibility *)
-
-Lemma simpl_gt_plus_l : (n,m,p:nat)(gt (plus p n) (plus p m))->(gt n m).
-Proof.
- Red; Intros n m p H; Apply simpl_lt_plus_l with p; Auto with arith.
-Qed.
-
-Lemma gt_reg_l : (n,m,p:nat)(gt n m)->(gt (plus p n) (plus p m)).
-Proof.
- Auto with arith.
-Qed.
-Hints Resolve gt_reg_l : arith v62.
diff --git a/theories7/Arith/Le.v b/theories7/Arith/Le.v
deleted file mode 100755
index cdb98645..00000000
--- a/theories7/Arith/Le.v
+++ /dev/null
@@ -1,122 +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: Le.v,v 1.1.2.1 2004/07/16 19:31:24 herbelin Exp $ i*)
-
-(** Order on natural numbers *)
-V7only [Import nat_scope.].
-Open Local Scope nat_scope.
-
-Implicit Variables Type m,n,p:nat.
-
-(** Reflexivity *)
-
-Theorem le_refl : (n:nat)(le n n).
-Proof.
-Exact le_n.
-Qed.
-
-(** Transitivity *)
-
-Theorem le_trans : (n,m,p:nat)(le n m)->(le m p)->(le n p).
-Proof.
- NewInduction 2; Auto.
-Qed.
-Hints Resolve le_trans : arith v62.
-
-(** Order, successor and predecessor *)
-
-Theorem le_n_S : (n,m:nat)(le n m)->(le (S n) (S m)).
-Proof.
- NewInduction 1; Auto.
-Qed.
-
-Theorem le_n_Sn : (n:nat)(le n (S n)).
-Proof.
- Auto.
-Qed.
-
-Theorem le_O_n : (n:nat)(le O n).
-Proof.
- NewInduction n ; Auto.
-Qed.
-
-Hints Resolve le_n_S le_n_Sn le_O_n le_n_S : arith v62.
-
-Theorem le_pred_n : (n:nat)(le (pred n) n).
-Proof.
-NewInduction n ; Auto with arith.
-Qed.
-Hints Resolve le_pred_n : arith v62.
-
-Theorem le_trans_S : (n,m:nat)(le (S n) m)->(le n m).
-Proof.
-Intros n m H ; Apply le_trans with (S n); Auto with arith.
-Qed.
-Hints Immediate le_trans_S : arith v62.
-
-Theorem le_S_n : (n,m:nat)(le (S n) (S m))->(le n m).
-Proof.
-Intros n m H ; Change (le (pred (S n)) (pred (S m))).
-Elim H ; Simpl ; Auto with arith.
-Qed.
-Hints Immediate le_S_n : arith v62.
-
-Theorem le_pred : (n,m:nat)(le n m)->(le (pred n) (pred m)).
-Proof.
-NewInduction n as [|n IHn]. Simpl. Auto with arith.
-NewDestruct m as [|m]. Simpl. Intro H. Inversion H.
-Simpl. Auto with arith.
-Qed.
-
-(** Comparison to 0 *)
-
-Theorem le_Sn_O : (n:nat)~(le (S n) O).
-Proof.
-Red ; Intros n H.
-Change (IsSucc O) ; Elim H ; Simpl ; Auto with arith.
-Qed.
-Hints Resolve le_Sn_O : arith v62.
-
-Theorem le_n_O_eq : (n:nat)(le n O)->(O=n).
-Proof.
-NewInduction n; Auto with arith.
-Intro; Contradiction le_Sn_O with n.
-Qed.
-Hints Immediate le_n_O_eq : arith v62.
-
-(** Negative properties *)
-
-Theorem le_Sn_n : (n:nat)~(le (S n) n).
-Proof.
-NewInduction n; Auto with arith.
-Qed.
-Hints Resolve le_Sn_n : arith v62.
-
-(** Antisymmetry *)
-
-Theorem le_antisym : (n,m:nat)(le n m)->(le m n)->(n=m).
-Proof.
-Intros n m h ; NewDestruct h as [|m0]; Auto with arith.
-Intros H1.
-Absurd (le (S m0) m0) ; Auto with arith.
-Apply le_trans with n ; Auto with arith.
-Qed.
-Hints Immediate le_antisym : arith v62.
-
-(** A different elimination principle for the order on natural numbers *)
-
-Lemma le_elim_rel : (P:nat->nat->Prop)
- ((p:nat)(P O p))->
- ((p,q:nat)(le p q)->(P p q)->(P (S p) (S q)))->
- (n,m:nat)(le n m)->(P n m).
-Proof.
-NewInduction n; Auto with arith.
-Intros m Le.
-Elim Le; Auto with arith.
-Qed.
diff --git a/theories7/Arith/Lt.v b/theories7/Arith/Lt.v
deleted file mode 100755
index 9bb1d564..00000000
--- a/theories7/Arith/Lt.v
+++ /dev/null
@@ -1,176 +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: Lt.v,v 1.1.2.1 2004/07/16 19:31:24 herbelin Exp $ i*)
-
-Require Le.
-V7only [Import nat_scope.].
-Open Local Scope nat_scope.
-
-Implicit Variables Type m,n,p:nat.
-
-(** Irreflexivity *)
-
-Theorem lt_n_n : (n:nat)~(lt n n).
-Proof le_Sn_n.
-Hints Resolve lt_n_n : arith v62.
-
-(** Relationship between [le] and [lt] *)
-
-Theorem lt_le_S : (n,p:nat)(lt n p)->(le (S n) p).
-Proof.
-Auto with arith.
-Qed.
-Hints Immediate lt_le_S : arith v62.
-
-Theorem lt_n_Sm_le : (n,m:nat)(lt n (S m))->(le n m).
-Proof.
-Auto with arith.
-Qed.
-Hints Immediate lt_n_Sm_le : arith v62.
-
-Theorem le_lt_n_Sm : (n,m:nat)(le n m)->(lt n (S m)).
-Proof.
-Auto with arith.
-Qed.
-Hints Immediate le_lt_n_Sm : arith v62.
-
-Theorem le_not_lt : (n,m:nat)(le n m) -> ~(lt m n).
-Proof.
-NewInduction 1; Auto with arith.
-Qed.
-
-Theorem lt_not_le : (n,m:nat)(lt n m) -> ~(le m n).
-Proof.
-Red; Intros n m Lt Le; Exact (le_not_lt m n Le Lt).
-Qed.
-Hints Immediate le_not_lt lt_not_le : arith v62.
-
-(** Asymmetry *)
-
-Theorem lt_not_sym : (n,m:nat)(lt n m) -> ~(lt m n).
-Proof.
-NewInduction 1; Auto with arith.
-Qed.
-
-(** Order and successor *)
-
-Theorem lt_n_Sn : (n:nat)(lt n (S n)).
-Proof.
-Auto with arith.
-Qed.
-Hints Resolve lt_n_Sn : arith v62.
-
-Theorem lt_S : (n,m:nat)(lt n m)->(lt n (S m)).
-Proof.
-Auto with arith.
-Qed.
-Hints Resolve lt_S : arith v62.
-
-Theorem lt_n_S : (n,m:nat)(lt n m)->(lt (S n) (S m)).
-Proof.
-Auto with arith.
-Qed.
-Hints Resolve lt_n_S : arith v62.
-
-Theorem lt_S_n : (n,m:nat)(lt (S n) (S m))->(lt n m).
-Proof.
-Auto with arith.
-Qed.
-Hints Immediate lt_S_n : arith v62.
-
-Theorem lt_O_Sn : (n:nat)(lt O (S n)).
-Proof.
-Auto with arith.
-Qed.
-Hints Resolve lt_O_Sn : arith v62.
-
-Theorem lt_n_O : (n:nat)~(lt n O).
-Proof le_Sn_O.
-Hints Resolve lt_n_O : arith v62.
-
-(** Predecessor *)
-
-Lemma S_pred : (n,m:nat)(lt m n)->n=(S (pred n)).
-Proof.
-NewInduction 1; Auto with arith.
-Qed.
-
-Lemma lt_pred : (n,p:nat)(lt (S n) p)->(lt n (pred p)).
-Proof.
-NewInduction 1; Simpl; Auto with arith.
-Qed.
-Hints Immediate lt_pred : arith v62.
-
-Lemma lt_pred_n_n : (n:nat)(lt O n)->(lt (pred n) n).
-NewDestruct 1; Simpl; Auto with arith.
-Qed.
-Hints Resolve lt_pred_n_n : arith v62.
-
-(** Transitivity properties *)
-
-Theorem lt_trans : (n,m,p:nat)(lt n m)->(lt m p)->(lt n p).
-Proof.
-NewInduction 2; Auto with arith.
-Qed.
-
-Theorem lt_le_trans : (n,m,p:nat)(lt n m)->(le m p)->(lt n p).
-Proof.
-NewInduction 2; Auto with arith.
-Qed.
-
-Theorem le_lt_trans : (n,m,p:nat)(le n m)->(lt m p)->(lt n p).
-Proof.
-NewInduction 2; Auto with arith.
-Qed.
-
-Hints Resolve lt_trans lt_le_trans le_lt_trans : arith v62.
-
-(** Large = strict or equal *)
-
-Theorem le_lt_or_eq : (n,m:nat)(le n m)->((lt n m) \/ n=m).
-Proof.
-NewInduction 1; Auto with arith.
-Qed.
-
-Theorem lt_le_weak : (n,m:nat)(lt n m)->(le n m).
-Proof.
-Auto with arith.
-Qed.
-Hints Immediate lt_le_weak : arith v62.
-
-(** Dichotomy *)
-
-Theorem le_or_lt : (n,m:nat)((le n m)\/(lt m n)).
-Proof.
-Intros n m; Pattern n m; Apply nat_double_ind; Auto with arith.
-NewInduction 1; Auto with arith.
-Qed.
-
-Theorem nat_total_order: (m,n: nat) ~ m = n -> (lt m n) \/ (lt n m).
-Proof.
-Intros m n diff.
-Elim (le_or_lt n m); [Intro H'0 | Auto with arith].
-Elim (le_lt_or_eq n m); Auto with arith.
-Intro H'; Elim diff; Auto with arith.
-Qed.
-
-(** Comparison to 0 *)
-
-Theorem neq_O_lt : (n:nat)(~O=n)->(lt O n).
-Proof.
-NewInduction n; Auto with arith.
-Intros; Absurd O=O; Trivial with arith.
-Qed.
-Hints Immediate neq_O_lt : arith v62.
-
-Theorem lt_O_neq : (n:nat)(lt O n)->(~O=n).
-Proof.
-NewInduction 1; Auto with arith.
-Qed.
-Hints Immediate lt_O_neq : arith v62.
diff --git a/theories7/Arith/Max.v b/theories7/Arith/Max.v
deleted file mode 100755
index aea389d1..00000000
--- a/theories7/Arith/Max.v
+++ /dev/null
@@ -1,87 +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: Max.v,v 1.1.2.1 2004/07/16 19:31:24 herbelin Exp $ i*)
-
-Require Arith.
-
-V7only [Import nat_scope.].
-Open Local Scope nat_scope.
-
-Implicit Variables Type m,n:nat.
-
-(** maximum of two natural numbers *)
-
-Fixpoint max [n:nat] : nat -> nat :=
-[m:nat]Cases n m of
- O _ => m
- | (S n') O => n
- | (S n') (S m') => (S (max n' m'))
- end.
-
-(** Simplifications of [max] *)
-
-Lemma max_SS : (n,m:nat)((S (max n m))=(max (S n) (S m))).
-Proof.
-Auto with arith.
-Qed.
-
-Lemma max_sym : (n,m:nat)(max n m)=(max m n).
-Proof.
-NewInduction n;NewInduction m;Simpl;Auto with arith.
-Qed.
-
-(** [max] and [le] *)
-
-Lemma max_l : (n,m:nat)(le m n)->(max n m)=n.
-Proof.
-NewInduction n;NewInduction m;Simpl;Auto with arith.
-Qed.
-
-Lemma max_r : (n,m:nat)(le n m)->(max n m)=m.
-Proof.
-NewInduction n;NewInduction m;Simpl;Auto with arith.
-Qed.
-
-Lemma le_max_l : (n,m:nat)(le n (max n m)).
-Proof.
-NewInduction n; Intros; Simpl; Auto with arith.
-Elim m; Intros; Simpl; Auto with arith.
-Qed.
-
-Lemma le_max_r : (n,m:nat)(le m (max n m)).
-Proof.
-NewInduction n; Simpl; Auto with arith.
-NewInduction m; Simpl; Auto with arith.
-Qed.
-Hints Resolve max_r max_l le_max_l le_max_r: arith v62.
-
-
-(** [max n m] is equal to [n] or [m] *)
-
-Lemma max_dec : (n,m:nat){(max n m)=n}+{(max n m)=m}.
-Proof.
-NewInduction n;NewInduction m;Simpl;Auto with arith.
-Elim (IHn m);Intro H;Elim H;Auto.
-Qed.
-
-Lemma max_case : (n,m:nat)(P:nat->Set)(P n)->(P m)->(P (max n m)).
-Proof.
-NewInduction n; Simpl; Auto with arith.
-NewInduction m; Intros; Simpl; Auto with arith.
-Pattern (max n m); Apply IHn ; Auto with arith.
-Qed.
-
-Lemma max_case2 : (n,m:nat)(P:nat->Prop)(P n)->(P m)->(P (max n m)).
-Proof.
-NewInduction n; Simpl; Auto with arith.
-NewInduction m; Intros; Simpl; Auto with arith.
-Pattern (max n m); Apply IHn ; Auto with arith.
-Qed.
-
-
diff --git a/theories7/Arith/Min.v b/theories7/Arith/Min.v
deleted file mode 100755
index fd5da61a..00000000
--- a/theories7/Arith/Min.v
+++ /dev/null
@@ -1,84 +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: Min.v,v 1.1.2.1 2004/07/16 19:31:24 herbelin Exp $ i*)
-
-Require Arith.
-
-V7only [Import nat_scope.].
-Open Local Scope nat_scope.
-
-Implicit Variables Type m,n:nat.
-
-(** minimum of two natural numbers *)
-
-Fixpoint min [n:nat] : nat -> nat :=
-[m:nat]Cases n m of
- O _ => O
- | (S n') O => O
- | (S n') (S m') => (S (min n' m'))
- end.
-
-(** Simplifications of [min] *)
-
-Lemma min_SS : (n,m:nat)((S (min n m))=(min (S n) (S m))).
-Proof.
-Auto with arith.
-Qed.
-
-Lemma min_sym : (n,m:nat)(min n m)=(min m n).
-Proof.
-NewInduction n;NewInduction m;Simpl;Auto with arith.
-Qed.
-
-(** [min] and [le] *)
-
-Lemma min_l : (n,m:nat)(le n m)->(min n m)=n.
-Proof.
-NewInduction n;NewInduction m;Simpl;Auto with arith.
-Qed.
-
-Lemma min_r : (n,m:nat)(le m n)->(min n m)=m.
-Proof.
-NewInduction n;NewInduction m;Simpl;Auto with arith.
-Qed.
-
-Lemma le_min_l : (n,m:nat)(le (min n m) n).
-Proof.
-NewInduction n; Intros; Simpl; Auto with arith.
-Elim m; Intros; Simpl; Auto with arith.
-Qed.
-
-Lemma le_min_r : (n,m:nat)(le (min n m) m).
-Proof.
-NewInduction n; Simpl; Auto with arith.
-NewInduction m; Simpl; Auto with arith.
-Qed.
-Hints Resolve min_l min_r le_min_l le_min_r : arith v62.
-
-(** [min n m] is equal to [n] or [m] *)
-
-Lemma min_dec : (n,m:nat){(min n m)=n}+{(min n m)=m}.
-Proof.
-NewInduction n;NewInduction m;Simpl;Auto with arith.
-Elim (IHn m);Intro H;Elim H;Auto.
-Qed.
-
-Lemma min_case : (n,m:nat)(P:nat->Set)(P n)->(P m)->(P (min n m)).
-Proof.
-NewInduction n; Simpl; Auto with arith.
-NewInduction m; Intros; Simpl; Auto with arith.
-Pattern (min n m); Apply IHn ; Auto with arith.
-Qed.
-
-Lemma min_case2 : (n,m:nat)(P:nat->Prop)(P n)->(P m)->(P (min n m)).
-Proof.
-NewInduction n; Simpl; Auto with arith.
-NewInduction m; Intros; Simpl; Auto with arith.
-Pattern (min n m); Apply IHn ; Auto with arith.
-Qed.
diff --git a/theories7/Arith/Minus.v b/theories7/Arith/Minus.v
deleted file mode 100755
index 709d5f0b..00000000
--- a/theories7/Arith/Minus.v
+++ /dev/null
@@ -1,120 +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: Minus.v,v 1.1.2.1 2004/07/16 19:31:24 herbelin Exp $ i*)
-
-(** Subtraction (difference between two natural numbers) *)
-
-Require Lt.
-Require Le.
-
-V7only [Import nat_scope.].
-Open Local Scope nat_scope.
-
-Implicit Variables Type m,n,p:nat.
-
-(** 0 is right neutral *)
-
-Lemma minus_n_O : (n:nat)(n=(minus n O)).
-Proof.
-NewInduction n; Simpl; Auto with arith.
-Qed.
-Hints Resolve minus_n_O : arith v62.
-
-(** Permutation with successor *)
-
-Lemma minus_Sn_m : (n,m:nat)(le m n)->((S (minus n m))=(minus (S n) m)).
-Proof.
-Intros n m Le; Pattern m n; Apply le_elim_rel; Simpl; Auto with arith.
-Qed.
-Hints Resolve minus_Sn_m : arith v62.
-
-Theorem pred_of_minus : (x:nat)(pred x)=(minus x (S O)).
-Intro x; NewInduction x; Simpl; Auto with arith.
-Qed.
-
-(** Diagonal *)
-
-Lemma minus_n_n : (n:nat)(O=(minus n n)).
-Proof.
-NewInduction n; Simpl; Auto with arith.
-Qed.
-Hints Resolve minus_n_n : arith v62.
-
-(** Simplification *)
-
-Lemma minus_plus_simpl :
- (n,m,p:nat)((minus n m)=(minus (plus p n) (plus p m))).
-Proof.
- NewInduction p; Simpl; Auto with arith.
-Qed.
-Hints Resolve minus_plus_simpl : arith v62.
-
-(** Relation with plus *)
-
-Lemma plus_minus : (n,m,p:nat)(n=(plus m p))->(p=(minus n m)).
-Proof.
-Intros n m p; Pattern m n; Apply nat_double_ind; Simpl; Intros.
-Replace (minus n0 O) with n0; Auto with arith.
-Absurd O=(S (plus n0 p)); Auto with arith.
-Auto with arith.
-Qed.
-Hints Immediate plus_minus : arith v62.
-
-Lemma minus_plus : (n,m:nat)(minus (plus n m) n)=m.
-Symmetry; Auto with arith.
-Qed.
-Hints Resolve minus_plus : arith v62.
-
-Lemma le_plus_minus : (n,m:nat)(le n m)->(m=(plus n (minus m n))).
-Proof.
-Intros n m Le; Pattern n m; Apply le_elim_rel; Simpl; Auto with arith.
-Qed.
-Hints Resolve le_plus_minus : arith v62.
-
-Lemma le_plus_minus_r : (n,m:nat)(le n m)->(plus n (minus m n))=m.
-Proof.
-Symmetry; Auto with arith.
-Qed.
-Hints Resolve le_plus_minus_r : arith v62.
-
-(** Relation with order *)
-
-Theorem le_minus: (i,h:nat) (le (minus i h) i).
-Proof.
-Intros i h;Pattern i h; Apply nat_double_ind; [
- Auto
-| Auto
-| Intros m n H; Simpl; Apply le_trans with m:=m; Auto ].
-Qed.
-
-Lemma lt_minus : (n,m:nat)(le m n)->(lt O m)->(lt (minus n m) n).
-Proof.
-Intros n m Le; Pattern m n; Apply le_elim_rel; Simpl; Auto with arith.
-Intros; Absurd (lt O O); Auto with arith.
-Intros p q lepq Hp gtp.
-Elim (le_lt_or_eq O p); Auto with arith.
-Auto with arith.
-NewInduction 1; Elim minus_n_O; Auto with arith.
-Qed.
-Hints Resolve lt_minus : arith v62.
-
-Lemma lt_O_minus_lt : (n,m:nat)(lt O (minus n m))->(lt m n).
-Proof.
-Intros n m; Pattern n m; Apply nat_double_ind; Simpl; Auto with arith.
-Intros; Absurd (lt O O); Trivial with arith.
-Qed.
-Hints Immediate lt_O_minus_lt : arith v62.
-
-Theorem inj_minus_aux: (x,y:nat) ~(le y x) -> (minus x y) = O.
-Intros y x; Pattern y x ; Apply nat_double_ind; [
- Simpl; Trivial with arith
-| Intros n H; Absurd (le O (S n)); [ Assumption | Apply le_O_n]
-| Simpl; Intros n m H1 H2; Apply H1;
- Unfold not ; Intros H3; Apply H2; Apply le_n_S; Assumption].
-Qed.
diff --git a/theories7/Arith/Mult.v b/theories7/Arith/Mult.v
deleted file mode 100755
index 9bd4aaf9..00000000
--- a/theories7/Arith/Mult.v
+++ /dev/null
@@ -1,224 +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: Mult.v,v 1.1.2.1 2004/07/16 19:31:25 herbelin Exp $ i*)
-
-Require Export Plus.
-Require Export Minus.
-Require Export Lt.
-Require Export Le.
-
-V7only [Import nat_scope.].
-Open Local Scope nat_scope.
-
-Implicit Variables Type m,n,p:nat.
-
-(** Zero property *)
-
-Lemma mult_0_r : (n:nat) (mult n O)=O.
-Proof.
-Intro; Symmetry; Apply mult_n_O.
-Qed.
-
-Lemma mult_0_l : (n:nat) (mult O n)=O.
-Proof.
-Reflexivity.
-Qed.
-
-(** Distributivity *)
-
-Lemma mult_plus_distr :
- (n,m,p:nat)((mult (plus n m) p)=(plus (mult n p) (mult m p))).
-Proof.
-Intros; Elim n; Simpl; Intros; Auto with arith.
-Elim plus_assoc_l; Elim H; Auto with arith.
-Qed.
-Hints Resolve mult_plus_distr : arith v62.
-
-Lemma mult_plus_distr_r : (n,m,p:nat) (mult n (plus m p))=(plus (mult n m) (mult n p)).
-Proof.
- NewInduction n. Trivial.
- Intros. Simpl. Rewrite (IHn m p). Apply sym_eq. Apply plus_permute_2_in_4.
-Qed.
-
-Lemma mult_minus_distr : (n,m,p:nat)((mult (minus n m) p)=(minus (mult n p) (mult m p))).
-Proof.
-Intros; Pattern n m; Apply nat_double_ind; Simpl; Intros; Auto with arith.
-Elim minus_plus_simpl; Auto with arith.
-Qed.
-Hints Resolve mult_minus_distr : arith v62.
-
-(** Associativity *)
-
-Lemma mult_assoc_r : (n,m,p:nat)((mult (mult n m) p) = (mult n (mult m p))).
-Proof.
-Intros; Elim n; Intros; Simpl; Auto with arith.
-Rewrite mult_plus_distr.
-Elim H; Auto with arith.
-Qed.
-Hints Resolve mult_assoc_r : arith v62.
-
-Lemma mult_assoc_l : (n,m,p:nat)(mult n (mult m p)) = (mult (mult n m) p).
-Proof.
-Auto with arith.
-Qed.
-Hints Resolve mult_assoc_l : arith v62.
-
-(** Commutativity *)
-
-Lemma mult_sym : (n,m:nat)(mult n m)=(mult m n).
-Proof.
-Intros; Elim n; Intros; Simpl; Auto with arith.
-Elim mult_n_Sm.
-Elim H; Apply plus_sym.
-Qed.
-Hints Resolve mult_sym : arith v62.
-
-(** 1 is neutral *)
-
-Lemma mult_1_n : (n:nat)(mult (S O) n)=n.
-Proof.
-Simpl; Auto with arith.
-Qed.
-Hints Resolve mult_1_n : arith v62.
-
-Lemma mult_n_1 : (n:nat)(mult n (S O))=n.
-Proof.
-Intro; Elim mult_sym; Auto with arith.
-Qed.
-Hints Resolve mult_n_1 : arith v62.
-
-(** Compatibility with orders *)
-
-Lemma mult_O_le : (n,m:nat)(m=O)\/(le n (mult m n)).
-Proof.
-NewInduction m; Simpl; Auto with arith.
-Qed.
-Hints Resolve mult_O_le : arith v62.
-
-Lemma mult_le_compat_l : (n,m,p:nat) (le n m) -> (le (mult p n) (mult p m)).
-Proof.
- NewInduction p as [|p IHp]. Intros. Simpl. Apply le_n.
- Intros. Simpl. Apply le_plus_plus. Assumption.
- Apply IHp. Assumption.
-Qed.
-Hints Resolve mult_le_compat_l : arith.
-V7only [
-Notation mult_le := [m,n,p:nat](mult_le_compat_l p n m).
-].
-
-
-Lemma le_mult_right : (m,n,p:nat)(le m n)->(le (mult m p) (mult n p)).
-Intros m n p H.
-Rewrite mult_sym. Rewrite (mult_sym n).
-Auto with arith.
-Qed.
-
-Lemma le_mult_mult :
- (m,n,p,q:nat)(le m n)->(le p q)->(le (mult m p) (mult n q)).
-Proof.
-Intros m n p q Hmn Hpq; NewInduction Hmn.
-NewInduction Hpq.
-(* m*p<=m*p *)
-Apply le_n.
-(* m*p<=m*m0 -> m*p<=m*(S m0) *)
-Rewrite <- mult_n_Sm; Apply le_trans with (mult m m0).
-Assumption.
-Apply le_plus_l.
-(* m*p<=m0*q -> m*p<=(S m0)*q *)
-Simpl; Apply le_trans with (mult m0 q).
-Assumption.
-Apply le_plus_r.
-Qed.
-
-Lemma mult_lt : (m,n,p:nat) (lt n p) -> (lt (mult (S m) n) (mult (S m) p)).
-Proof.
- Intro m; NewInduction m. Intros. Simpl. Rewrite <- plus_n_O. Rewrite <- plus_n_O. Assumption.
- Intros. Exact (lt_plus_plus ? ? ? ? H (IHm ? ? H)).
-Qed.
-
-Hints Resolve mult_lt : arith.
-V7only [
-Notation lt_mult_left := mult_lt.
-(* Theorem lt_mult_left :
- (x,y,z:nat) (lt x y) -> (lt (mult (S z) x) (mult (S z) y)).
-*)
-].
-
-Lemma lt_mult_right :
- (m,n,p:nat) (lt m n) -> (lt (0) p) -> (lt (mult m p) (mult n p)).
-Intros m n p H H0.
-NewInduction p.
-Elim (lt_n_n ? H0).
-Rewrite mult_sym.
-Replace (mult n (S p)) with (mult (S p) n); Auto with arith.
-Qed.
-
-Lemma mult_le_conv_1 : (m,n,p:nat) (le (mult (S m) n) (mult (S m) p)) -> (le n p).
-Proof.
- Intros m n p H. Elim (le_or_lt n p). Trivial.
- Intro H0. Cut (lt (mult (S m) n) (mult (S m) n)). Intro. Elim (lt_n_n ? H1).
- Apply le_lt_trans with m:=(mult (S m) p). Assumption.
- Apply mult_lt. Assumption.
-Qed.
-
-(** n|->2*n and n|->2n+1 have disjoint image *)
-
-V7only [ (* From Zdivides *) ].
-Theorem odd_even_lem:
- (p, q : ?) ~ (plus (mult (2) p) (1)) = (mult (2) q).
-Intros p; Elim p; Auto.
-Intros q; Case q; Simpl.
-Red; Intros; Discriminate.
-Intros q'; Rewrite [x, y : ?] (plus_sym x (S y)); Simpl; Red; Intros;
- Discriminate.
-Intros p' H q; Case q.
-Simpl; Red; Intros; Discriminate.
-Intros q'; Red; Intros H0; Case (H q').
-Replace (mult (S (S O)) q') with (minus (mult (S (S O)) (S q')) (2)).
-Rewrite <- H0; Simpl; Auto.
-Repeat Rewrite [x, y : ?] (plus_sym x (S y)); Simpl; Auto.
-Simpl; Repeat Rewrite [x, y : ?] (plus_sym x (S y)); Simpl; Auto.
-Case q'; Simpl; Auto.
-Qed.
-
-
-(** Tail-recursive mult *)
-
-(** [tail_mult] is an alternative definition for [mult] which is
- tail-recursive, whereas [mult] is not. This can be useful
- when extracting programs. *)
-
-Fixpoint mult_acc [s,m,n:nat] : nat :=
- Cases n of
- O => s
- | (S p) => (mult_acc (tail_plus m s) m p)
- end.
-
-Lemma mult_acc_aux : (n,s,m:nat)(plus s (mult n m))= (mult_acc s m n).
-Proof.
-NewInduction n as [|p IHp]; Simpl;Auto.
-Intros s m; Rewrite <- plus_tail_plus; Rewrite <- IHp.
-Rewrite <- plus_assoc_r; Apply (f_equal2 nat nat);Auto.
-Rewrite plus_sym;Auto.
-Qed.
-
-Definition tail_mult := [n,m:nat](mult_acc O m n).
-
-Lemma mult_tail_mult : (n,m:nat)(mult n m)=(tail_mult n m).
-Proof.
-Intros; Unfold tail_mult; Rewrite <- mult_acc_aux;Auto.
-Qed.
-
-(** [TailSimpl] transforms any [tail_plus] and [tail_mult] into [plus]
- and [mult] and simplify *)
-
-Tactic Definition TailSimpl :=
- Repeat Rewrite <- plus_tail_plus;
- Repeat Rewrite <- mult_tail_mult;
- Simpl.
diff --git a/theories7/Arith/Peano_dec.v b/theories7/Arith/Peano_dec.v
deleted file mode 100755
index 6646545a..00000000
--- a/theories7/Arith/Peano_dec.v
+++ /dev/null
@@ -1,36 +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: Peano_dec.v,v 1.1.2.1 2004/07/16 19:31:25 herbelin Exp $ i*)
-
-Require Decidable.
-
-V7only [Import nat_scope.].
-Open Local Scope nat_scope.
-
-Implicit Variables Type m,n,x,y:nat.
-
-Theorem O_or_S : (n:nat)({m:nat|(S m)=n})+{O=n}.
-Proof.
-NewInduction n.
-Auto.
-Left; Exists n; Auto.
-Defined.
-
-Theorem eq_nat_dec : (n,m:nat){n=m}+{~(n=m)}.
-Proof.
-NewInduction n; NewInduction m; Auto.
-Elim (IHn m); Auto.
-Defined.
-
-Hints Resolve O_or_S eq_nat_dec : arith.
-
-Theorem dec_eq_nat:(x,y:nat)(decidable (x=y)).
-Intros x y; Unfold decidable; Elim (eq_nat_dec x y); Auto with arith.
-Defined.
-
diff --git a/theories7/Arith/Plus.v b/theories7/Arith/Plus.v
deleted file mode 100755
index 23488b4c..00000000
--- a/theories7/Arith/Plus.v
+++ /dev/null
@@ -1,223 +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: Plus.v,v 1.5.2.1 2004/07/16 19:31:25 herbelin Exp $ i*)
-
-(** Properties of addition *)
-
-Require Le.
-Require Lt.
-
-V7only [Import nat_scope.].
-Open Local Scope nat_scope.
-
-Implicit Variables Type m,n,p,q:nat.
-
-(** Zero is neutral *)
-
-Lemma plus_0_l : (n:nat) (O+n)=n.
-Proof.
-Reflexivity.
-Qed.
-
-Lemma plus_0_r : (n:nat) (n+O)=n.
-Proof.
-Intro; Symmetry; Apply plus_n_O.
-Qed.
-
-(** Commutativity *)
-
-Lemma plus_sym : (n,m:nat)(n+m)=(m+n).
-Proof.
-Intros n m ; Elim n ; Simpl ; Auto with arith.
-Intros y H ; Elim (plus_n_Sm m y) ; Auto with arith.
-Qed.
-Hints Immediate plus_sym : arith v62.
-
-(** Associativity *)
-
-Lemma plus_Snm_nSm : (n,m:nat)((S n)+m)=(n+(S m)).
-Intros.
-Simpl.
-Rewrite -> (plus_sym n m).
-Rewrite -> (plus_sym n (S m)).
-Trivial with arith.
-Qed.
-
-Lemma plus_assoc_l : (n,m,p:nat)((n+(m+p))=((n+m)+p)).
-Proof.
-Intros n m p; Elim n; Simpl; Auto with arith.
-Qed.
-Hints Resolve plus_assoc_l : arith v62.
-
-Lemma plus_permute : (n,m,p:nat) ((n+(m+p))=(m+(n+p))).
-Proof.
-Intros; Rewrite (plus_assoc_l m n p); Rewrite (plus_sym m n); Auto with arith.
-Qed.
-
-Lemma plus_assoc_r : (n,m,p:nat)(((n+m)+p)=(n+(m+p))).
-Proof.
-Auto with arith.
-Qed.
-Hints Resolve plus_assoc_r : arith v62.
-
-(** Simplification *)
-
-Lemma plus_reg_l : (m,p,n:nat)((n+m)=(n+p))->(m=p).
-Proof.
-Intros m p n; NewInduction n ; Simpl ; Auto with arith.
-Qed.
-V7only [
-(* Compatibility order of arguments *)
-Notation "'simpl_plus_l' c" := [a,b:nat](plus_reg_l a b c)
- (at level 10, c at next level).
-Notation "'simpl_plus_l' c a" := [b:nat](plus_reg_l a b c)
- (at level 10, a, c at next level).
-Notation "'simpl_plus_l' c a b" := (plus_reg_l a b c)
- (at level 10, a, b, c at next level).
-Notation simpl_plus_l := plus_reg_l.
-].
-
-Lemma plus_le_reg_l : (n,m,p:nat)((p+n)<=(p+m))->(n<=m).
-Proof.
-NewInduction p; Simpl; Auto with arith.
-Qed.
-V7only [
-(* Compatibility order of arguments *)
-Notation "'simpl_le_plus_l' c" := [a,b:nat](plus_le_reg_l a b c)
- (at level 10, c at next level).
-Notation "'simpl_le_plus_l' c a" := [b:nat](plus_le_reg_l a b c)
- (at level 10, a, c at next level).
-Notation "'simpl_le_plus_l' c a b" := (plus_le_reg_l a b c)
- (at level 10, a, b, c at next level).
-Notation simpl_le_plus_l := [p,n,m:nat](plus_le_reg_l n m p).
-].
-
-Lemma simpl_lt_plus_l : (n,m,p:nat) (p+n)<(p+m) -> n<m.
-Proof.
-NewInduction p; Simpl; Auto with arith.
-Qed.
-
-(** Compatibility with order *)
-
-Lemma le_reg_l : (n,m,p:nat) n<=m -> (p+n)<=(p+m).
-Proof.
-NewInduction p; Simpl; Auto with arith.
-Qed.
-Hints Resolve le_reg_l : arith v62.
-
-Lemma le_reg_r : (a,b,c:nat) a<=b -> (a+c)<=(b+c).
-Proof.
-NewInduction 1 ; Simpl; Auto with arith.
-Qed.
-Hints Resolve le_reg_r : arith v62.
-
-Lemma le_plus_l : (n,m:nat) n<=(n+m).
-Proof.
-NewInduction n; Simpl; Auto with arith.
-Qed.
-Hints Resolve le_plus_l : arith v62.
-
-Lemma le_plus_r : (n,m:nat) m<=(n+m).
-Proof.
-Intros n m; Elim n; Simpl; Auto with arith.
-Qed.
-Hints Resolve le_plus_r : arith v62.
-
-Theorem le_plus_trans : (n,m,p:nat) n<=m -> n<=(m+p).
-Proof.
-Intros; Apply le_trans with m:=m; Auto with arith.
-Qed.
-Hints Resolve le_plus_trans : arith v62.
-
-Theorem lt_plus_trans : (n,m,p:nat) n<m -> n<(m+p).
-Proof.
-Intros; Apply lt_le_trans with m:=m; Auto with arith.
-Qed.
-Hints Immediate lt_plus_trans : arith v62.
-
-Lemma lt_reg_l : (n,m,p:nat) n<m -> (p+n)<(p+m).
-Proof.
-NewInduction p; Simpl; Auto with arith.
-Qed.
-Hints Resolve lt_reg_l : arith v62.
-
-Lemma lt_reg_r : (n,m,p:nat) n<m -> (n+p)<(m+p).
-Proof.
-Intros n m p H ; Rewrite (plus_sym n p) ; Rewrite (plus_sym m p).
-Elim p; Auto with arith.
-Qed.
-Hints Resolve lt_reg_r : arith v62.
-
-Lemma le_plus_plus : (n,m,p,q:nat) n<=m -> p<=q -> (n+p)<=(m+q).
-Proof.
-Intros n m p q H H0.
-Elim H; Simpl; Auto with arith.
-Qed.
-
-Lemma le_lt_plus_plus : (n,m,p,q:nat) n<=m -> p<q -> (n+p)<(m+q).
-Proof.
- Unfold lt. Intros. Change ((S n)+p)<=(m+q). Rewrite plus_Snm_nSm.
- Apply le_plus_plus; Assumption.
-Qed.
-
-Lemma lt_le_plus_plus : (n,m,p,q:nat) n<m -> p<=q -> (n+p)<(m+q).
-Proof.
- Unfold lt. Intros. Change ((S n)+p)<=(m+q). Apply le_plus_plus; Assumption.
-Qed.
-
-Lemma lt_plus_plus : (n,m,p,q:nat) n<m -> p<q -> (n+p)<(m+q).
-Proof.
- Intros. Apply lt_le_plus_plus. Assumption.
- Apply lt_le_weak. Assumption.
-Qed.
-
-(** Inversion lemmas *)
-
-Lemma plus_is_O : (m,n:nat) (m+n)=O -> m=O /\ n=O.
-Proof.
- Intro m; NewDestruct m; Auto.
- Intros. Discriminate H.
-Qed.
-
-Definition plus_is_one :
- (m,n:nat) (m+n)=(S O) -> {m=O /\ n=(S O)}+{m=(S O) /\ n=O}.
-Proof.
- Intro m; NewDestruct m; Auto.
- NewDestruct n; Auto.
- Intros.
- Simpl in H. Discriminate H.
-Defined.
-
-(** Derived properties *)
-
-Lemma plus_permute_2_in_4 : (m,n,p,q:nat) ((m+n)+(p+q))=((m+p)+(n+q)).
-Proof.
- Intros m n p q.
- Rewrite <- (plus_assoc_l m n (p+q)). Rewrite (plus_assoc_l n p q).
- Rewrite (plus_sym n p). Rewrite <- (plus_assoc_l p n q). Apply plus_assoc_l.
-Qed.
-
-(** Tail-recursive plus *)
-
-(** [tail_plus] is an alternative definition for [plus] which is
- tail-recursive, whereas [plus] is not. This can be useful
- when extracting programs. *)
-
-Fixpoint plus_acc [q,n:nat] : nat :=
- Cases n of
- O => q
- | (S p) => (plus_acc (S q) p)
- end.
-
-Definition tail_plus := [n,m:nat](plus_acc m n).
-
-Lemma plus_tail_plus : (n,m:nat)(n+m)=(tail_plus n m).
-Unfold tail_plus; NewInduction n as [|n IHn]; Simpl; Auto.
-Intro m; Rewrite <- IHn; Simpl; Auto.
-Qed.
diff --git a/theories7/Arith/Wf_nat.v b/theories7/Arith/Wf_nat.v
deleted file mode 100755
index be1003ce..00000000
--- a/theories7/Arith/Wf_nat.v
+++ /dev/null
@@ -1,200 +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: Wf_nat.v,v 1.1.2.1 2004/07/16 19:31:25 herbelin Exp $ i*)
-
-(** Well-founded relations and natural numbers *)
-
-Require Lt.
-
-V7only [Import nat_scope.].
-Open Local Scope nat_scope.
-
-Implicit Variables Type m,n,p:nat.
-
-Chapter Well_founded_Nat.
-
-Variable A : Set.
-
-Variable f : A -> nat.
-Definition ltof := [a,b:A](lt (f a) (f b)).
-Definition gtof := [a,b:A](gt (f b) (f a)).
-
-Theorem well_founded_ltof : (well_founded A ltof).
-Proof.
-Red.
-Cut (n:nat)(a:A)(lt (f a) n)->(Acc A ltof a).
-Intros H a; Apply (H (S (f a))); Auto with arith.
-NewInduction n.
-Intros; Absurd (lt (f a) O); Auto with arith.
-Intros a ltSma.
-Apply Acc_intro.
-Unfold ltof; Intros b ltfafb.
-Apply IHn.
-Apply lt_le_trans with (f a); Auto with arith.
-Qed.
-
-Theorem well_founded_gtof : (well_founded A gtof).
-Proof well_founded_ltof.
-
-(** It is possible to directly prove the induction principle going
- back to primitive recursion on natural numbers ([induction_ltof1])
- or to use the previous lemmas to extract a program with a fixpoint
- ([induction_ltof2])
-
-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)));;
-]]
-
-the ML-like program for [induction_ltof2] is : [[
- let induction_ltof2 F a = indrec a
- where rec indrec a = F a indrec;;
-]] *)
-
-Theorem induction_ltof1
- : (P:A->Set)((x:A)((y:A)(ltof y x)->(P y))->(P x))->(a:A)(P a).
-Proof.
-Intros P F; Cut (n:nat)(a:A)(lt (f a) n)->(P a).
-Intros H a; Apply (H (S (f a))); Auto with arith.
-NewInduction n.
-Intros; Absurd (lt (f a) O); Auto with arith.
-Intros a ltSma.
-Apply F.
-Unfold ltof; Intros b ltfafb.
-Apply IHn.
-Apply lt_le_trans with (f a); Auto with arith.
-Defined.
-
-Theorem induction_gtof1
- : (P:A->Set)((x:A)((y:A)(gtof y x)->(P y))->(P x))->(a:A)(P a).
-Proof.
-Exact induction_ltof1.
-Defined.
-
-Theorem induction_ltof2
- : (P:A->Set)((x:A)((y:A)(ltof y x)->(P y))->(P x))->(a:A)(P a).
-Proof.
-Exact (well_founded_induction A ltof well_founded_ltof).
-Defined.
-
-Theorem induction_gtof2
- : (P:A->Set)((x:A)((y:A)(gtof y x)->(P y))->(P x))->(a:A)(P a).
-Proof.
-Exact induction_ltof2.
-Defined.
-
-(** If a relation [R] is compatible with [lt] i.e. if [x R y => f(x) < f(y)]
- then [R] is well-founded. *)
-
-Variable R : A->A->Prop.
-
-Hypothesis H_compat : (x,y:A) (R x y) -> (lt (f x) (f y)).
-
-Theorem well_founded_lt_compat : (well_founded A R).
-Proof.
-Red.
-Cut (n:nat)(a:A)(lt (f a) n)->(Acc A R a).
-Intros H a; Apply (H (S (f a))); Auto with arith.
-NewInduction n.
-Intros; Absurd (lt (f a) O); Auto with arith.
-Intros a ltSma.
-Apply Acc_intro.
-Intros b ltfafb.
-Apply IHn.
-Apply lt_le_trans with (f a); Auto with arith.
-Qed.
-
-End Well_founded_Nat.
-
-Lemma lt_wf : (well_founded nat lt).
-Proof (well_founded_ltof nat [m:nat]m).
-
-Lemma lt_wf_rec1 : (p:nat)(P:nat->Set)
- ((n:nat)((m:nat)(lt m n)->(P m))->(P n)) -> (P p).
-Proof.
-Exact [p:nat][P:nat->Set][F:(n:nat)((m:nat)(lt m n)->(P m))->(P n)]
- (induction_ltof1 nat [m:nat]m P F p).
-Defined.
-
-Lemma lt_wf_rec : (p:nat)(P:nat->Set)
- ((n:nat)((m:nat)(lt m n)->(P m))->(P n)) -> (P p).
-Proof.
-Exact [p:nat][P:nat->Set][F:(n:nat)((m:nat)(lt m n)->(P m))->(P n)]
- (induction_ltof2 nat [m:nat]m P F p).
-Defined.
-
-Lemma lt_wf_ind : (p:nat)(P:nat->Prop)
- ((n:nat)((m:nat)(lt m n)->(P m))->(P n)) -> (P p).
-Intro p; Intros; Elim (lt_wf p); Auto with arith.
-Qed.
-
-Lemma gt_wf_rec : (p:nat)(P:nat->Set)
- ((n:nat)((m:nat)(gt n m)->(P m))->(P n)) -> (P p).
-Proof.
-Exact lt_wf_rec.
-Defined.
-
-Lemma gt_wf_ind : (p:nat)(P:nat->Prop)
- ((n:nat)((m:nat)(gt n m)->(P m))->(P n)) -> (P p).
-Proof lt_wf_ind.
-
-Lemma lt_wf_double_rec :
- (P:nat->nat->Set)
- ((n,m:nat)((p,q:nat)(lt p n)->(P p q))->((p:nat)(lt p m)->(P n p))->(P n m))
- -> (p,q:nat)(P p q).
-Intros P Hrec p; Pattern p; Apply lt_wf_rec.
-Intros n H q; Pattern q; Apply lt_wf_rec; Auto with arith.
-Defined.
-
-Lemma lt_wf_double_ind :
- (P:nat->nat->Prop)
- ((n,m:nat)((p,q:nat)(lt p n)->(P p q))->((p:nat)(lt p m)->(P n p))->(P n m))
- -> (p,q:nat)(P p q).
-Intros P Hrec p; Pattern p; Apply lt_wf_ind.
-Intros n H q; Pattern q; Apply lt_wf_ind; Auto with arith.
-Qed.
-
-Hints Resolve lt_wf : arith.
-Hints Resolve well_founded_lt_compat : arith.
-
-Section LT_WF_REL.
-Variable A :Set.
-Variable R:A->A->Prop.
-
-(* Relational form of inversion *)
-Variable F : A -> nat -> Prop.
-Definition inv_lt_rel
- [x,y]:=(EX n | (F x n) & (m:nat)(F y m)->(lt n m)).
-
-Hypothesis F_compat : (x,y:A) (R x y) -> (inv_lt_rel x y).
-Remark acc_lt_rel :
- (x:A)(EX n | (F x n))->(Acc A R x).
-Intros x (n,fxn); Generalize x fxn; Clear x fxn.
-Pattern n; Apply lt_wf_ind; Intros.
-Constructor; Intros.
-Case (F_compat y x); Trivial; Intros.
-Apply (H x0); Auto.
-Save.
-
-Theorem well_founded_inv_lt_rel_compat : (well_founded A R).
-Constructor; Intros.
-Case (F_compat y a); Trivial; Intros.
-Apply acc_lt_rel; Trivial.
-Exists x; Trivial.
-Save.
-
-
-End LT_WF_REL.
-
-Lemma well_founded_inv_rel_inv_lt_rel
- : (A:Set)(F:A->nat->Prop)(well_founded A (inv_lt_rel A F)).
-Intros; Apply (well_founded_inv_lt_rel_compat A (inv_lt_rel A F) F); Trivial.
-Save.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 06:32:20 +0000