diff options
Diffstat (limited to 'theories7/Arith')
-rwxr-xr-x | theories7/Arith/Arith.v | 21 | ||||
-rwxr-xr-x | theories7/Arith/Between.v | 185 | ||||
-rw-r--r-- | theories7/Arith/Bool_nat.v | 43 | ||||
-rwxr-xr-x | theories7/Arith/Compare.v | 60 | ||||
-rwxr-xr-x | theories7/Arith/Compare_dec.v | 109 | ||||
-rwxr-xr-x | theories7/Arith/Div.v | 64 | ||||
-rw-r--r-- | theories7/Arith/Div2.v | 174 | ||||
-rwxr-xr-x | theories7/Arith/EqNat.v | 78 | ||||
-rw-r--r-- | theories7/Arith/Euclid.v | 65 | ||||
-rw-r--r-- | theories7/Arith/Even.v | 310 | ||||
-rw-r--r-- | theories7/Arith/Factorial.v | 51 | ||||
-rwxr-xr-x | theories7/Arith/Gt.v | 149 | ||||
-rwxr-xr-x | theories7/Arith/Le.v | 122 | ||||
-rwxr-xr-x | theories7/Arith/Lt.v | 176 | ||||
-rwxr-xr-x | theories7/Arith/Max.v | 87 | ||||
-rwxr-xr-x | theories7/Arith/Min.v | 84 | ||||
-rwxr-xr-x | theories7/Arith/Minus.v | 120 | ||||
-rwxr-xr-x | theories7/Arith/Mult.v | 224 | ||||
-rwxr-xr-x | theories7/Arith/Peano_dec.v | 36 | ||||
-rwxr-xr-x | theories7/Arith/Plus.v | 223 | ||||
-rwxr-xr-x | theories7/Arith/Wf_nat.v | 200 |
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. |