diff options
| author |  mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-19 13:07:42 +0000 |
|---|---|---|
| committer | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-19 13:07:42 +0000 |
| commit | cb9061d894d516e4607a9237813402d929384b26 (patch) | |
| tree | 13137c2d2587c29483dbee0035ae1eab20f6342b /theories/Zarith | |
| parent | 97271bd7c99f2a6de4b022af420f7a6050803492 (diff) | |
remplace Zarith par ZArith
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1625 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Zarith')
| -rw-r--r-- | theories/Zarith/Wf_Z.v | 133 | ||||
| -rw-r--r-- | theories/Zarith/ZArith.v | 23 | ||||
| -rw-r--r-- | theories/Zarith/ZArith_dec.v | 127 | ||||
| -rw-r--r-- | theories/Zarith/Zmisc.v | 433 | ||||
| -rw-r--r-- | theories/Zarith/Zsyntax.v | 213 | ||||
| -rw-r--r-- | theories/Zarith/auxiliary.v | 930 | ||||
| -rw-r--r-- | theories/Zarith/fast_integer.v | 1486 | ||||
| -rwxr-xr-x | theories/Zarith/intro.tex | 5 | ||||
| -rw-r--r-- | theories/Zarith/zarith_aux.v | 741 |
9 files changed, 0 insertions, 4091 deletions
diff --git a/theories/Zarith/Wf_Z.v b/theories/Zarith/Wf_Z.v deleted file mode 100644 index eab0874c0..000000000 --- a/theories/Zarith/Wf_Z.v +++ /dev/null @@ -1,133 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(* $Id$ *) - -Require fast_integer. -Require zarith_aux. -Require auxiliary. -Require Zsyntax. - -(* Our purpose is to write an induction shema for {0,1,2,...} - similar to the nat schema (Theorem [Natlike_rec]). For that the - following implications will be used : -\begin{verbatim} - (n:nat)(Q n)==(n:nat)(P (inject_nat n)) ===> (x:Z)`x > 0) -> (P x) - - /\ - || - || - - (Q O) (n:nat)(Q n)->(Q (S n)) <=== (P 0) (x:Z) (P x) -> (P (Zs x)) - - <=== (inject_nat (S n))=(Zs (inject_nat n)) - - <=== inject_nat_complete - - Then the diagram will be closed and the theorem proved. -\end{verbatim} -*) - -Lemma inject_nat_complete : - (x:Z)`0 <= x` -> (EX n:nat | x=(inject_nat n)). -Destruct x; Intros; -[ Exists O; Auto with arith -| Specialize (ZL4 p); Intros Hp; Elim Hp; Intros; - Exists (S x0); Intros; Simpl; - Specialize (bij1 x0); Intro Hx0; - Rewrite <- H0 in Hx0; - Apply f_equal with f:=POS; - Apply convert_intro; Auto with arith -| Absurd `0 <= (NEG p)`; - [ Unfold Zle; Simpl; Do 2 (Unfold not); Auto with arith - | Assumption] -]. -Save. - -Lemma ZL4_inf: (y:positive) { h:nat | (convert y)=(S h) }. -Induction y; [ - Intros p H;Elim H; Intros x H1; Exists (plus (S x) (S x)); - Unfold convert ;Simpl; Rewrite ZL0; Rewrite ZL2; Unfold convert in H1; - Rewrite H1; Auto with arith -| Intros p H1;Elim H1;Intros x H2; Exists (plus x (S x)); Unfold convert; - Simpl; Rewrite ZL0; Rewrite ZL2;Unfold convert in H2; Rewrite H2; Auto with arith -| Exists O ;Auto with arith]. -Save. - -Lemma inject_nat_complete_inf : - (x:Z)`0 <= x` -> { n:nat | (x=(inject_nat n)) }. -Destruct x; Intros; -[ Exists O; Auto with arith -| Specialize (ZL4_inf p); Intros Hp; Elim Hp; Intros x0 H0; - Exists (S x0); Intros; Simpl; - Specialize (bij1 x0); Intro Hx0; - Rewrite <- H0 in Hx0; - Apply f_equal with f:=POS; - Apply convert_intro; Auto with arith -| Absurd `0 <= (NEG p)`; - [ Unfold Zle; Simpl; Do 2 (Unfold not); Auto with arith - | Assumption] -]. -Save. - -Lemma inject_nat_prop : - (P:Z->Prop)((n:nat)(P (inject_nat n))) -> - (x:Z) `0 <= x` -> (P x). -Intros. -Specialize (inject_nat_complete x H0). -Intros Hn; Elim Hn; Intros. -Rewrite -> H1; Apply H. -Save. - -Lemma ZERO_le_inj : - (n:nat) `0 <= (inject_nat n)`. -Induction n; Simpl; Intros; -[ Apply Zle_n -| Unfold Zle; Simpl; Discriminate]. -Save. - -Lemma natlike_ind : (P:Z->Prop) (P `0`) -> - ((x:Z)(`0 <= x` -> (P x) -> (P (Zs x)))) -> - (x:Z) `0 <= x` -> (P x). -Intros; Apply inject_nat_prop; -[ Induction n; - [ Simpl; Assumption - | Intros; Rewrite -> (inj_S n0); - Exact (H0 (inject_nat n0) (ZERO_le_inj n0) H2) ] -| Assumption]. -Save. - -Lemma Z_lt_induction : - (P:Z->Prop) - ((x:Z)((y:Z)`0 <= y < x`->(P y))->(P x)) - -> (x:Z)`0 <= x`->(P x). -Proof. -Intros P H x Hx. -Cut (x:Z)`0 <= x`->(y:Z)`0 <= y < x`->(P y). -Intro. -Apply (H0 (Zs x)). -Auto with zarith. - -Split; [ Assumption | Exact (Zlt_n_Sn x) ]. - -Intros x0 Hx0; Generalize Hx0; Pattern x0; Apply natlike_ind. -Intros. -Absurd `0 <= 0`; Try Assumption. -Apply Zgt_not_le. -Apply Zgt_le_trans with m:=y. -Apply Zlt_gt. -Intuition. Intuition. - -Intros. Apply H. Intros. -Apply (H1 H0). -Split; [ Intuition | Idtac ]. -Apply Zlt_le_trans with y. Intuition. -Apply Zgt_S_le. Apply Zlt_gt. Intuition. - -Assumption. -Save. diff --git a/theories/Zarith/ZArith.v b/theories/Zarith/ZArith.v deleted file mode 100644 index b9b572137..000000000 --- a/theories/Zarith/ZArith.v +++ /dev/null @@ -1,23 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(*i $Id$ i*) - -(*s Library for manipulating integers based on binary encoding *) - -Require Export fast_integer. -Require Export zarith_aux. -Require Export auxiliary. -Require Export Zsyntax. -Require Export ZArith_dec. -Require Export Zmisc. -Require Export Wf_Z. - -Hints Resolve Zle_n Zplus_sym Zplus_assoc Zmult_sym Zmult_assoc - Zero_left Zero_right Zmult_one Zplus_inverse_l Zplus_inverse_r - Zmult_plus_distr_l Zmult_plus_distr_r : zarith. diff --git a/theories/Zarith/ZArith_dec.v b/theories/Zarith/ZArith_dec.v deleted file mode 100644 index ee7ee48b7..000000000 --- a/theories/Zarith/ZArith_dec.v +++ /dev/null @@ -1,127 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(*i $Id$ i*) - -Require Sumbool. - -Require fast_integer. -Require zarith_aux. -Require auxiliary. -Require Zsyntax. - -Lemma Dcompare_inf : (r:relation) {r=EGAL} + {r=INFERIEUR} + {r=SUPERIEUR}. -Proof. -Induction r; Auto with arith. -Save. - -Lemma Zcompare_rec : - (P:Set)(x,y:Z) - ((Zcompare x y)=EGAL -> P) -> - ((Zcompare x y)=INFERIEUR -> P) -> - ((Zcompare x y)=SUPERIEUR -> P) -> - P. -Proof. -Intros P x y H1 H2 H3. -Elim (Dcompare_inf (Zcompare x y)). -Intro H. Elim H; Auto with arith. Auto with arith. -Save. - - -Section decidability. - -Local inf_decidable := [P:Prop] {P}+{~P}. - -Variables x,y : Z. - - -Theorem Z_eq_dec : (inf_decidable (x=y)). -Proof. -Unfold inf_decidable. -Apply Zcompare_rec with x:=x y:=y. -Intro. Left. Elim (Zcompare_EGAL x y); Auto with arith. -Intro H3. Right. Elim (Zcompare_EGAL x y). Intros H1 H2. Unfold not. Intro H4. - Rewrite (H2 H4) in H3. Discriminate H3. -Intro H3. Right. Elim (Zcompare_EGAL x y). Intros H1 H2. Unfold not. Intro H4. - Rewrite (H2 H4) in H3. Discriminate H3. -Save. - -Theorem Z_lt_dec : (inf_decidable (Zlt x y)). -Proof. -Unfold inf_decidable Zlt. -Apply Zcompare_rec with x:=x y:=y; Intro H. -Right. Rewrite H. Discriminate. -Left; Assumption. -Right. Rewrite H. Discriminate. -Save. - -Theorem Z_le_dec : (inf_decidable (Zle x y)). -Proof. -Unfold inf_decidable Zle. -Apply Zcompare_rec with x:=x y:=y; Intro H. -Left. Rewrite H. Discriminate. -Left. Rewrite H. Discriminate. -Right. Tauto. -Save. - -Theorem Z_gt_dec : (inf_decidable (Zgt x y)). -Proof. -Unfold inf_decidable Zgt. -Apply Zcompare_rec with x:=x y:=y; Intro H. -Right. Rewrite H. Discriminate. -Right. Rewrite H. Discriminate. -Left; Assumption. -Save. - -Theorem Z_ge_dec : (inf_decidable (Zge x y)). -Proof. -Unfold inf_decidable Zge. -Apply Zcompare_rec with x:=x y:=y; Intro H. -Left. Rewrite H. Discriminate. -Right. Tauto. -Left. Rewrite H. Discriminate. -Save. - -Theorem Z_lt_ge_dec : {`x < y`}+{`x >= y`}. -Proof Z_lt_dec. - -Theorem Z_le_gt_dec : {`x <= y`}+{`x > y`}. -Proof. -Elim Z_le_dec; Auto with arith. -Intro. Right. Apply not_Zle; Auto with arith. -Save. - -Theorem Z_gt_le_dec : {`x > y`}+{`x <= y`}. -Proof Z_gt_dec. - -Theorem Z_ge_lt_dec : {`x >= y`}+{`x < y`}. -Proof. -Elim Z_ge_dec; Auto with arith. -Intro. Right. Apply not_Zge; Auto with arith. -Save. - - -Theorem Z_le_lt_eq_dec : `x <= y` -> {`x < y`}+{x=y}. -Proof. -Intro H. -Apply Zcompare_rec with x:=x y:=y. -Intro. Right. Elim (Zcompare_EGAL x y); Auto with arith. -Intro. Left. Elim (Zcompare_EGAL x y); Auto with arith. -Intro H1. Absurd `x > y`; Auto with arith. -Save. - - -End decidability. - - -Theorem Z_zerop : (x:Z){(`x = 0`)}+{(`x <> 0`)}. -Proof [x:Z](Z_eq_dec x ZERO). - -Definition Z_notzerop := [x:Z](sumbool_not ? ? (Z_zerop x)). - -Definition Z_noteq_dec := [x,y:Z](sumbool_not ? ? (Z_eq_dec x y)). diff --git a/theories/Zarith/Zmisc.v b/theories/Zarith/Zmisc.v deleted file mode 100644 index 663fe535c..000000000 --- a/theories/Zarith/Zmisc.v +++ /dev/null @@ -1,433 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(*i $Id$ i*) - -(********************************************************) -(* Module Zmisc.v : *) -(* Definitions et lemmes complementaires *) -(* Division euclidienne *) -(* Patrick Loiseleur, avril 1997 *) -(********************************************************) - -Require fast_integer. -Require zarith_aux. -Require auxiliary. -Require Zsyntax. -Require Bool. - -(********************************************************************** - Overview of the sections of this file : - - - logic : Logic complements. - - numbers : a few very simple lemmas for manipulating the - constructors [POS], [NEG], [ZERO] and [xI], [xO], [xH] - - registers : defining arrays of bits and their relation with integers. - - iter : the n-th iterate of a function is defined for n:nat and n:positive. - The two notions are identified and an invariant conservation theorem - is proved. - - recursors : Here a nat-like recursor is built. - - arith : lemmas about [< <= ?= + *] ... - -************************************************************************) - -Section logic. - -Lemma rename : (A:Set)(P:A->Prop)(x:A) ((y:A)(x=y)->(P y)) -> (P x). -Auto with arith. -Save. - -End logic. - -Section numbers. - -Definition entier_of_Z := [z:Z]Case z of Nul Pos Pos end. -Definition Z_of_entier := [x:entier]Case x of ZERO POS end. - -(*i Coercion Z_of_entier : entier >-> Z. i*) - -Lemma POS_xI : (p:positive) (POS (xI p))=`2*(POS p) + 1`. -Intro; Apply refl_equal. -Save. -Lemma POS_xO : (p:positive) (POS (xO p))=`2*(POS p)`. -Intro; Apply refl_equal. -Save. -Lemma NEG_xI : (p:positive) (NEG (xI p))=`2*(NEG p) - 1`. -Intro; Apply refl_equal. -Save. -Lemma NEG_xO : (p:positive) (NEG (xO p))=`2*(NEG p)`. -Intro; Apply refl_equal. -Save. - -Lemma POS_add : (p,p':positive)`(POS (add p p'))=(POS p)+(POS p')`. -Induction p; Induction p'; Simpl; Auto with arith. -Save. - -Lemma NEG_add : (p,p':positive)`(NEG (add p p'))=(NEG p)+(NEG p')`. -Induction p; Induction p'; Simpl; Auto with arith. -Save. - -Definition Zle_bool := [x,y:Z]Case `x ?= y` of true true false end. -Definition Zge_bool := [x,y:Z]Case `x ?= y` of true false true end. -Definition Zlt_bool := [x,y:Z]Case `x ?= y` of false true false end. -Definition Zgt_bool := [x,y:Z]Case ` x ?= y` of false false true end. -Definition Zeq_bool := [x,y:Z]Cases `x ?= y` of EGAL => true | _ => false end. -Definition Zneq_bool := [x,y:Z]Cases `x ?= y` of EGAL =>false | _ => true end. - -End numbers. - -Section iterate. - -(* l'itere n-ieme d'une fonction f*) -Fixpoint iter_nat[n:nat] : (A:Set)(f:A->A)A->A := - [A:Set][f:A->A][x:A] - Cases n of - O => x - | (S n') => (f (iter_nat n' A f x)) - end. - -Fixpoint iter_pos[n:positive] : (A:Set)(f:A->A)A->A := - [A:Set][f:A->A][x:A] - Cases n of - xH => (f x) - | (xO n') => (iter_pos n' A f (iter_pos n' A f x)) - | (xI n') => (f (iter_pos n' A f (iter_pos n' A f x))) - end. - -Definition iter := - [n:Z][A:Set][f:A->A][x:A]Cases n of - ZERO => x - | (POS p) => (iter_pos p A f x) - | (NEG p) => x - end. - -Theorem iter_nat_plus : - (n,m:nat)(A:Set)(f:A->A)(x:A) - (iter_nat (plus n m) A f x)=(iter_nat n A f (iter_nat m A f x)). - -Induction n; -[ Simpl; Auto with arith -| Intros; Simpl; Apply f_equal with f:=f; Apply H -]. -Save. - -Theorem iter_convert : (n:positive)(A:Set)(f:A->A)(x:A) - (iter_pos n A f x) = (iter_nat (convert n) A f x). - -Induction n; -[ Intros; Simpl; Rewrite -> (H A f x); - Rewrite -> (H A f (iter_nat (convert p) A f x)); - Rewrite -> (ZL6 p); Symmetry; Apply f_equal with f:=f; - Apply iter_nat_plus -| Intros; Unfold convert; Simpl; Rewrite -> (H A f x); - Rewrite -> (H A f (iter_nat (convert p) A f x)); - Rewrite -> (ZL6 p); Symmetry; - Apply iter_nat_plus -| Simpl; Auto with arith -]. -Save. - -Theorem iter_pos_add : - (n,m:positive)(A:Set)(f:A->A)(x:A) - (iter_pos (add n m) A f x)=(iter_pos n A f (iter_pos m A f x)). - -Intros. -Rewrite -> (iter_convert m A f x). -Rewrite -> (iter_convert n A f (iter_nat (convert m) A f x)). -Rewrite -> (iter_convert (add n m) A f x). -Rewrite -> (convert_add n m). -Apply iter_nat_plus. -Save. - -(* Preservation of invariants : if f : A->A preserves the invariant Inv, - then the iterates of f also preserve it. *) - -Theorem iter_nat_invariant : - (n:nat)(A:Set)(f:A->A)(Inv:A->Prop) - ((x:A)(Inv x)->(Inv (f x)))->(x:A)(Inv x)->(Inv (iter_nat n A f x)). -Induction n; Intros; -[ Trivial with arith -| Simpl; Apply H0 with x:=(iter_nat n0 A f x); Apply H; Trivial with arith]. -Save. - -Theorem iter_pos_invariant : - (n:positive)(A:Set)(f:A->A)(Inv:A->Prop) - ((x:A)(Inv x)->(Inv (f x)))->(x:A)(Inv x)->(Inv (iter_pos n A f x)). -Intros; Rewrite iter_convert; Apply iter_nat_invariant; Trivial with arith. -Save. - -End iterate. - - -Section arith. - -Lemma ZERO_le_POS : (p:positive) `0 <= (POS p)`. -Intro; Unfold Zle; Unfold Zcompare; Discriminate. -Save. - -Lemma POS_gt_ZERO : (p:positive) `(POS p) > 0`. -Intro; Unfold Zgt; Simpl; Trivial with arith. -Save. - -Lemma Zlt_ZERO_pred_le_ZERO : (x:Z) `0 < x` -> `0 <= (Zpred x)`. -Intros. -Rewrite (Zs_pred x) in H. -Apply Zgt_S_le. -Apply Zlt_gt. -Assumption. -Save. - -(* Zeven, Zodd, Zdiv2 and their related properties *) - -Definition Zeven := - [z:Z]Cases z of ZERO => True - | (POS (xO _)) => True - | (NEG (xO _)) => True - | _ => False - end. - -Definition Zodd := - [z:Z]Cases z of (POS xH) => True - | (NEG xH) => True - | (POS (xI _)) => True - | (NEG (xI _)) => True - | _ => False - end. - -Definition Zeven_bool := - [z:Z]Cases z of ZERO => true - | (POS (xO _)) => true - | (NEG (xO _)) => true - | _ => false - end. - -Definition Zodd_bool := - [z:Z]Cases z of ZERO => false - | (POS (xO _)) => false - | (NEG (xO _)) => false - | _ => true - end. - -Lemma Zeven_odd_dec : (z:Z) { (Zeven z) }+{ (Zodd z) }. -Proof. - Intro z. Case z; - [ Left; Compute; Trivial - | Intro p; Case p; Intros; - (Right; Compute; Exact I) Orelse (Left; Compute; Exact I) - | Intro p; Case p; Intros; - (Right; Compute; Exact I) Orelse (Left; Compute; Exact I) ]. - (*i was - Realizer Zeven_bool. - Repeat Program; Compute; Trivial. - i*) -Save. - -Lemma Zeven_dec : (z:Z) { (Zeven z) }+{ ~(Zeven z) }. -Proof. - Intro z. Case z; - [ Left; Compute; Trivial - | Intro p; Case p; Intros; - (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) - | Intro p; Case p; Intros; - (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) ]. - (*i was - Realizer Zeven_bool. - Repeat Program; Compute; Trivial. - i*) -Save. - -Lemma Zodd_dec : (z:Z) { (Zodd z) }+{ ~(Zodd z) }. -Proof. - Intro z. Case z; - [ Right; Compute; Trivial - | Intro p; Case p; Intros; - (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) - | Intro p; Case p; Intros; - (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) ]. - (*i was - Realizer Zodd_bool. - Repeat Program; Compute; Trivial. - i*) -Save. - -Lemma Zeven_not_Zodd : (z:Z)(Zeven z) -> ~(Zodd z). -Proof. - Destruct z; [ Idtac | Destruct p | Destruct p ]; Compute; Trivial. -Save. - -Lemma Zodd_not_Zeven : (z:Z)(Zodd z) -> ~(Zeven z). -Proof. - Destruct z; [ Idtac | Destruct p | Destruct p ]; Compute; Trivial. -Save. - -Hints Unfold Zeven Zodd : zarith. - -(* Zdiv2 is defined on all Z, but notice that for odd negative integers - * it is not the euclidean quotient: in that case we have n = 2*(n/2)-1 - *) - -Definition Zdiv2_pos := - [z:positive]Cases z of xH => xH - | (xO p) => p - | (xI p) => p - end. - -Definition Zdiv2 := - [z:Z]Cases z of ZERO => ZERO - | (POS xH) => ZERO - | (POS p) => (POS (Zdiv2_pos p)) - | (NEG xH) => ZERO - | (NEG p) => (NEG (Zdiv2_pos p)) - end. - -Lemma Zeven_div2 : (x:Z) (Zeven x) -> `x = 2*(Zdiv2 x)`. -Proof. -Destruct x. -Auto with arith. -Destruct p; Auto with arith. -Intros. Absurd (Zeven (POS (xI p0))); Red; Auto with arith. -Intros. Absurd (Zeven `1`); Red; Auto with arith. -Destruct p; Auto with arith. -Intros. Absurd (Zeven (NEG (xI p0))); Red; Auto with arith. -Intros. Absurd (Zeven `-1`); Red; Auto with arith. -Save. - -Lemma Zodd_div2 : (x:Z) `x >= 0` -> (Zodd x) -> `x = 2*(Zdiv2 x)+1`. -Proof. -Destruct x. -Intros. Absurd (Zodd `0`); Red; Auto with arith. -Destruct p; Auto with arith. -Intros. Absurd (Zodd (POS (xO p0))); Red; Auto with arith. -Intros. Absurd `(NEG p) >= 0`; Red; Auto with arith. -Save. - -Lemma Z_modulo_2 : (x:Z) `x >= 0` -> { y:Z | `x=2*y` }+{ y:Z | `x=2*y+1` }. -Proof. -Intros x Hx. -Elim (Zeven_odd_dec x); Intro. -Left. Split with (Zdiv2 x). Exact (Zeven_div2 x a). -Right. Split with (Zdiv2 x). Exact (Zodd_div2 x Hx b). -Save. - -(* Very simple *) -Lemma Zminus_Zplus_compatible : - (x,y,n:Z) `(x+n) - (y+n) = x - y`. -Intros. -Unfold Zminus. -Rewrite -> Zopp_Zplus. -Rewrite -> (Zplus_sym (Zopp y) (Zopp n)). -Rewrite -> Zplus_assoc. -Rewrite <- (Zplus_assoc x n (Zopp n)). -Rewrite -> (Zplus_inverse_r n). -Rewrite <- Zplus_n_O. -Reflexivity. -Save. - -(* Decompose an egality between two ?= relations into 3 implications *) -Theorem Zcompare_egal_dec : - (x1,y1,x2,y2:Z) - (`x1 < y1`->`x2 < y2`) - ->(`x1 ?= y1`=EGAL -> `x2 ?= y2`=EGAL) - ->(`x1 > y1`->`x2 > y2`)->`x1 ?= y1`=`x2 ?= y2`. -Intros x1 y1 x2 y2. -Unfold Zgt; Unfold Zlt; -Case `x1 ?= y1`; Case `x2 ?= y2`; Auto with arith; Symmetry; Auto with arith. -Save. - -Theorem Zcompare_elim : - (c1,c2,c3:Prop)(x,y:Z) - ((x=y) -> c1) ->(`x < y` -> c2) ->(`x > y`-> c3) - -> Case `x ?= y`of c1 c2 c3 end. - -Intros. -Apply rename with x:=`x ?= y`; Intro r; Elim r; -[ Intro; Apply H; Apply (let (h1, h2)=(Zcompare_EGAL x y) in h1); Assumption -| Unfold Zlt in H0; Assumption -| Unfold Zgt in H1; Assumption ]. -Save. - -Lemma Zcompare_x_x : (x:Z) `x ?= x` = EGAL. -Intro; Apply Case (Zcompare_EGAL x x) of [h1,h2: ?]h2 end. -Apply refl_equal. -Save. - -Lemma Zlt_not_eq : (x,y:Z)`x < y` -> ~x=y. -Proof. -Intros. -Unfold Zlt in H. -Unfold not. -Intro. -Generalize (proj2 ? ? (Zcompare_EGAL x y) H0). -Intro. -Rewrite H1 in H. -Discriminate H. -Save. - -Lemma Zcompare_eq_case : - (c1,c2,c3:Prop)(x,y:Z) c1 -> x=y -> (Case `x ?= y` of c1 c2 c3 end). -Intros. -Rewrite -> (Case (Zcompare_EGAL x y) of [h1,h2: ?]h2 end H0). -Assumption. -Save. - -(* Four very basic lemmas about Zle, Zlt, Zge, Zgt *) -Lemma Zle_Zcompare : - (x,y:Z)`x <= y` -> Case `x ?= y` of True True False end. -Intros x y; Unfold Zle; Elim `x ?=y`; Auto with arith. -Save. - -Lemma Zlt_Zcompare : - (x,y:Z)`x < y` -> Case `x ?= y` of False True False end. -Intros x y; Unfold Zlt; Elim `x ?=y`; Intros; Discriminate Orelse Trivial with arith. -Save. - -Lemma Zge_Zcompare : - (x,y:Z)` x >= y`-> Case `x ?= y` of True False True end. -Intros x y; Unfold Zge; Elim `x ?=y`; Auto with arith. -Save. - -Lemma Zgt_Zcompare : - (x,y:Z)`x > y` -> Case `x ?= y` of False False True end. -Intros x y; Unfold Zgt; Elim `x ?= y`; Intros; Discriminate Orelse Trivial with arith. -Save. - -(* Lemmas about Zmin *) - -Lemma Zmin_plus : (x,y,n:Z) `(Zmin (x+n)(y+n))=(Zmin x y)+n`. -Intros; Unfold Zmin. -Rewrite (Zplus_sym x n); -Rewrite (Zplus_sym y n); -Rewrite (Zcompare_Zplus_compatible x y n). -Case `x ?= y`; Apply Zplus_sym. -Save. - -(* Lemmas about absolu *) - -Lemma absolu_lt : (x,y:Z) `0 <= x < y` -> (lt (absolu x) (absolu y)). -Proof. -Intros x y. Case x; Simpl. Case y; Simpl. - -Intro. Absurd `0 < 0`. Compute. Intro H0. Discriminate H0. Intuition. -Intros. Elim (ZL4 p). Intros. Rewrite H0. Auto with arith. -Intros. Elim (ZL4 p). Intros. Rewrite H0. Auto with arith. - -Case y; Simpl. -Intros. Absurd `(POS p) < 0`. Compute. Intro H0. Discriminate H0. Intuition. -Intros. Change (gt (convert p) (convert p0)). -Apply compare_convert_SUPERIEUR. -Elim H; Auto with arith. Intro. Exact (ZC2 p0 p). - -Intros. Absurd `(POS p0) < (NEG p)`. -Compute. Intro H0. Discriminate H0. Intuition. - -Intros. Absurd `0 <= (NEG p)`. Compute. Auto with arith. Intuition. -Save. - - -End arith. - diff --git a/theories/Zarith/Zsyntax.v b/theories/Zarith/Zsyntax.v deleted file mode 100644 index adc1fb64b..000000000 --- a/theories/Zarith/Zsyntax.v +++ /dev/null @@ -1,213 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(* $Id$ *) - -Require Export fast_integer. -Require Export zarith_aux. - -Axiom My_special_variable0 : positive->positive. -Axiom My_special_variable1 : positive->positive. - -Grammar znatural ident := - nat_id [ prim:var($id) ] -> [$id] - -with number := - -with negnumber := - -with formula : constr := - form_expr [ expr($p) ] -> [$p] -| form_eq [ expr($p) "=" expr($c) ] -> [ (eq Z $p $c) ] -| form_le [ expr($p) "<=" expr($c) ] -> [ (Zle $p $c) ] -| form_lt [ expr($p) "<" expr($c) ] -> [ (Zlt $p $c) ] -| form_ge [ expr($p) ">=" expr($c) ] -> [ (Zge $p $c) ] -| form_gt [ expr($p) ">" expr($c) ] -> [ (Zgt $p $c) ] -| form_eq_eq [ expr($p) "=" expr($c) "=" expr($c1) ] - -> [ (eq Z $p $c)/\(eq Z $c $c1) ] -| form_le_le [ expr($p) "<=" expr($c) "<=" expr($c1) ] - -> [ (Zle $p $c)/\(Zle $c $c1) ] -| form_le_lt [ expr($p) "<=" expr($c) "<" expr($c1) ] - -> [ (Zle $p $c)/\(Zlt $c $c1) ] -| form_lt_le [ expr($p) "<" expr($c) "<=" expr($c1) ] - -> [ (Zlt $p $c)/\(Zle $c $c1) ] -| form_lt_lt [ expr($p) "<" expr($c) "<" expr($c1) ] - -> [ (Zlt $p $c)/\(Zlt $c $c1) ] -| form_neq [ expr($p) "<>" expr($c) ] -> [ ~(eq Z $p $c) ] -| form_comp [ expr($p) "?=" expr($c) ] -> [ (Zcompare $p $c) ] - -with expr : constr := - expr_plus [ expr($p) "+" expr($c) ] -> [ (Zplus $p $c) ] -| expr_minus [ expr($p) "-" expr($c) ] -> [ (Zminus $p $c) ] -| expr2 [ expr2($e) ] -> [$e] - -with expr2 : constr := - expr_mult [ expr2($p) "*" expr2($c) ] -> [ (Zmult $p $c) ] -| expr1 [ expr1($e) ] -> [$e] - -with expr1 : constr := - expr_abs [ "|" expr($c) "|" ] -> [ (Zabs $c) ] -| expr0 [ expr0($e) ] -> [$e] - -with expr0 : constr := - expr_id [ constr:global($c) ] -> [ $c ] -| expr_com [ "[" constr:constr($c) "]" ] -> [$c] -| expr_appl [ "(" application($a) ")" ] -> [$a] -| expr_num [ number($s) ] -> [$s ] -| expr_negnum [ "-" negnumber($n) ] -> [ $n ] -| expr_inv [ "-" expr0($c) ] -> [ (Zopp $c) ] - -with application : constr := - apply [ application($p) expr($c1) ] -> [ ($p $c1) ] -| pair [ expr($p) "," expr($c) ] -> [ ($p, $c) ] -| appl0 [ expr($a) ] -> [$a] -. - -Grammar constr constr0 := - z_in_com [ "`" znatural:formula($c) "`" ] -> [$c]. - -Grammar constr pattern := - z_in_pattern [ "`" znatural:number($c) "`" ] -> [$c]. - -(* The symbols "`" "`" must be printed just once at the top of the expession, - to avoid printings like |``x` + `y`` < `45`| - for |x + y < 45|. - So when a Z-expression is to be printed, its sub-expresssions are - enclosed into an ast (ZEXPR $subexpr). (ZEXPR $s) is printed like $s - but without symbols "`" "`" around. *) - -(* There is just one problem: NEG and Zopp have the same printing rules. - If Zopp is opaque, we may not be able to solve a goal like - ` -5 = -5 ` by reflexivity. (In fact, this precise Goal is solved - by the Reflexivity tactic, but more complex problems may arise *) -(* SOLUTION : Print (Zopp 5) for constants and -x for variables *) - -Syntax constr - level 0: - My_special_variable0 [ My_special_variable0 ] -> [ "POS" ] - | My_special_variable1 [ My_special_variable1 ] -> [ "NEG" ] - | Zle [ (Zle $n1 $n2) ] -> - [[<hov 0> "`" (ZEXPR $n1) [1 0] "<= " (ZEXPR $n2) "`"]] - | Zlt [ (Zlt $n1 $n2) ] -> - [[<hov 0> "`" (ZEXPR $n1) [1 0] "< "(ZEXPR $n2) "`" ]] - | Zge [ (Zge $n1 $n2) ] -> - [[<hov 0> "`" (ZEXPR $n1) [1 0] ">= "(ZEXPR $n2) "`" ]] - | Zgt [ (Zgt $n1 $n2) ] -> - [[<hov 0> "`" (ZEXPR $n1) [1 0] "> "(ZEXPR $n2) "`" ]] - | Zcompare [<<(Zcompare $n1 $n2)>>] -> - [[<hov 0> "`" (ZEXPR $n1) [1 0] "?= " (ZEXPR $n2) "`" ]] - | Zeq [ (eq Z $n1 $n2) ] -> - [[<hov 0> "`" (ZEXPR $n1) [1 0] "= "(ZEXPR $n2)"`"]] - | Zneq [ ~(eq Z $n1 $n2) ] -> - [[<hov 0> "`" (ZEXPR $n1) [1 0] "<> "(ZEXPR $n2) "`"]] - | Zle_Zle [ (Zle $n1 $n2)/\(Zle $n2 $n3) ] -> - [[<hov 0> "`" (ZEXPR $n1) [1 0] "<= " (ZEXPR $n2) - [1 0] "<= " (ZEXPR $n3) "`"]] - | Zle_Zlt [ (Zle $n1 $n2)/\(Zlt $n2 $n3) ] -> - [[<hov 0> "`" (ZEXPR $n1) [1 0] "<= "(ZEXPR $n2) - [1 0] "< " (ZEXPR $n3) "`"]] - | Zlt_Zle [ (Zlt $n1 $n2)/\(Zle $n2 $n3) ] -> - [[<hov 0> "`" (ZEXPR $n1) [1 0] "< " (ZEXPR $n2) - [1 0] "<= " (ZEXPR $n3) "`"]] - | Zlt_Zlt [ (Zlt $n1 $n2)/\(Zlt $n2 $n3) ] -> - [[<hov 0> "`" (ZEXPR $n1) [1 0] "< " (ZEXPR $n2) - [1 0] "< " (ZEXPR $n3) "`"]] - | ZZero [ ZERO ] -> ["`0`"] - | ZPos [ (POS $r) ] -> [$r:"positive_printer"] - | ZNeg [ (NEG $r) ] -> [$r:"negative_printer"] - ; - - level 7: - Zplus [ (Zplus $n1 $n2) ] - -> [ [<hov 0> "`"(ZEXPR $n1):E "+" [0 0] (ZEXPR $n2):L "`"] ] - | Zminus [ (Zminus $n1 $n2) ] - -> [ [<hov 0> "`"(ZEXPR $n1):E "-" [0 0] (ZEXPR $n2):L "`"] ] - ; - - level 6: - Zmult [ (Zmult $n1 $n2) ] - -> [ [<hov 0> "`"(ZEXPR $n1):E "*" [0 0] (ZEXPR $n2):L "`"] ] - ; - - level 8: - Zopp [ (Zopp $n1) ] -> [ [<hov 0> "`" "-"(ZEXPR $n1):E "`"] ] - | Zopp_POS [ (Zopp (POS $r)) ] -> - [ [<hov 0> "`(" "Zopp" [1 0] $r:"positive_printer_inside" ")`"] ] - | Zopp_ZERO [ (Zopp ZERO) ] -> [ [<hov 0> "`(" "Zopp" [1 0] "0" ")`"] ] - | Zopp_NEG [ (Zopp (NEG $r)) ] -> - [ [<hov 0> "`(" "Zopp" [1 0] "(" $r:"negative_printer_inside" "))`"] ] - ; - - level 4: - Zabs [ (Zabs $n1) ] -> [ [<hov 0> "`|"(ZEXPR $n1):E "|`"] ] - ; - - level 0: - escape_inside [ << (ZEXPR $r) >> ] -> [ "[" $r:E "]" ] - ; - - level 4: - Zappl_inside [ << (ZEXPR (APPLIST $h ($LIST $t))) >> ] - -> [ [<hov 0> "("(ZEXPR $h):E [1 0] (APPLINSIDETAIL ($LIST $t)):E ")"] ] - | Zappl_inside_tail [ << (APPLINSIDETAIL $h ($LIST $t)) >> ] - -> [(ZEXPR $h):E [1 0] (APPLINSIDETAIL ($LIST $t)):E] - | Zappl_inside_one [ << (APPLINSIDETAIL $e) >> ] ->[(ZEXPR $e):E] - | pair_inside [ << (ZEXPR <<(pair $s1 $s2 $z1 $z2)>>) >> ] - -> [ [<hov 0> "("(ZEXPR $z1):E "," [1 0] (ZEXPR $z2):E ")"] ] - ; - - level 3: - var_inside [ << (ZEXPR ($VAR $i)) >> ] -> [$i] - | const_inside [ << (ZEXPR (CONST $c)) >> ] -> [(CONST $c)] - | mutind_inside [ << (ZEXPR (MUTIND $i $n)) >> ] - -> [(MUTIND $i $n)] - | mutconstruct_inside [ << (ZEXPR (MUTCONSTRUCT $c1 $c2 $c3)) >> ] - -> [ (MUTCONSTRUCT $c1 $c2 $c3) ] - (* Added by JCF, 9/3/98 *) - | implicit_head_inside [ << (ZEXPR (XTRA "!" $c)) >> ] -> [ $c ] - | implicit_arg_inside [ << (ZEXPR (XTRA "!" $n $c)) >> ] -> [ ] - - ; - - level 7: - Zplus_inside - [ << (ZEXPR <<(Zplus $n1 $n2)>>) >> ] - -> [ (ZEXPR $n1):E "+" [0 0] (ZEXPR $n2):L ] - | Zminus_inside - [ << (ZEXPR <<(Zminus $n1 $n2)>>) >> ] - -> [ (ZEXPR $n1):E "-" [0 0] (ZEXPR $n2):L ] - ; - - level 6: - Zmult_inside - [ << (ZEXPR <<(Zmult $n1 $n2)>>) >> ] - -> [ (ZEXPR $n1):E "*" [0 0] (ZEXPR $n2):L ] - ; - - level 5: - Zopp_inside [ << (ZEXPR <<(Zopp $n1)>>) >> ] -> [ "(-" (ZEXPR $n1):E ")" ] - ; - - level 10: - Zopp_POS_inside [ << (ZEXPR <<(Zopp (POS $r))>>) >> ] -> - [ [<hov 0> "Zopp" [1 0] $r:"positive_printer_inside" ] ] - | Zopp_ZERO_inside [ << (ZEXPR <<(Zopp ZERO)>>) >> ] -> - [ [<hov 0> "Zopp" [1 0] "0"] ] - | Zopp_NEG_inside [ << (ZEXPR <<(Zopp (NEG $r))>>) >> ] -> - [ [<hov 0> "Zopp" [1 0] $r:"negative_printer_inside" ] ] - ; - - level 4: - Zabs_inside [ << (ZEXPR <<(Zabs $n1)>>) >> ] -> [ "|" (ZEXPR $n1) "|"] - ; - - level 0: - ZZero_inside [ << (ZEXPR <<ZERO>>) >> ] -> ["0"] - | ZPos_inside [ << (ZEXPR <<(POS $p)>>) >>] -> [$p:"positive_printer_inside"] - | ZNeg_inside [ << (ZEXPR <<(NEG $p)>>) >> ] -> - [$p:"negative_printer_inside"]. diff --git a/theories/Zarith/auxiliary.v b/theories/Zarith/auxiliary.v deleted file mode 100644 index 9a827f104..000000000 --- a/theories/Zarith/auxiliary.v +++ /dev/null @@ -1,930 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) -(**************************************************************************) -(* *) -(* Binary Integers *) -(* *) -(* Pierre Crégut (CNET, Lannion, France) *) -(* *) -(**************************************************************************) - -(* $Id$ *) - -Require Export Arith. -Require fast_integer. -Require zarith_aux. -Require Decidable. -Require Peano_dec. -Require Export Compare_dec. - -Definition neq := [x,y:nat] ~(x=y). -Definition Zne := [x,y:Z] ~(x=y). -Theorem add_un_Zs : (x:positive) (POS (add_un x)) = (Zs (POS x)). -Intro; Rewrite -> ZL12; Unfold Zs; Simpl; Trivial with arith. -Save. - -Theorem inj_S : (y:nat) (inject_nat (S y)) = (Zs (inject_nat y)). -Induction y; [ - Unfold Zs ; Simpl; Trivial with arith -| Intros n; Intros H; - Change (POS (add_un (anti_convert n)))=(Zs (inject_nat (S n))); - Rewrite add_un_Zs; Trivial with arith]. -Save. - -Theorem Zplus_S_n: (x,y:Z) (Zplus (Zs x) y) = (Zs (Zplus x y)). -Intros x y; Unfold Zs; Rewrite (Zplus_sym (Zplus x y)); Rewrite Zplus_assoc; -Rewrite (Zplus_sym (POS xH)); Trivial with arith. -Save. - -Theorem inj_plus : - (x,y:nat) (inject_nat (plus x y)) = (Zplus (inject_nat x) (inject_nat y)). - -Induction x; Induction y; [ - Simpl; Trivial with arith -| Simpl; Trivial with arith -| Simpl; Rewrite <- plus_n_O; Trivial with arith -| Intros m H1; Change (inject_nat (S (plus n (S m))))= - (Zplus (inject_nat (S n)) (inject_nat (S m))); - Rewrite inj_S; Rewrite H; Do 2 Rewrite inj_S; Rewrite Zplus_S_n; Trivial with arith]. -Save. - -Theorem inj_mult : - (x,y:nat) (inject_nat (mult x y)) = (Zmult (inject_nat x) (inject_nat y)). - -Induction x; [ - Simpl; Trivial with arith -| Intros n H y; Rewrite -> inj_S; Rewrite <- Zmult_Sm_n; - Rewrite <- H;Rewrite <- inj_plus; Simpl; Rewrite plus_sym; Trivial with arith]. -Save. - -Theorem inj_neq: - (x,y:nat) (neq x y) -> (Zne (inject_nat x) (inject_nat y)). - -Unfold neq Zne not ; Intros x y H1 H2; Apply H1; Generalize H2; -Case x; Case y; Intros; [ - Auto with arith -| Discriminate H0 -| Discriminate H0 -| Simpl in H0; Injection H0; Do 2 Rewrite <- bij1; Intros E; Rewrite E; Auto with arith]. -Save. - -Theorem inj_le: - (x,y:nat) (le x y) -> (Zle (inject_nat x) (inject_nat y)). - -Intros x y; Intros H; Elim H; [ - Unfold Zle ; Elim (Zcompare_EGAL (inject_nat x) (inject_nat x)); - Intros H1 H2; Rewrite H2; [ Discriminate | Trivial with arith] -| Intros m H1 H2; Apply Zle_trans with (inject_nat m); - [Assumption | Rewrite inj_S; Apply Zle_n_Sn]]. -Save. - -Theorem inj_lt: (x,y:nat) (lt x y) -> (Zlt (inject_nat x) (inject_nat y)). -Intros x y H; Apply Zgt_lt; Apply Zle_S_gt; Rewrite <- inj_S; Apply inj_le; -Exact H. -Save. - -Theorem inj_gt: (x,y:nat) (gt x y) -> (Zgt (inject_nat x) (inject_nat y)). -Intros x y H; Apply Zlt_gt; Apply inj_lt; Exact H. -Save. - -Theorem inj_ge: (x,y:nat) (ge x y) -> (Zge (inject_nat x) (inject_nat y)). -Intros x y H; Apply Zle_ge; Apply inj_le; Apply H. -Save. - -Theorem inj_eq: (x,y:nat) x=y -> (inject_nat x) = (inject_nat y). -Intros x y H; Rewrite H; Trivial with arith. -Save. - -Theorem intro_Z : - (x:nat) (EX y:Z | (inject_nat x)=y /\ - (Zle ZERO (Zplus (Zmult y (POS xH)) ZERO))). -Intros x; Exists (inject_nat x); Split; [ - Trivial with arith -| Rewrite Zmult_sym; Rewrite Zmult_one; Rewrite Zero_right; - Unfold Zle ; Elim x; Intros;Simpl; Discriminate ]. -Save. - -Theorem inj_minus1 : - (x,y:nat) (le y x) -> - (inject_nat (minus x y)) = (Zminus (inject_nat x) (inject_nat y)). -Intros x y H; Apply (Zsimpl_plus_l (inject_nat y)); Unfold Zminus ; -Rewrite Zplus_permute; Rewrite Zplus_inverse_r; Rewrite <- inj_plus; -Rewrite <- (le_plus_minus y x H);Rewrite Zero_right; Trivial with arith. -Save. - -Theorem inj_minus2: (x,y:nat) (gt y x) -> (inject_nat (minus x y)) = ZERO. -Intros x y H; Rewrite inj_minus_aux; [ Trivial with arith | Apply gt_not_le; Assumption]. -Save. - -Theorem dec_eq: (x,y:Z) (decidable (x=y)). -Intros x y; Unfold decidable ; Elim (Zcompare_EGAL x y); -Intros H1 H2; Elim (Dcompare (Zcompare x y)); [ - Tauto - | Intros H3; Right; Unfold not ; Intros H4; - Elim H3; Rewrite (H2 H4); Intros H5; Discriminate H5]. -Save. - -Theorem dec_Zne: (x,y:Z) (decidable (Zne x y)). -Intros x y; Unfold decidable Zne ; Elim (Zcompare_EGAL x y). -Intros H1 H2; Elim (Dcompare (Zcompare x y)); - [ Right; Rewrite H1; Auto - | Left; Unfold not; Intro; Absurd (Zcompare x y)=EGAL; - [ Elim H; Intros HR; Rewrite HR; Discriminate - | Auto]]. -Save. - -Theorem dec_Zle: (x,y:Z) (decidable (Zle x y)). -Intros x y; Unfold decidable Zle ; Elim (Zcompare x y); [ - Left; Discriminate - | Left; Discriminate - | Right; Unfold not ; Intros H; Apply H; Trivial with arith]. -Save. - -Theorem dec_Zgt: (x,y:Z) (decidable (Zgt x y)). -Intros x y; Unfold decidable Zgt ; Elim (Zcompare x y); - [ Right; Discriminate | Right; Discriminate | Auto with arith]. -Save. - -Theorem dec_Zge: (x,y:Z) (decidable (Zge x y)). -Intros x y; Unfold decidable Zge ; Elim (Zcompare x y); [ - Left; Discriminate -| Right; Unfold not ; Intros H; Apply H; Trivial with arith -| Left; Discriminate]. -Save. - -Theorem dec_Zlt: (x,y:Z) (decidable (Zlt x y)). -Intros x y; Unfold decidable Zlt ; Elim (Zcompare x y); - [ Right; Discriminate | Auto with arith | Right; Discriminate]. -Save. -Theorem dec_eq_nat:(x,y:nat)(decidable (x=y)). -Intros x y; Unfold decidable; Elim (eq_nat_dec x y); Auto with arith. -Save. - -Theorem not_Zge : (x,y:Z) ~(Zge x y) -> (Zlt x y). -Unfold Zge Zlt ; Intros x y H; Apply dec_not_not; - [ Exact (dec_Zlt x y) | Assumption]. -Save. - -Theorem not_Zlt : (x,y:Z) ~(Zlt x y) -> (Zge x y). -Unfold Zlt Zge; Auto with arith. -Save. - -Theorem not_Zle : (x,y:Z) ~(Zle x y) -> (Zgt x y). -Unfold Zle Zgt ; Intros x y H; Apply dec_not_not; - [ Exact (dec_Zgt x y) | Assumption]. - Save. - -Theorem not_Zgt : (x,y:Z) ~(Zgt x y) -> (Zle x y). -Unfold Zgt Zle; Auto with arith. -Save. - -Theorem not_Zeq : (x,y:Z) ~ x=y -> (Zlt x y) \/ (Zlt y x). - -Intros x y; Elim (Dcompare (Zcompare x y)); [ - Intros H1 H2; Absurd x=y; [ Assumption | Elim (Zcompare_EGAL x y); Auto with arith] -| Unfold Zlt ; Intros H; Elim H; Intros H1; - [Auto with arith | Right; Elim (Zcompare_ANTISYM x y); Auto with arith]]. -Save. - -Lemma new_var: (x:Z) (EX y:Z |(x=y)). -Intros x; Exists x; Trivial with arith. -Save. - -Theorem Zne_left : (x,y:Z) (Zne x y) -> (Zne (Zplus x (Zopp y)) ZERO). -Intros x y; Unfold Zne; Unfold not; Intros H1 H2; Apply H1; -Apply Zsimpl_plus_l with (Zopp y); Rewrite Zplus_inverse_l; Rewrite Zplus_sym; -Trivial with arith. -Save. - -Theorem Zegal_left : (x,y:Z) (x=y) -> (Zplus x (Zopp y)) = ZERO. -Intros x y H; -Apply (Zsimpl_plus_l y);Rewrite -> Zplus_permute; -Rewrite -> Zplus_inverse_r;Do 2 Rewrite -> Zero_right;Assumption. -Save. - -Theorem Zle_left : (x,y:Z) (Zle x y) -> (Zle ZERO (Zplus y (Zopp x))). -Intros x y H; Replace ZERO with (Zplus x (Zopp x)). -Apply Zle_reg_r; Trivial. -Apply Zplus_inverse_r. -Save. - -Theorem Zle_left_rev : (x,y:Z) (Zle ZERO (Zplus y (Zopp x))) - -> (Zle x y). -Intros x y H; Apply (Zsimpl_le_plus_r (Zopp x)). -Rewrite Zplus_inverse_r; Trivial. -Save. - -Theorem Zlt_left_rev : (x,y:Z) (Zlt ZERO (Zplus y (Zopp x))) - -> (Zlt x y). -Intros x y H; Apply Zsimpl_lt_plus_r with (Zopp x). -Rewrite Zplus_inverse_r; Trivial. -Save. - -Theorem Zlt_left : - (x,y:Z) (Zlt x y) -> (Zle ZERO (Zplus (Zplus y (NEG xH)) (Zopp x))). -Intros x y H; Apply Zle_left; Apply Zle_S_n; -Change (Zle (Zs x) (Zs (Zpred y))); Rewrite <- Zs_pred; Apply Zlt_le_S; -Assumption. -Save. - -Theorem Zlt_left_lt : - (x,y:Z) (Zlt x y) -> (Zlt ZERO (Zplus y (Zopp x))). -Intros x y H; Replace ZERO with (Zplus x (Zopp x)). -Apply Zlt_reg_r; Trivial. -Apply Zplus_inverse_r. -Save. - -Theorem Zge_left : (x,y:Z) (Zge x y) -> (Zle ZERO (Zplus x (Zopp y))). -Intros x y H; Apply Zle_left; Apply Zge_le; Assumption. -Save. - -Theorem Zgt_left : - (x,y:Z) (Zgt x y) -> (Zle ZERO (Zplus (Zplus x (NEG xH)) (Zopp y))). -Intros x y H; Apply Zlt_left; Apply Zgt_lt; Assumption. -Save. - -Theorem Zgt_left_gt : - (x,y:Z) (Zgt x y) -> (Zgt (Zplus x (Zopp y)) ZERO). -Intros x y H; Replace ZERO with (Zplus y (Zopp y)). -Apply Zgt_reg_r; Trivial. -Apply Zplus_inverse_r. -Save. - -Theorem Zgt_left_rev : (x,y:Z) (Zgt (Zplus x (Zopp y)) ZERO) - -> (Zgt x y). -Intros x y H; Apply Zsimpl_gt_plus_r with (Zopp y). -Rewrite Zplus_inverse_r; Trivial. -Save. - -Theorem Zopp_one : (x:Z)(Zopp x)=(Zmult x (NEG xH)). -Induction x; Intros; Rewrite Zmult_sym; Auto with arith. -Save. - -Theorem Zopp_Zmult_r : (x,y:Z)(Zopp (Zmult x y)) = (Zmult x (Zopp y)). -Intros x y; Rewrite Zmult_sym; Rewrite <- Zopp_Zmult; Apply Zmult_sym. -Save. - -Theorem Zmult_Zopp_left : (x,y:Z)(Zmult (Zopp x) y) = (Zmult x (Zopp y)). -Intros; Rewrite Zopp_Zmult; Rewrite Zopp_Zmult_r; Trivial with arith. -Save. - -Theorem Zopp_Zmult_l : (x,y:Z)(Zopp (Zmult x y)) = (Zmult (Zopp x) y). -Intros x y; Symmetry; Apply Zopp_Zmult. -Save. - -Theorem Zred_factor0 : (x:Z) x = (Zmult x (POS xH)). -Intro x; Rewrite (Zmult_n_1 x); Trivial with arith. -Save. - -Theorem Zred_factor1 : (x:Z) (Zplus x x) = (Zmult x (POS (xO xH))). -Intros x; Pattern 1 2 x ; Rewrite <- (Zmult_n_1 x); -Rewrite <- Zmult_plus_distr_r; Auto with arith. -Save. - -Theorem Zred_factor2 : - (x,y:Z) (Zplus x (Zmult x y)) = (Zmult x (Zplus (POS xH) y)). - -Intros x y; Pattern 1 x ; Rewrite <- (Zmult_n_1 x); -Rewrite <- Zmult_plus_distr_r; Trivial with arith. -Save. - -Theorem Zred_factor3 : - (x,y:Z) (Zplus (Zmult x y) x) = (Zmult x (Zplus (POS xH) y)). - -Intros x y; Pattern 2 x ; Rewrite <- (Zmult_n_1 x); -Rewrite <- Zmult_plus_distr_r; Rewrite Zplus_sym; Trivial with arith. -Save. -Theorem Zred_factor4 : - (x,y,z:Z) (Zplus (Zmult x y) (Zmult x z)) = (Zmult x (Zplus y z)). -Intros x y z; Symmetry; Apply Zmult_plus_distr_r. -Save. - -Theorem Zred_factor5 : (x,y:Z) (Zplus (Zmult x ZERO) y) = y. - -Intros x y; Rewrite <- Zmult_n_O;Auto with arith. -Save. - -Theorem Zred_factor6 : (x:Z) x = (Zplus x ZERO). - -Intro; Rewrite Zero_right; Trivial with arith. -Save. - -Theorem Zcompare_Zplus_compatible2 : - (r:relation)(x,y,z,t:Z) - (Zcompare x y) = r -> (Zcompare z t) = r -> - (Zcompare (Zplus x z) (Zplus y t)) = r. - -Intros r x y z t; Case r; [ - Intros H1 H2; Elim (Zcompare_EGAL x y); Elim (Zcompare_EGAL z t); - Intros H3 H4 H5 H6; Rewrite H3; [ - Rewrite H5; [ Elim (Zcompare_EGAL (Zplus y t) (Zplus y t)); Auto with arith | Auto with arith ] - | Auto with arith ] -| Intros H1 H2; Elim (Zcompare_ANTISYM (Zplus y t) (Zplus x z)); - Intros H3 H4; Apply H3; - Apply Zcompare_trans_SUPERIEUR with y:=(Zplus y z) ; [ - Rewrite Zcompare_Zplus_compatible; - Elim (Zcompare_ANTISYM t z); Auto with arith - | Do 2 Rewrite <- (Zplus_sym z); - Rewrite Zcompare_Zplus_compatible; - Elim (Zcompare_ANTISYM y x); Auto with arith] -| Intros H1 H2; - Apply Zcompare_trans_SUPERIEUR with y:=(Zplus x t) ; [ - Rewrite Zcompare_Zplus_compatible; Assumption - | Do 2 Rewrite <- (Zplus_sym t); - Rewrite Zcompare_Zplus_compatible; Assumption]]. -Save. - -Lemma add_x_x : (x:positive) (add x x) = (xO x). -Intros p; Apply convert_intro; Simpl; Rewrite convert_add; -Unfold 3 convert ; Simpl; Rewrite ZL6; Trivial with arith. -Save. - -Theorem Zcompare_Zmult_compatible : - (x:positive)(y,z:Z) - (Zcompare (Zmult (POS x) y) (Zmult (POS x) z)) = (Zcompare y z). - -Induction x; [ - Intros p H y z; - Cut (POS (xI p))=(Zplus (Zplus (POS p) (POS p)) (POS xH)); [ - Intros E; Rewrite E; Do 4 Rewrite Zmult_plus_distr_l; - Do 2 Rewrite Zmult_one; - Apply Zcompare_Zplus_compatible2; [ - Apply Zcompare_Zplus_compatible2; Apply H - | Trivial with arith] - | Simpl; Rewrite (add_x_x p); Trivial with arith] -| Intros p H y z; Cut (POS (xO p))=(Zplus (POS p) (POS p)); [ - Intros E; Rewrite E; Do 2 Rewrite Zmult_plus_distr_l; - Apply Zcompare_Zplus_compatible2; Apply H - | Simpl; Rewrite (add_x_x p); Trivial with arith] - | Intros y z; Do 2 Rewrite Zmult_one; Trivial with arith]. -Save. - -Theorem Zmult_eq: - (x,y:Z) ~(x=ZERO) -> (Zmult y x) = ZERO -> y = ZERO. - -Intros x y; Case x; [ - Intro; Absurd ZERO=ZERO; Auto with arith -| Intros p H1 H2; Elim (Zcompare_EGAL y ZERO); - Intros H3 H4; Apply H3; Rewrite <- (Zcompare_Zmult_compatible p); - Rewrite -> Zero_mult_right; Rewrite -> Zmult_sym; - Elim (Zcompare_EGAL (Zmult y (POS p)) ZERO); Auto with arith -| Intros p H1 H2; Apply Zopp_intro; Simpl; - Elim (Zcompare_EGAL (Zopp y) ZERO); Intros H3 H4; Apply H3; - Rewrite <- (Zcompare_Zmult_compatible p); - Rewrite -> Zero_mult_right; Rewrite -> Zmult_sym; - Rewrite -> Zmult_Zopp_left; Simpl; - Elim (Zcompare_EGAL (Zmult y (NEG p)) ZERO); Auto with arith]. -Save. - -Theorem Z_eq_mult: - (x,y:Z) y = ZERO -> (Zmult y x) = ZERO. -Intros x y H; Rewrite H; Auto with arith. -Save. - -Theorem Zmult_le: - (x,y:Z) (Zgt x ZERO) -> (Zle ZERO (Zmult y x)) -> (Zle ZERO y). - -Intros x y; Case x; [ - Simpl; Unfold Zgt ; Simpl; Intros H; Discriminate H -| Intros p H1; Unfold Zle; Rewrite -> Zmult_sym; - Pattern 1 ZERO ; Rewrite <- (Zero_mult_right (POS p)); - Rewrite Zcompare_Zmult_compatible; Auto with arith -| Intros p; Unfold Zgt ; Simpl; Intros H; Discriminate H]. -Save. - -Theorem Zle_ZERO_mult : - (x,y:Z) (Zle ZERO x) -> (Zle ZERO y) -> (Zle ZERO (Zmult x y)). -Intros x y; Case x. -Intros; Rewrite Zero_mult_left; Trivial. -Intros p H1; Unfold Zle. - Pattern 2 ZERO ; Rewrite <- (Zero_mult_right (POS p)). - Rewrite Zcompare_Zmult_compatible; Trivial. -Intros p H1 H2; Absurd (Zgt ZERO (NEG p)); Trivial. -Unfold Zgt; Simpl; Auto with zarith. -Save. - -Lemma Zgt_ZERO_mult: (a,b:Z) (Zgt a ZERO)->(Zgt b ZERO) - ->(Zgt (Zmult a b) ZERO). -Intros x y; Case x. -Intros H; Discriminate H. -Intros p H1; Unfold Zgt; -Pattern 2 ZERO ; Rewrite <- (Zero_mult_right (POS p)). - Rewrite Zcompare_Zmult_compatible; Trivial. -Intros p H; Discriminate H. -Save. - -Theorem Zle_mult: - (x,y:Z) (Zgt x ZERO) -> (Zle ZERO y) -> (Zle ZERO (Zmult y x)). -Intros x y H1 H2; Apply Zle_ZERO_mult; Trivial. -Apply Zlt_le_weak; Apply Zgt_lt; Trivial. -Save. - -Theorem Zmult_lt: - (x,y:Z) (Zgt x ZERO) -> (Zlt ZERO (Zmult y x)) -> (Zlt ZERO y). - -Intros x y; Case x; [ - Simpl; Unfold Zgt ; Simpl; Intros H; Discriminate H -| Intros p H1; Unfold Zlt; Rewrite -> Zmult_sym; - Pattern 1 ZERO ; Rewrite <- (Zero_mult_right (POS p)); - Rewrite Zcompare_Zmult_compatible; Auto with arith -| Intros p; Unfold Zgt ; Simpl; Intros H; Discriminate H]. -Save. - -Theorem Zmult_gt: - (x,y:Z) (Zgt x ZERO) -> (Zgt (Zmult x y) ZERO) -> (Zgt y ZERO). - -Intros x y; Case x. - Intros H; Discriminate H. - Intros p H1; Unfold Zgt. - Pattern 1 ZERO ; Rewrite <- (Zero_mult_right (POS p)). - Rewrite Zcompare_Zmult_compatible; Trivial. -Intros p H; Discriminate H. -Save. - -Theorem Zle_mult_approx: - (x,y,z:Z) (Zgt x ZERO) -> (Zgt z ZERO) -> (Zle ZERO y) -> - (Zle ZERO (Zplus (Zmult y x) z)). - -Intros x y z H1 H2 H3; Apply Zle_trans with m:=(Zmult y x) ; [ - Apply Zle_mult; Assumption -| Pattern 1 (Zmult y x) ; Rewrite <- Zero_right; Apply Zle_reg_l; - Apply Zlt_le_weak; Apply Zgt_lt; Assumption]. -Save. - -Lemma Zle_Zmult_pos_right : - (a,b,c : Z) - (Zle a b) -> (Zle ZERO c) -> (Zle (Zmult a c) (Zmult b c)). -Intros a b c H1 H2; Apply Zle_left_rev. -Rewrite Zopp_Zmult_l. -Rewrite <- Zmult_plus_distr_l. -Apply Zle_ZERO_mult; Trivial. -Apply Zle_left; Trivial. -Save. - -Lemma Zle_Zmult_pos_left : - (a,b,c : Z) - (Zle a b) -> (Zle ZERO c) -> (Zle (Zmult c a) (Zmult c b)). -Intros a b c H1 H2; Rewrite (Zmult_sym c a);Rewrite (Zmult_sym c b). -Apply Zle_Zmult_pos_right; Trivial. -Save. - -Lemma Zge_Zmult_pos_right : - (a,b,c : Z) - (Zge a b) -> (Zge c ZERO) -> (Zge (Zmult a c) (Zmult b c)). -Intros a b c H1 H2; Apply Zle_ge. -Apply Zle_Zmult_pos_right; Apply Zge_le; Trivial. -Save. - -Lemma Zge_Zmult_pos_left : - (a,b,c : Z) - (Zge a b) -> (Zge c ZERO) -> (Zge (Zmult c a) (Zmult c b)). -Intros a b c H1 H2; Apply Zle_ge. -Apply Zle_Zmult_pos_left; Apply Zge_le; Trivial. -Save. - -Lemma Zge_Zmult_pos_compat : - (a,b,c,d : Z) - (Zge a c) -> (Zge b d) -> (Zge c ZERO) -> (Zge d ZERO) - -> (Zge (Zmult a b) (Zmult c d)). -Intros a b c d H0 H1 H2 H3. -Apply Zge_trans with (Zmult a d). -Apply Zge_Zmult_pos_left; Trivial. -Apply Zge_trans with c; Trivial. -Apply Zge_Zmult_pos_right; Trivial. -Save. - -Lemma Zle_mult_simpl - : (a,b,c:Z) (Zgt c ZERO)->(Zle (Zmult a c) (Zmult b c))->(Zle a b). -Intros a b c H1 H2; Apply Zle_left_rev. -Apply Zmult_le with c; Trivial. -Rewrite Zmult_plus_distr_l. -Rewrite <- Zopp_Zmult_l. -Apply Zle_left; Trivial. -Save. - - -Lemma Zge_mult_simpl - : (a,b,c:Z) (Zgt c ZERO)->(Zge (Zmult a c) (Zmult b c))->(Zge a b). -Intros a b c H1 H2; Apply Zle_ge; Apply Zle_mult_simpl with c; Trivial. -Apply Zge_le; Trivial. -Save. - -Lemma Zgt_mult_simpl - : (a,b,c:Z) (Zgt c ZERO)->(Zgt (Zmult a c) (Zmult b c))->(Zgt a b). -Intros a b c H1 H2; Apply Zgt_left_rev. -Apply Zmult_gt with c; Trivial. -Rewrite Zmult_sym. -Rewrite Zmult_plus_distr_l. -Rewrite <- Zopp_Zmult_l. -Apply Zgt_left_gt; Trivial. -Save. - -Lemma Zgt_square_simpl: -(x, y : Z) (Zge x ZERO) -> (Zge y ZERO) - -> (Zgt (Zmult x x) (Zmult y y)) -> (Zgt x y). -Intros x y H0 H1 H2. -Case (dec_Zlt y x). -Intro; Apply Zlt_gt; Trivial. -Intros H3; Cut (Zge y x). -Intros H. -Elim Zgt_not_le with 1 := H2. -Apply Zge_le. -Apply Zge_Zmult_pos_compat; Auto. -Apply not_Zlt; Trivial. -Qed. - - -Theorem Zmult_le_approx: - (x,y,z:Z) (Zgt x ZERO) -> (Zgt x z) -> - (Zle ZERO (Zplus (Zmult y x) z)) -> (Zle ZERO y). - -Intros x y z H1 H2 H3; Apply Zlt_n_Sm_le; Apply (Zmult_lt x); [ - Assumption - | Apply Zle_lt_trans with 1:=H3 ; Rewrite <- Zmult_Sm_n; - Apply Zlt_reg_l; Apply Zgt_lt; Assumption]. - -Save. - -Theorem OMEGA1 : (x,y:Z) (x=y) -> (Zle ZERO x) -> (Zle ZERO y). -Intros x y H; Rewrite H; Auto with arith. -Save. - -Theorem OMEGA2 : (x,y:Z) (Zle ZERO x) -> (Zle ZERO y) -> (Zle ZERO (Zplus x y)). -Intros x y H1 H2;Rewrite <- (Zero_left ZERO); Apply Zle_plus_plus; Assumption. -Save. - -Theorem OMEGA3 : (x,y,k:Z)(Zgt k ZERO)-> (x=(Zmult y k)) -> (x=ZERO) -> (y=ZERO). - -Intros x y k H1 H2 H3; Apply (Zmult_eq k); [ - Unfold not ; Intros H4; Absurd (Zgt k ZERO); [ - Rewrite H4; Unfold Zgt ; Simpl; Discriminate | Assumption] - | Rewrite <- H2; Assumption]. -Save. - -Theorem OMEGA4 : - (x,y,z:Z)(Zgt x ZERO) -> (Zgt y x) -> ~(Zplus (Zmult z y) x) = ZERO. - -Unfold not ; Intros x y z H1 H2 H3; Cut (Zgt y ZERO); [ - Intros H4; Cut (Zle ZERO (Zplus (Zmult z y) x)); [ - Intros H5; Generalize (Zmult_le_approx y z x H4 H2 H5) ; Intros H6; - Absurd (Zgt (Zplus (Zmult z y) x) ZERO); [ - Rewrite -> H3; Unfold Zgt ; Simpl; Discriminate - | Apply Zle_gt_trans with x ; [ - Pattern 1 x ; Rewrite <- (Zero_left x); Apply Zle_reg_r; - Rewrite -> Zmult_sym; Generalize H4 ; Unfold Zgt; - Case y; [ - Simpl; Intros H7; Discriminate H7 - | Intros p H7; Rewrite <- (Zero_mult_right (POS p)); - Unfold Zle ; Rewrite -> Zcompare_Zmult_compatible; Exact H6 - | Simpl; Intros p H7; Discriminate H7] - | Assumption]] - | Rewrite -> H3; Unfold Zle ; Simpl; Discriminate] - | Apply Zgt_trans with x ; [ Assumption | Assumption]]. -Save. - -Theorem OMEGA5: (x,y,z:Z)(x=ZERO) -> (y=ZERO) -> (Zplus x (Zmult y z)) = ZERO. - -Intros x y z H1 H2; Rewrite H1; Rewrite H2; Simpl; Trivial with arith. -Save. -Theorem OMEGA6: - (x,y,z:Z)(Zle ZERO x) -> (y=ZERO) -> (Zle ZERO (Zplus x (Zmult y z))). - -Intros x y z H1 H2; Rewrite H2; Simpl; Rewrite Zero_right; Assumption. -Save. - -Theorem OMEGA7: - (x,y,z,t:Z)(Zgt z ZERO) -> (Zgt t ZERO) -> (Zle ZERO x) -> (Zle ZERO y) -> - (Zle ZERO (Zplus (Zmult x z) (Zmult y t))). - -Intros x y z t H1 H2 H3 H4; Rewrite <- (Zero_left ZERO); -Apply Zle_plus_plus; Apply Zle_mult; Assumption. -Save. - -Theorem OMEGA8: (x,y:Z) (Zle ZERO x) -> (Zle ZERO y) -> x = (Zopp y) -> x = ZERO. - -Intros x y H1 H2 H3; Elim (Zle_lt_or_eq ZERO x H1); [ - Intros H4; Absurd (Zlt ZERO x); [ - Change (Zge ZERO x); Apply Zle_ge; Apply (Zsimpl_le_plus_l y); - Rewrite -> H3; Rewrite Zplus_inverse_r; Rewrite Zero_right; Assumption - | Assumption] -| Intros H4; Rewrite -> H4; Trivial with arith]. -Save. - -Theorem OMEGA9:(x,y,z,t:Z) y=ZERO -> x = z -> - (Zplus y (Zmult (Zplus (Zopp x) z) t)) = ZERO. - -Intros x y z t H1 H2; Rewrite H2; Rewrite Zplus_inverse_l; -Rewrite Zero_mult_left; Rewrite Zero_right; Assumption. -Save. -Theorem OMEGA10:(v,c1,c2,l1,l2,k1,k2:Z) - (Zplus (Zmult (Zplus (Zmult v c1) l1) k1) (Zmult (Zplus (Zmult v c2) l2) k2)) - = (Zplus (Zmult v (Zplus (Zmult c1 k1) (Zmult c2 k2))) - (Zplus (Zmult l1 k1) (Zmult l2 k2))). - -Intros; Repeat (Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r); -Repeat Rewrite Zmult_assoc; Repeat Elim Zplus_assoc; -Rewrite (Zplus_permute (Zmult l1 k1) (Zmult (Zmult v c2) k2)); Trivial with arith. -Save. - -Theorem OMEGA11:(v1,c1,l1,l2,k1:Z) - (Zplus (Zmult (Zplus (Zmult v1 c1) l1) k1) l2) - = (Zplus (Zmult v1 (Zmult c1 k1)) (Zplus (Zmult l1 k1) l2)). - -Intros; Repeat (Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r); -Repeat Rewrite Zmult_assoc; Repeat Elim Zplus_assoc; Trivial with arith. -Save. - -Theorem OMEGA12:(v2,c2,l1,l2,k2:Z) - (Zplus l1 (Zmult (Zplus (Zmult v2 c2) l2) k2)) - = (Zplus (Zmult v2 (Zmult c2 k2)) (Zplus l1 (Zmult l2 k2))). - -Intros; Repeat (Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r); -Repeat Rewrite Zmult_assoc; Repeat Elim Zplus_assoc; Rewrite Zplus_permute; -Trivial with arith. -Save. - -Theorem OMEGA13:(v,l1,l2:Z)(x:positive) - (Zplus (Zplus (Zmult v (POS x)) l1) (Zplus (Zmult v (NEG x)) l2)) - = (Zplus l1 l2). - -Intros; Rewrite Zplus_assoc; Rewrite (Zplus_sym (Zmult v (POS x)) l1); -Rewrite (Zplus_assoc_r l1); Rewrite <- Zmult_plus_distr_r; -Rewrite <- Zopp_NEG; Rewrite (Zplus_sym (Zopp (NEG x)) (NEG x)); -Rewrite Zplus_inverse_r; Rewrite Zero_mult_right; Rewrite Zero_right; Trivial with arith. -Save. - -Theorem OMEGA14:(v,l1,l2:Z)(x:positive) - (Zplus (Zplus (Zmult v (NEG x)) l1) (Zplus (Zmult v (POS x)) l2)) - = (Zplus l1 l2). - -Intros; Rewrite Zplus_assoc; Rewrite (Zplus_sym (Zmult v (NEG x)) l1); -Rewrite (Zplus_assoc_r l1); Rewrite <- Zmult_plus_distr_r; -Rewrite <- Zopp_NEG; Rewrite Zplus_inverse_r; Rewrite Zero_mult_right; -Rewrite Zero_right; Trivial with arith. -Save. -Theorem OMEGA15:(v,c1,c2,l1,l2,k2:Z) - (Zplus (Zplus (Zmult v c1) l1) (Zmult (Zplus (Zmult v c2) l2) k2)) - = (Zplus (Zmult v (Zplus c1 (Zmult c2 k2))) - (Zplus l1 (Zmult l2 k2))). - -Intros; Repeat (Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r); -Repeat Rewrite Zmult_assoc; Repeat Elim Zplus_assoc; -Rewrite (Zplus_permute l1 (Zmult (Zmult v c2) k2)); Trivial with arith. -Save. - -Theorem OMEGA16: - (v,c,l,k:Z) - (Zmult (Zplus (Zmult v c) l) k) = (Zplus (Zmult v (Zmult c k)) (Zmult l k)). - -Intros; Repeat (Rewrite Zmult_plus_distr_l Orelse Rewrite Zmult_plus_distr_r); -Repeat Rewrite Zmult_assoc; Repeat Elim Zplus_assoc; Trivial with arith. -Save. - -Theorem OMEGA17: - (x,y,z:Z)(Zne x ZERO) -> (y=ZERO) -> (Zne (Zplus x (Zmult y z)) ZERO). - -Unfold Zne not; Intros x y z H1 H2 H3; Apply H1; -Apply Zsimpl_plus_l with (Zmult y z); Rewrite Zplus_sym; Rewrite H3; -Rewrite H2; Auto with arith. -Save. - -Theorem OMEGA18: -(x,y,k:Z) (x=(Zmult y k)) -> (Zne x ZERO) -> (Zne y ZERO). - -Unfold Zne not; Intros x y k H1 H2 H3; Apply H2; Rewrite H1; Rewrite H3; Auto with arith. -Save. - -Theorem OMEGA19: - (x:Z) (Zne x ZERO) -> - (Zle ZERO (Zplus x (NEG xH))) \/ (Zle ZERO (Zplus (Zmult x (NEG xH)) (NEG xH))). - -Unfold Zne ; Intros x H; Elim (Zle_or_lt ZERO x); [ - Intros H1; Elim Zle_lt_or_eq with 1:=H1; [ - Intros H2; Left; Change (Zle ZERO (Zpred x)); Apply Zle_S_n; - Rewrite <- Zs_pred; Apply Zlt_le_S; Assumption - | Intros H2; Absurd x=ZERO; Auto with arith] -| Intros H1; Right; Rewrite <- Zopp_one; Rewrite Zplus_sym; - Apply Zle_left; Apply Zle_S_n; Simpl; Apply Zlt_le_S; Auto with arith]. -Save. - -Theorem OMEGA20: - (x,y,z:Z)(Zne x ZERO) -> (y=ZERO) -> (Zne (Zplus x (Zmult y z)) ZERO). - -Unfold Zne not; Intros x y z H1 H2 H3; Apply H1; Rewrite H2 in H3; -Simpl in H3; Rewrite (Zero_right x) in H3; Trivial with arith. -Save. - -Definition fast_Zplus_sym := -[x,y:Z][P:Z -> Prop][H: (P (Zplus y x))] - (eq_ind_r Z (Zplus y x) P H (Zplus x y) (Zplus_sym x y)). - -Definition fast_Zplus_assoc_r := -[n,m,p:Z][P:Z -> Prop][H : (P (Zplus n (Zplus m p)))] - (eq_ind_r Z (Zplus n (Zplus m p)) P H (Zplus (Zplus n m) p) (Zplus_assoc_r n m p)). - -Definition fast_Zplus_assoc_l := -[n,m,p:Z][P:Z -> Prop][H : (P (Zplus (Zplus n m) p))] - (eq_ind_r Z (Zplus (Zplus n m) p) P H (Zplus n (Zplus m p)) - (Zplus_assoc_l n m p)). - -Definition fast_Zplus_permute := -[n,m,p:Z][P:Z -> Prop][H : (P (Zplus m (Zplus n p)))] - (eq_ind_r Z (Zplus m (Zplus n p)) P H (Zplus n (Zplus m p)) - (Zplus_permute n m p)). - -Definition fast_OMEGA10 := -[v,c1,c2,l1,l2,k1,k2:Z][P:Z -> Prop] -[H : (P (Zplus (Zmult v (Zplus (Zmult c1 k1) (Zmult c2 k2))) - (Zplus (Zmult l1 k1) (Zmult l2 k2))))] - (eq_ind_r Z - (Zplus (Zmult v (Zplus (Zmult c1 k1) (Zmult c2 k2))) - (Zplus (Zmult l1 k1) (Zmult l2 k2))) - P H - (Zplus (Zmult (Zplus (Zmult v c1) l1) k1) - (Zmult (Zplus (Zmult v c2) l2) k2)) - (OMEGA10 v c1 c2 l1 l2 k1 k2)). - -Definition fast_OMEGA11 := -[v1,c1,l1,l2,k1:Z][P:Z -> Prop] -[H : (P (Zplus (Zmult v1 (Zmult c1 k1)) (Zplus (Zmult l1 k1) l2)))] - (eq_ind_r Z - (Zplus (Zmult v1 (Zmult c1 k1)) (Zplus (Zmult l1 k1) l2)) - P H - (Zplus (Zmult (Zplus (Zmult v1 c1) l1) k1) l2) - (OMEGA11 v1 c1 l1 l2 k1)). -Definition fast_OMEGA12 := -[v2,c2,l1,l2,k2:Z][P:Z -> Prop] -[H : (P (Zplus (Zmult v2 (Zmult c2 k2)) (Zplus l1 (Zmult l2 k2))))] - (eq_ind_r Z - (Zplus (Zmult v2 (Zmult c2 k2)) (Zplus l1 (Zmult l2 k2))) - P H - (Zplus l1 (Zmult (Zplus (Zmult v2 c2) l2) k2)) - (OMEGA12 v2 c2 l1 l2 k2)). - -Definition fast_OMEGA15 := -[v,c1,c2,l1,l2,k2 :Z][P:Z -> Prop] -[H : (P (Zplus (Zmult v (Zplus c1 (Zmult c2 k2))) (Zplus l1 (Zmult l2 k2))))] - (eq_ind_r Z - (Zplus (Zmult v (Zplus c1 (Zmult c2 k2))) (Zplus l1 (Zmult l2 k2))) - P H - (Zplus (Zplus (Zmult v c1) l1) (Zmult (Zplus (Zmult v c2) l2) k2)) - (OMEGA15 v c1 c2 l1 l2 k2)). -Definition fast_OMEGA16 := -[v,c,l,k :Z][P:Z -> Prop] -[H : (P (Zplus (Zmult v (Zmult c k)) (Zmult l k)))] - (eq_ind_r Z - (Zplus (Zmult v (Zmult c k)) (Zmult l k)) - P H - (Zmult (Zplus (Zmult v c) l) k) - (OMEGA16 v c l k)). - -Definition fast_OMEGA13 := -[v,l1,l2 :Z][x:positive][P:Z -> Prop] -[H : (P (Zplus l1 l2))] - (eq_ind_r Z - (Zplus l1 l2) - P H - (Zplus (Zplus (Zmult v (POS x)) l1) (Zplus (Zmult v (NEG x)) l2)) - (OMEGA13 v l1 l2 x )). - -Definition fast_OMEGA14 := -[v,l1,l2 :Z][x:positive][P:Z -> Prop] -[H : (P (Zplus l1 l2))] - (eq_ind_r Z - (Zplus l1 l2) - P H - (Zplus (Zplus (Zmult v (NEG x)) l1) (Zplus (Zmult v (POS x)) l2)) - (OMEGA14 v l1 l2 x )). -Definition fast_Zred_factor0:= -[x:Z][P:Z -> Prop] -[H : (P (Zmult x (POS xH)) )] - (eq_ind_r Z - (Zmult x (POS xH)) - P H - x - (Zred_factor0 x)). - -Definition fast_Zopp_one := -[x:Z][P:Z -> Prop] -[H : (P (Zmult x (NEG xH)))] - (eq_ind_r Z - (Zmult x (NEG xH)) - P H - (Zopp x) - (Zopp_one x)). - -Definition fast_Zmult_sym := -[x,y :Z][P:Z -> Prop] -[H : (P (Zmult y x))] - (eq_ind_r Z -(Zmult y x) - P H -(Zmult x y) - (Zmult_sym x y )). - -Definition fast_Zopp_Zplus := -[x,y :Z][P:Z -> Prop] -[H : (P (Zplus (Zopp x) (Zopp y)) )] - (eq_ind_r Z - (Zplus (Zopp x) (Zopp y)) - P H - (Zopp (Zplus x y)) - (Zopp_Zplus x y )). - -Definition fast_Zopp_Zopp := -[x:Z][P:Z -> Prop] -[H : (P x )] (eq_ind_r Z x P H (Zopp (Zopp x)) (Zopp_Zopp x)). - -Definition fast_Zopp_Zmult_r := -[x,y:Z][P:Z -> Prop] -[H : (P (Zmult x (Zopp y)))] - (eq_ind_r Z - (Zmult x (Zopp y)) - P H - (Zopp (Zmult x y)) - (Zopp_Zmult_r x y )). - -Definition fast_Zmult_plus_distr := -[n,m,p:Z][P:Z -> Prop] -[H : (P (Zplus (Zmult n p) (Zmult m p)))] - (eq_ind_r Z - (Zplus (Zmult n p) (Zmult m p)) - P H - (Zmult (Zplus n m) p) - (Zmult_plus_distr_l n m p)). -Definition fast_Zmult_Zopp_left:= -[x,y:Z][P:Z -> Prop] -[H : (P (Zmult x (Zopp y)))] - (eq_ind_r Z - (Zmult x (Zopp y)) - P H - (Zmult (Zopp x) y) - (Zmult_Zopp_left x y)). - -Definition fast_Zmult_assoc_r := -[n,m,p :Z][P:Z -> Prop] -[H : (P (Zmult n (Zmult m p)))] - (eq_ind_r Z - (Zmult n (Zmult m p)) - P H - (Zmult (Zmult n m) p) - (Zmult_assoc_r n m p)). - -Definition fast_Zred_factor1 := -[x:Z][P:Z -> Prop] -[H : (P (Zmult x (POS (xO xH))) )] - (eq_ind_r Z - (Zmult x (POS (xO xH))) - P H - (Zplus x x) - (Zred_factor1 x)). - -Definition fast_Zred_factor2 := -[x,y:Z][P:Z -> Prop] -[H : (P (Zmult x (Zplus (POS xH) y)))] - (eq_ind_r Z - (Zmult x (Zplus (POS xH) y)) - P H - (Zplus x (Zmult x y)) - (Zred_factor2 x y)). -Definition fast_Zred_factor3 := -[x,y:Z][P:Z -> Prop] -[H : (P (Zmult x (Zplus (POS xH) y)))] - (eq_ind_r Z - (Zmult x (Zplus (POS xH) y)) - P H - (Zplus (Zmult x y) x) - (Zred_factor3 x y)). - -Definition fast_Zred_factor4 := -[x,y,z:Z][P:Z -> Prop] -[H : (P (Zmult x (Zplus y z)))] - (eq_ind_r Z - (Zmult x (Zplus y z)) - P H - (Zplus (Zmult x y) (Zmult x z)) - (Zred_factor4 x y z)). - -Definition fast_Zred_factor5 := -[x,y:Z][P:Z -> Prop] -[H : (P y)] - (eq_ind_r Z - y - P H - (Zplus (Zmult x ZERO) y) - (Zred_factor5 x y)). - -Definition fast_Zred_factor6 := -[x :Z][P:Z -> Prop] -[H : (P(Zplus x ZERO) )] - (eq_ind_r Z - (Zplus x ZERO) - P H - x - (Zred_factor6 x )). - diff --git a/theories/Zarith/fast_integer.v b/theories/Zarith/fast_integer.v deleted file mode 100644 index f64093034..000000000 --- a/theories/Zarith/fast_integer.v +++ /dev/null @@ -1,1486 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(*i $Id$ i*) - -(**************************************************************************) -(*s Binary Integers *) -(* *) -(* Pierre Crégut (CNET, Lannion, France) *) -(**************************************************************************) - -Require Le. -Require Lt. -Require Plus. -Require Mult. -Require Minus. - -(*s Definition of fast binary integers *) -Section fast_integers. - -Inductive positive : Set := - xI : positive -> positive -| xO : positive -> positive -| xH : positive. - -Inductive Z : Set := - ZERO : Z | POS : positive -> Z | NEG : positive -> Z. - -Inductive relation : Set := - EGAL :relation | INFERIEUR : relation | SUPERIEUR : relation. - -(*s Addition *) -Fixpoint add_un [x:positive]:positive := - <positive> Cases x of - (xI x') => (xO (add_un x')) - | (xO x') => (xI x') - | xH => (xO xH) - end. - -Fixpoint add [x,y:positive]:positive := - <positive>Cases x of - (xI x') => <positive>Cases y of - (xI y') => (xO (add_carry x' y')) - | (xO y') => (xI (add x' y')) - | xH => (xO (add_un x')) - end - | (xO x') => <positive>Cases y of - (xI y') => (xI (add x' y')) - | (xO y') => (xO (add x' y')) - | xH => (xI x') - end - | xH => <positive>Cases y of - (xI y') => (xO (add_un y')) - | (xO y') => (xI y') - | xH => (xO xH) - end - end -with add_carry [x,y:positive]:positive := - <positive>Cases x of - (xI x') => <positive>Cases y of - (xI y') => (xI (add_carry x' y')) - | (xO y') => (xO (add_carry x' y')) - | xH => (xI (add_un x')) - end - | (xO x') => <positive>Cases y of - (xI y') => (xO (add_carry x' y')) - | (xO y') => (xI (add x' y')) - | xH => (xO (add_un x')) - end - | xH => <positive>Cases y of - (xI y') => (xI (add_un y')) - | (xO y') => (xO (add_un y')) - | xH => (xI xH) - end - end. - -(*s From positive to natural numbers *) -Fixpoint positive_to_nat [x:positive]:nat -> nat := - [pow2:nat] - <nat> Cases x of - (xI x') => (plus pow2 (positive_to_nat x' (plus pow2 pow2))) - | (xO x') => (positive_to_nat x' (plus pow2 pow2)) - | xH => pow2 - end. - -Definition convert := [x:positive] (positive_to_nat x (S O)). - -(*s From natural numbers to positive *) -Fixpoint anti_convert [n:nat]: positive := - <positive> Cases n of - O => xH - | (S x') => (add_un (anti_convert x')) - end. - -(* Correctness of addition *) -Lemma convert_add_un : - (x:positive)(m:nat) - (positive_to_nat (add_un x) m) = (plus m (positive_to_nat x m)). -Proof. -Induction x; Simpl; Auto with arith; Intros x' H0 m; Rewrite H0; -Rewrite plus_assoc_l; Trivial with arith. -Save. - -Theorem convert_add_carry : - (x,y:positive)(m:nat) - (positive_to_nat (add_carry x y) m) = - (plus m (positive_to_nat (add x y) m)). -Proof. -Induction x; Induction y; Simpl; Auto with arith; [ - Intros y' H1 m; Rewrite H; Rewrite plus_assoc_l; Trivial with arith -| Intros y' H1 m; Rewrite H; Rewrite plus_assoc_l; Trivial with arith -| Intros m; Rewrite convert_add_un; Rewrite plus_assoc_l; Trivial with arith -| Intros y' H m; Rewrite convert_add_un; Apply plus_assoc_r ]. -Save. - -Theorem cvt_carry : - (x,y:positive)(convert (add_carry x y)) = (S (convert (add x y))). -Proof. -Intros;Unfold convert; Rewrite convert_add_carry; Simpl; Trivial with arith. -Save. - -Theorem add_verif : - (x,y:positive)(m:nat) - (positive_to_nat (add x y) m) = - (plus (positive_to_nat x m) (positive_to_nat y m)). -Proof. -Induction x;Induction y;Simpl;Auto with arith; [ - Intros y' H1 m;Rewrite convert_add_carry; Rewrite H; - Rewrite plus_assoc_r; Rewrite plus_assoc_r; - Rewrite (plus_permute m (positive_to_nat p (plus m m))); Trivial with arith -| Intros y' H1 m; Rewrite H; Apply plus_assoc_l -| Intros m; Rewrite convert_add_un; - Rewrite (plus_sym (plus m (positive_to_nat p (plus m m)))); - Apply plus_assoc_r -| Intros y' H1 m; Rewrite H; Apply plus_permute -| Intros y' H1 m; Rewrite convert_add_un; Apply plus_assoc_r ]. -Save. - -Theorem convert_add: - (x,y:positive) (convert (add x y)) = (plus (convert x) (convert y)). -Proof. -Intros x y; Exact (add_verif x y (S O)). -Save. - -(*s Correctness of conversion *) -Theorem bij1 : (m:nat) (convert (anti_convert m)) = (S m). -Proof. -Induction m; [ - Unfold convert; Simpl; Trivial with arith -| Unfold convert; Intros n H; Simpl; Rewrite convert_add_un; Rewrite H; Auto with arith]. -Save. - -Theorem compare_positive_to_nat_O : - (p:positive)(m:nat)(le m (positive_to_nat p m)). -Induction p; Simpl; Auto with arith. -Intros; Apply le_trans with (plus m m); Auto with arith. -Save. - -Theorem compare_convert_O : (p:positive)(lt O (convert p)). -Intro; Unfold convert; Apply lt_le_trans with (S O); Auto with arith. -Apply compare_positive_to_nat_O. -Save. - -Hints Resolve compare_convert_O. - -(*s Subtraction *) -Fixpoint double_moins_un [x:positive]:positive := - <positive>Cases x of - (xI x') => (xI (xO x')) - | (xO x') => (xI (double_moins_un x')) - | xH => xH - end. - -Definition sub_un := [x:positive] - <positive> Cases x of - (xI x') => (xO x') - | (xO x') => (double_moins_un x') - | xH => xH - end. - -Lemma sub_add_one : (x:positive) (sub_un (add_un x)) = x. -Proof. -(Induction x; [Idtac | Idtac | Simpl;Auto with arith ]); -(Intros p; Elim p; [Idtac | Idtac | Simpl;Auto with arith]); -Simpl; Intros q H1 H2; Case H2; Simpl; Trivial with arith. -Save. - -Lemma is_double_moins_un : (x:positive) (add_un (double_moins_un x)) = (xO x). -Proof. -(Induction x;Simpl;Auto with arith); Intros m H;Rewrite H;Trivial with arith. -Save. - -Lemma add_sub_one : (x:positive) (x=xH) \/ (add_un (sub_un x)) = x. -Proof. -Induction x; [ - Simpl; Auto with arith -| Simpl; Intros;Right;Apply is_double_moins_un -| Auto with arith ]. -Save. - -Lemma ZL0 : (S (S O))=(plus (S O) (S O)). -Proof. Auto with arith. Save. - -Lemma ZL1: (y:positive)(xO (add_un y)) = (add_un (add_un (xO y))). -Proof. -Induction y; Simpl; Auto with arith. -Save. - -Lemma ZL2: - (y:positive)(m:nat) - (positive_to_nat y (plus m m)) = - (plus (positive_to_nat y m) (positive_to_nat y m)). -Proof. -Induction y; [ - Intros p H m; Simpl; Rewrite H; Rewrite plus_assoc_r; - Rewrite (plus_permute m (positive_to_nat p (plus m m))); - Rewrite plus_assoc_r; Auto with arith -| Intros p H m; Simpl; Rewrite H; Auto with arith -| Intro;Simpl; Trivial with arith ]. -Save. - -Lemma ZL3: (x:nat) (add_un (anti_convert (plus x x))) = (xO (anti_convert x)). -Proof. -Induction x; [ - Simpl; Auto with arith -| Intros y H; Simpl; Rewrite plus_sym; Simpl; Rewrite H; Rewrite ZL1;Auto with arith]. -Save. - -Lemma ZL4: (y:positive) (EX h:nat |(convert y)=(S h)). -Proof. -Induction y; [ - Intros p H;Elim H; Intros x H1; Exists (plus (S x) (S x)); - Unfold convert ;Simpl; Rewrite ZL0; Rewrite ZL2; Unfold convert in H1; - Rewrite H1; Auto with arith -| Intros p H1;Elim H1;Intros x H2; Exists (plus x (S x)); Unfold convert; - Simpl; Rewrite ZL0; Rewrite ZL2;Unfold convert in H2; Rewrite H2; Auto with arith -| Exists O ;Auto with arith ]. -Save. - -Lemma ZL5: (x:nat) (anti_convert (plus (S x) (S x))) = (xI (anti_convert x)). -Proof. -Induction x;Simpl; [ - Auto with arith -| Intros y H; Rewrite <- plus_n_Sm; Simpl; Rewrite H; Auto with arith]. -Save. - -Lemma bij2 : (x:positive) (anti_convert (convert x)) = (add_un x). -Proof. -Induction x; [ - Intros p H; Simpl; Rewrite <- H; Rewrite ZL0;Rewrite ZL2; Elim (ZL4 p); - Unfold convert; Intros n H1;Rewrite H1; Rewrite ZL3; Auto with arith - -| Intros p H; Unfold convert ;Simpl; Rewrite ZL0; Rewrite ZL2; - Rewrite <- (sub_add_one - (anti_convert - (plus (positive_to_nat p (S O)) (positive_to_nat p (S O))))); - Rewrite <- (sub_add_one (xI p)); - Simpl;Rewrite <- H;Elim (ZL4 p); Unfold convert ;Intros n H1;Rewrite H1; - Rewrite ZL5; Simpl; Trivial with arith -| Unfold convert; Simpl; Auto with arith ]. -Save. - -(*s Comparison of positive *) -Fixpoint compare [x,y:positive]: relation -> relation := - [r:relation] <relation> Cases x of - (xI x') => <relation>Cases y of - (xI y') => (compare x' y' r) - | (xO y') => (compare x' y' SUPERIEUR) - | xH => SUPERIEUR - end - | (xO x') => <relation>Cases y of - (xI y') => (compare x' y' INFERIEUR) - | (xO y') => (compare x' y' r) - | xH => SUPERIEUR - end - | xH => <relation>Cases y of - (xI y') => INFERIEUR - | (xO y') => INFERIEUR - | xH => r - end - end. - -Theorem compare_convert1 : - (x,y:positive) - ~(compare x y SUPERIEUR) = EGAL /\ ~(compare x y INFERIEUR) = EGAL. -Proof. -Induction x;Induction y;Split;Simpl;Auto with arith; - Discriminate Orelse (Elim (H p0); Auto with arith). -Save. - -Theorem compare_convert_EGAL : (x,y:positive) (compare x y EGAL) = EGAL -> x=y. -Proof. -Induction x;Induction y;Simpl;Auto with arith; [ - Intros z H1 H2; Rewrite (H z); Trivial with arith -| Intros z H1 H2; Absurd (compare p z SUPERIEUR)=EGAL ; - [ Elim (compare_convert1 p z);Auto with arith | Assumption ] -| Intros H1;Discriminate H1 -| Intros z H1 H2; Absurd (compare p z INFERIEUR) = EGAL; - [ Elim (compare_convert1 p z);Auto with arith | Assumption ] -| Intros z H1 H2 ;Rewrite (H z);Auto with arith -| Intros H1;Discriminate H1 -| Intros p H H1;Discriminate H1 -| Intros p H H1;Discriminate H1 ]. -Save. - -Lemma ZL6: - (p:positive) (positive_to_nat p (S(S O))) = (plus (convert p) (convert p)). -Proof. -Intros p;Rewrite ZL0; Rewrite ZL2; Trivial with arith. -Save. - -Lemma ZL7: - (m,n:nat) (lt m n) -> (lt (plus m m) (plus n n)). -Proof. -Intros m n H; Apply lt_trans with m:=(plus m n); [ - Apply lt_reg_l with 1:=H -| Rewrite (plus_sym m n); Apply lt_reg_l with 1:=H ]. -Save. - -Lemma ZL8: - (m,n:nat) (lt m n) -> (lt (S (plus m m)) (plus n n)). -Proof. -Intros m n H; Apply le_lt_trans with m:=(plus m n); [ - Change (lt (plus m m) (plus m n)) ; Apply lt_reg_l with 1:=H -| Rewrite (plus_sym m n); Apply lt_reg_l with 1:=H ]. -Save. - -Lemma ZLSI: - (x,y:positive) (compare x y SUPERIEUR) = INFERIEUR -> - (compare x y EGAL) = INFERIEUR. -Proof. -Induction x;Induction y;Simpl;Auto with arith; - Discriminate Orelse Intros H;Discriminate H. -Save. - -Lemma ZLIS: - (x,y:positive) (compare x y INFERIEUR) = SUPERIEUR -> - (compare x y EGAL) = SUPERIEUR. -Proof. -Induction x;Induction y;Simpl;Auto with arith; - Discriminate Orelse Intros H;Discriminate H. -Save. - -Lemma ZLII: - (x,y:positive) (compare x y INFERIEUR) = INFERIEUR -> - (compare x y EGAL) = INFERIEUR \/ x = y. -Proof. -(Induction x;Induction y;Simpl;Auto with arith;Try Discriminate); - Intros z H1 H2; Elim (H z H2);Auto with arith; Intros E;Rewrite E; - Auto with arith. -Save. - -Lemma ZLSS: - (x,y:positive) (compare x y SUPERIEUR) = SUPERIEUR -> - (compare x y EGAL) = SUPERIEUR \/ x = y. -Proof. -(Induction x;Induction y;Simpl;Auto with arith;Try Discriminate); - Intros z H1 H2; Elim (H z H2);Auto with arith; Intros E;Rewrite E; - Auto with arith. -Save. - -Theorem compare_convert_INFERIEUR : - (x,y:positive) (compare x y EGAL) = INFERIEUR -> - (lt (convert x) (convert y)). -Proof. -Induction x;Induction y; [ - Intros z H1 H2; Unfold convert ;Simpl; Apply lt_n_S; - Do 2 Rewrite ZL6; Apply ZL7; Apply H; Simpl in H2; Assumption -| Intros q H1 H2; Unfold convert ;Simpl; Do 2 Rewrite ZL6; - Apply ZL8; Apply H;Simpl in H2; Apply ZLSI;Assumption -| Simpl; Intros H1;Discriminate H1 -| Simpl; Intros q H1 H2; Unfold convert ;Simpl;Do 2 Rewrite ZL6; - Elim (ZLII p q H2); [ - Intros H3;Apply lt_S;Apply ZL7; Apply H;Apply H3 - | Intros E;Rewrite E;Apply lt_n_Sn] -| Simpl;Intros q H1 H2; Unfold convert ;Simpl;Do 2 Rewrite ZL6; - Apply ZL7;Apply H;Assumption -| Simpl; Intros H1;Discriminate H1 -| Intros q H1 H2; Unfold convert ;Simpl; Apply lt_n_S; Rewrite ZL6; - Elim (ZL4 q);Intros h H3; Rewrite H3;Simpl; Apply lt_O_Sn -| Intros q H1 H2; Unfold convert ;Simpl; Rewrite ZL6; Elim (ZL4 q);Intros h H3; - Rewrite H3; Simpl; Rewrite <- plus_n_Sm; Apply lt_n_S; Apply lt_O_Sn -| Simpl; Intros H;Discriminate H ]. -Save. - -Theorem compare_convert_SUPERIEUR : - (x,y:positive) (compare x y EGAL)=SUPERIEUR -> (gt (convert x) (convert y)). -Proof. -Unfold gt; Induction x;Induction y; [ - Simpl;Intros q H1 H2; Unfold convert ;Simpl;Do 2 Rewrite ZL6; - Apply lt_n_S; Apply ZL7; Apply H;Assumption -| Simpl;Intros q H1 H2; Unfold convert ;Simpl; Do 2 Rewrite ZL6; - Elim (ZLSS p q H2); [ - Intros H3;Apply lt_S;Apply ZL7;Apply H;Assumption - | Intros E;Rewrite E;Apply lt_n_Sn] -| Intros H1;Unfold convert ;Simpl; Rewrite ZL6;Elim (ZL4 p); - Intros h H3;Rewrite H3;Simpl; Apply lt_n_S; Apply lt_O_Sn -| Simpl;Intros q H1 H2;Unfold convert ;Simpl;Do 2 Rewrite ZL6; - Apply ZL8; Apply H; Apply ZLIS; Assumption -| Simpl;Intros q H1 H2; Unfold convert ;Simpl;Do 2 Rewrite ZL6; - Apply ZL7;Apply H;Assumption -| Intros H1;Unfold convert ;Simpl; Rewrite ZL6; Elim (ZL4 p); - Intros h H3;Rewrite H3;Simpl; Rewrite <- plus_n_Sm;Apply lt_n_S; - Apply lt_O_Sn -| Simpl; Intros q H1 H2;Discriminate H2 -| Simpl; Intros q H1 H2;Discriminate H2 -| Simpl;Intros H;Discriminate H ]. -Save. - -Lemma Dcompare : (r:relation) r=EGAL \/ r = INFERIEUR \/ r = SUPERIEUR. -Proof. -Induction r; Auto with arith. -Save. - -Theorem convert_compare_INFERIEUR : - (x,y:positive)(lt (convert x) (convert y)) -> (compare x y EGAL) = INFERIEUR. -Proof. -Intros x y; Unfold gt; Elim (Dcompare (compare x y EGAL)); [ - Intros E; Rewrite (compare_convert_EGAL x y E); - Intros H;Absurd (lt (convert y) (convert y)); [ Apply lt_n_n | Assumption ] -| Intros H;Elim H; [ - Auto with arith - | Intros H1 H2; Absurd (lt (convert x) (convert y)); [ - Apply lt_not_sym; Change (gt (convert x) (convert y)); - Apply compare_convert_SUPERIEUR; Assumption - | Assumption ]]]. -Save. - -Theorem convert_compare_SUPERIEUR : - (x,y:positive)(gt (convert x) (convert y)) -> (compare x y EGAL) = SUPERIEUR. -Proof. -Intros x y; Unfold gt; Elim (Dcompare (compare x y EGAL)); [ - Intros E; Rewrite (compare_convert_EGAL x y E); - Intros H;Absurd (lt (convert y) (convert y)); [ Apply lt_n_n | Assumption ] -| Intros H;Elim H; [ - Intros H1 H2; Absurd (lt (convert y) (convert x)); [ - Apply lt_not_sym; Apply compare_convert_INFERIEUR; Assumption - | Assumption ] - | Auto with arith]]. -Save. - -Theorem convert_compare_EGAL: (x:positive)(compare x x EGAL)=EGAL. -Induction x; Auto with arith. -Save. - -(*s Natural numbers coded with positive *) - -Inductive entier: Set := Nul : entier | Pos : positive -> entier. - -Definition Un_suivi_de := - [x:entier]<entier> Cases x of Nul => (Pos xH) | (Pos p) => (Pos (xI p)) end. - -Definition Zero_suivi_de := - [x:entier]<entier> Cases x of Nul => Nul | (Pos p) => (Pos (xO p)) end. - -Definition double_moins_deux := - [x:positive] <entier>Cases x of - (xI x') => (Pos (xO (xO x'))) - | (xO x') => (Pos (xO (double_moins_un x'))) - | xH => Nul - end. -Lemma ZS: (p:entier) (Zero_suivi_de p) = Nul -> p = Nul. -Proof. -Induction p;Simpl; [ Trivial with arith | Intros q H;Discriminate H ]. -Save. - -Lemma US: (p:entier) ~(Un_suivi_de p)=Nul. -Proof. -Induction p; Intros; Discriminate. -Save. - -Lemma USH: (p:entier) (Un_suivi_de p) = (Pos xH) -> p = Nul. -Proof. -Induction p;Simpl; [ Trivial with arith | Intros q H;Discriminate H ]. -Save. - -Lemma ZSH: (p:entier) ~(Zero_suivi_de p)= (Pos xH). -Proof. -Induction p; Intros; Discriminate. -Save. - -Fixpoint sub_pos[x,y:positive]:entier := - <entier>Cases x of - (xI x') => <entier>Cases y of - (xI y') => (Zero_suivi_de (sub_pos x' y')) - | (xO y') => (Un_suivi_de (sub_pos x' y')) - | xH => (Pos (xO x')) - end - | (xO x') => <entier>Cases y of - (xI y') => (Un_suivi_de (sub_neg x' y')) - | (xO y') => (Zero_suivi_de (sub_pos x' y')) - | xH => (Pos (double_moins_un x')) - end - | xH => <entier>Cases y of - (xI y') => (Pos (double_moins_un y')) - | (xO y') => (double_moins_deux y') - | xH => Nul - end - end -with sub_neg [x,y:positive]:entier := - <entier>Cases x of - (xI x') => <entier>Cases y of - (xI y') => (Un_suivi_de (sub_neg x' y')) - | (xO y') => (Zero_suivi_de (sub_pos x' y')) - | xH => (Pos (double_moins_un x')) - end - | (xO x') => <entier>Cases y of - (xI y') => (Zero_suivi_de (sub_neg x' y')) - | (xO y') => (Un_suivi_de (sub_neg x' y')) - | xH => (double_moins_deux x') - end - | xH => <entier>Cases y of - (xI y') => (Pos (xO y')) - | (xO y') => (Pos (double_moins_un y')) - | xH => Nul - end - end. - -Theorem sub_pos_x_x : (x:positive) (sub_pos x x) = Nul. -Proof. -Induction x; [ - Simpl; Intros p H;Rewrite H;Simpl; Trivial with arith -| Intros p H;Simpl;Rewrite H;Auto with arith -| Auto with arith ]. -Save. - -Theorem ZL10: (x,y:positive) - (compare x y EGAL) = SUPERIEUR -> - (sub_pos x y) = (Pos xH) -> (sub_neg x y) = Nul. -Proof. -Induction x;Induction y; [ - Intros q H1 H2 H3; Absurd (sub_pos (xI p) (xI q))=(Pos xH); - [ Simpl; Apply ZSH | Assumption ] -| Intros q H1 H2 H3; Simpl in H3; Cut (sub_pos p q)=Nul; [ - Intros H4;Simpl;Rewrite H4; Simpl; Trivial with arith - | Apply USH;Assumption ] -| Simpl; Intros H1 H2;Discriminate H2 -| Intros q H1 H2; - Change (Un_suivi_de (sub_neg p q))=(Pos xH) - -> (Zero_suivi_de (sub_neg p q))=Nul; - Intros H3; Rewrite (USH (sub_neg p q) H3); Simpl; Auto with arith -| Intros q H1 H2 H3; Absurd (sub_pos (xO p) (xO q))=(Pos xH); - [ Simpl; Apply ZSH | Assumption ] -| Intros H1; Elim p; [ - Simpl; Intros q H2 H3;Discriminate H3 - | Simpl; Intros q H2 H3;Discriminate H3 - | Simpl; Auto with arith ] -| Simpl; Intros q H1 H2 H3;Discriminate H2 -| Simpl; Intros q H1 H2 H3;Discriminate H2 -| Simpl; Intros H;Discriminate H ]. -Save. - -Lemma ZL11: (x:positive) (x=xH) \/ ~(x=xH). -Proof. -Intros x;Case x;Intros; (Left;Reflexivity) Orelse (Right;Discriminate). -Save. - -Lemma ZL12: (q:positive) (add_un q) = (add q xH). -Proof. -Induction q; Intros; Simpl; Trivial with arith. -Save. - -Lemma ZL12bis: (q:positive) (add_un q) = (add xH q). -Proof. -Induction q; Intros; Simpl; Trivial with arith. -Save. - -Theorem ZL13: - (x,y:positive)(add_carry x y) = (add_un (add x y)). -Proof. -(Induction x;Induction y;Simpl;Auto with arith); Intros q H1;Rewrite H; - Auto with arith. -Save. - -Theorem ZL14: - (x,y:positive)(add x (add_un y)) = (add_un (add x y)). -Proof. -Induction x;Induction y;Simpl;Auto with arith; [ - Intros q H1; Rewrite ZL13; Rewrite H; Auto with arith -| Intros q H1; Rewrite ZL13; Auto with arith -| Elim p;Simpl;Auto with arith -| Intros q H1;Rewrite H;Auto with arith -| Elim p;Simpl;Auto with arith ]. -Save. - -Theorem ZL15: - (q,z:positive) ~z=xH -> (add_carry q (sub_un z)) = (add q z). -Proof. -Intros q z H; Elim (add_sub_one z); [ - Intro;Absurd z=xH;Auto with arith -| Intros E;Pattern 2 z ;Rewrite <- E; Rewrite ZL14; Rewrite ZL13; Trivial with arith ]. -Save. - -Theorem sub_pos_SUPERIEUR: - (x,y:positive)(compare x y EGAL)=SUPERIEUR -> - (EX h:positive | (sub_pos x y) = (Pos h) /\ (add y h) = x /\ - (h = xH \/ (sub_neg x y) = (Pos (sub_un h)))). -Proof. -Induction x;Induction y; [ - Intros q H1 H2; Elim (H q H2); Intros z H3;Elim H3;Intros H4 H5; - Elim H5;Intros H6 H7; Exists (xO z); Split; [ - Simpl; Rewrite H4; Auto with arith - | Split; [ - Simpl; Rewrite H6; Auto with arith - | Right; Simpl; Elim (ZL11 z); [ - Intros H8; Simpl; Rewrite ZL10; [ - Rewrite H8; Auto with arith - | Exact H2 - | Rewrite <- H8; Auto with arith ] - | Intro H8; Elim H7; [ - Intro H9; Absurd z=xH; Auto with arith - | Intros H9;Simpl;Rewrite H9;Generalize H8 ;Case z;Auto with arith; - Intros H10;Absurd xH=xH;Auto with arith ]]]] -| Intros q H1 H2; Simpl in H2; Elim ZLSS with 1:=H2; [ - Intros H3;Elim (H q H3); Intros z H4; Exists (xI z); - Elim H4;Intros H5 H6;Elim H6;Intros H7 H8; Split; [ - Simpl;Rewrite H5;Auto with arith - | Split; [ - Simpl; Rewrite H7; Trivial with arith - | Right;Change (Zero_suivi_de (sub_pos p q))=(Pos (sub_un (xI z))); - Rewrite H5; Auto with arith ]] - | Intros H3; Exists xH; Rewrite H3; Split; [ - Simpl; Rewrite sub_pos_x_x; Auto with arith - | Split; Auto with arith ]] -| Intros H1; Exists (xO p); Auto with arith -| Intros q H1 H2; Simpl in H2; Elim (H q); [ - Intros z H3; Elim H3;Intros H4 H5;Elim H5;Intros H6 H7; - Elim (ZL11 z); [ - Intros vZ; Exists xH; Split; [ - Change (Un_suivi_de (sub_neg p q))=(Pos xH); - Rewrite ZL10; [ Auto with arith | Apply ZLIS;Assumption | Rewrite <- vZ;Assumption ] - | Split; [ - Simpl; Rewrite ZL12; Rewrite <- vZ; Rewrite H6; Trivial with arith - | Auto with arith ]] - | Exists (xI (sub_un z)); Elim H7;[ - Intros H8; Absurd z=xH;Assumption - | Split; [ - Simpl;Rewrite H8; Trivial with arith - | Split; [ - Change (xO (add_carry q (sub_un z)))=(xO p); Rewrite ZL15; [ - Rewrite H6;Trivial with arith - | Assumption ] - | Right; Change (Zero_suivi_de (sub_neg p q)) = - (Pos (sub_un (xI (sub_un z)))); - Rewrite H8; Auto with arith]]]] - | Apply ZLIS; Assumption ] -| Intros q H1 H2; Simpl in H2; Elim (H q H2); Intros z H3; - Exists (xO z); Elim H3;Intros H4 H5;Elim H5;Intros H6 H7; Split; [ - Simpl; Rewrite H4;Auto with arith - | Split; [ - Simpl;Rewrite H6;Auto with arith - | Right; Change (Un_suivi_de (sub_neg p q))=(Pos (double_moins_un z)); - Elim (ZL11 z); [ - Simpl; Intros H8;Rewrite H8; Simpl; - Cut (sub_neg p q)=Nul;[ - Intros H9;Rewrite H9;Auto with arith - | Apply ZL10;[Assumption|Rewrite <- H8;Assumption]] - | Intros H8;Elim H7; [ - Intros H9;Absurd z=xH;Auto with arith - | Intros H9;Rewrite H9; Generalize H8 ;Elim z; Simpl; Auto with arith; - Intros H10;Absurd xH=xH;Auto with arith ]]]] -| Intros H1; Exists (double_moins_un p); Split; [ - Auto with arith - | Split; [ - Elim p;Simpl;Auto with arith; Intros q H2; Rewrite ZL12bis; Rewrite H2; Trivial with arith - | Change (double_moins_un p)=xH \/ - (double_moins_deux p)=(Pos (sub_un (double_moins_un p))); - Case p;Simpl;Auto with arith ]] -| Intros p H1 H2;Simpl in H2; Discriminate H2 -| Intros p H1 H2;Simpl in H2;Discriminate H2 -| Intros H1;Simpl in H1;Discriminate H1 ]. -Save. - -Lemma ZC1: - (x,y:positive)(compare x y EGAL)=SUPERIEUR -> (compare y x EGAL)=INFERIEUR. -Proof. -Intros x y H;Apply convert_compare_INFERIEUR; -Change (gt (convert x) (convert y));Apply compare_convert_SUPERIEUR; -Assumption. -Save. - -Lemma ZC2: - (x,y:positive)(compare x y EGAL)=INFERIEUR -> (compare y x EGAL)=SUPERIEUR. -Proof. -Intros x y H;Apply convert_compare_SUPERIEUR;Unfold gt; -Apply compare_convert_INFERIEUR;Assumption. -Save. - -Lemma ZC3: (x,y:positive)(compare x y EGAL)=EGAL -> (compare y x EGAL)=EGAL. -Proof. -Intros x y H; Rewrite (compare_convert_EGAL x y H); -Apply convert_compare_EGAL. -Save. - -Definition Op := [r:relation] - <relation>Cases r of - EGAL => EGAL - | INFERIEUR => SUPERIEUR - | SUPERIEUR => INFERIEUR - end. - -Lemma ZC4: (x,y:positive) (compare x y EGAL) = (Op (compare y x EGAL)). -Proof. -(((Intros x y;Elim (Dcompare (compare y x EGAL));[Idtac | Intros H;Elim H]); -Intros E;Rewrite E;Simpl); [Apply ZC3 | Apply ZC2 | Apply ZC1 ]); Assumption. -Save. - -Theorem add_sym : (x,y:positive) (add x y) = (add y x). -Proof. -Induction x;Induction y;Simpl;Auto with arith; Intros q H1; [ - Clear H1; Do 2 Rewrite ZL13; Rewrite H;Auto with arith -| Rewrite H;Auto with arith | Rewrite H;Auto with arith | Rewrite H;Auto with arith ]. -Save. - -Lemma bij3: (x:positive)(sub_un (anti_convert (convert x))) = x. -Proof. -Intros x; Rewrite bij2; Rewrite sub_add_one; Trivial with arith. -Save. - -Lemma convert_intro : (x,y:positive)(convert x)=(convert y) -> x=y. -Proof. -Intros x y H;Rewrite <- (bij3 x);Rewrite <- (bij3 y); Rewrite H; Trivial with arith. -Save. - -Lemma simpl_add_r : (x,y,z:positive) (add x z)=(add y z) -> x=y. -Proof. -Intros x y z H;Apply convert_intro; -Apply (simpl_plus_l (convert z)); Do 2 Rewrite (plus_sym (convert z)); -Do 2 Rewrite <- convert_add; Rewrite H; Trivial with arith. -Save. - -Lemma simpl_add_l : (x,y,z:positive) (add x y)=(add x z) -> y=z. -Proof. -Intros x y z H;Apply convert_intro; -Apply (simpl_plus_l (convert x)); Do 2 Rewrite <- convert_add; -Rewrite H; Trivial with arith. -Save. - -Theorem add_assoc: (x,y,z:positive)(add x (add y z)) = (add (add x y) z). -Proof. -Intros x y z; Apply convert_intro; Do 4 Rewrite convert_add; -Apply plus_assoc_l. -Save. - -Local true_sub := [x,y:positive] - <positive> Cases (sub_pos x y) of Nul => xH | (Pos z) => z end. -Proof. -Theorem sub_add: -(x,y:positive) (compare x y EGAL) = SUPERIEUR -> (add y (true_sub x y)) = x. - -Intros x y H;Elim sub_pos_SUPERIEUR with 1:=H; -Intros z H1;Elim H1;Intros H2 H3; Elim H3;Intros H4 H5; -Unfold true_sub ;Rewrite H2; Exact H4. -Save. - -Theorem true_sub_convert: - (x,y:positive) (compare x y EGAL) = SUPERIEUR -> - (convert (true_sub x y)) = (minus (convert x) (convert y)). -Proof. -Intros x y H; Apply (simpl_plus_l (convert y)); -Rewrite le_plus_minus_r; [ - Rewrite <- convert_add; Rewrite sub_add; Auto with arith -| Apply lt_le_weak; Exact (compare_convert_SUPERIEUR x y H)]. -Save. - -(*s Addition on integers *) -Definition Zplus := [x,y:Z] - <Z>Cases x of - ZERO => y - | (POS x') => - <Z>Cases y of - ZERO => x - | (POS y') => (POS (add x' y')) - | (NEG y') => - <Z>Cases (compare x' y' EGAL) of - EGAL => ZERO - | INFERIEUR => (NEG (true_sub y' x')) - | SUPERIEUR => (POS (true_sub x' y')) - end - end - | (NEG x') => - <Z>Cases y of - ZERO => x - | (POS y') => - <Z>Cases (compare x' y' EGAL) of - EGAL => ZERO - | INFERIEUR => (POS (true_sub y' x')) - | SUPERIEUR => (NEG (true_sub x' y')) - end - | (NEG y') => (NEG (add x' y')) - end - end. - -(*s Opposite *) - -Definition Zopp := [x:Z] - <Z>Cases x of - ZERO => ZERO - | (POS x) => (NEG x) - | (NEG x) => (POS x) - end. - -Theorem Zero_left: (x:Z) (Zplus ZERO x) = x. -Proof. -Induction x; Auto with arith. -Save. - -Theorem Zopp_Zopp: (x:Z) (Zopp (Zopp x)) = x. -Proof. -Induction x; Auto with arith. -Save. - -(*s Addition and opposite *) -Theorem Zero_right: (x:Z) (Zplus x ZERO) = x. -Proof. -Induction x; Auto with arith. -Save. - -Theorem Zplus_inverse_r: (x:Z) (Zplus x (Zopp x)) = ZERO. -Proof. -Induction x; [ - Simpl;Auto with arith -| Simpl; Intros p;Rewrite (convert_compare_EGAL p); Auto with arith -| Simpl; Intros p;Rewrite (convert_compare_EGAL p); Auto with arith ]. -Save. - -Theorem Zopp_Zplus: - (x,y:Z) (Zopp (Zplus x y)) = (Zplus (Zopp x) (Zopp y)). -Proof. -(Intros x y;Case x;Case y;Auto with arith); -Intros p q;Simpl;Case (compare q p EGAL);Auto with arith. -Save. - -Theorem Zplus_sym: (x,y:Z) (Zplus x y) = (Zplus y x). -Proof. -Induction x;Induction y;Simpl;Auto with arith; [ - Intros q;Rewrite add_sym;Auto with arith -| Intros q; Rewrite (ZC4 q p); - (Elim (Dcompare (compare p q EGAL));[Idtac|Intros H;Elim H]); - Intros E;Rewrite E;Auto with arith -| Intros q; Rewrite (ZC4 q p); - (Elim (Dcompare (compare p q EGAL));[Idtac|Intros H;Elim H]); - Intros E;Rewrite E;Auto with arith -| Intros q;Rewrite add_sym;Auto with arith ]. -Save. - -Theorem Zplus_inverse_l: (x:Z) (Zplus (Zopp x) x) = ZERO. -Proof. -Intro; Rewrite Zplus_sym; Apply Zplus_inverse_r. -Save. - -Theorem Zopp_intro : (x,y:Z) (Zopp x) = (Zopp y) -> x = y. -Proof. -Intros x y;Case x;Case y;Simpl;Intros; [ - Trivial with arith | Discriminate H | Discriminate H | Discriminate H -| Simplify_eq H; Intro E; Rewrite E; Trivial with arith -| Discriminate H | Discriminate H | Discriminate H -| Simplify_eq H; Intro E; Rewrite E; Trivial with arith ]. -Save. - -Theorem Zopp_NEG : (x:positive) (Zopp (NEG x)) = (POS x). -Proof. -Induction x; Auto with arith. -Save. - -Hints Resolve Zero_left Zero_right. - -Theorem weak_assoc : - (x,y:positive)(z:Z) (Zplus (POS x) (Zplus (POS y) z))= - (Zplus (Zplus (POS x) (POS y)) z). -Proof. -Intros x y z';Case z'; [ - Auto with arith -| Intros z;Simpl; Rewrite add_assoc;Auto with arith -| Intros z; Simpl; - (Elim (Dcompare (compare y z EGAL));[Idtac|Intros H;Elim H;Clear H]); - Intros E0;Rewrite E0; - (Elim (Dcompare (compare (add x y) z EGAL));[Idtac|Intros H;Elim H; - Clear H]);Intros E1;Rewrite E1; [ - Absurd (compare (add x y) z EGAL)=EGAL; [ (* Cas 1 *) - Rewrite convert_compare_SUPERIEUR; [ - Discriminate - | Rewrite convert_add; Rewrite (compare_convert_EGAL y z E0); - Elim (ZL4 x);Intros k E2;Rewrite E2; Simpl; Unfold gt lt; Apply le_n_S; - Apply le_plus_r ] - | Assumption ] - | Absurd (compare (add x y) z EGAL)=INFERIEUR; [ (* Cas 2 *) - Rewrite convert_compare_SUPERIEUR; [ - Discriminate - | Rewrite convert_add; Rewrite (compare_convert_EGAL y z E0); - Elim (ZL4 x);Intros k E2;Rewrite E2; Simpl; Unfold gt lt; Apply le_n_S; - Apply le_plus_r] - | Assumption ] - | Rewrite (compare_convert_EGAL y z E0); (* Cas 3 *) - Elim (sub_pos_SUPERIEUR (add x z) z);[ - Intros t H; Elim H;Intros H1 H2;Elim H2;Intros H3 H4; - Unfold true_sub; Rewrite H1; Cut x=t; [ - Intros E;Rewrite E;Auto with arith - | Apply simpl_add_r with z:=z; Rewrite <- H3; Rewrite add_sym; Trivial with arith ] - | Pattern 1 z; Rewrite <- (compare_convert_EGAL y z E0); Assumption ] - | Elim (sub_pos_SUPERIEUR z y); [ (* Cas 4 *) - Intros k H;Elim H;Intros H1 H2;Elim H2;Intros H3 H4; Unfold 1 true_sub; - Rewrite H1; Cut x=k; [ - Intros E;Rewrite E; Rewrite (convert_compare_EGAL k); Trivial with arith - | Apply simpl_add_r with z:=y; Rewrite (add_sym k y); Rewrite H3; - Apply compare_convert_EGAL; Assumption ] - | Apply ZC2;Assumption] - | Elim (sub_pos_SUPERIEUR z y); [ (* Cas 5 *) - Intros k H;Elim H;Intros H1 H2;Elim H2;Intros H3 H4; - Unfold 1 3 5 true_sub; Rewrite H1; - Cut (compare x k EGAL)=INFERIEUR; [ - Intros E2;Rewrite E2; Elim (sub_pos_SUPERIEUR k x); [ - Intros i H5;Elim H5;Intros H6 H7;Elim H7;Intros H8 H9; - Elim (sub_pos_SUPERIEUR z (add x y)); [ - Intros j H10;Elim H10;Intros H11 H12;Elim H12;Intros H13 H14; - Unfold true_sub ;Rewrite H6;Rewrite H11; Cut i=j; [ - Intros E;Rewrite E;Auto with arith - | Apply (simpl_add_l (add x y)); Rewrite H13; - Rewrite (add_sym x y); Rewrite <- add_assoc; Rewrite H8; - Assumption ] - | Apply ZC2; Assumption] - | Apply ZC2;Assumption] - | Apply convert_compare_INFERIEUR; - Apply simpl_lt_plus_l with p:=(convert y); - Do 2 Rewrite <- convert_add; Apply compare_convert_INFERIEUR; - Rewrite H3; Rewrite add_sym; Assumption ] - | Apply ZC2; Assumption ] - | Elim (sub_pos_SUPERIEUR z y); [ (* Cas 6 *) - Intros k H;Elim H;Intros H1 H2;Elim H2;Intros H3 H4; - Elim (sub_pos_SUPERIEUR (add x y) z); [ - Intros i H5;Elim H5;Intros H6 H7;Elim H7;Intros H8 H9; - Unfold true_sub; Rewrite H1;Rewrite H6; - Cut (compare x k EGAL)=SUPERIEUR; [ - Intros H10;Elim (sub_pos_SUPERIEUR x k H10); - Intros j H11;Elim H11;Intros H12 H13;Elim H13;Intros H14 H15; - Rewrite H10; Rewrite H12; Cut i=j; [ - Intros H16;Rewrite H16;Auto with arith - | Apply (simpl_add_l (add z k)); Rewrite <- (add_assoc z k j); - Rewrite H14; Rewrite (add_sym z k); Rewrite <- add_assoc; - Rewrite H8; Rewrite (add_sym x y); Rewrite add_assoc; - Rewrite (add_sym k y); Rewrite H3; Trivial with arith] - | Apply convert_compare_SUPERIEUR; Unfold lt gt; - Apply simpl_lt_plus_l with p:=(convert y); - Do 2 Rewrite <- convert_add; Apply compare_convert_INFERIEUR; - Rewrite H3; Rewrite add_sym; Apply ZC1; Assumption ] - | Assumption ] - | Apply ZC2;Assumption ] - | Absurd (compare (add x y) z EGAL)=EGAL; [ (* Cas 7 *) - Rewrite convert_compare_SUPERIEUR; [ - Discriminate - | Rewrite convert_add; Unfold gt;Apply lt_le_trans with m:=(convert y);[ - Apply compare_convert_INFERIEUR; Apply ZC1; Assumption - | Apply le_plus_r]] - | Assumption ] - | Absurd (compare (add x y) z EGAL)=INFERIEUR; [ (* Cas 8 *) - Rewrite convert_compare_SUPERIEUR; [ - Discriminate - | Unfold gt; Apply lt_le_trans with m:=(convert y);[ - Exact (compare_convert_SUPERIEUR y z E0) - | Rewrite convert_add; Apply le_plus_r]] - | Assumption ] - | Elim sub_pos_SUPERIEUR with 1:=E0;Intros k H1; (* Cas 9 *) - Elim sub_pos_SUPERIEUR with 1:=E1; Intros i H2;Elim H1;Intros H3 H4; - Elim H4;Intros H5 H6; Elim H2;Intros H7 H8;Elim H8;Intros H9 H10; - Unfold true_sub ;Rewrite H3;Rewrite H7; Cut (add x k)=i; [ - Intros E;Rewrite E;Auto with arith - | Apply (simpl_add_l z);Rewrite (add_sym x k); - Rewrite add_assoc; Rewrite H5;Rewrite H9; - Rewrite add_sym; Trivial with arith ]]]. -Save. - -Hints Resolve weak_assoc. - -Theorem Zplus_assoc : - (x,y,z:Z) (Zplus x (Zplus y z))= (Zplus (Zplus x y) z). -Proof. -Intros x y z;Case x;Case y;Case z;Auto with arith; Intros; [ -(*i Apply weak_assoc -| Apply weak_assoc -| i*) Rewrite (Zplus_sym (NEG p0)); Rewrite weak_assoc; - Rewrite (Zplus_sym (Zplus (POS p1) (NEG p0))); Rewrite weak_assoc; - Rewrite (Zplus_sym (POS p1)); Trivial with arith -| Apply Zopp_intro; Do 4 Rewrite Zopp_Zplus; - Do 2 Rewrite Zopp_NEG; Rewrite Zplus_sym; Rewrite <- weak_assoc; - Rewrite (Zplus_sym (Zopp (POS p1))); - Rewrite (Zplus_sym (Zplus (POS p0) (Zopp (POS p1)))); - Rewrite (weak_assoc p); Rewrite weak_assoc; Rewrite (Zplus_sym (POS p0)); - Trivial with arith -| Rewrite Zplus_sym; Rewrite (Zplus_sym (POS p0) (POS p)); - Rewrite <- weak_assoc; Rewrite Zplus_sym; Rewrite (Zplus_sym (POS p0)); - Trivial with arith -| Apply Zopp_intro; Do 4 Rewrite Zopp_Zplus; - Do 2 Rewrite Zopp_NEG; Rewrite (Zplus_sym (Zopp (POS p0))); - Rewrite weak_assoc; Rewrite (Zplus_sym (Zplus (POS p1) (Zopp (POS p0)))); - Rewrite weak_assoc;Rewrite (Zplus_sym (POS p)); Trivial with arith -| Apply Zopp_intro; Do 4 Rewrite Zopp_Zplus; Do 2 Rewrite Zopp_NEG; - Apply weak_assoc -| Apply Zopp_intro; Do 4 Rewrite Zopp_Zplus; Do 2 Rewrite Zopp_NEG; - Apply weak_assoc] -. -Save. - -Lemma Zplus_simpl : (n,m,p,q:Z) n=m -> p=q -> (Zplus n p)=(Zplus m q). -Proof. -Intros; Elim H; Elim H0; Auto with arith. -Save. - -(*s Addition on positive numbers *) -Fixpoint times1 [x:positive] : (positive -> positive) -> positive -> positive:= - [f:positive -> positive][y:positive] - <positive> Cases x of - (xI x') => (add (f y) (times1 x' [z:positive](xO (f z)) y)) - | (xO x') => (times1 x' [z:positive](xO (f z)) y) - | xH => (f y) - end. - -Local times := [x:positive](times1 x [y:positive]y). - -Theorem times1_convert : - (x,y:positive)(f:positive -> positive) - (convert (times1 x f y)) = (mult (convert x) (convert (f y))). -Proof. -Induction x; [ - Intros x' H y f; Simpl; Rewrite ZL6; Rewrite convert_add; - Rewrite H; Unfold 3 convert; Simpl; Rewrite ZL6; - Rewrite (mult_sym (convert x')); Do 2 Rewrite mult_plus_distr; - Rewrite (mult_sym (convert x')); Trivial with arith -| Intros x' H y f; Simpl; Rewrite H; Unfold 2 3 convert; Simpl; - Do 2 Rewrite ZL6; Rewrite (mult_sym (convert x')); - Do 2 Rewrite mult_plus_distr; Rewrite (mult_sym (convert x')); Auto with arith -| Simpl; Intros;Rewrite <- plus_n_O; Trivial with arith ]. -Save. - -(*s Correctness of multiplication on positive *) -Theorem times_convert : - (x,y:positive) (convert (times x y)) = (mult (convert x) (convert y)). -Proof. -Intros x y;Unfold times; Rewrite times1_convert; Trivial with arith. -Save. - -(*s Multiplication on integers *) -Definition Zmult := [x,y:Z] - <Z>Cases x of - ZERO => ZERO - | (POS x') => - <Z>Cases y of - ZERO => ZERO - | (POS y') => (POS (times x' y')) - | (NEG y') => (NEG (times x' y')) - end - | (NEG x') => - <Z>Cases y of - ZERO => ZERO - | (POS y') => (NEG (times x' y')) - | (NEG y') => (POS (times x' y')) - end - end. - -Theorem times_assoc : - ((x,y,z:positive) (times x (times y z))= (times (times x y) z)). -Proof. -Intros x y z;Apply convert_intro; Do 4 Rewrite times_convert; -Apply mult_assoc_l. -Save. - -Theorem times_sym : (x,y:positive) (times x y) = (times y x). -Proof. -Intros x y; Apply convert_intro; Do 2 Rewrite times_convert; Apply mult_sym. -Save. - -Theorem Zmult_sym : (x,y:Z) (Zmult x y) = (Zmult y x). -Proof. -Induction x; Induction y; Simpl; Auto with arith; Intro q; Rewrite (times_sym p q); Auto with arith. -Save. - -Theorem Zmult_assoc : - (x,y,z:Z) (Zmult x (Zmult y z))= (Zmult (Zmult x y) z). -Proof. -Induction x; Induction y; Induction z; Simpl; Auto with arith; Intro p1; -Rewrite times_assoc; Auto with arith. -Save. - -Theorem Zmult_one: - (x:Z) (Zmult (POS xH) x) = x. -Proof. -Induction x; Simpl; Unfold times; Auto with arith. -Save. - -Theorem times_add_distr: - (x,y,z:positive) (times x (add y z)) = (add (times x y) (times x z)). -Proof. -Intros x y z;Apply convert_intro;Rewrite times_convert; -Do 2 Rewrite convert_add; Do 2 Rewrite times_convert; -Do 3 Rewrite (mult_sym (convert x)); Apply mult_plus_distr. -Save. - -Theorem lt_mult_left : - (x,y,z:nat) (lt x y) -> (lt (mult (S z) x) (mult (S z) y)). -Proof. -Intros x y z H;Elim z; [ - Simpl; Do 2 Rewrite <- plus_n_O; Assumption -| Simpl; Intros n H1; Apply lt_trans with m:=(plus y (plus x (mult n x))); [ - Rewrite (plus_sym x (plus x (mult n x))); - Rewrite (plus_sym y (plus x (mult n x))); Apply lt_reg_l; Assumption - | Apply lt_reg_l;Assumption ]]. -Save. - -Theorem times_true_sub_distr: - (x,y,z:positive) (compare y z EGAL) = SUPERIEUR -> - (times x (true_sub y z)) = (true_sub (times x y) (times x z)). -Proof. -Intros x y z H; Apply convert_intro; -Rewrite times_convert; Rewrite true_sub_convert; [ - Rewrite true_sub_convert; [ - Do 2 Rewrite times_convert; - Do 3 Rewrite (mult_sym (convert x));Apply mult_minus_distr - | Apply convert_compare_SUPERIEUR; Do 2 Rewrite times_convert; - Unfold gt; Elim (ZL4 x);Intros h H1;Rewrite H1; Apply lt_mult_left; - Exact (compare_convert_SUPERIEUR y z H) ] -| Assumption ]. -Save. - -Theorem Zero_mult_left: (x:Z) (Zmult ZERO x) = ZERO. -Proof. -Induction x; Auto with arith. -Save. - -Theorem Zero_mult_right: (x:Z) (Zmult x ZERO) = ZERO. -Proof. -Induction x; Auto with arith. -Save. - -Hints Resolve Zero_mult_left Zero_mult_right. - -(* Multiplication and Opposite *) -Theorem Zopp_Zmult: - (x,y:Z) (Zmult (Zopp x) y) = (Zopp (Zmult x y)). -Proof. -Intros x y; Case x; Case y; Simpl; Auto with arith. -Save. - -Theorem Zmult_Zopp_Zopp: - (x,y:Z) (Zmult (Zopp x) (Zopp y)) = (Zmult x y). -Proof. -Destruct x; Destruct y; Reflexivity. -Save. - -Theorem weak_Zmult_plus_distr_r: - (x:positive)(y,z:Z) - (Zmult (POS x) (Zplus y z)) = (Zplus (Zmult (POS x) y) (Zmult (POS x) z)). -Proof. -Intros x y' z';Case y';Case z';Auto with arith;Intros y z; - (Simpl; Rewrite times_add_distr; Trivial with arith) -Orelse - (Simpl; (Elim (Dcompare (compare z y EGAL));[Idtac|Intros H;Elim H; - Clear H]);Intros E0;Rewrite E0; [ - Rewrite (compare_convert_EGAL z y E0); - Rewrite (convert_compare_EGAL (times x y)); Trivial with arith - | Cut (compare (times x z) (times x y) EGAL)=INFERIEUR; [ - Intros E;Rewrite E; Rewrite times_true_sub_distr; [ - Trivial with arith - | Apply ZC2;Assumption ] - | Apply convert_compare_INFERIEUR;Do 2 Rewrite times_convert; - Elim (ZL4 x);Intros h H1;Rewrite H1;Apply lt_mult_left; - Exact (compare_convert_INFERIEUR z y E0)] - | Cut (compare (times x z) (times x y) EGAL)=SUPERIEUR; [ - Intros E;Rewrite E; Rewrite times_true_sub_distr; Auto with arith - | Apply convert_compare_SUPERIEUR; Unfold gt; Do 2 Rewrite times_convert; - Elim (ZL4 x);Intros h H1;Rewrite H1;Apply lt_mult_left; - Exact (compare_convert_SUPERIEUR z y E0) ]]). -Save. - -Theorem Zmult_plus_distr_r: - (x,y,z:Z) (Zmult x (Zplus y z)) = (Zplus (Zmult x y) (Zmult x z)). -Proof. -Intros x y z; Case x; [ - Auto with arith -| Intros x';Apply weak_Zmult_plus_distr_r -| Intros p; Apply Zopp_intro; Rewrite Zopp_Zplus; - Do 3 Rewrite <- Zopp_Zmult; Rewrite Zopp_NEG; - Apply weak_Zmult_plus_distr_r ]. -Save. - -(*s Comparison on integers *) -Definition Zcompare := [x,y:Z] - <relation>Cases x of - ZERO => <relation>Cases y of - ZERO => EGAL - | (POS y') => INFERIEUR - | (NEG y') => SUPERIEUR - end - | (POS x') => <relation>Cases y of - ZERO => SUPERIEUR - | (POS y') => (compare x' y' EGAL) - | (NEG y') => SUPERIEUR - end - | (NEG x') => <relation>Cases y of - ZERO => INFERIEUR - | (POS y') => INFERIEUR - | (NEG y') => (Op (compare x' y' EGAL)) - end - end. - -Theorem Zcompare_EGAL : (x,y:Z) (Zcompare x y) = EGAL <-> x = y. -Proof. -Intros x y;Split; [ - Case x;Case y;Simpl;Auto with arith; Try (Intros;Discriminate H); [ - Intros x' y' H; Rewrite (compare_convert_EGAL y' x' H); Trivial with arith - | Intros x' y' H; Rewrite (compare_convert_EGAL y' x'); [ - Trivial with arith - | Generalize H; Case (compare y' x' EGAL); - Trivial with arith Orelse (Intros C;Discriminate C)]] -| Intros E;Rewrite E; Case y; [ - Trivial with arith - | Simpl;Exact convert_compare_EGAL - | Simpl; Intros p;Rewrite convert_compare_EGAL;Auto with arith ]]. -Save. - -Theorem Zcompare_ANTISYM : - (x,y:Z) (Zcompare x y) = SUPERIEUR <-> (Zcompare y x) = INFERIEUR. -Proof. -Intros x y;Split; [ - Case x;Case y;Simpl;Intros;(Trivial with arith Orelse Discriminate H Orelse - (Apply ZC1; Assumption) Orelse - (Cut (compare p p0 EGAL)=SUPERIEUR; [ - Intros H1;Rewrite H1;Auto with arith - | Apply ZC2; Generalize H ; Case (compare p0 p EGAL); - Trivial with arith Orelse (Intros H2;Discriminate H2)])) -| Case x;Case y;Simpl;Intros;(Trivial with arith Orelse Discriminate H Orelse - (Apply ZC2; Assumption) Orelse - (Cut (compare p0 p EGAL)=INFERIEUR; [ - Intros H1;Rewrite H1;Auto with arith - | Apply ZC1; Generalize H ; Case (compare p p0 EGAL); - Trivial with arith Orelse (Intros H2;Discriminate H2)]))]. -Save. - -Theorem le_minus: (i,h:nat) (le (minus i h) i). -Proof. -Intros i h;Pattern i h; Apply nat_double_ind; [ - Auto with arith -| Auto with arith -| Intros m n H; Simpl; Apply le_trans with m:=m; Auto with arith ]. -Save. - -Lemma ZL16: (p,q:positive)(lt (minus (convert p) (convert q)) (convert p)). -Proof. -Intros p q; Elim (ZL4 p);Elim (ZL4 q); Intros h H1 i H2; -Rewrite H1;Rewrite H2; Simpl;Unfold lt; Apply le_n_S; Apply le_minus. -Save. - -Lemma ZL17: (p,q:positive)(lt (convert p) (convert (add p q))). -Proof. -Intros p q; Rewrite convert_add;Unfold lt;Elim (ZL4 q); Intros k H;Rewrite H; -Rewrite plus_sym;Simpl; Apply le_n_S; Apply le_plus_r. -Save. - -Theorem Zcompare_Zopp : - (x,y:Z) (Zcompare x y) = (Zcompare (Zopp y) (Zopp x)). -Proof. -(Intros x y;Case x;Case y;Simpl;Auto with arith); -Intros;Rewrite <- ZC4;Trivial with arith. -Save. - -Hints Resolve convert_compare_EGAL. - -Theorem weaken_Zcompare_Zplus_compatible : - ((x,y:Z) (z:positive) - (Zcompare (Zplus (POS z) x) (Zplus (POS z) y)) = (Zcompare x y)) -> - (x,y,z:Z) (Zcompare (Zplus z x) (Zplus z y)) = (Zcompare x y). -Proof. -(Intros H x y z;Case x;Case y;Case z;Auto with arith; -Try (Intros; Rewrite Zcompare_Zopp; Do 2 Rewrite Zopp_Zplus; - Rewrite Zopp_NEG; Rewrite H; Simpl; Auto with arith)); -Try (Intros; Simpl; Rewrite <- ZC4; Auto with arith). -Save. - -Hints Resolve ZC4. - -Theorem weak_Zcompare_Zplus_compatible : - (x,y:Z) (z:positive) - (Zcompare (Zplus (POS z) x) (Zplus (POS z) y)) = (Zcompare x y). -Proof. -Intros x y z;Case x;Case y;Simpl;Auto with arith; [ - Intros p;Apply convert_compare_INFERIEUR; Apply ZL17 -| Intros p;(Elim (Dcompare(compare z p EGAL));[Idtac|Intros H;Elim H; - Clear H]);Intros E;Rewrite E;Auto with arith; - Apply convert_compare_SUPERIEUR; Rewrite true_sub_convert; [ Unfold gt ; - Apply ZL16 | Assumption ] -| Intros p;(Elim (Dcompare(compare z p EGAL));[Idtac|Intros H;Elim H; - Clear H]);Intros E;Auto with arith; Apply convert_compare_SUPERIEUR; - Unfold gt;Apply ZL17 -| Intros p q; - (Elim (Dcompare (compare q p EGAL));[Idtac|Intros H;Elim H;Clear H]); - Intros E;Rewrite E;[ - Rewrite (compare_convert_EGAL q p E); Apply convert_compare_EGAL - | Apply convert_compare_INFERIEUR;Do 2 Rewrite convert_add;Apply lt_reg_l; - Apply compare_convert_INFERIEUR with 1:=E - | Apply convert_compare_SUPERIEUR;Unfold gt ;Do 2 Rewrite convert_add; - Apply lt_reg_l;Exact (compare_convert_SUPERIEUR q p E) ] -| Intros p q; - (Elim (Dcompare (compare z p EGAL));[Idtac|Intros H;Elim H;Clear H]); - Intros E;Rewrite E;Auto with arith; - Apply convert_compare_SUPERIEUR; Rewrite true_sub_convert; [ - Unfold gt; Apply lt_trans with m:=(convert z); [Apply ZL16 | Apply ZL17] - | Assumption ] -| Intros p;(Elim (Dcompare(compare z p EGAL));[Idtac|Intros H;Elim H; - Clear H]);Intros E;Rewrite E;Auto with arith; Simpl; - Apply convert_compare_INFERIEUR;Rewrite true_sub_convert;[Apply ZL16| - Assumption] -| Intros p q; - (Elim (Dcompare (compare z q EGAL));[Idtac|Intros H;Elim H;Clear H]); - Intros E;Rewrite E;Auto with arith; Simpl;Apply convert_compare_INFERIEUR; - Rewrite true_sub_convert;[ - Apply lt_trans with m:=(convert z) ;[Apply ZL16|Apply ZL17] - | Assumption] -| Intros p q; - (Elim (Dcompare (compare z q EGAL));[Idtac|Intros H;Elim H;Clear H]); - Intros E0;Rewrite E0; - (Elim (Dcompare (compare z p EGAL));[Idtac|Intros H;Elim H;Clear H]); - Intros E1;Rewrite E1; - (Elim (Dcompare (compare q p EGAL));[Idtac|Intros H;Elim H;Clear H]); - Intros E2;Rewrite E2;Auto with arith; [ - Absurd (compare q p EGAL)=INFERIEUR; [ - Rewrite <- (compare_convert_EGAL z q E0); - Rewrite <- (compare_convert_EGAL z p E1); - Rewrite (convert_compare_EGAL z); Discriminate - | Assumption ] - | Absurd (compare q p EGAL)=SUPERIEUR; [ - Rewrite <- (compare_convert_EGAL z q E0); - Rewrite <- (compare_convert_EGAL z p E1); - Rewrite (convert_compare_EGAL z);Discriminate - | Assumption] - | Absurd (compare z p EGAL)=INFERIEUR; [ - Rewrite (compare_convert_EGAL z q E0); - Rewrite <- (compare_convert_EGAL q p E2); - Rewrite (convert_compare_EGAL q);Discriminate - | Assumption ] - | Absurd (compare z p EGAL)=INFERIEUR; [ - Rewrite (compare_convert_EGAL z q E0); Rewrite E2;Discriminate - | Assumption] - | Absurd (compare z p EGAL)=SUPERIEUR;[ - Rewrite (compare_convert_EGAL z q E0); - Rewrite <- (compare_convert_EGAL q p E2); - Rewrite (convert_compare_EGAL q);Discriminate - | Assumption] - | Absurd (compare z p EGAL)=SUPERIEUR;[ - Rewrite (compare_convert_EGAL z q E0);Rewrite E2;Discriminate - | Assumption] - | Absurd (compare z q EGAL)=INFERIEUR;[ - Rewrite (compare_convert_EGAL z p E1); - Rewrite (compare_convert_EGAL q p E2); - Rewrite (convert_compare_EGAL p); Discriminate - | Assumption] - | Absurd (compare p q EGAL)=SUPERIEUR; [ - Rewrite <- (compare_convert_EGAL z p E1); - Rewrite E0; Discriminate - | Apply ZC2;Assumption ] - | Simpl; Rewrite (compare_convert_EGAL q p E2); - Rewrite (convert_compare_EGAL (true_sub p z)); Auto with arith - | Simpl; Rewrite <- ZC4; Apply convert_compare_SUPERIEUR; - Rewrite true_sub_convert; [ - Rewrite true_sub_convert; [ - Unfold gt; Apply simpl_lt_plus_l with p:=(convert z); - Rewrite le_plus_minus_r; [ - Rewrite le_plus_minus_r; [ - Apply compare_convert_INFERIEUR;Assumption - | Apply lt_le_weak; Apply compare_convert_INFERIEUR;Assumption ] - | Apply lt_le_weak; Apply compare_convert_INFERIEUR;Assumption ] - | Apply ZC2;Assumption ] - | Apply ZC2;Assumption ] - | Simpl; Rewrite <- ZC4; Apply convert_compare_INFERIEUR; - Rewrite true_sub_convert; [ - Rewrite true_sub_convert; [ - Apply simpl_lt_plus_l with p:=(convert z); - Rewrite le_plus_minus_r; [ - Rewrite le_plus_minus_r; [ - Apply compare_convert_INFERIEUR;Apply ZC1;Assumption - | Apply lt_le_weak; Apply compare_convert_INFERIEUR;Assumption ] - | Apply lt_le_weak; Apply compare_convert_INFERIEUR;Assumption ] - | Apply ZC2;Assumption] - | Apply ZC2;Assumption ] - | Absurd (compare z q EGAL)=INFERIEUR; [ - Rewrite (compare_convert_EGAL q p E2);Rewrite E1;Discriminate - | Assumption ] - | Absurd (compare q p EGAL)=INFERIEUR; [ - Cut (compare q p EGAL)=SUPERIEUR; [ - Intros E;Rewrite E;Discriminate - | Apply convert_compare_SUPERIEUR; Unfold gt; - Apply lt_trans with m:=(convert z); [ - Apply compare_convert_INFERIEUR;Apply ZC1;Assumption - | Apply compare_convert_INFERIEUR;Assumption ]] - | Assumption ] - | Absurd (compare z q EGAL)=SUPERIEUR; [ - Rewrite (compare_convert_EGAL z p E1); - Rewrite (compare_convert_EGAL q p E2); - Rewrite (convert_compare_EGAL p); Discriminate - | Assumption ] - | Absurd (compare z q EGAL)=SUPERIEUR; [ - Rewrite (compare_convert_EGAL z p E1); - Rewrite ZC1; [Discriminate | Assumption ] - | Assumption ] - | Absurd (compare z q EGAL)=SUPERIEUR; [ - Rewrite (compare_convert_EGAL q p E2); Rewrite E1; Discriminate - | Assumption ] - | Absurd (compare q p EGAL)=SUPERIEUR; [ - Rewrite ZC1; [ - Discriminate - | Apply convert_compare_SUPERIEUR; Unfold gt; - Apply lt_trans with m:=(convert z); [ - Apply compare_convert_INFERIEUR;Apply ZC1;Assumption - | Apply compare_convert_INFERIEUR;Assumption ]] - | Assumption ] - | Simpl; Rewrite (compare_convert_EGAL q p E2); Apply convert_compare_EGAL - | Simpl; Apply convert_compare_SUPERIEUR; Unfold gt; - Rewrite true_sub_convert; [ - Rewrite true_sub_convert; [ - Apply simpl_lt_plus_l with p:=(convert p); Rewrite le_plus_minus_r; [ - Rewrite plus_sym; Apply simpl_lt_plus_l with p:=(convert q); - Rewrite plus_assoc_l; Rewrite le_plus_minus_r; [ - Rewrite (plus_sym (convert q)); Apply lt_reg_l; - Apply compare_convert_INFERIEUR;Assumption - | Apply lt_le_weak; Apply compare_convert_INFERIEUR; - Apply ZC1;Assumption ] - | Apply lt_le_weak; Apply compare_convert_INFERIEUR;Apply ZC1; - Assumption ] - | Assumption ] - | Assumption ] - | Simpl; Apply convert_compare_INFERIEUR; Rewrite true_sub_convert; [ - Rewrite true_sub_convert; [ - Apply simpl_lt_plus_l with p:=(convert q); Rewrite le_plus_minus_r; [ - Rewrite plus_sym; Apply simpl_lt_plus_l with p:=(convert p); - Rewrite plus_assoc_l; Rewrite le_plus_minus_r; [ - Rewrite (plus_sym (convert p)); Apply lt_reg_l; - Apply compare_convert_INFERIEUR;Apply ZC1;Assumption - | Apply lt_le_weak; Apply compare_convert_INFERIEUR;Apply ZC1; - Assumption ] - | Apply lt_le_weak;Apply compare_convert_INFERIEUR;Apply ZC1;Assumption] - | Assumption] - | Assumption]]]. -Save. - -Theorem Zcompare_Zplus_compatible : - (x,y,z:Z) (Zcompare (Zplus z x) (Zplus z y)) = (Zcompare x y). -Proof. -Exact (weaken_Zcompare_Zplus_compatible weak_Zcompare_Zplus_compatible). -Save. - -Theorem Zcompare_trans_SUPERIEUR : - (x,y,z:Z) (Zcompare x y) = SUPERIEUR -> - (Zcompare y z) = SUPERIEUR -> - (Zcompare x z) = SUPERIEUR. -Proof. -Intros x y z;Case x;Case y;Case z; Simpl; -Try (Intros; Discriminate H Orelse Discriminate H0); -Auto with arith; [ - Intros p q r H H0;Apply convert_compare_SUPERIEUR; Unfold gt; - Apply lt_trans with m:=(convert q); - Apply compare_convert_INFERIEUR;Apply ZC1;Assumption -| Intros p q r; Do 3 Rewrite <- ZC4; Intros H H0; - Apply convert_compare_SUPERIEUR;Unfold gt;Apply lt_trans with m:=(convert q); - Apply compare_convert_INFERIEUR;Apply ZC1;Assumption ]. -Save. - -Lemma SUPERIEUR_POS : - (x,y:Z) (Zcompare x y) = SUPERIEUR -> - (EX h:positive |(Zplus x (Zopp y)) = (POS h)). -Proof. -Intros x y;Case x;Case y; [ - Simpl; Intros H; Discriminate H -| Simpl; Intros p H; Discriminate H -| Intros p H; Exists p; Simpl; Auto with arith -| Intros p H; Exists p; Simpl; Auto with arith -| Intros q p H; Exists (true_sub p q); Unfold Zplus Zopp; - Unfold Zcompare in H; Rewrite H; Trivial with arith -| Intros q p H; Exists (add p q); Simpl; Trivial with arith -| Simpl; Intros p H; Discriminate H -| Simpl; Intros q p H; Discriminate H -| Unfold Zcompare; Intros q p; Rewrite <- ZC4; Intros H; Exists (true_sub q p); - Simpl; Rewrite (ZC1 q p H); Trivial with arith]. -Save. -End fast_integers. diff --git a/theories/Zarith/intro.tex b/theories/Zarith/intro.tex deleted file mode 100755 index 9694eaac8..000000000 --- a/theories/Zarith/intro.tex +++ /dev/null @@ -1,5 +0,0 @@ -The {\tt ZArith} library deals with binary integers (those used -by the {\tt Omega} decision tactic). -Here are defined various arithmetical notions and their properties, -similar to those of {\tt Arith}. - diff --git a/theories/Zarith/zarith_aux.v b/theories/Zarith/zarith_aux.v deleted file mode 100644 index 856082b92..000000000 --- a/theories/Zarith/zarith_aux.v +++ /dev/null @@ -1,741 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) -(*i $Id$ i*) - -(**************************************************************************) -(*s Binary Integers *) -(* *) -(* Pierre Crégut (CNET, Lannion, France) *) -(**************************************************************************) - -Require Arith. -Require Export fast_integer. - -Meta Definition ElimCompare com1 com2:= - Elim (Dcompare (Zcompare com1 com2)); [ - Idtac - | Intro hidden_auxiliary; Elim hidden_auxiliary; - Clear hidden_auxiliary ] . - -(*s Order relations *) -Definition Zlt := [x,y:Z](Zcompare x y) = INFERIEUR. -Definition Zgt := [x,y:Z](Zcompare x y) = SUPERIEUR. -Definition Zle := [x,y:Z]~(Zcompare x y) = SUPERIEUR. -Definition Zge := [x,y:Z]~(Zcompare x y) = INFERIEUR. - -(*s Absolu function *) -Definition absolu [x:Z] : nat := - Cases x of - ZERO => O - | (POS p) => (convert p) - | (NEG p) => (convert p) - end. - -Definition Zabs [z:Z] : Z := - Cases z of - ZERO => ZERO - | (POS p) => (POS p) - | (NEG p) => (POS p) - end. - -(*s Properties of absolu function *) - -Lemma Zabs_eq : (x:Z) (Zle ZERO x) -> (Zabs x)=x. -Destruct x; Auto with arith. -Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith. -Save. - -(*s From nat to Z *) -Definition inject_nat := - [x:nat]Cases x of - O => ZERO - | (S y) => (POS (anti_convert y)) - end. - -(*s Successor and Predecessor functions on Z *) -Definition Zs := [x:Z](Zplus x (POS xH)). -Definition Zpred := [x:Z](Zplus x (NEG xH)). - -(* Properties of the order relation *) -Theorem Zgt_Sn_n : (n:Z)(Zgt (Zs n) n). - -Intros n; Unfold Zgt Zs; Pattern 2 n; Rewrite <- (Zero_right n); -Rewrite Zcompare_Zplus_compatible;Auto with arith. -Save. - -(*s Properties of the order *) -Theorem Zle_gt_trans : (n,m,p:Z)(Zle m n)->(Zgt m p)->(Zgt n p). - -Unfold Zle Zgt; Intros n m p H1 H2; (ElimCompare 'm 'n); [ - Intro E; Elim (Zcompare_EGAL m n); Intros H3 H4;Rewrite <- (H3 E); Assumption -| Intro H3; Apply Zcompare_trans_SUPERIEUR with y:=m;[ - Elim (Zcompare_ANTISYM n m); Intros H4 H5;Apply H5; Assumption - | Assumption ] -| Intro H3; Absurd (Zcompare m n)=SUPERIEUR;Assumption ]. -Save. - -Theorem Zgt_le_trans : (n,m,p:Z)(Zgt n m)->(Zle p m)->(Zgt n p). - -Unfold Zle Zgt ;Intros n m p H1 H2; (ElimCompare 'p 'm); [ - Intros E;Elim (Zcompare_EGAL p m);Intros H3 H4; Rewrite (H3 E); Assumption -| Intro H3; Apply Zcompare_trans_SUPERIEUR with y:=m; [ - Assumption - | Elim (Zcompare_ANTISYM m p); Auto with arith ] -| Intro H3; Absurd (Zcompare p m)=SUPERIEUR;Assumption ]. -Save. - -Theorem Zle_S_gt : (n,m:Z) (Zle (Zs n) m) -> (Zgt m n). - -Intros n m H;Apply Zle_gt_trans with m:=(Zs n);[ Assumption | Apply Zgt_Sn_n ]. -Save. - -Theorem Zcompare_n_S : (n,m:Z)(Zcompare (Zs n) (Zs m)) = (Zcompare n m). -Intros n m;Unfold Zs ;Do 2 Rewrite -> [t:Z](Zplus_sym t (POS xH)); -Rewrite -> Zcompare_Zplus_compatible;Auto with arith. -Save. - -Theorem Zgt_n_S : (n,m:Z)(Zgt m n) -> (Zgt (Zs m) (Zs n)). - -Unfold Zgt; Intros n m H; Rewrite Zcompare_n_S; Auto with arith. -Save. - -Lemma Zle_not_gt : (n,m:Z)(Zle n m) -> ~(Zgt n m). - -Unfold Zle Zgt; Auto with arith. -Save. - -Lemma Zgt_antirefl : (n:Z)~(Zgt n n). - -Unfold Zgt ;Intros n; Elim (Zcompare_EGAL n n); Intros H1 H2; -Rewrite H2; [ Discriminate | Trivial with arith ]. -Save. - -Lemma Zgt_not_sym : (n,m:Z)(Zgt n m) -> ~(Zgt m n). - -Unfold Zgt ;Intros n m H; Elim (Zcompare_ANTISYM n m); Intros H1 H2; -Rewrite -> H1; [ Discriminate | Assumption ]. -Save. - -Lemma Zgt_not_le : (n,m:Z)(Zgt n m) -> ~(Zle n m). - -Unfold Zgt Zle not; Auto with arith. -Save. - -Lemma Zgt_trans : (n,m,p:Z)(Zgt n m)->(Zgt m p)->(Zgt n p). - -Unfold Zgt; Exact Zcompare_trans_SUPERIEUR. -Save. - -Lemma Zle_gt_S : (n,p:Z)(Zle n p)->(Zgt (Zs p) n). - -Unfold Zle Zgt ;Intros n p H; (ElimCompare 'n 'p); [ - Intros H1;Elim (Zcompare_EGAL n p);Intros H2 H3; Rewrite <- H2; [ - Exact (Zgt_Sn_n n) - | Assumption ] - -| Intros H1;Apply Zcompare_trans_SUPERIEUR with y:=p; [ - Exact (Zgt_Sn_n p) - | Elim (Zcompare_ANTISYM p n); Auto with arith ] -| Intros H1;Absurd (Zcompare n p)=SUPERIEUR;Assumption ]. -Save. - -Lemma Zgt_pred - : (n,p:Z)(Zgt p (Zs n))->(Zgt (Zpred p) n). - -Unfold Zgt Zs Zpred ;Intros n p H; -Rewrite <- [x,y:Z](Zcompare_Zplus_compatible x y (POS xH)); -Rewrite (Zplus_sym p); Rewrite Zplus_assoc; Rewrite [x:Z](Zplus_sym x n); -Simpl; Assumption. -Save. - -Lemma Zsimpl_gt_plus_l - : (n,m,p:Z)(Zgt (Zplus p n) (Zplus p m))->(Zgt n m). - -Unfold Zgt; Intros n m p H; - Rewrite <- (Zcompare_Zplus_compatible n m p); Assumption. -Save. - -Lemma Zsimpl_gt_plus_r - : (n,m,p:Z)(Zgt (Zplus n p) (Zplus m p))->(Zgt n m). - -Intros n m p H; Apply Zsimpl_gt_plus_l with p. -Rewrite (Zplus_sym p n); Rewrite (Zplus_sym p m); Trivial. - -Save. - -Lemma Zgt_reg_l - : (n,m,p:Z)(Zgt n m)->(Zgt (Zplus p n) (Zplus p m)). - -Unfold Zgt; Intros n m p H; Rewrite (Zcompare_Zplus_compatible n m p); -Assumption. -Save. - -Lemma Zgt_reg_r : (n,m,p:Z)(Zgt n m)->(Zgt (Zplus n p) (Zplus m p)). -Intros n m p H; Rewrite (Zplus_sym n p); Rewrite (Zplus_sym m p); Apply Zgt_reg_l; Trivial. -Save. - -Theorem Zcompare_et_un: - (x,y:Z) (Zcompare x y)=SUPERIEUR <-> - ~(Zcompare x (Zplus y (POS xH)))=INFERIEUR. - -Intros x y; Split; [ - Intro H; (ElimCompare 'x '(Zplus y (POS xH)));[ - Intro H1; Rewrite H1; Discriminate - | Intros H1; Elim SUPERIEUR_POS with 1:=H; Intros h H2; - Absurd (gt (convert h) O) /\ (lt (convert h) (S O)); [ - Unfold not ;Intros H3;Elim H3;Intros H4 H5; Absurd (gt (convert h) O); [ - Unfold gt ;Apply le_not_lt; Apply le_S_n; Exact H5 - | Assumption] - | Split; [ - Elim (ZL4 h); Intros i H3;Rewrite H3; Apply gt_Sn_O - | Change (lt (convert h) (convert xH)); - Apply compare_convert_INFERIEUR; - Change (Zcompare (POS h) (POS xH))=INFERIEUR; - Rewrite <- H2; Rewrite <- [m,n:Z](Zcompare_Zplus_compatible m n y); - Rewrite (Zplus_sym x);Rewrite Zplus_assoc; Rewrite Zplus_inverse_r; - Simpl; Exact H1 ]] - | Intros H1;Rewrite -> H1;Discriminate ] -| Intros H; (ElimCompare 'x '(Zplus y (POS xH))); [ - Intros H1;Elim (Zcompare_EGAL x (Zplus y (POS xH))); Intros H2 H3; - Rewrite (H2 H1); Exact (Zgt_Sn_n y) - | Intros H1;Absurd (Zcompare x (Zplus y (POS xH)))=INFERIEUR;Assumption - | Intros H1; Apply Zcompare_trans_SUPERIEUR with y:=(Zs y); - [ Exact H1 | Exact (Zgt_Sn_n y) ]]]. -Save. - -Lemma Zgt_S_n : (n,p:Z)(Zgt (Zs p) (Zs n))->(Zgt p n). - -Unfold Zs Zgt;Intros n p;Do 2 Rewrite -> [m:Z](Zplus_sym m (POS xH)); -Rewrite -> (Zcompare_Zplus_compatible p n (POS xH));Trivial with arith. -Save. - -Lemma Zle_S_n : (n,m:Z) (Zle (Zs m) (Zs n)) -> (Zle m n). - -Unfold Zle not ;Intros m n H1 H2;Apply H1; -Unfold Zs ;Do 2 Rewrite <- (Zplus_sym (POS xH)); -Rewrite -> (Zcompare_Zplus_compatible n m (POS xH));Assumption. -Save. - -Lemma Zgt_le_S : (n,p:Z)(Zgt p n)->(Zle (Zs n) p). - -Unfold Zgt Zle; Intros n p H; Elim (Zcompare_et_un p n); Intros H1 H2; -Unfold not ;Intros H3; Unfold not in H1; Apply H1; [ - Assumption -| Elim (Zcompare_ANTISYM (Zplus n (POS xH)) p);Intros H4 H5;Apply H4;Exact H3]. -Save. - -Lemma Zgt_S_le : (n,p:Z)(Zgt (Zs p) n)->(Zle n p). - -Intros n p H;Apply Zle_S_n; Apply Zgt_le_S; Assumption. -Save. - -Theorem Zgt_S : (n,m:Z)(Zgt (Zs n) m)->((Zgt n m)\/(<Z>m=n)). - -Intros n m H; Unfold Zgt; (ElimCompare 'n 'm); [ - Elim (Zcompare_EGAL n m); Intros H1 H2 H3;Rewrite -> H1;Auto with arith -| Intros H1;Absurd (Zcompare m n)=SUPERIEUR; - [ Exact (Zgt_S_le m n H) | Elim (Zcompare_ANTISYM m n); Auto with arith ] -| Auto with arith ]. -Save. - -Theorem Zgt_trans_S : (n,m,p:Z)(Zgt (Zs n) m)->(Zgt m p)->(Zgt n p). - -Intros n m p H1 H2;Apply Zle_gt_trans with m:=m; - [ Apply Zgt_S_le; Assumption | Assumption ]. -Save. - -Theorem Zeq_S : (n,m:Z) n=m -> (Zs n)=(Zs m). -Intros n m H; Rewrite H; Auto with arith. -Save. - -Theorem Zpred_Sn : (m:Z) m=(Zpred (Zs m)). -Intros m; Unfold Zpred Zs; Rewrite <- Zplus_assoc; Simpl; -Rewrite Zplus_sym; Auto with arith. -Save. - -Theorem Zeq_add_S : (n,m:Z) (Zs n)=(Zs m) -> n=m. -Intros n m H. -Change (Zplus (Zplus (NEG xH) (POS xH)) n)= - (Zplus (Zplus (NEG xH) (POS xH)) m); -Do 2 Rewrite <- Zplus_assoc; Do 2 Rewrite (Zplus_sym (POS xH)); -Unfold Zs in H;Rewrite H; Trivial with arith. -Save. - -Theorem Znot_eq_S : (n,m:Z) ~(n=m) -> ~((Zs n)=(Zs m)). - -Unfold not ;Intros n m H1 H2;Apply H1;Apply Zeq_add_S; Assumption. -Save. - -Lemma Zsimpl_plus_l : (n,m,p:Z)(Zplus n m)=(Zplus n p)->m=p. -Intros n m p H; Cut (Zplus (Zopp n) (Zplus n m))=(Zplus (Zopp n) (Zplus n p));[ - Do 2 Rewrite -> Zplus_assoc; Rewrite -> (Zplus_sym (Zopp n) n); - Rewrite -> Zplus_inverse_r;Simpl; Trivial with arith -| Rewrite -> H; Trivial with arith ]. -Save. - -Theorem Zn_Sn : (n:Z) ~(n=(Zs n)). -Intros n;Cut ~ZERO=(POS xH);[ - Unfold not ;Intros H1 H2;Apply H1;Apply (Zsimpl_plus_l n);Rewrite Zero_right; - Exact H2 -| Discriminate ]. -Save. - -Lemma Zplus_n_O : (n:Z) n=(Zplus n ZERO). -Intro; Rewrite Zero_right; Trivial with arith. -Save. - -Lemma Zplus_unit_left : (n,m:Z) (Zplus n ZERO)=m -> n=m. -Intro; Rewrite Zero_right; Trivial with arith. -Save. - -Lemma Zplus_unit_right : (n,m:Z) n=(Zplus m ZERO) -> n=m. -Intros n m; Rewrite (Zero_right m); Trivial with arith. -Save. - -Lemma Zplus_n_Sm : (n,m:Z) (Zs (Zplus n m))=(Zplus n (Zs m)). - -Intros n m; Unfold Zs; Rewrite Zplus_assoc; Trivial with arith. -Save. - -Lemma Zmult_n_O : (n:Z) ZERO=(Zmult n ZERO). - -Intro;Rewrite Zmult_sym;Simpl; Trivial with arith. -Save. - -Lemma Zmult_n_Sm : (n,m:Z) (Zplus (Zmult n m) n)=(Zmult n (Zs m)). - -Intros n m;Unfold Zs; Rewrite Zmult_plus_distr_r; -Rewrite (Zmult_sym n (POS xH));Rewrite Zmult_one; Trivial with arith. -Save. - -Theorem Zle_n : (n:Z) (Zle n n). -Intros n;Elim (Zcompare_EGAL n n);Unfold Zle ;Intros H1 H2;Rewrite H2; - [ Discriminate | Trivial with arith ]. -Save. - -Theorem Zle_refl : (n,m:Z) n=m -> (Zle n m). -Intros; Rewrite H; Apply Zle_n. -Save. - -Theorem Zle_trans : (n,m,p:Z)(Zle n m)->(Zle m p)->(Zle n p). - -Intros n m p;Unfold 1 3 Zle; Unfold not; Intros H1 H2 H3;Apply H1; -Exact (Zgt_le_trans n p m H3 H2). -Save. - -Theorem Zle_n_Sn : (n:Z)(Zle n (Zs n)). - -Intros n; Apply Zgt_S_le;Apply Zgt_trans with m:=(Zs n) ;Apply Zgt_Sn_n. -Save. - -Lemma Zle_n_S : (n,m:Z) (Zle m n) -> (Zle (Zs m) (Zs n)). - -Unfold Zle not ;Intros m n H1 H2; Apply H1; -Rewrite <- (Zcompare_Zplus_compatible n m (POS xH)); -Do 2 Rewrite (Zplus_sym (POS xH)); Exact H2. -Save. - -Hints Resolve Zle_n Zle_n_Sn Zle_trans Zle_n_S : zarith. -Hints Immediate Zle_refl : zarith. - -Lemma Zs_pred : (n:Z) n=(Zs (Zpred n)). - -Intros n; Unfold Zs Zpred ;Rewrite <- Zplus_assoc; Simpl; Rewrite Zero_right; -Trivial with arith. -Save. - -Hints Immediate Zs_pred : zarith. - -Theorem Zle_pred_n : (n:Z)(Zle (Zpred n) n). - -Intros n;Pattern 2 n ;Rewrite Zs_pred; Apply Zle_n_Sn. -Save. - -Theorem Zle_trans_S : (n,m:Z)(Zle (Zs n) m)->(Zle n m). - -Intros n m H;Apply Zle_trans with m:=(Zs n); [ Apply Zle_n_Sn | Assumption ]. -Save. - -Theorem Zle_Sn_n : (n:Z)~(Zle (Zs n) n). - -Intros n; Apply Zgt_not_le; Apply Zgt_Sn_n. -Save. - -Theorem Zle_antisym : (n,m:Z)(Zle n m)->(Zle m n)->(n=m). - -Unfold Zle ;Intros n m H1 H2; (ElimCompare 'n 'm); [ - Elim (Zcompare_EGAL n m);Auto with arith -| Intros H3;Absurd (Zcompare m n)=SUPERIEUR; [ - Assumption - | Elim (Zcompare_ANTISYM m n);Auto with arith ] -| Intros H3;Absurd (Zcompare n m)=SUPERIEUR;Assumption ]. -Save. - -Theorem Zgt_lt : (m,n:Z) (Zgt m n) -> (Zlt n m). -Unfold Zgt Zlt ;Intros m n H; Elim (Zcompare_ANTISYM m n); Auto with arith. -Save. - -Theorem Zlt_gt : (m,n:Z) (Zlt m n) -> (Zgt n m). -Unfold Zgt Zlt ;Intros m n H; Elim (Zcompare_ANTISYM n m); Auto with arith. -Save. - -Theorem Zge_le : (m,n:Z) (Zge m n) -> (Zle n m). -Intros m n; Change ~(Zlt m n)-> ~(Zgt n m); -Unfold not; Intros H1 H2; Apply H1; Apply Zgt_lt; Assumption. -Save. - -Theorem Zle_ge : (m,n:Z) (Zle m n) -> (Zge n m). -Intros m n; Change ~(Zgt m n)-> ~(Zlt n m); -Unfold not; Intros H1 H2; Apply H1; Apply Zlt_gt; Assumption. -Save. - -Theorem Zge_trans : (n, m, p : Z) (Zge n m) -> (Zge m p) -> (Zge n p). -Intros n m p H1 H2. -Apply Zle_ge. -Apply Zle_trans with m; Apply Zge_le; Trivial. -Save. - -Theorem Zlt_n_Sn : (n:Z)(Zlt n (Zs n)). -Intro n; Apply Zgt_lt; Apply Zgt_Sn_n. -Save. -Theorem Zlt_S : (n,m:Z)(Zlt n m)->(Zlt n (Zs m)). -Intros n m H;Apply Zgt_lt; Apply Zgt_trans with m:=m; [ - Apply Zgt_Sn_n -| Apply Zlt_gt; Assumption ]. -Save. - -Theorem Zlt_n_S : (n,m:Z)(Zlt n m)->(Zlt (Zs n) (Zs m)). -Intros n m H;Apply Zgt_lt;Apply Zgt_n_S;Apply Zlt_gt; Assumption. -Save. - -Theorem Zlt_S_n : (n,m:Z)(Zlt (Zs n) (Zs m))->(Zlt n m). - -Intros n m H;Apply Zgt_lt;Apply Zgt_S_n;Apply Zlt_gt; Assumption. -Save. - -Theorem Zlt_n_n : (n:Z)~(Zlt n n). - -Intros n;Elim (Zcompare_EGAL n n); Unfold Zlt ;Intros H1 H2; -Rewrite H2; [ Discriminate | Trivial with arith ]. -Save. - -Lemma Zlt_pred : (n,p:Z)(Zlt (Zs n) p)->(Zlt n (Zpred p)). - -Intros n p H;Apply Zlt_S_n; Rewrite <- Zs_pred; Assumption. -Save. - -Lemma Zlt_pred_n_n : (n:Z)(Zlt (Zpred n) n). - -Intros n; Apply Zlt_S_n; Rewrite <- Zs_pred; Apply Zlt_n_Sn. -Save. - -Theorem Zlt_le_S : (n,p:Z)(Zlt n p)->(Zle (Zs n) p). -Intros n p H; Apply Zgt_le_S; Apply Zlt_gt; Assumption. -Save. - -Theorem Zlt_n_Sm_le : (n,m:Z)(Zlt n (Zs m))->(Zle n m). -Intros n m H; Apply Zgt_S_le; Apply Zlt_gt; Assumption. -Save. - -Theorem Zle_lt_n_Sm : (n,m:Z)(Zle n m)->(Zlt n (Zs m)). -Intros n m H; Apply Zgt_lt; Apply Zle_gt_S; Assumption. -Save. - -Theorem Zlt_le_weak : (n,m:Z)(Zlt n m)->(Zle n m). -Unfold Zlt Zle ;Intros n m H;Rewrite H;Discriminate. -Save. - -Theorem Zlt_trans : (n,m,p:Z)(Zlt n m)->(Zlt m p)->(Zlt n p). -Intros n m p H1 H2; Apply Zgt_lt; Apply Zgt_trans with m:= m; -Apply Zlt_gt; Assumption. -Save. -Theorem Zlt_le_trans : (n,m,p:Z)(Zlt n m)->(Zle m p)->(Zlt n p). -Intros n m p H1 H2;Apply Zgt_lt;Apply Zle_gt_trans with m:=m; - [ Assumption | Apply Zlt_gt;Assumption ]. -Save. - -Theorem Zle_lt_trans : (n,m,p:Z)(Zle n m)->(Zlt m p)->(Zlt n p). - -Intros n m p H1 H2;Apply Zgt_lt;Apply Zgt_le_trans with m:=m; - [ Apply Zlt_gt;Assumption | Assumption ]. -Save. - -Theorem Zle_lt_or_eq : (n,m:Z)(Zle n m)->((Zlt n m) \/ n=m). - -Unfold Zle Zlt ;Intros n m H; (ElimCompare 'n 'm); [ - Elim (Zcompare_EGAL n m);Auto with arith -| Auto with arith -| Intros H';Absurd (Zcompare n m)=SUPERIEUR;Assumption ]. -Save. - -Theorem Zle_or_lt : (n,m:Z)((Zle n m)\/(Zlt m n)). - -Unfold Zle Zlt ;Intros n m; (ElimCompare 'n 'm); [ - Intros E;Rewrite -> E;Left;Discriminate -| Intros E;Rewrite -> E;Left;Discriminate -| Elim (Zcompare_ANTISYM n m); Auto with arith ]. -Save. - -Theorem Zle_not_lt : (n,m:Z)(Zle n m) -> ~(Zlt m n). - -Unfold Zle Zlt; Unfold not ;Intros n m H1 H2;Apply H1; -Elim (Zcompare_ANTISYM n m);Auto with arith. -Save. - -Theorem Zlt_not_le : (n,m:Z)(Zlt n m) -> ~(Zle m n). -Unfold Zlt Zle not ;Intros n m H1 H2; Apply H2; Elim (Zcompare_ANTISYM m n); -Auto with arith. -Save. - -Theorem Zlt_not_sym : (n,m:Z)(Zlt n m) -> ~(Zlt m n). -Intros n m H;Apply Zle_not_lt; Apply Zlt_le_weak; Assumption. -Save. - -Theorem Zle_le_S : (x,y:Z)(Zle x y)->(Zle x (Zs y)). -Intros. -Apply Zle_trans with y; Trivial with zarith. -Save. - -Hints Resolve Zle_le_S : zarith. - -Definition Zmin := [n,m:Z] - <Z>Cases (Zcompare n m) of - EGAL => n - | INFERIEUR => n - | SUPERIEUR => m - end. - -Lemma Zmin_SS : (n,m:Z)((Zs (Zmin n m))=(Zmin (Zs n) (Zs m))). - -Intros n m;Unfold Zmin; Rewrite (Zcompare_n_S n m); -(ElimCompare 'n 'm);Intros E;Rewrite E;Auto with arith. -Save. - -Lemma Zle_min_l : (n,m:Z)(Zle (Zmin n m) n). - -Intros n m;Unfold Zmin ; (ElimCompare 'n 'm);Intros E;Rewrite -> E; - [ Apply Zle_n | Apply Zle_n | Apply Zlt_le_weak; Apply Zgt_lt;Exact E ]. -Save. - -Lemma Zle_min_r : (n,m:Z)(Zle (Zmin n m) m). - -Intros n m;Unfold Zmin ; (ElimCompare 'n 'm);Intros E;Rewrite -> E;[ - Unfold Zle ;Rewrite -> E;Discriminate -| Unfold Zle ;Rewrite -> E;Discriminate -| Apply Zle_n ]. -Save. - -Lemma Zmin_case : (n,m:Z)(P:Z->Set)(P n)->(P m)->(P (Zmin n m)). -Intros n m P H1 H2; Unfold Zmin; Case (Zcompare n m);Auto with arith. -Save. - -Lemma Zmin_or : (n,m:Z)(Zmin n m)=n \/ (Zmin n m)=m. -Unfold Zmin; Intros; Elim (Zcompare n m); Auto. -Save. - -Lemma Zmin_n_n : (n:Z) (Zmin n n)=n. -Unfold Zmin; Intros; Elim (Zcompare n n); Auto. -Save. - -Lemma Zplus_assoc_l : (n,m,p:Z)((Zplus n (Zplus m p))=(Zplus (Zplus n m) p)). - -Exact Zplus_assoc. -Save. - -Lemma Zplus_assoc_r : (n,m,p:Z)(Zplus (Zplus n m) p) =(Zplus n (Zplus m p)). - -Intros; Symmetry; Apply Zplus_assoc. -Save. - -Lemma Zplus_permute : (n,m,p:Z) (Zplus n (Zplus m p))=(Zplus m (Zplus n p)). - -Intros n m p; -Rewrite Zplus_sym;Rewrite <- Zplus_assoc; Rewrite (Zplus_sym p n); Trivial with arith. -Save. - -Lemma Zsimpl_le_plus_l : (p,n,m:Z)(Zle (Zplus p n) (Zplus p m))->(Zle n m). - -Intros p n m; Unfold Zle not ;Intros H1 H2;Apply H1; -Rewrite (Zcompare_Zplus_compatible n m p); Assumption. -Save. - -Lemma Zsimpl_le_plus_r : (p,n,m:Z)(Zle (Zplus n p) (Zplus m p))->(Zle n m). - -Intros p n m H; Apply Zsimpl_le_plus_l with p. -Rewrite (Zplus_sym p n); Rewrite (Zplus_sym p m); Trivial. -Save. - -Lemma Zle_reg_l : (n,m,p:Z)(Zle n m)->(Zle (Zplus p n) (Zplus p m)). - -Intros n m p; Unfold Zle not ;Intros H1 H2;Apply H1; -Rewrite <- (Zcompare_Zplus_compatible n m p); Assumption. -Save. - -Lemma Zle_reg_r : (a,b,c:Z) (Zle a b)->(Zle (Zplus a c) (Zplus b c)). - -Intros a b c;Do 2 Rewrite [n:Z](Zplus_sym n c); Exact (Zle_reg_l a b c). -Save. - -Lemma Zle_plus_plus : - (n,m,p,q:Z) (Zle n m)->(Zle p q)->(Zle (Zplus n p) (Zplus m q)). - -Intros n m p q; Intros H1 H2;Apply Zle_trans with m:=(Zplus n q); [ - Apply Zle_reg_l;Assumption | Apply Zle_reg_r;Assumption ]. -Save. - -Lemma Zplus_Snm_nSm : (n,m:Z)(Zplus (Zs n) m)=(Zplus n (Zs m)). - -Unfold Zs ;Intros n m; Rewrite <- Zplus_assoc; Rewrite (Zplus_sym (POS xH)); -Trivial with arith. -Save. - -Lemma Zsimpl_lt_plus_l - : (n,m,p:Z)(Zlt (Zplus p n) (Zplus p m))->(Zlt n m). - -Unfold Zlt ;Intros n m p; - Rewrite Zcompare_Zplus_compatible;Trivial with arith. -Save. - -Lemma Zsimpl_lt_plus_r - : (n,m,p:Z)(Zlt (Zplus n p) (Zplus m p))->(Zlt n m). - -Intros n m p H; Apply Zsimpl_lt_plus_l with p. -Rewrite (Zplus_sym p n); Rewrite (Zplus_sym p m); Trivial. -Save. - -Lemma Zlt_reg_l : (n,m,p:Z)(Zlt n m)->(Zlt (Zplus p n) (Zplus p m)). -Unfold Zlt ;Intros n m p; Rewrite Zcompare_Zplus_compatible;Trivial with arith. -Save. - -Lemma Zlt_reg_r : (n,m,p:Z)(Zlt n m)->(Zlt (Zplus n p) (Zplus m p)). -Intros n m p H; Rewrite (Zplus_sym n p); Rewrite (Zplus_sym m p); Apply Zlt_reg_l; Trivial. -Save. - -Lemma Zlt_le_reg : - (a,b,c,d:Z) (Zlt a b)->(Zle c d)->(Zlt (Zplus a c) (Zplus b d)). -Intros a b c d H0 H1. -Apply Zlt_le_trans with (Zplus b c). -Apply Zlt_reg_r; Trivial. -Apply Zle_reg_l; Trivial. -Save. - - -Lemma Zle_lt_reg : - (a,b,c,d:Z) (Zle a b)->(Zlt c d)->(Zlt (Zplus a c) (Zplus b d)). -Intros a b c d H0 H1. -Apply Zle_lt_trans with (Zplus b c). -Apply Zle_reg_r; Trivial. -Apply Zlt_reg_l; Trivial. -Save. - - -Definition Zminus := [m,n:Z](Zplus m (Zopp n)). - -Lemma Zminus_plus_simpl : - (n,m,p:Z)((Zminus n m)=(Zminus (Zplus p n) (Zplus p m))). - -Intros n m p;Unfold Zminus; Rewrite Zopp_Zplus; Rewrite Zplus_assoc; -Rewrite (Zplus_sym p); Rewrite <- (Zplus_assoc n p); Rewrite Zplus_inverse_r; -Rewrite Zero_right; Trivial with arith. -Save. - -Lemma Zminus_n_O : (n:Z)(n=(Zminus n ZERO)). - -Intro; Unfold Zminus; Simpl;Rewrite Zero_right; Trivial with arith. -Save. - -Lemma Zminus_n_n : (n:Z)(ZERO=(Zminus n n)). -Intro; Unfold Zminus; Rewrite Zplus_inverse_r; Trivial with arith. -Save. - -Lemma Zplus_minus : (n,m,p:Z)(n=(Zplus m p))->(p=(Zminus n m)). - -Intros n m p H;Unfold Zminus;Apply (Zsimpl_plus_l m); -Rewrite (Zplus_sym m (Zplus n (Zopp m))); Rewrite <- Zplus_assoc; -Rewrite Zplus_inverse_l; Rewrite Zero_right; Rewrite H; Trivial with arith. -Save. - -Lemma Zminus_plus : (n,m:Z)(Zminus (Zplus n m) n)=m. -Intros n m;Unfold Zminus ;Rewrite -> (Zplus_sym n m);Rewrite <- Zplus_assoc; -Rewrite -> Zplus_inverse_r; Apply Zero_right. -Save. - -Lemma Zle_plus_minus : (n,m:Z) (Zplus n (Zminus m n))=m. - -Unfold Zminus; Intros n m; Rewrite Zplus_permute; Rewrite Zplus_inverse_r; -Apply Zero_right. -Save. - -Lemma Zminus_Sn_m : (n,m:Z)((Zs (Zminus n m))=(Zminus (Zs n) m)). - -Intros n m;Unfold Zminus Zs; Rewrite (Zplus_sym n (Zopp m)); -Rewrite <- Zplus_assoc;Apply Zplus_sym. -Save. - -Lemma Zlt_minus : (n,m:Z)(Zlt ZERO m)->(Zlt (Zminus n m) n). - -Intros n m H; Apply Zsimpl_lt_plus_l with p:=m; Rewrite Zle_plus_minus; -Pattern 1 n ;Rewrite <- (Zero_right n); Rewrite (Zplus_sym m n); -Apply Zlt_reg_l; Assumption. -Save. - -Lemma Zlt_O_minus_lt : (n,m:Z)(Zlt ZERO (Zminus n m))->(Zlt m n). - -Intros n m H; Apply Zsimpl_lt_plus_l with p:=(Zopp m); Rewrite Zplus_inverse_l; -Rewrite Zplus_sym;Exact H. -Save. - -Lemma Zmult_plus_distr_l : - (n,m,p:Z)((Zmult (Zplus n m) p)=(Zplus (Zmult n p) (Zmult m p))). - -Intros n m p;Rewrite Zmult_sym;Rewrite Zmult_plus_distr_r; -Do 2 Rewrite -> (Zmult_sym p); Trivial with arith. -Save. - -Lemma Zmult_minus_distr : - (n,m,p:Z)((Zmult (Zminus n m) p)=(Zminus (Zmult n p) (Zmult m p))). -Intros n m p;Unfold Zminus; Rewrite Zmult_plus_distr_l; Rewrite Zopp_Zmult; -Trivial with arith. -Save. - -Lemma Zmult_assoc_r : (n,m,p:Z)((Zmult (Zmult n m) p) = (Zmult n (Zmult m p))). -Intros n m p; Rewrite Zmult_assoc; Trivial with arith. -Save. - -Lemma Zmult_assoc_l : (n,m,p:Z)(Zmult n (Zmult m p)) = (Zmult (Zmult n m) p). -Intros n m p; Rewrite Zmult_assoc; Trivial with arith. -Save. - -Theorem Zmult_permute : (n,m,p:Z)(Zmult n (Zmult m p)) = (Zmult m (Zmult n p)). -Intros; Rewrite -> (Zmult_assoc m n p); Rewrite -> (Zmult_sym m n). -Apply Zmult_assoc. -Save. - -Lemma Zmult_1_n : (n:Z)(Zmult (POS xH) n)=n. -Exact Zmult_one. -Save. - -Lemma Zmult_n_1 : (n:Z)(Zmult n (POS xH))=n. -Intro; Rewrite Zmult_sym; Apply Zmult_one. -Save. - -Lemma Zmult_Sm_n : (n,m:Z) (Zplus (Zmult n m) m)=(Zmult (Zs n) m). -Intros n m; Unfold Zs; Rewrite Zmult_plus_distr_l; Rewrite Zmult_1_n; -Trivial with arith. -Save. - - - - -(* - Just for compatibility with previous versions - Use [Zmult_plus_distr_r] and [Zmult_plus_distr_l] rather than - their synomymous -*) -Definition Zmult_Zplus_distr := Zmult_plus_distr_r. -Definition Zmult_plus_distr := Zmult_plus_distr_l. |