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, 2581 insertions, 0 deletions
diff --git a/theories7/Arith/Arith.v b/theories7/Arith/Arith.v new file mode 100755 index 00000000..181fadbc --- /dev/null +++ b/theories7/Arith/Arith.v @@ -0,0 +1,21 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..b3fef325 --- /dev/null +++ b/theories7/Arith/Between.v @@ -0,0 +1,185 @@ +(************************************************************************) +(* 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 new file mode 100644 index 00000000..c36f8f15 --- /dev/null +++ b/theories7/Arith/Bool_nat.v @@ -0,0 +1,43 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..1bca3fbe --- /dev/null +++ b/theories7/Arith/Compare.v @@ -0,0 +1,60 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..504c0562 --- /dev/null +++ b/theories7/Arith/Compare_dec.v @@ -0,0 +1,109 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..59694628 --- /dev/null +++ b/theories7/Arith/Div.v @@ -0,0 +1,64 @@ +(************************************************************************) +(* 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 new file mode 100644 index 00000000..8bd0160f --- /dev/null +++ b/theories7/Arith/Div2.v @@ -0,0 +1,174 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..9f5ee7ee --- /dev/null +++ b/theories7/Arith/EqNat.v @@ -0,0 +1,78 @@ +(************************************************************************) +(* 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 new file mode 100644 index 00000000..adeaf713 --- /dev/null +++ b/theories7/Arith/Euclid.v @@ -0,0 +1,65 @@ +(************************************************************************) +(* 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 new file mode 100644 index 00000000..bcc413f5 --- /dev/null +++ b/theories7/Arith/Even.v @@ -0,0 +1,310 @@ +(************************************************************************) +(* 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 new file mode 100644 index 00000000..a8a60c98 --- /dev/null +++ b/theories7/Arith/Factorial.v @@ -0,0 +1,51 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..16b6f203 --- /dev/null +++ b/theories7/Arith/Gt.v @@ -0,0 +1,149 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..cdb98645 --- /dev/null +++ b/theories7/Arith/Le.v @@ -0,0 +1,122 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..9bb1d564 --- /dev/null +++ b/theories7/Arith/Lt.v @@ -0,0 +1,176 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..aea389d1 --- /dev/null +++ b/theories7/Arith/Max.v @@ -0,0 +1,87 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..fd5da61a --- /dev/null +++ b/theories7/Arith/Min.v @@ -0,0 +1,84 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..709d5f0b --- /dev/null +++ b/theories7/Arith/Minus.v @@ -0,0 +1,120 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..9bd4aaf9 --- /dev/null +++ b/theories7/Arith/Mult.v @@ -0,0 +1,224 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..6646545a --- /dev/null +++ b/theories7/Arith/Peano_dec.v @@ -0,0 +1,36 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..23488b4c --- /dev/null +++ b/theories7/Arith/Plus.v @@ -0,0 +1,223 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..be1003ce --- /dev/null +++ b/theories7/Arith/Wf_nat.v @@ -0,0 +1,200 @@ +(************************************************************************) +(* 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. |