diff options
24 files changed, 4107 insertions, 15 deletions
diff --git a/theories/Relations/Newman.v b/theories/Relations/Newman.v index c5f3f7ddb..966a755c5 100755 --- a/theories/Relations/Newman.v +++ b/theories/Relations/Newman.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Rstar. diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v index 412533d8d..5c3a46529 100755 --- a/theories/Relations/Operators_Properties.v +++ b/theories/Relations/Operators_Properties.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) (****************************************************************************) (* Bruno Barras *) diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v index afd9e7588..35c670574 100755 --- a/theories/Relations/Relation_Definitions.v +++ b/theories/Relations/Relation_Definitions.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) Section Relation_Definition. diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v index d5b592628..a5ee00157 100755 --- a/theories/Relations/Relation_Operators.v +++ b/theories/Relations/Relation_Operators.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) (****************************************************************************) (* Bruno Barras Cristina Cornes *) diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v index ff17058f4..60cb9b4d7 100755 --- a/theories/Relations/Relations.v +++ b/theories/Relations/Relations.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Export Relation_Definitions. Require Export Relation_Operators. diff --git a/theories/Relations/Rstar.v b/theories/Relations/Rstar.v index 86b121883..0df3af6b4 100755 --- a/theories/Relations/Rstar.v +++ b/theories/Relations/Rstar.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) (* Properties of a binary relation R on type A *) diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v index a4e2bedfd..7de40a413 100644 --- a/theories/Wellfounded/Disjoint_Union.v +++ b/theories/Wellfounded/Disjoint_Union.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) (****************************************************************************) (* Cristina Cornes *) diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v index b104152f5..66ef2346e 100644 --- a/theories/Wellfounded/Inclusion.v +++ b/theories/Wellfounded/Inclusion.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) (****************************************************************************) (* Bruno Barras *) diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v index e0c5dc914..ffe56c0da 100644 --- a/theories/Wellfounded/Inverse_Image.v +++ b/theories/Wellfounded/Inverse_Image.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) (****************************************************************************) (* Bruno Barras *) diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v index 6a4ac7652..4ccc9e68d 100644 --- a/theories/Wellfounded/Lexicographic_Exponentiation.v +++ b/theories/Wellfounded/Lexicographic_Exponentiation.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) (****************************************************************************) (* Cristina Cornes *) diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index 419f545f5..104b8b437 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) (****************************************************************************) (* Bruno Barras Cristina Cornes *) diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v index b89e6c15b..992099809 100644 --- a/theories/Wellfounded/Transitive_Closure.v +++ b/theories/Wellfounded/Transitive_Closure.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) (****************************************************************************) (* Bruno Barras *) diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v index 697313f0a..1a3625b01 100644 --- a/theories/Wellfounded/Union.v +++ b/theories/Wellfounded/Union.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) (****************************************************************************) (* Bruno Barras *) diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v index 12f65b44e..ba9910440 100644 --- a/theories/Wellfounded/Well_Ordering.v +++ b/theories/Wellfounded/Well_Ordering.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) (****************************************************************************) (* Cristina Cornes *) diff --git a/theories/Wellfounded/Wellfounded.v b/theories/Wellfounded/Wellfounded.v index 696a9ea0c..10fca099c 100644 --- a/theories/Wellfounded/Wellfounded.v +++ b/theories/Wellfounded/Wellfounded.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Export Disjoint_Union. Require Export Inclusion. diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v new file mode 100644 index 000000000..d9cf77c75 --- /dev/null +++ b/theories/ZArith/Wf_Z.v @@ -0,0 +1,133 @@ +(***********************************************************************) +(* 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 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 new file mode 100644 index 000000000..b9b572137 --- /dev/null +++ b/theories/ZArith/ZArith.v @@ -0,0 +1,23 @@ +(***********************************************************************) +(* 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 new file mode 100644 index 000000000..ee7ee48b7 --- /dev/null +++ b/theories/ZArith/ZArith_dec.v @@ -0,0 +1,127 @@ +(***********************************************************************) +(* 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 new file mode 100644 index 000000000..663fe535c --- /dev/null +++ b/theories/ZArith/Zmisc.v @@ -0,0 +1,433 @@ +(***********************************************************************) +(* 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 new file mode 100644 index 000000000..4e92f7cd7 --- /dev/null +++ b/theories/ZArith/Zsyntax.v @@ -0,0 +1,213 @@ +(***********************************************************************) +(* 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 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 new file mode 100644 index 000000000..7a4ebae68 --- /dev/null +++ b/theories/ZArith/auxiliary.v @@ -0,0 +1,930 @@ +(***********************************************************************) +(* 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) *) +(* *) +(**************************************************************************) + +(*i $Id$ i*) + +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 new file mode 100644 index 000000000..f64093034 --- /dev/null +++ b/theories/ZArith/fast_integer.v @@ -0,0 +1,1486 @@ +(***********************************************************************) +(* 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 new file mode 100755 index 000000000..21e52c198 --- /dev/null +++ b/theories/ZArith/intro.tex @@ -0,0 +1,6 @@ +\section{Binary integers : ZArith} +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 new file mode 100644 index 000000000..856082b92 --- /dev/null +++ b/theories/ZArith/zarith_aux.v @@ -0,0 +1,741 @@ +(***********************************************************************) +(* 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. |