From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- theories7/ZArith/BinInt.v | 1005 +++++++++++++++++++++++++++++++++++++++ theories7/ZArith/Wf_Z.v | 194 ++++++++ theories7/ZArith/ZArith.v | 22 + theories7/ZArith/ZArith_base.v | 39 ++ theories7/ZArith/ZArith_dec.v | 243 ++++++++++ theories7/ZArith/Zabs.v | 138 ++++++ theories7/ZArith/Zbinary.v | 425 +++++++++++++++++ theories7/ZArith/Zbool.v | 158 ++++++ theories7/ZArith/Zcompare.v | 480 +++++++++++++++++++ theories7/ZArith/Zcomplements.v | 212 +++++++++ theories7/ZArith/Zdiv.v | 432 +++++++++++++++++ theories7/ZArith/Zeven.v | 184 +++++++ theories7/ZArith/Zhints.v | 387 +++++++++++++++ theories7/ZArith/Zlogarithm.v | 272 +++++++++++ theories7/ZArith/Zmin.v | 102 ++++ theories7/ZArith/Zmisc.v | 188 ++++++++ theories7/ZArith/Znat.v | 138 ++++++ theories7/ZArith/Znumtheory.v | 629 ++++++++++++++++++++++++ theories7/ZArith/Zorder.v | 969 +++++++++++++++++++++++++++++++++++++ theories7/ZArith/Zpower.v | 394 +++++++++++++++ theories7/ZArith/Zsqrt.v | 136 ++++++ theories7/ZArith/Zsyntax.v | 278 +++++++++++ theories7/ZArith/Zwf.v | 96 ++++ theories7/ZArith/auxiliary.v | 219 +++++++++ theories7/ZArith/fast_integer.v | 191 ++++++++ theories7/ZArith/zarith_aux.v | 163 +++++++ 26 files changed, 7694 insertions(+) create mode 100644 theories7/ZArith/BinInt.v create mode 100644 theories7/ZArith/Wf_Z.v create mode 100644 theories7/ZArith/ZArith.v create mode 100644 theories7/ZArith/ZArith_base.v create mode 100644 theories7/ZArith/ZArith_dec.v create mode 100644 theories7/ZArith/Zabs.v create mode 100644 theories7/ZArith/Zbinary.v create mode 100644 theories7/ZArith/Zbool.v create mode 100644 theories7/ZArith/Zcompare.v create mode 100644 theories7/ZArith/Zcomplements.v create mode 100644 theories7/ZArith/Zdiv.v create mode 100644 theories7/ZArith/Zeven.v create mode 100644 theories7/ZArith/Zhints.v create mode 100644 theories7/ZArith/Zlogarithm.v create mode 100644 theories7/ZArith/Zmin.v create mode 100644 theories7/ZArith/Zmisc.v create mode 100644 theories7/ZArith/Znat.v create mode 100644 theories7/ZArith/Znumtheory.v create mode 100644 theories7/ZArith/Zorder.v create mode 100644 theories7/ZArith/Zpower.v create mode 100644 theories7/ZArith/Zsqrt.v create mode 100644 theories7/ZArith/Zsyntax.v create mode 100644 theories7/ZArith/Zwf.v create mode 100644 theories7/ZArith/auxiliary.v create mode 100644 theories7/ZArith/fast_integer.v create mode 100644 theories7/ZArith/zarith_aux.v (limited to 'theories7/ZArith') diff --git a/theories7/ZArith/BinInt.v b/theories7/ZArith/BinInt.v new file mode 100644 index 00000000..9071896b --- /dev/null +++ b/theories7/ZArith/BinInt.v @@ -0,0 +1,1005 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Z | NEG : positive -> Z. + +(** Declare Scope Z_scope with Key Z *) +Delimits Scope Z_scope with Z. + +(** Automatically open scope positive_scope for the constructors of Z *) +Bind Scope Z_scope with Z. +Arguments Scope POS [ positive_scope ]. +Arguments Scope NEG [ positive_scope ]. + +(** Subtraction of positive into Z *) + +Definition Zdouble_plus_one [x:Z] := + Cases x of + | ZERO => (POS xH) + | (POS p) => (POS (xI p)) + | (NEG p) => (NEG (double_moins_un p)) + end. + +Definition Zdouble_minus_one [x:Z] := + Cases x of + | ZERO => (NEG xH) + | (NEG p) => (NEG (xI p)) + | (POS p) => (POS (double_moins_un p)) + end. + +Definition Zdouble [x:Z] := + Cases x of + | ZERO => ZERO + | (POS p) => (POS (xO p)) + | (NEG p) => (NEG (xO p)) + end. + +Fixpoint ZPminus [x,y:positive] : Z := + Cases x y of + | (xI x') (xI y') => (Zdouble (ZPminus x' y')) + | (xI x') (xO y') => (Zdouble_plus_one (ZPminus x' y')) + | (xI x') xH => (POS (xO x')) + | (xO x') (xI y') => (Zdouble_minus_one (ZPminus x' y')) + | (xO x') (xO y') => (Zdouble (ZPminus x' y')) + | (xO x') xH => (POS (double_moins_un x')) + | xH (xI y') => (NEG (xO y')) + | xH (xO y') => (NEG (double_moins_un y')) + | xH xH => ZERO + end. + +(** Addition on integers *) + +Definition Zplus := [x,y:Z] + Cases x y of + ZERO y => y + | x ZERO => x + | (POS x') (POS y') => (POS (add x' y')) + | (POS x') (NEG y') => + Cases (compare x' y' EGAL) of + | EGAL => ZERO + | INFERIEUR => (NEG (true_sub y' x')) + | SUPERIEUR => (POS (true_sub x' y')) + end + | (NEG x') (POS y') => + Cases (compare x' y' EGAL) of + | EGAL => ZERO + | INFERIEUR => (POS (true_sub y' x')) + | SUPERIEUR => (NEG (true_sub x' y')) + end + | (NEG x') (NEG y') => (NEG (add x' y')) + end. + +V8Infix "+" Zplus : Z_scope. + +(** Opposite *) + +Definition Zopp := [x:Z] + Cases x of + ZERO => ZERO + | (POS x) => (NEG x) + | (NEG x) => (POS x) + end. + +V8Notation "- x" := (Zopp x) : Z_scope. + +(** Successor on integers *) + +Definition Zs := [x:Z](Zplus x (POS xH)). + +(** Predecessor on integers *) + +Definition Zpred := [x:Z](Zplus x (NEG xH)). + +(** Subtraction on integers *) + +Definition Zminus := [m,n:Z](Zplus m (Zopp n)). + +V8Infix "-" Zminus : Z_scope. + +(** Multiplication on integers *) + +Definition Zmult := [x,y:Z] + Cases x y of + | ZERO _ => ZERO + | _ ZERO => ZERO + | (POS x') (POS y') => (POS (times x' y')) + | (POS x') (NEG y') => (NEG (times x' y')) + | (NEG x') (POS y') => (NEG (times x' y')) + | (NEG x') (NEG y') => (POS (times x' y')) + end. + +V8Infix "*" Zmult : Z_scope. + +(** Comparison of integers *) + +Definition Zcompare := [x,y:Z] + Cases x y of + | ZERO ZERO => EGAL + | ZERO (POS y') => INFERIEUR + | ZERO (NEG y') => SUPERIEUR + | (POS x') ZERO => SUPERIEUR + | (POS x') (POS y') => (compare x' y' EGAL) + | (POS x') (NEG y') => SUPERIEUR + | (NEG x') ZERO => INFERIEUR + | (NEG x') (POS y') => INFERIEUR + | (NEG x') (NEG y') => (Op (compare x' y' EGAL)) + end. + +V8Infix "?=" Zcompare (at level 70, no associativity) : Z_scope. + +Tactic Definition ElimCompare com1 com2:= + Case (Dcompare (Zcompare com1 com2)); [ Idtac | + Let x = FreshId "H" In Intro x; Case x; Clear x ]. + +(** Sign function *) + +Definition Zsgn [z:Z] : Z := + Cases z of + ZERO => ZERO + | (POS p) => (POS xH) + | (NEG p) => (NEG xH) + end. + +(** Direct, easier to handle variants of successor and addition *) + +Definition Zsucc' [x:Z] := + Cases x of + | ZERO => (POS xH) + | (POS x') => (POS (add_un x')) + | (NEG x') => (ZPminus xH x') + end. + +Definition Zpred' [x:Z] := + Cases x of + | ZERO => (NEG xH) + | (POS x') => (ZPminus x' xH) + | (NEG x') => (NEG (add_un x')) + end. + +Definition Zplus' := [x,y:Z] + Cases x y of + ZERO y => y + | x ZERO => x + | (POS x') (POS y') => (POS (add x' y')) + | (POS x') (NEG y') => (ZPminus x' y') + | (NEG x') (POS y') => (ZPminus y' x') + | (NEG x') (NEG y') => (NEG (add x' y')) + end. + +Open Local Scope Z_scope. + +(**********************************************************************) +(** Inductive specification of Z *) + +Theorem Zind : (P:(Z ->Prop)) + (P ZERO) -> ((x:Z)(P x) ->(P (Zsucc' x))) -> ((x:Z)(P x) ->(P (Zpred' x))) -> + (z:Z)(P z). +Proof. +Intros P H0 Hs Hp z; NewDestruct z. + Assumption. + Apply Pind with P:=[p](P (POS p)). + Change (P (Zsucc' ZERO)); Apply Hs; Apply H0. + Intro n; Exact (Hs (POS n)). + Apply Pind with P:=[p](P (NEG p)). + Change (P (Zpred' ZERO)); Apply Hp; Apply H0. + Intro n; Exact (Hp (NEG n)). +Qed. + +(**********************************************************************) +(** Properties of opposite on binary integer numbers *) + +Theorem Zopp_NEG : (x:positive) (Zopp (NEG x)) = (POS x). +Proof. +Reflexivity. +Qed. + +(** [opp] is involutive *) + +Theorem Zopp_Zopp: (x:Z) (Zopp (Zopp x)) = x. +Proof. +Intro x; NewDestruct x; Reflexivity. +Qed. + +(** Injectivity of the opposite *) + +Theorem Zopp_intro : (x,y:Z) (Zopp x) = (Zopp y) -> x = y. +Proof. +Intros x y;Case x;Case y;Simpl;Intros; [ + Trivial | Discriminate H | Discriminate H | Discriminate H +| Simplify_eq H; Intro E; Rewrite E; Trivial +| Discriminate H | Discriminate H | Discriminate H +| Simplify_eq H; Intro E; Rewrite E; Trivial ]. +Qed. + +(**********************************************************************) +(* Properties of the direct definition of successor and predecessor *) + +Lemma Zpred'_succ' : (x:Z)(Zpred' (Zsucc' x))=x. +Proof. +Intro x; NewDestruct x; Simpl. + Reflexivity. +NewDestruct p; Simpl; Try Rewrite double_moins_un_add_un_xI; Reflexivity. +NewDestruct p; Simpl; Try Rewrite is_double_moins_un; Reflexivity. +Qed. + +Lemma Zsucc'_discr : (x:Z)x<>(Zsucc' x). +Proof. +Intro x; NewDestruct x; Simpl. + Discriminate. + Injection; Apply add_un_discr. + NewDestruct p; Simpl. + Discriminate. + Intro H; Symmetry in H; Injection H; Apply double_moins_un_xO_discr. + Discriminate. +Qed. + +(**********************************************************************) +(** Other properties of binary integer numbers *) + +Lemma ZL0 : (S (S O))=(plus (S O) (S O)). +Proof. +Reflexivity. +Qed. + +(**********************************************************************) +(** Properties of the addition on integers *) + +(** zero is left neutral for addition *) + +Theorem Zero_left: (x:Z) (Zplus ZERO x) = x. +Proof. +Intro x; NewDestruct x; Reflexivity. +Qed. + +(** zero is right neutral for addition *) + +Theorem Zero_right: (x:Z) (Zplus x ZERO) = x. +Proof. +Intro x; NewDestruct x; Reflexivity. +Qed. + +(** addition is commutative *) + +Theorem Zplus_sym: (x,y:Z) (Zplus x y) = (Zplus y x). +Proof. +Intro x;NewInduction x as [|p|p];Intro y; NewDestruct y as [|q|q];Simpl;Try Reflexivity. + Rewrite add_sym; Reflexivity. + Rewrite ZC4; NewDestruct (compare q p EGAL); Reflexivity. + Rewrite ZC4; NewDestruct (compare q p EGAL); Reflexivity. + Rewrite add_sym; Reflexivity. +Qed. + +(** opposite distributes over addition *) + +Theorem Zopp_Zplus: + (x,y:Z) (Zopp (Zplus x y)) = (Zplus (Zopp x) (Zopp y)). +Proof. +Intro x; NewDestruct x as [|p|p]; Intro y; NewDestruct y as [|q|q]; Simpl; + Reflexivity Orelse NewDestruct (compare p q EGAL); Reflexivity. +Qed. + +(** opposite is inverse for addition *) + +Theorem Zplus_inverse_r: (x:Z) (Zplus x (Zopp x)) = ZERO. +Proof. +Intro x; NewDestruct x as [|p|p]; Simpl; [ + Reflexivity +| Rewrite (convert_compare_EGAL p); Reflexivity +| Rewrite (convert_compare_EGAL p); Reflexivity ]. +Qed. + +Theorem Zplus_inverse_l: (x:Z) (Zplus (Zopp x) x) = ZERO. +Proof. +Intro; Rewrite Zplus_sym; Apply Zplus_inverse_r. +Qed. + +Hints Local Resolve Zero_left Zero_right. + +(** addition is associative *) + +Lemma 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; ElimPcompare y z; + Intros E0;Rewrite E0; + ElimPcompare '(add x y) 'z;Intros E1;Rewrite E1; [ + Absurd (compare (add x y) z EGAL)=EGAL; [ (* Case 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; [ (* Case 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); (* Case 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); [ (* Case 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); [ (* Case 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); [ (* Case 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; [ (* Case 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; [ (* Case 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; (* Case 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 ]]]. +Qed. + +Hints Local Resolve weak_assoc. + +Theorem Zplus_assoc : + (n,m,p:Z) (Zplus n (Zplus m p))= (Zplus (Zplus n m) p). +Proof. +Intros x y z;Case x;Case y;Case z;Auto with arith; Intros; [ + 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] +. +Qed. + +V7only [Notation Zplus_assoc_l := Zplus_assoc.]. + +Lemma Zplus_assoc_r : (n,m,p:Z)(Zplus (Zplus n m) p) =(Zplus n (Zplus m p)). +Proof. +Intros; Symmetry; Apply Zplus_assoc. +Qed. + +(** Associativity mixed with commutativity *) + +Theorem Zplus_permute : (n,m,p:Z) (Zplus n (Zplus m p))=(Zplus m (Zplus n p)). +Proof. +Intros n m p; +Rewrite Zplus_sym;Rewrite <- Zplus_assoc; Rewrite (Zplus_sym p n); Trivial with arith. +Qed. + +(** addition simplifies *) + +Theorem 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 ]. +Qed. + +(** addition and successor permutes *) + +Lemma Zplus_S_n: (x,y:Z) (Zplus (Zs x) y) = (Zs (Zplus x y)). +Proof. +Intros x y; Unfold Zs; Rewrite (Zplus_sym (Zplus x y)); Rewrite Zplus_assoc; +Rewrite (Zplus_sym (POS xH)); Trivial with arith. +Qed. + +Lemma Zplus_n_Sm : (n,m:Z) (Zs (Zplus n m))=(Zplus n (Zs m)). +Proof. +Intros n m; Unfold Zs; Rewrite Zplus_assoc; Trivial with arith. +Qed. + +Lemma Zplus_Snm_nSm : (n,m:Z)(Zplus (Zs n) m)=(Zplus n (Zs m)). +Proof. +Unfold Zs ;Intros n m; Rewrite <- Zplus_assoc; Rewrite (Zplus_sym (POS xH)); +Trivial with arith. +Qed. + +(** Misc properties, usually redundant or non natural *) + +Lemma Zplus_n_O : (n:Z) n=(Zplus n ZERO). +Proof. +Symmetry; Apply Zero_right. +Qed. + +Lemma Zplus_unit_left : (n,m:Z) (Zplus n ZERO)=m -> n=m. +Proof. +Intros n m; Rewrite Zero_right; Intro; Assumption. +Qed. + +Lemma Zplus_unit_right : (n,m:Z) n=(Zplus m ZERO) -> n=m. +Proof. +Intros n m; Rewrite Zero_right; Intro; Assumption. +Qed. + +Lemma Zplus_simpl : (x,y,z,t:Z) x=y -> z=t -> (Zplus x z)=(Zplus y t). +Proof. +Intros; Rewrite H; Rewrite H0; Reflexivity. +Qed. + +Lemma Zplus_Zopp_expand : (x,y,z:Z) + (Zplus x (Zopp y))=(Zplus (Zplus x (Zopp z)) (Zplus z (Zopp y))). +Proof. +Intros x y z. +Rewrite <- (Zplus_assoc x). +Rewrite (Zplus_assoc (Zopp z)). +Rewrite Zplus_inverse_l. +Reflexivity. +Qed. + +(**********************************************************************) +(** Properties of successor and predecessor on binary integer numbers *) + +Theorem Zn_Sn : (x:Z) ~ x=(Zs x). +Proof. +Intros n;Cut ~ZERO=(POS xH);[ + Unfold not ;Intros H1 H2;Apply H1;Apply (Zsimpl_plus_l n);Rewrite Zero_right; + Exact H2 +| Discriminate ]. +Qed. + +Theorem add_un_Zs : (x:positive) (POS (add_un x)) = (Zs (POS x)). +Proof. +Intro; Rewrite -> ZL12; Unfold Zs; Simpl; Trivial with arith. +Qed. + +(** successor and predecessor are inverse functions *) + +Theorem Zs_pred : (n:Z) n=(Zs (Zpred n)). +Proof. +Intros n; Unfold Zs Zpred ;Rewrite <- Zplus_assoc; Simpl; Rewrite Zero_right; +Trivial with arith. +Qed. + +Hints Immediate Zs_pred : zarith. + +Theorem Zpred_Sn : (x:Z) x=(Zpred (Zs x)). +Proof. +Intros m; Unfold Zpred Zs; Rewrite <- Zplus_assoc; Simpl; +Rewrite Zplus_sym; Auto with arith. +Qed. + +Theorem Zeq_add_S : (n,m:Z) (Zs n)=(Zs m) -> n=m. +Proof. +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. +Qed. + +(** Misc properties, usually redundant or non natural *) + +Lemma Zeq_S : (n,m:Z) n=m -> (Zs n)=(Zs m). +Proof. +Intros n m H; Rewrite H; Reflexivity. +Qed. + +Lemma Znot_eq_S : (n,m:Z) ~(n=m) -> ~((Zs n)=(Zs m)). +Proof. +Unfold not ;Intros n m H1 H2;Apply H1;Apply Zeq_add_S; Assumption. +Qed. + +(**********************************************************************) +(** Properties of subtraction on binary integer numbers *) + +Lemma Zminus_0_r : (x:Z) (Zminus x ZERO)=x. +Proof. +Intro; Unfold Zminus; Simpl;Rewrite Zero_right; Trivial with arith. +Qed. + +Lemma Zminus_n_O : (x:Z) x=(Zminus x ZERO). +Proof. +Intro; Symmetry; Apply Zminus_0_r. +Qed. + +Lemma Zminus_diag : (n:Z)(Zminus n n)=ZERO. +Proof. +Intro; Unfold Zminus; Rewrite Zplus_inverse_r; Trivial with arith. +Qed. + +Lemma Zminus_n_n : (n:Z)(ZERO=(Zminus n n)). +Proof. +Intro; Symmetry; Apply Zminus_diag. +Qed. + +Lemma Zplus_minus : (x,y,z:Z)(x=(Zplus y z))->(z=(Zminus x y)). +Proof. +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. +Qed. + +Lemma Zminus_plus : (x,y:Z)(Zminus (Zplus x y) x)=y. +Proof. +Intros n m;Unfold Zminus ;Rewrite -> (Zplus_sym n m);Rewrite <- Zplus_assoc; +Rewrite -> Zplus_inverse_r; Apply Zero_right. +Qed. + +Lemma Zle_plus_minus : (n,m:Z) (Zplus n (Zminus m n))=m. +Proof. +Unfold Zminus; Intros n m; Rewrite Zplus_permute; Rewrite Zplus_inverse_r; +Apply Zero_right. +Qed. + +Lemma Zminus_Sn_m : (n,m:Z)((Zs (Zminus n m))=(Zminus (Zs n) m)). +Proof. +Intros n m;Unfold Zminus Zs; Rewrite (Zplus_sym n (Zopp m)); +Rewrite <- Zplus_assoc;Apply Zplus_sym. +Qed. + +Lemma Zminus_plus_simpl_l : + (x,y,z:Z)(Zminus (Zplus z x) (Zplus z y))=(Zminus x y). +Proof. +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. +Qed. + +Lemma Zminus_plus_simpl : + (x,y,z:Z)((Zminus x y)=(Zminus (Zplus z x) (Zplus z y))). +Proof. +Intros; Symmetry; Apply Zminus_plus_simpl_l. +Qed. + +Lemma Zminus_Zplus_compatible : + (x,y,z:Z) (Zminus (Zplus x z) (Zplus y z)) = (Zminus x y). +Intros x y n. +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. +Qed. + +(** Misc redundant properties *) + +V7only [Set Implicit Arguments.]. + +Lemma Zeq_Zminus : (x,y:Z)x=y -> (Zminus x y)=ZERO. +Proof. +Intros x y H; Rewrite H; Symmetry; Apply Zminus_n_n. +Qed. + +Lemma Zminus_Zeq : (x,y:Z)(Zminus x y)=ZERO -> x=y. +Proof. +Intros x y H; Rewrite <- (Zle_plus_minus y x); Rewrite H; Apply Zero_right. +Qed. + +V7only [Unset Implicit Arguments.]. + +(**********************************************************************) +(** Properties of multiplication on binary integer numbers *) + +(** One is neutral for multiplication *) + +Theorem Zmult_1_n : (n:Z)(Zmult (POS xH) n)=n. +Proof. +Intro x; NewDestruct x; Reflexivity. +Qed. +V7only [Notation Zmult_one := Zmult_1_n.]. + +Theorem Zmult_n_1 : (n:Z)(Zmult n (POS xH))=n. +Proof. +Intro x; NewDestruct x; Simpl; Try Rewrite times_x_1; Reflexivity. +Qed. + +(** Zero property of multiplication *) + +Theorem Zero_mult_left: (x:Z) (Zmult ZERO x) = ZERO. +Proof. +Intro x; NewDestruct x; Reflexivity. +Qed. + +Theorem Zero_mult_right: (x:Z) (Zmult x ZERO) = ZERO. +Proof. +Intro x; NewDestruct x; Reflexivity. +Qed. + +Hints Local Resolve Zero_mult_left Zero_mult_right. + +Lemma Zmult_n_O : (n:Z) ZERO=(Zmult n ZERO). +Proof. +Intro x; NewDestruct x; Reflexivity. +Qed. + +(** Commutativity of multiplication *) + +Theorem Zmult_sym : (x,y:Z) (Zmult x y) = (Zmult y x). +Proof. +Intros x y; NewDestruct x as [|p|p]; NewDestruct y as [|q|q]; Simpl; + Try Rewrite (times_sym p q); Reflexivity. +Qed. + +(** Associativity of multiplication *) + +Theorem Zmult_assoc : + (x,y,z:Z) (Zmult x (Zmult y z))= (Zmult (Zmult x y) z). +Proof. +Intros x y z; NewDestruct x; NewDestruct y; NewDestruct z; Simpl; + Try Rewrite times_assoc; Reflexivity. +Qed. +V7only [Notation Zmult_assoc_l := Zmult_assoc.]. + +Lemma Zmult_assoc_r : (n,m,p:Z)((Zmult (Zmult n m) p) = (Zmult n (Zmult m p))). +Proof. +Intros n m p; Rewrite Zmult_assoc; Trivial with arith. +Qed. + +(** Associativity mixed with commutativity *) + +Theorem Zmult_permute : (n,m,p:Z)(Zmult n (Zmult m p)) = (Zmult m (Zmult n p)). +Proof. +Intros x y z; Rewrite -> (Zmult_assoc y x z); Rewrite -> (Zmult_sym y x). +Apply Zmult_assoc. +Qed. + +(** Z is integral *) + +Theorem Zmult_eq: (x,y:Z) ~(x=ZERO) -> (Zmult y x) = ZERO -> y = ZERO. +Proof. +Intros x y; NewDestruct x as [|p|p]. + Intro H; Absurd ZERO=ZERO; Trivial. + Intros _ H; NewDestruct y as [|q|q]; Reflexivity Orelse Discriminate. + Intros _ H; NewDestruct y as [|q|q]; Reflexivity Orelse Discriminate. +Qed. + +V7only [Set Implicit Arguments.]. + +Theorem Zmult_zero : (x,y:Z)(Zmult x y)=ZERO -> x=ZERO \/ y=ZERO. +Proof. +Intros x y; NewDestruct x; NewDestruct y; Auto; Simpl; Intro H; Discriminate H. +Qed. + +V7only [Unset Implicit Arguments.]. + +Lemma Zmult_1_inversion_l : + (x,y:Z) (Zmult x y)=(POS xH) -> x=(POS xH) \/ x=(NEG xH). +Proof. +Intros x y; NewDestruct x as [|p|p]; Intro; [ Discriminate | Left | Right ]; + (NewDestruct y as [|q|q]; Try Discriminate; + Simpl in H; Injection H; Clear H; Intro H; + Rewrite times_one_inversion_l with 1:=H; Reflexivity). +Qed. + +(** Multiplication and Opposite *) + +Theorem Zopp_Zmult_l : (x,y:Z)(Zopp (Zmult x y)) = (Zmult (Zopp x) y). +Proof. +Intros x y; NewDestruct x; NewDestruct y; Reflexivity. +Qed. + +Theorem Zopp_Zmult_r : (x,y:Z)(Zopp (Zmult x y)) = (Zmult x (Zopp y)). +Intros x y; Rewrite (Zmult_sym x y); Rewrite Zopp_Zmult_l; Apply Zmult_sym. +Qed. + +Lemma Zopp_Zmult: (x,y:Z) (Zmult (Zopp x) y) = (Zopp (Zmult x y)). +Proof. +Intros x y; Symmetry; Apply Zopp_Zmult_l. +Qed. + +Theorem Zmult_Zopp_left : (x,y:Z)(Zmult (Zopp x) y) = (Zmult x (Zopp y)). +Intros x y; Rewrite Zopp_Zmult; Rewrite Zopp_Zmult_r; Trivial with arith. +Qed. + +Theorem Zmult_Zopp_Zopp: (x,y:Z) (Zmult (Zopp x) (Zopp y)) = (Zmult x y). +Proof. +Intros x y; NewDestruct x; NewDestruct y; Reflexivity. +Qed. + +Theorem Zopp_one : (x:Z)(Zopp x)=(Zmult x (NEG xH)). +Intro x; NewInduction x; Intros; Rewrite Zmult_sym; Auto with arith. +Qed. + +(** Distributivity of multiplication over addition *) + +Lemma 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; ElimPcompare z y; 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) ]]). +Qed. + +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 ]. +Qed. + +Theorem Zmult_plus_distr_l : + (n,m,p:Z)((Zmult (Zplus n m) p)=(Zplus (Zmult n p) (Zmult m p))). +Proof. +Intros n m p;Rewrite Zmult_sym;Rewrite Zmult_plus_distr_r; +Do 2 Rewrite -> (Zmult_sym p); Trivial with arith. +Qed. + +(** Distributivity of multiplication over subtraction *) + +Lemma Zmult_Zminus_distr_l : + (x,y,z:Z)((Zmult (Zminus x y) z)=(Zminus (Zmult x z) (Zmult y z))). +Proof. +Intros x y z; Unfold Zminus. +Rewrite <- Zopp_Zmult. +Apply Zmult_plus_distr_l. +Qed. + +V7only [Notation Zmult_minus_distr := Zmult_Zminus_distr_l.]. + +Lemma Zmult_Zminus_distr_r : + (x,y,z:Z)(Zmult z (Zminus x y)) = (Zminus (Zmult z x) (Zmult z y)). +Proof. +Intros x y z; Rewrite (Zmult_sym z (Zminus x y)). +Rewrite (Zmult_sym z x). +Rewrite (Zmult_sym z y). +Apply Zmult_Zminus_distr_l. +Qed. + +(** Simplification of multiplication for non-zero integers *) +V7only [Set Implicit Arguments.]. + +Lemma Zmult_reg_left : (x,y,z:Z) z<>ZERO -> (Zmult z x)=(Zmult z y) -> x=y. +Proof. +Intros x y z H H0. +Generalize (Zeq_Zminus H0). +Intro. +Apply Zminus_Zeq. +Rewrite <- Zmult_Zminus_distr_r in H1. +Clear H0; NewDestruct (Zmult_zero H1). +Contradiction. +Trivial. +Qed. + +Lemma Zmult_reg_right : (x,y,z:Z) z<>ZERO -> (Zmult x z)=(Zmult y z) -> x=y. +Proof. +Intros x y z Hz. +Rewrite (Zmult_sym x z). +Rewrite (Zmult_sym y z). +Intro; Apply Zmult_reg_left with z; Assumption. +Qed. +V7only [Unset Implicit Arguments.]. + +(** Addition and multiplication by 2 *) + +Lemma Zplus_Zmult_2 : (x:Z) (Zplus x x) = (Zmult x (POS (xO xH))). +Proof. +Intros x; Pattern 1 2 x ; Rewrite <- (Zmult_n_1 x); +Rewrite <- Zmult_plus_distr_r; Reflexivity. +Qed. + +(** Multiplication and successor *) + +Lemma Zmult_succ_r : (n,m:Z) (Zmult n (Zs m))=(Zplus (Zmult n m) n). +Proof. +Intros n m;Unfold Zs; Rewrite Zmult_plus_distr_r; +Rewrite (Zmult_sym n (POS xH));Rewrite Zmult_one; Trivial with arith. +Qed. + +Lemma Zmult_n_Sm : (n,m:Z) (Zplus (Zmult n m) n)=(Zmult n (Zs m)). +Proof. +Intros; Symmetry; Apply Zmult_succ_r. +Qed. + +Lemma Zmult_succ_l : (n,m:Z) (Zmult (Zs n) m)=(Zplus (Zmult n m) m). +Proof. +Intros n m; Unfold Zs; Rewrite Zmult_plus_distr_l; Rewrite Zmult_1_n; +Trivial with arith. +Qed. + +Lemma Zmult_Sm_n : (n,m:Z) (Zplus (Zmult n m) m)=(Zmult (Zs n) m). +Proof. +Intros; Symmetry; Apply Zmult_succ_l. +Qed. + +(** Misc redundant properties *) + +Lemma Z_eq_mult: + (x,y:Z) y = ZERO -> (Zmult y x) = ZERO. +Intros x y H; Rewrite H; Auto with arith. +Qed. + +(**********************************************************************) +(** Relating binary positive numbers and binary integers *) + +Lemma POS_xI : (p:positive) (POS (xI p))=(Zplus (Zmult (POS (xO xH)) (POS p)) (POS xH)). +Proof. +Intro; Apply refl_equal. +Qed. + +Lemma POS_xO : (p:positive) (POS (xO p))=(Zmult (POS (xO xH)) (POS p)). +Proof. +Intro; Apply refl_equal. +Qed. + +Lemma NEG_xI : (p:positive) (NEG (xI p))=(Zminus (Zmult (POS (xO xH)) (NEG p)) (POS xH)). +Proof. +Intro; Apply refl_equal. +Qed. + +Lemma NEG_xO : (p:positive) (NEG (xO p))=(Zmult (POS (xO xH)) (NEG p)). +Proof. +Reflexivity. +Qed. + +Lemma POS_add : (p,p':positive)(POS (add p p'))=(Zplus (POS p) (POS p')). +Proof. +Intros p p'; NewDestruct p; NewDestruct p'; Reflexivity. +Qed. + +Lemma NEG_add : (p,p':positive)(NEG (add p p'))=(Zplus (NEG p) (NEG p')). +Proof. +Intros p p'; NewDestruct p; NewDestruct p'; Reflexivity. +Qed. + +(**********************************************************************) +(** 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. +Definition Zne := [x,y:Z] ~(x=y). + +V8Infix "<=" Zle : Z_scope. +V8Infix "<" Zlt : Z_scope. +V8Infix ">=" Zge : Z_scope. +V8Infix ">" Zgt : Z_scope. + +V8Notation "x <= y <= z" := (Zle x y)/\(Zle y z) :Z_scope. +V8Notation "x <= y < z" := (Zle x y)/\(Zlt y z) :Z_scope. +V8Notation "x < y < z" := (Zlt x y)/\(Zlt y z) :Z_scope. +V8Notation "x < y <= z" := (Zlt x y)/\(Zle y z) :Z_scope. + +(**********************************************************************) +(** Absolute value on integers *) + +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. + +(**********************************************************************) +(** From [nat] to [Z] *) + +Definition inject_nat := + [x:nat]Cases x of + O => ZERO + | (S y) => (POS (anti_convert y)) + end. + +Require BinNat. + +Definition entier_of_Z := + [z:Z]Cases z of ZERO => Nul | (POS p) => (Pos p) | (NEG p) => (Pos p) end. + +Definition Z_of_entier := + [x:entier]Cases x of Nul => ZERO | (Pos p) => (POS p) end. diff --git a/theories7/ZArith/Wf_Z.v b/theories7/ZArith/Wf_Z.v new file mode 100644 index 00000000..e6cf4610 --- /dev/null +++ b/theories7/ZArith/Wf_Z.v @@ -0,0 +1,194 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (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. *) + +Lemma inject_nat_complete : + (x:Z)`0 <= x` -> (EX n:nat | x=(inject_nat n)). +Intro x; NewDestruct x; Intros; +[ Exists O; Auto with arith +| Specialize (ZL4 p); Intros Hp; Elim Hp; Intros; + Exists (S x); Intros; Simpl; + Specialize (bij1 x); 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] +]. +Qed. + +Lemma ZL4_inf: (y:positive) { h:nat | (convert y)=(S h) }. +Intro y; NewInduction y as [p H|p H1|]; [ + 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 +| 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]. +Qed. + +Lemma inject_nat_complete_inf : + (x:Z)`0 <= x` -> { n:nat | (x=(inject_nat n)) }. +Intro x; NewDestruct 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] +]. +Qed. + +Lemma inject_nat_prop : + (P:Z->Prop)((n:nat)(P (inject_nat n))) -> + (x:Z) `0 <= x` -> (P x). +Intros P H x H0. +Specialize (inject_nat_complete x H0). +Intros Hn; Elim Hn; Intros. +Rewrite -> H1; Apply H. +Qed. + +Lemma inject_nat_set : + (P:Z->Set)((n:nat)(P (inject_nat n))) -> + (x:Z) `0 <= x` -> (P x). +Intros P H x H0. +Specialize (inject_nat_complete_inf x H0). +Intros Hn; Elim Hn; Intros. +Rewrite -> p; Apply H. +Qed. + +Lemma natlike_ind : (P:Z->Prop) (P `0`) -> + ((x:Z)(`0 <= x` -> (P x) -> (P (Zs x)))) -> + (x:Z) `0 <= x` -> (P x). +Intros P H H0 x H1; Apply inject_nat_prop; +[ Induction n; + [ Simpl; Assumption + | Intros; Rewrite -> (inj_S n0); + Exact (H0 (inject_nat n0) (ZERO_le_inj n0) H2) ] +| Assumption]. +Qed. + +Lemma natlike_rec : (P:Z->Set) (P `0`) -> + ((x:Z)(`0 <= x` -> (P x) -> (P (Zs x)))) -> + (x:Z) `0 <= x` -> (P x). +Intros P H H0 x H1; Apply inject_nat_set; +[ Induction n; + [ Simpl; Assumption + | Intros; Rewrite -> (inj_S n0); + Exact (H0 (inject_nat n0) (ZERO_le_inj n0) H2) ] +| Assumption]. +Qed. + +Section Efficient_Rec. + +(** [natlike_rec2] is the same as [natlike_rec], but with a different proof, designed + to give a better extracted term. *) + +Local R := [a,b:Z]`0<=a`/\`a (convert p) | ZERO => O | (NEG _) => O end. +Apply well_founded_lt_compat with f. +Unfold R f; Clear f R. +Intros x y; Case x; Intros; Elim H; Clear H. +Case y; Intros; Apply compare_convert_O Orelse Inversion H0. +Case y; Intros; Apply compare_convert_INFERIEUR Orelse Inversion H0; Auto. +Intros; Elim H; Auto. +Qed. + +Lemma natlike_rec2 : (P:Z->Type)(P `0`) -> + ((z:Z)`0<=z` -> (P z) -> (P (Zs z))) -> (z:Z)`0<=z` -> (P z). +Proof. +Intros P Ho Hrec z; Pattern z; Apply (well_founded_induction_type Z R R_wf). +Intro x; Case x. +Trivial. +Intros. +Assert `0<=(Zpred (POS p))`. +Apply Zlt_ZERO_pred_le_ZERO; Unfold Zlt; Simpl; Trivial. +Rewrite Zs_pred. +Apply Hrec. +Auto. +Apply X; Auto; Unfold R; Intuition; Apply Zlt_pred_n_n. +Intros; Elim H; Simpl; Trivial. +Qed. + +(** A variant of the previous using [Zpred] instead of [Zs]. *) + +Lemma natlike_rec3 : (P:Z->Type)(P `0`) -> + ((z:Z)`0 (P (Zpred z)) -> (P z)) -> (z:Z)`0<=z` -> (P z). +Proof. +Intros P Ho Hrec z; Pattern z; Apply (well_founded_induction_type Z R R_wf). +Intro x; Case x. +Trivial. +Intros; Apply Hrec. +Unfold Zlt; Trivial. +Assert `0<=(Zpred (POS p))`. +Apply Zlt_ZERO_pred_le_ZERO; Unfold Zlt; Simpl; Trivial. +Apply X; Auto; Unfold R; Intuition; Apply Zlt_pred_n_n. +Intros; Elim H; Simpl; Trivial. +Qed. + +(** A more general induction principal using [Zlt]. *) + +Lemma Z_lt_rec : (P:Z->Type) + ((x:Z)((y:Z)`0 <= y < x`->(P y))->(P x)) -> (x:Z)`0 <= x`->(P x). +Proof. +Intros P Hrec z; Pattern z; Apply (well_founded_induction_type Z R R_wf). +Intro x; Case x; Intros. +Apply Hrec; Intros. +Assert H2: `0<0`. + Apply Zle_lt_trans with y; Intuition. +Inversion H2. +Firstorder. +Unfold Zle Zcompare in H; Elim H; Auto. +Defined. + +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. +Exact Z_lt_rec. +Qed. + +End Efficient_Rec. diff --git a/theories7/ZArith/ZArith.v b/theories7/ZArith/ZArith.v new file mode 100644 index 00000000..e1746433 --- /dev/null +++ b/theories7/ZArith/ZArith.v @@ -0,0 +1,22 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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. +Defined. + +Section decidability. + +Variables x,y : Z. + +(** Decidability of equality on binary integers *) + +Definition Z_eq_dec : {x=y}+{~x=y}. +Proof. +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. +Defined. + +(** Decidability of order on binary integers *) + +Definition Z_lt_dec : {(Zlt x y)}+{~(Zlt x y)}. +Proof. +Unfold Zlt. +Apply Zcompare_rec with x:=x y:=y; Intro H. +Right. Rewrite H. Discriminate. +Left; Assumption. +Right. Rewrite H. Discriminate. +Defined. + +Definition Z_le_dec : {(Zle x y)}+{~(Zle x y)}. +Proof. +Unfold Zle. +Apply Zcompare_rec with x:=x y:=y; Intro H. +Left. Rewrite H. Discriminate. +Left. Rewrite H. Discriminate. +Right. Tauto. +Defined. + +Definition Z_gt_dec : {(Zgt x y)}+{~(Zgt x y)}. +Proof. +Unfold Zgt. +Apply Zcompare_rec with x:=x y:=y; Intro H. +Right. Rewrite H. Discriminate. +Right. Rewrite H. Discriminate. +Left; Assumption. +Defined. + +Definition Z_ge_dec : {(Zge x y)}+{~(Zge x y)}. +Proof. +Unfold Zge. +Apply Zcompare_rec with x:=x y:=y; Intro H. +Left. Rewrite H. Discriminate. +Right. Tauto. +Left. Rewrite H. Discriminate. +Defined. + +Definition Z_lt_ge_dec : {`x < y`}+{`x >= y`}. +Proof. +Exact Z_lt_dec. +Defined. + +V7only [ (* From Zextensions *) ]. +Lemma Z_lt_le_dec: {`x < y`}+{`y <= x`}. +Proof. +Intros. +Elim Z_lt_ge_dec. +Intros; Left; Assumption. +Intros; Right; Apply Zge_le; Assumption. +Qed. + +Definition Z_le_gt_dec : {`x <= y`}+{`x > y`}. +Proof. +Elim Z_le_dec; Auto with arith. +Intro. Right. Apply not_Zle; Auto with arith. +Defined. + +Definition Z_gt_le_dec : {`x > y`}+{`x <= y`}. +Proof. +Exact Z_gt_dec. +Defined. + +Definition Z_ge_lt_dec : {`x >= y`}+{`x < y`}. +Proof. +Elim Z_ge_dec; Auto with arith. +Intro. Right. Apply not_Zge; Auto with arith. +Defined. + +Definition 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. +Defined. + +End decidability. + +(** Cotransitivity of order on binary integers *) + +Lemma Zlt_cotrans:(n,m:Z)`n(p:Z){`n{`0{`x<0`}+{`y<0`}. +Proof. + Intros x y H; + Case (Zlt_cotrans `x+y` `0` H x); + Intro Hxy; + [ Right; + Apply Zsimpl_lt_plus_l with p:=`x`; + Rewrite Zero_right + | Left + ]; + Assumption. +Defined. + +Lemma not_Zeq_inf:(x,y:Z)`x<>y`->{`xy`}+{`x=y`}. +Proof. + Intros x y. + Case (Z_lt_ge_dec x y). + Intro H. + Left. + Left. + Assumption. + Intro H. + Generalize (Zge_le ? ? H). + Intro H0. + Case (Z_le_lt_eq_dec y x H0). + Intro H1. + Left. + Right. + Apply Zlt_gt. + Assumption. + Intro. + Right. + Symmetry. + Assumption. +Defined. + + +Lemma Z_dec':(x,y:Z){`x 0`)}. +Proof. +Exact [x:Z](Z_eq_dec x ZERO). +Defined. + +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/theories7/ZArith/Zabs.v b/theories7/ZArith/Zabs.v new file mode 100644 index 00000000..57778cae --- /dev/null +++ b/theories7/ZArith/Zabs.v @@ -0,0 +1,138 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (Zabs x)=x. +Intro x; NewDestruct x; Auto with arith. +Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith. +Qed. + +Lemma Zabs_non_eq : (x:Z) (Zle x ZERO) -> (Zabs x)=(Zopp x). +Proof. +Intro x; NewDestruct x; Auto with arith. +Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith. +Qed. + +V7only [ (* From Zdivides *) ]. +Theorem Zabs_Zopp: (z : Z) (Zabs (Zopp z)) = (Zabs z). +Proof. +Intros z; Case z; Simpl; Auto. +Qed. + +(** Proving a property of the absolute value by cases *) + +Lemma Zabs_ind : + (P:Z->Prop)(x:Z)(`x >= 0` -> (P x)) -> (`x <= 0` -> (P `-x`)) -> + (P `|x|`). +Proof. +Intros P x H H0; Elim (Z_lt_ge_dec x `0`); Intro. +Assert `x<=0`. Apply Zlt_le_weak; Assumption. +Rewrite Zabs_non_eq. Apply H0. Assumption. Assumption. +Rewrite Zabs_eq. Apply H; Assumption. Apply Zge_le. Assumption. +Save. + +V7only [ (* From Zdivides *) ]. +Theorem Zabs_intro: (P : ?) (z : Z) (P (Zopp z)) -> (P z) -> (P (Zabs z)). +Intros P z; Case z; Simpl; Auto. +Qed. + +Definition Zabs_dec : (x:Z){x=(Zabs x)}+{x=(Zopp (Zabs x))}. +Proof. +Intro x; NewDestruct x;Auto with arith. +Defined. + +Lemma Zabs_pos : (x:Z)(Zle ZERO (Zabs x)). +Intro x; NewDestruct x;Auto with arith; Compute; Intros H;Inversion H. +Qed. + +V7only [ (* From Zdivides *) ]. +Theorem Zabs_eq_case: + (z1, z2 : Z) (Zabs z1) = (Zabs z2) -> z1 = z2 \/ z1 = (Zopp z2). +Proof. +Intros z1 z2; Case z1; Case z2; Simpl; Auto; Try (Intros; Discriminate); + Intros p1 p2 H1; Injection H1; (Intros H2; Rewrite H2); Auto. +Qed. + +(** Triangular inequality *) + +Hints Local Resolve Zle_NEG_POS :zarith. + +V7only [ (* From Zdivides *) ]. +Theorem Zabs_triangle: + (z1, z2 : Z) (Zle (Zabs (Zplus z1 z2)) (Zplus (Zabs z1) (Zabs z2))). +Proof. +Intros z1 z2; Case z1; Case z2; Try (Simpl; Auto with zarith; Fail). +Intros p1 p2; + Apply Zabs_intro + with P := [x : ?] (Zle x (Zplus (Zabs (POS p2)) (Zabs (NEG p1)))); + Try Rewrite Zopp_Zplus; Auto with zarith. +Apply Zle_plus_plus; Simpl; Auto with zarith. +Apply Zle_plus_plus; Simpl; Auto with zarith. +Intros p1 p2; + Apply Zabs_intro + with P := [x : ?] (Zle x (Zplus (Zabs (POS p2)) (Zabs (NEG p1)))); + Try Rewrite Zopp_Zplus; Auto with zarith. +Apply Zle_plus_plus; Simpl; Auto with zarith. +Apply Zle_plus_plus; Simpl; Auto with zarith. +Qed. + +(** Absolute value and multiplication *) + +Lemma Zsgn_Zabs: (x:Z)(Zmult x (Zsgn x))=(Zabs x). +Proof. +Intro x; NewDestruct x; Rewrite Zmult_sym; Auto with arith. +Qed. + +Lemma Zabs_Zsgn: (x:Z)(Zmult (Zabs x) (Zsgn x))=x. +Proof. +Intro x; NewDestruct x; Rewrite Zmult_sym; Auto with arith. +Qed. + +V7only [ (* From Zdivides *) ]. +Theorem Zabs_Zmult: + (z1, z2 : Z) (Zabs (Zmult z1 z2)) = (Zmult (Zabs z1) (Zabs z2)). +Proof. +Intros z1 z2; Case z1; Case z2; Simpl; Auto. +Qed. + +(** absolute value in nat is compatible with order *) + +Lemma absolu_lt : (x,y:Z) (Zle ZERO x)/\(Zlt x y) -> (lt (absolu x) (absolu y)). +Proof. +Intros x y. Case x; Simpl. Case y; Simpl. + +Intro. Absurd (Zlt ZERO ZERO). 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 (Zlt (POS p) ZERO). 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 (Zlt (POS p0) (NEG p)). +Compute. Intro H0. Discriminate H0. Intuition. + +Intros. Absurd (Zle ZERO (NEG p)). Compute. Auto with arith. Intuition. +Qed. diff --git a/theories7/ZArith/Zbinary.v b/theories7/ZArith/Zbinary.v new file mode 100644 index 00000000..c3efbe1e --- /dev/null +++ b/theories7/ZArith/Zbinary.v @@ -0,0 +1,425 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Z + two_power_nat_S + : (n:nat)`(two_power_nat (S n)) = 2*(two_power_nat n)` + Z_lt_ge_dec + : (x,y:Z){`x < y`}+{`x >= y`} +*) + + +Section VALUE_OF_BOOLEAN_VECTORS. + +(* +Les calculs sont effectués dans la convention positive usuelle. +Les valeurs correspondent soit à l'écriture binaire (nat), +soit au complément à deux (int). +On effectue le calcul suivant le schéma de Horner. +Le complément à deux n'a de sens que sur les vecteurs de taille +supérieure ou égale à un, le bit de signe étant évalué négativement. +*) + +Definition bit_value [b:bool] : Z := +Cases b of + | true => `1` + | false => `0` +end. + +Lemma binary_value : (n:nat) (Bvector n) -> Z. +Proof. + Induction n; Intros. + Exact `0`. + + Inversion H0. + Exact (Zplus (bit_value a) (Zmult `2` (H H2))). +Defined. + +Lemma two_compl_value : (n:nat) (Bvector (S n)) -> Z. +Proof. + Induction n; Intros. + Inversion H. + Exact (Zopp (bit_value a)). + + Inversion H0. + Exact (Zplus (bit_value a) (Zmult `2` (H H2))). +Defined. + +(* +Coq < Eval Compute in (binary_value (3) (Bcons true (2) (Bcons false (1) (Bcons true (0) Bnil)))). + = `5` + : Z +*) + +(* +Coq < Eval Compute in (two_compl_value (3) (Bcons true (3) (Bcons false (2) (Bcons true (1) (Bcons true (0) Bnil))))). + = `-3` + : Z +*) + +End VALUE_OF_BOOLEAN_VECTORS. + +Section ENCODING_VALUE. + +(* +On calcule la valeur binaire selon un schema de Horner. +Le calcul s'arrete à la longueur du vecteur sans vérification. +On definit une fonction Zmod2 calquee sur Zdiv2 mais donnant le quotient +de la division z=2q+r avec 0<=r<=1. +La valeur en complément à deux est calculée selon un schema de Horner +avec Zmod2, le paramètre est la taille moins un. +*) + +Definition Zmod2 := [z:Z] Cases z of + | ZERO => `0` + | ((POS p)) => Cases p of + | (xI q) => (POS q) + | (xO q) => (POS q) + | xH => `0` + end + | ((NEG p)) => Cases p of + | (xI q) => `(NEG q) - 1` + | (xO q) => (NEG q) + | xH => `-1` + end + end. + +V7only [ +Notation double_moins_un_add_un := + [p](sym_eq ? ? ? (double_moins_un_add_un_xI p)). +]. + +Lemma Zmod2_twice : (z:Z) + `z = (2*(Zmod2 z) + (bit_value (Zodd_bool z)))`. +Proof. + NewDestruct z; Simpl. + Trivial. + + NewDestruct p; Simpl; Trivial. + + NewDestruct p; Simpl. + NewDestruct p as [p|p|]; Simpl. + Rewrite <- (double_moins_un_add_un_xI p); Trivial. + + Trivial. + + Trivial. + + Trivial. + + Trivial. +Save. + +Lemma Z_to_binary : (n:nat) Z -> (Bvector n). +Proof. + Induction n; Intros. + Exact Bnil. + + Exact (Bcons (Zodd_bool H0) n0 (H (Zdiv2 H0))). +Defined. + +(* +Eval Compute in (Z_to_binary (5) `5`). + = (Vcons bool true (4) + (Vcons bool false (3) + (Vcons bool true (2) + (Vcons bool false (1) (Vcons bool false (0) (Vnil bool)))))) + : (Bvector (5)) +*) + +Lemma Z_to_two_compl : (n:nat) Z -> (Bvector (S n)). +Proof. + Induction n; Intros. + Exact (Bcons (Zodd_bool H) (0) Bnil). + + Exact (Bcons (Zodd_bool H0) (S n0) (H (Zmod2 H0))). +Defined. + +(* +Eval Compute in (Z_to_two_compl (3) `0`). + = (Vcons bool false (3) + (Vcons bool false (2) + (Vcons bool false (1) (Vcons bool false (0) (Vnil bool))))) + : (vector bool (4)) + +Eval Compute in (Z_to_two_compl (3) `5`). + = (Vcons bool true (3) + (Vcons bool false (2) + (Vcons bool true (1) (Vcons bool false (0) (Vnil bool))))) + : (vector bool (4)) + +Eval Compute in (Z_to_two_compl (3) `-5`). + = (Vcons bool true (3) + (Vcons bool true (2) + (Vcons bool false (1) (Vcons bool true (0) (Vnil bool))))) + : (vector bool (4)) +*) + +End ENCODING_VALUE. + +Section Z_BRIC_A_BRAC. + +(* +Bibliotheque de lemmes utiles dans la section suivante. +Utilise largement ZArith. +Meriterait d'etre reecrite. +*) + +Lemma binary_value_Sn : (n:nat) (b:bool) (bv : (Bvector n)) + (binary_value (S n) (Vcons bool b n bv))=`(bit_value b) + 2*(binary_value n bv)`. +Proof. + Intros; Auto. +Save. + +Lemma Z_to_binary_Sn : (n:nat) (b:bool) (z:Z) + `z>=0`-> + (Z_to_binary (S n) `(bit_value b) + 2*z`)=(Bcons b n (Z_to_binary n z)). +Proof. + NewDestruct b; NewDestruct z; Simpl; Auto. + Intro H; Elim H; Trivial. +Save. + +Lemma binary_value_pos : (n:nat) (bv:(Bvector n)) + `(binary_value n bv) >= 0`. +Proof. + NewInduction bv as [|a n v IHbv]; Simpl. + Omega. + + NewDestruct a; NewDestruct (binary_value n v); Simpl; Auto. + Auto with zarith. +Save. + +V7only [Notation add_un_double_moins_un_xO := is_double_moins_un.]. + +Lemma two_compl_value_Sn : (n:nat) (bv : (Bvector (S n))) (b:bool) + (two_compl_value (S n) (Bcons b (S n) bv)) = + `(bit_value b) + 2*(two_compl_value n bv)`. +Proof. + Intros; Auto. +Save. + +Lemma Z_to_two_compl_Sn : (n:nat) (b:bool) (z:Z) + (Z_to_two_compl (S n) `(bit_value b) + 2*z`) = + (Bcons b (S n) (Z_to_two_compl n z)). +Proof. + NewDestruct b; NewDestruct z as [|p|p]; Auto. + NewDestruct p as [p|p|]; Auto. + NewDestruct p as [p|p|]; Simpl; Auto. + Intros; Rewrite (add_un_double_moins_un_xO p); Trivial. +Save. + +Lemma Z_to_binary_Sn_z : (n:nat) (z:Z) + (Z_to_binary (S n) z)=(Bcons (Zodd_bool z) n (Z_to_binary n (Zdiv2 z))). +Proof. + Intros; Auto. +Save. + +Lemma Z_div2_value : (z:Z) + ` z>=0 `-> + `(bit_value (Zodd_bool z))+2*(Zdiv2 z) = z`. +Proof. + NewDestruct z as [|p|p]; Auto. + NewDestruct p; Auto. + Intro H; Elim H; Trivial. +Save. + +Lemma Zdiv2_pos : (z:Z) + ` z >= 0 ` -> + `(Zdiv2 z) >= 0 `. +Proof. + NewDestruct z as [|p|p]. + Auto. + + NewDestruct p; Auto. + Simpl; Intros; Omega. + + Intro H; Elim H; Trivial. + +Save. + +Lemma Zdiv2_two_power_nat : (z:Z) (n:nat) + ` z >= 0 ` -> + ` z < (two_power_nat (S n)) ` -> + `(Zdiv2 z) < (two_power_nat n) `. +Proof. + Intros. + Cut (Zlt (Zmult `2` (Zdiv2 z)) (Zmult `2` (two_power_nat n))); Intros. + Omega. + + Rewrite <- two_power_nat_S. + NewDestruct (Zeven_odd_dec z); Intros. + Rewrite <- Zeven_div2; Auto. + + Generalize (Zodd_div2 z H z0); Omega. +Save. + +(* + +Lemma Z_minus_one_or_zero : (z:Z) + `z >= -1` -> + `z < 1` -> + {`z=-1`} + {`z=0`}. +Proof. + NewDestruct z; Auto. + NewDestruct p; Auto. + Tauto. + + Tauto. + + Intros. + Right; Omega. + + NewDestruct p. + Tauto. + + Tauto. + + Intros; Left; Omega. +Save. +*) + +Lemma Z_to_two_compl_Sn_z : (n:nat) (z:Z) + (Z_to_two_compl (S n) z)=(Bcons (Zodd_bool z) (S n) (Z_to_two_compl n (Zmod2 z))). +Proof. + Intros; Auto. +Save. + +Lemma Zeven_bit_value : (z:Z) + (Zeven z) -> + `(bit_value (Zodd_bool z))=0`. +Proof. + NewDestruct z; Unfold bit_value; Auto. + NewDestruct p; Tauto Orelse (Intro H; Elim H). + NewDestruct p; Tauto Orelse (Intro H; Elim H). +Save. + +Lemma Zodd_bit_value : (z:Z) + (Zodd z) -> + `(bit_value (Zodd_bool z))=1`. +Proof. + NewDestruct z; Unfold bit_value; Auto. + Intros; Elim H. + NewDestruct p; Tauto Orelse (Intros; Elim H). + NewDestruct p; Tauto Orelse (Intros; Elim H). +Save. + +Lemma Zge_minus_two_power_nat_S : (n:nat) (z:Z) + `z >= (-(two_power_nat (S n)))`-> + `(Zmod2 z) >= (-(two_power_nat n))`. +Proof. + Intros n z; Rewrite (two_power_nat_S n). + Generalize (Zmod2_twice z). + NewDestruct (Zeven_odd_dec z) as [H|H]. + Rewrite (Zeven_bit_value z H); Intros; Omega. + + Rewrite (Zodd_bit_value z H); Intros; Omega. +Save. + +Lemma Zlt_two_power_nat_S : (n:nat) (z:Z) + `z < (two_power_nat (S n))`-> + `(Zmod2 z) < (two_power_nat n)`. +Proof. + Intros n z; Rewrite (two_power_nat_S n). + Generalize (Zmod2_twice z). + NewDestruct (Zeven_odd_dec z) as [H|H]. + Rewrite (Zeven_bit_value z H); Intros; Omega. + + Rewrite (Zodd_bit_value z H); Intros; Omega. +Save. + +End Z_BRIC_A_BRAC. + +Section COHERENT_VALUE. + +(* +On vérifie que dans l'intervalle de définition les fonctions sont +réciproques l'une de l'autre. +Elles utilisent les lemmes du bric-a-brac. +*) + +Lemma binary_to_Z_to_binary : (n:nat) (bv : (Bvector n)) + (Z_to_binary n (binary_value n bv))=bv. +Proof. + NewInduction bv as [|a n bv IHbv]. + Auto. + + Rewrite binary_value_Sn. + Rewrite Z_to_binary_Sn. + Rewrite IHbv; Trivial. + + Apply binary_value_pos. +Save. + +Lemma two_compl_to_Z_to_two_compl : (n:nat) (bv : (Bvector n)) (b:bool) + (Z_to_two_compl n (two_compl_value n (Bcons b n bv)))= + (Bcons b n bv). +Proof. + NewInduction bv as [|a n bv IHbv]; Intro b. + NewDestruct b; Auto. + + Rewrite two_compl_value_Sn. + Rewrite Z_to_two_compl_Sn. + Rewrite IHbv; Trivial. +Save. + +Lemma Z_to_binary_to_Z : (n:nat) (z : Z) + `z >= 0 `-> + `z < (two_power_nat n) `-> + (binary_value n (Z_to_binary n z))=z. +Proof. + NewInduction n as [|n IHn]. + Unfold two_power_nat shift_nat; Simpl; Intros; Omega. + + Intros; Rewrite Z_to_binary_Sn_z. + Rewrite binary_value_Sn. + Rewrite IHn. + Apply Z_div2_value; Auto. + + Apply Zdiv2_pos; Trivial. + + Apply Zdiv2_two_power_nat; Trivial. +Save. + +Lemma Z_to_two_compl_to_Z : (n:nat) (z : Z) + `z >= -(two_power_nat n) `-> + `z < (two_power_nat n) `-> + (two_compl_value n (Z_to_two_compl n z))=z. +Proof. + NewInduction n as [|n IHn]. + Unfold two_power_nat shift_nat; Simpl; Intros. + Assert `z=-1`\/`z=0`. Omega. +Intuition; Subst z; Trivial. + + Intros; Rewrite Z_to_two_compl_Sn_z. + Rewrite two_compl_value_Sn. + Rewrite IHn. + Generalize (Zmod2_twice z); Omega. + + Apply Zge_minus_two_power_nat_S; Auto. + + Apply Zlt_two_power_nat_S; Auto. +Save. + +End COHERENT_VALUE. + diff --git a/theories7/ZArith/Zbool.v b/theories7/ZArith/Zbool.v new file mode 100644 index 00000000..258a485d --- /dev/null +++ b/theories7/ZArith/Zbool.v @@ -0,0 +1,158 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* false | _ => true end. +Definition Zge_bool := + [x,y:Z]Cases `x ?= y` of INFERIEUR => false | _ => true end. +Definition Zlt_bool := + [x,y:Z]Cases `x ?= y` of INFERIEUR => true | _ => false end. +Definition Zgt_bool := + [x,y:Z]Cases ` x ?= y` of SUPERIEUR => true | _ => false 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. + +Lemma Zle_cases : (x,y:Z)if (Zle_bool x y) then `x<=y` else `x>y`. +Proof. +Intros x y; Unfold Zle_bool Zle Zgt. +Case (Zcompare x y); Auto; Discriminate. +Qed. + +Lemma Zlt_cases : (x,y:Z)if (Zlt_bool x y) then `x=y`. +Proof. +Intros x y; Unfold Zlt_bool Zlt Zge. +Case (Zcompare x y); Auto; Discriminate. +Qed. + +Lemma Zge_cases : (x,y:Z)if (Zge_bool x y) then `x>=y` else `xy` else `x<=y`. +Proof. +Intros x y; Unfold Zgt_bool Zgt Zle. +Case (Zcompare x y); Auto; Discriminate. +Qed. + +(** Lemmas on [Zle_bool] used in contrib/graphs *) + +Lemma Zle_bool_imp_le : (x,y:Z) (Zle_bool x y)=true -> (Zle x y). +Proof. + Unfold Zle_bool Zle. Intros x y. Unfold not. + Case (Zcompare x y); Intros; Discriminate. +Qed. + +Lemma Zle_imp_le_bool : (x,y:Z) (Zle x y) -> (Zle_bool x y)=true. +Proof. + Unfold Zle Zle_bool. Intros x y. Case (Zcompare x y); Trivial. Intro. Elim (H (refl_equal ? ?)). +Qed. + +Lemma Zle_bool_refl : (x:Z) (Zle_bool x x)=true. +Proof. + Intro. Apply Zle_imp_le_bool. Apply Zle_refl. Reflexivity. +Qed. + +Lemma Zle_bool_antisym : (x,y:Z) (Zle_bool x y)=true -> (Zle_bool y x)=true -> x=y. +Proof. + Intros. Apply Zle_antisym. Apply Zle_bool_imp_le. Assumption. + Apply Zle_bool_imp_le. Assumption. +Qed. + +Lemma Zle_bool_trans : (x,y,z:Z) (Zle_bool x y)=true -> (Zle_bool y z)=true -> (Zle_bool x z)=true. +Proof. + Intros x y z; Intros. Apply Zle_imp_le_bool. Apply Zle_trans with m:=y. Apply Zle_bool_imp_le. Assumption. + Apply Zle_bool_imp_le. Assumption. +Qed. + +Definition Zle_bool_total : (x,y:Z) {(Zle_bool x y)=true}+{(Zle_bool y x)=true}. +Proof. + Intros x y; Intros. Unfold Zle_bool. Cut (Zcompare x y)=SUPERIEUR<->(Zcompare y x)=INFERIEUR. + Case (Zcompare x y). Left . Reflexivity. + Left . Reflexivity. + Right . Rewrite (proj1 ? ? H (refl_equal ? ?)). Reflexivity. + Apply Zcompare_ANTISYM. +Defined. + +Lemma Zle_bool_plus_mono : (x,y,z,t:Z) (Zle_bool x y)=true -> (Zle_bool z t)=true -> + (Zle_bool (Zplus x z) (Zplus y t))=true. +Proof. + Intros. Apply Zle_imp_le_bool. Apply Zle_plus_plus. Apply Zle_bool_imp_le. Assumption. + Apply Zle_bool_imp_le. Assumption. +Qed. + +Lemma Zone_pos : (Zle_bool `1` `0`)=false. +Proof. + Reflexivity. +Qed. + +Lemma Zone_min_pos : (x:Z) (Zle_bool x `0`)=false -> (Zle_bool `1` x)=true. +Proof. + Intros x; Intros. Apply Zle_imp_le_bool. Change (Zle (Zs ZERO) x). Apply Zgt_le_S. Generalize H. + Unfold Zle_bool Zgt. Case (Zcompare x ZERO). Intro H0. Discriminate H0. + Intro H0. Discriminate H0. + Reflexivity. +Qed. + + + Lemma Zle_is_le_bool : (x,y:Z) (Zle x y) <-> (Zle_bool x y)=true. + Proof. + Intros. Split. Intro. Apply Zle_imp_le_bool. Assumption. + Intro. Apply Zle_bool_imp_le. Assumption. + Qed. + + Lemma Zge_is_le_bool : (x,y:Z) (Zge x y) <-> (Zle_bool y x)=true. + Proof. + Intros. Split. Intro. Apply Zle_imp_le_bool. Apply Zge_le. Assumption. + Intro. Apply Zle_ge. Apply Zle_bool_imp_le. Assumption. + Qed. + + Lemma Zlt_is_le_bool : (x,y:Z) (Zlt x y) <-> (Zle_bool x `y-1`)=true. + Proof. + Intros x y. Split. Intro. Apply Zle_imp_le_bool. Apply Zlt_n_Sm_le. Rewrite (Zs_pred y) in H. + Assumption. + Intro. Rewrite (Zs_pred y). Apply Zle_lt_n_Sm. Apply Zle_bool_imp_le. Assumption. + Qed. + + Lemma Zgt_is_le_bool : (x,y:Z) (Zgt x y) <-> (Zle_bool y `x-1`)=true. + Proof. + Intros x y. Apply iff_trans with `y < x`. Split. Exact (Zgt_lt x y). + Exact (Zlt_gt y x). + Exact (Zlt_is_le_bool y x). + Qed. + diff --git a/theories7/ZArith/Zcompare.v b/theories7/ZArith/Zcompare.v new file mode 100644 index 00000000..fd11ae9b --- /dev/null +++ b/theories7/ZArith/Zcompare.v @@ -0,0 +1,480 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* x = y. +Proof. +Intros x y; NewDestruct x as [|x'|x'];NewDestruct y as [|y'|y'];Simpl;Intro H; Reflexivity Orelse Try Discriminate H; [ + Rewrite (compare_convert_EGAL x' y' H); Reflexivity + | Rewrite (compare_convert_EGAL x' y'); [ + Reflexivity + | NewDestruct (compare x' y' EGAL); + Reflexivity Orelse Discriminate]]. +Qed. + +Lemma Zcompare_EGAL : (x,y:Z) (Zcompare x y) = EGAL <-> x = y. +Proof. +Intros x y;Split; Intro E; [ Apply Zcompare_EGAL_eq; Assumption + | Rewrite E; Apply Zcompare_x_x ]. +Qed. + +Lemma Zcompare_antisym : + (x,y:Z)(Op (Zcompare x y)) = (Zcompare y x). +Proof. +Intros x y; NewDestruct x; NewDestruct y; Simpl; + Reflexivity Orelse Discriminate H Orelse + Rewrite Pcompare_antisym; Reflexivity. +Qed. + +Lemma Zcompare_ANTISYM : + (x,y:Z) (Zcompare x y) = SUPERIEUR <-> (Zcompare y x) = INFERIEUR. +Proof. +Intros x y; Split; Intro H; [ + Change INFERIEUR with (Op SUPERIEUR); + Rewrite <- Zcompare_antisym; Rewrite H; Reflexivity +| Change SUPERIEUR with (Op INFERIEUR); + Rewrite <- Zcompare_antisym; Rewrite H; Reflexivity ]. +Qed. + +(** Transitivity of comparison *) + +Lemma 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 ]. +Qed. + +(** Comparison and opposite *) + +Lemma 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. +Qed. + +Hints Local Resolve convert_compare_EGAL. + +(** Comparison first-order specification *) + +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]. +Qed. + +(** Comparison and addition *) + +Lemma weaken_Zcompare_Zplus_compatible : + ((n,m:Z) (p:positive) + (Zcompare (Zplus (POS p) n) (Zplus (POS p) m)) = (Zcompare n m)) -> + (x,y,z:Z) (Zcompare (Zplus z x) (Zplus z y)) = (Zcompare x y). +Proof. +Intros H x y z; NewDestruct z; [ + Reflexivity +| Apply H +| Rewrite (Zcompare_Zopp x y); Rewrite Zcompare_Zopp; + Do 2 Rewrite Zopp_Zplus; Rewrite Zopp_NEG; Apply H ]. +Qed. + +Hints Local Resolve ZC4. + +Lemma 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;ElimPcompare z p;Intros E;Rewrite E;Auto with arith; + Apply convert_compare_SUPERIEUR; Rewrite true_sub_convert; [ Unfold gt ; + Apply ZL16 | Assumption ] +| Intros p;ElimPcompare z p; + Intros E;Auto with arith; Apply convert_compare_SUPERIEUR; + Unfold gt;Apply ZL17 +| Intros p q; + ElimPcompare q p; + 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; + ElimPcompare z p; + 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;ElimPcompare z p;Intros E;Rewrite E;Auto with arith; Simpl; + Apply convert_compare_INFERIEUR;Rewrite true_sub_convert;[Apply ZL16| + Assumption] +| Intros p q; + ElimPcompare z q; + 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; ElimPcompare z q; Intros E0;Rewrite E0; + ElimPcompare z p; Intros E1;Rewrite E1; ElimPcompare q p; + 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]]]. +Qed. + +Lemma 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). +Qed. + +Lemma 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. +Proof. +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]]. +Qed. + +Lemma Zcompare_Zs_SUPERIEUR : (x:Z)(Zcompare (Zs x) x)=SUPERIEUR. +Proof. +Intro x; Unfold Zs; Pattern 2 x; Rewrite <- (Zero_right x); +Rewrite Zcompare_Zplus_compatible;Reflexivity. +Qed. + +Lemma Zcompare_et_un: + (x,y:Z) (Zcompare x y)=SUPERIEUR <-> + ~(Zcompare x (Zplus y (POS xH)))=INFERIEUR. +Proof. +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 (Zcompare_Zs_SUPERIEUR 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 (Zcompare_Zs_SUPERIEUR y)]]]. +Qed. + +(** Successor and comparison *) + +Lemma Zcompare_n_S : (n,m:Z)(Zcompare (Zs n) (Zs m)) = (Zcompare n m). +Proof. +Intros n m;Unfold Zs ;Do 2 Rewrite -> [t:Z](Zplus_sym t (POS xH)); +Rewrite -> Zcompare_Zplus_compatible;Auto with arith. +Qed. + +(** Multiplication and comparison *) + +Lemma Zcompare_Zmult_compatible : + (x:positive)(y,z:Z) + (Zcompare (Zmult (POS x) y) (Zmult (POS x) z)) = (Zcompare y z). +Proof. +Intros x; NewInduction x as [p H|p H|]; [ + Intros 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 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]. +Qed. + + +(** Reverting [x ?= y] to trichotomy *) + +Lemma rename : (A:Set)(P:A->Prop)(x:A) ((y:A)(x=y)->(P y)) -> (P x). +Proof. +Auto with arith. +Qed. + +Lemma Zcompare_elim : + (c1,c2,c3:Prop)(x,y:Z) + ((x=y) -> c1) ->(`x c2) ->(`x>y`-> c3) + -> Cases (Zcompare x y) of EGAL => c1 | INFERIEUR => c2 | SUPERIEUR => c3 end. +Proof. +Intros c1 c2 c3 x y; Intros. +Apply rename with x:=(Zcompare x y); Intro r; Elim r; +[ Intro; Apply H; Apply (Zcompare_EGAL_eq x y); Assumption +| Unfold Zlt in H0; Assumption +| Unfold Zgt in H1; Assumption ]. +Qed. + +Lemma Zcompare_eq_case : + (c1,c2,c3:Prop)(x,y:Z) c1 -> x=y -> + Cases (Zcompare x y) of EGAL => c1 | INFERIEUR => c2 | SUPERIEUR => c3 end. +Proof. +Intros c1 c2 c3 x y; Intros. +Rewrite H0; Rewrite (Zcompare_x_x). +Assumption. +Qed. + +(** Decompose an egality between two [?=] relations into 3 implications *) + +Lemma Zcompare_egal_dec : + (x1,y1,x2,y2:Z) + (`x1`x2((Zcompare x1 y1)=EGAL -> (Zcompare x2 y2)=EGAL) + ->(`x1>y1`->`x2>y2`)->(Zcompare x1 y1)=(Zcompare x2 y2). +Proof. +Intros x1 y1 x2 y2. +Unfold Zgt; Unfold Zlt; +Case (Zcompare x1 y1); Case (Zcompare x2 y2); Auto with arith; Symmetry; Auto with arith. +Qed. + +(** Relating [x ?= y] to [Zle], [Zlt], [Zge] or [Zgt] *) + +Lemma Zle_Zcompare : + (x,y:Z)`x<=y` -> + Cases (Zcompare x y) of EGAL => True | INFERIEUR => True | SUPERIEUR => False end. +Proof. +Intros x y; Unfold Zle; Elim (Zcompare x y); Auto with arith. +Qed. + +Lemma Zlt_Zcompare : + (x,y:Z)`x + Cases (Zcompare x y) of EGAL => False | INFERIEUR => True | SUPERIEUR => False end. +Proof. +Intros x y; Unfold Zlt; Elim (Zcompare x y); Intros; Discriminate Orelse Trivial with arith. +Qed. + +Lemma Zge_Zcompare : + (x,y:Z)`x>=y`-> + Cases (Zcompare x y) of EGAL => True | INFERIEUR => False | SUPERIEUR => True end. +Proof. +Intros x y; Unfold Zge; Elim (Zcompare x y); Auto with arith. +Qed. + +Lemma Zgt_Zcompare : + (x,y:Z)`x>y` -> + Cases (Zcompare x y) of EGAL => False | INFERIEUR => False | SUPERIEUR => True end. +Proof. +Intros x y; Unfold Zgt; Elim (Zcompare x y); Intros; Discriminate Orelse Trivial with arith. +Qed. + +(**********************************************************************) +(* Other properties *) + +V7only [Set Implicit Arguments.]. + +Lemma Zcompare_Zmult_left : (x,y,z:Z)`z>0` -> `x ?= y`=`z*x ?= z*y`. +Proof. +Intros x y z H; NewDestruct z. + Discriminate H. + Rewrite Zcompare_Zmult_compatible; Reflexivity. + Discriminate H. +Qed. + +Lemma Zcompare_Zmult_right : (x,y,z:Z)` z>0` -> `x ?= y`=`x*z ?= y*z`. +Proof. +Intros x y z H; +Rewrite (Zmult_sym x z); +Rewrite (Zmult_sym y z); +Apply Zcompare_Zmult_left; Assumption. +Qed. + +V7only [Unset Implicit Arguments.]. + diff --git a/theories7/ZArith/Zcomplements.v b/theories7/ZArith/Zcomplements.v new file mode 100644 index 00000000..72d837b6 --- /dev/null +++ b/theories7/ZArith/Zcomplements.v @@ -0,0 +1,212 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* xH + | (xO a') => (xO (floor_pos a')) + | (xI b') => (xO (floor_pos b')) + end. + +Definition floor := [a:positive](POS (floor_pos a)). + +Lemma floor_gt0 : (x:positive) `(floor x) > 0`. +Proof. +Intro. +Compute. +Trivial. +Qed. + +Lemma floor_ok : (a:positive) + `(floor a) <= (POS a) < 2*(floor a)`. +Proof. +Unfold floor. +Intro a; NewInduction a as [p|p|]. + +Simpl. +Repeat Rewrite POS_xI. +Rewrite (POS_xO (xO (floor_pos p))). +Rewrite (POS_xO (floor_pos p)). +Omega. + +Simpl. +Repeat Rewrite POS_xI. +Rewrite (POS_xO (xO (floor_pos p))). +Rewrite (POS_xO (floor_pos p)). +Rewrite (POS_xO p). +Omega. + +Simpl; Omega. +Qed. + +(**********************************************************************) +(** Two more induction principles over [Z]. *) + +Theorem Z_lt_abs_rec : (P: Z -> Set) + ((n: Z) ((m: Z) `|m|<|n|` -> (P m)) -> (P n)) -> (p: Z) (P p). +Proof. +Intros P HP p. +LetTac Q:=[z]`0<=z`->(P z)*(P `-z`). +Cut (Q `|p|`);[Intros|Apply (Z_lt_rec Q);Auto with zarith]. +Elim (Zabs_dec p);Intro eq;Rewrite eq;Elim H;Auto with zarith. +Unfold Q;Clear Q;Intros. +Apply pair;Apply HP. +Rewrite Zabs_eq;Auto;Intros. +Elim (H `|m|`);Intros;Auto with zarith. +Elim (Zabs_dec m);Intro eq;Rewrite eq;Trivial. +Rewrite Zabs_non_eq;Auto with zarith. +Rewrite Zopp_Zopp;Intros. +Elim (H `|m|`);Intros;Auto with zarith. +Elim (Zabs_dec m);Intro eq;Rewrite eq;Trivial. +Qed. + +Theorem Z_lt_abs_induction : (P: Z -> Prop) + ((n: Z) ((m: Z) `|m|<|n|` -> (P m)) -> (P n)) -> (p: Z) (P p). +Proof. +Intros P HP p. +LetTac Q:=[z]`0<=z`->(P z) /\ (P `-z`). +Cut (Q `|p|`);[Intros|Apply (Z_lt_induction Q);Auto with zarith]. +Elim (Zabs_dec p);Intro eq;Rewrite eq;Elim H;Auto with zarith. +Unfold Q;Clear Q;Intros. +Split;Apply HP. +Rewrite Zabs_eq;Auto;Intros. +Elim (H `|m|`);Intros;Auto with zarith. +Elim (Zabs_dec m);Intro eq;Rewrite eq;Trivial. +Rewrite Zabs_non_eq;Auto with zarith. +Rewrite Zopp_Zopp;Intros. +Elim (H `|m|`);Intros;Auto with zarith. +Elim (Zabs_dec m);Intro eq;Rewrite eq;Trivial. +Qed. +V7only [Unset Implicit Arguments.]. + +(** To do case analysis over the sign of [z] *) + +Lemma Zcase_sign : (x:Z)(P:Prop) + (`x=0` -> P) -> + (`x>0` -> P) -> + (`x<0` -> P) -> P. +Proof. +Intros x P Hzero Hpos Hneg. +Induction x. +Apply Hzero; Trivial. +Apply Hpos; Apply POS_gt_ZERO. +Apply Hneg; Apply NEG_lt_ZERO. +Save. + +Lemma sqr_pos : (x:Z)`x*x >= 0`. +Proof. +Intro x. +Apply (Zcase_sign x `x*x >= 0`). +Intros H; Rewrite H; Omega. +Intros H; Replace `0` with `0*0`. +Apply Zge_Zmult_pos_compat; Omega. +Omega. +Intros H; Replace `0` with `0*0`. +Replace `x*x` with `(-x)*(-x)`. +Apply Zge_Zmult_pos_compat; Omega. +Ring. +Omega. +Save. + +(**********************************************************************) +(** A list length in Z, tail recursive. *) + +Require PolyList. + +Fixpoint Zlength_aux [acc: Z; A:Set; l:(list A)] : Z := Cases l of + nil => acc + | (cons _ l) => (Zlength_aux (Zs acc) A l) +end. + +Definition Zlength := (Zlength_aux 0). +Implicits Zlength [1]. + +Section Zlength_properties. + +Variable A:Set. + +Implicit Variable Type l:(list A). + +Lemma Zlength_correct : (l:(list A))(Zlength l)=(inject_nat (length l)). +Proof. +Assert (l:(list A))(acc:Z)(Zlength_aux acc A l)=acc+(inject_nat (length l)). +Induction l. +Simpl; Auto with zarith. +Intros; Simpl (length (cons a l0)); Rewrite inj_S. +Simpl; Rewrite H; Auto with zarith. +Unfold Zlength; Intros; Rewrite H; Auto. +Qed. + +Lemma Zlength_nil : (Zlength 1!A (nil A))=0. +Proof. +Auto. +Qed. + +Lemma Zlength_cons : (x:A)(l:(list A))(Zlength (cons x l))=(Zs (Zlength l)). +Proof. +Intros; Do 2 Rewrite Zlength_correct. +Simpl (length (cons x l)); Rewrite inj_S; Auto. +Qed. + +Lemma Zlength_nil_inv : (l:(list A))(Zlength l)=0 -> l=(nil ?). +Proof. +Intro l; Rewrite Zlength_correct. +Case l; Auto. +Intros x l'; Simpl (length (cons x l')). +Rewrite inj_S. +Intros; ElimType False; Generalize (ZERO_le_inj (length l')); Omega. +Qed. + +End Zlength_properties. + +Implicits Zlength_correct [1]. +Implicits Zlength_cons [1]. +Implicits Zlength_nil_inv [1]. diff --git a/theories7/ZArith/Zdiv.v b/theories7/ZArith/Zdiv.v new file mode 100644 index 00000000..84d53931 --- /dev/null +++ b/theories7/ZArith/Zdiv.v @@ -0,0 +1,432 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Z*Z := [b:Z] + Cases a of + | xH => if `(Zge_bool b 2)` then `(0,1)` else `(1,0)` + | (xO a') => + let (q,r) = (Zdiv_eucl_POS a' b) in + [r':=`2*r`] if `(Zgt_bool b r')` then `(2*q,r')` else `(2*q+1,r'-b)` + | (xI a') => + let (q,r) = (Zdiv_eucl_POS a' b) in + [r':=`2*r+1`] if `(Zgt_bool b r')` then `(2*q,r')` else `(2*q+1,r'-b)` + end. + + +(** + + Euclidean division of integers. + + Total function than returns (0,0) when dividing by 0. + +*) + +(* + + The pseudo-code is: + + if b = 0 : (0,0) + + if b <> 0 and a = 0 : (0,0) + + if b > 0 and a < 0 : let (q,r) = div_eucl_pos (-a) b in + if r = 0 then (-q,0) else (-(q+1),b-r) + + if b < 0 and a < 0 : let (q,r) = div_eucl (-a) (-b) in (q,-r) + + if b < 0 and a > 0 : let (q,r) = div_eucl a (-b) in + if r = 0 then (-q,0) else (-(q+1),b+r) + + In other word, when b is non-zero, q is chosen to be the greatest integer + smaller or equal to a/b. And sgn(r)=sgn(b) and |r| < |b|. + +*) + +Definition Zdiv_eucl [a,b:Z] : Z*Z := + Cases a b of + | ZERO _ => `(0,0)` + | _ ZERO => `(0,0)` + | (POS a') (POS _) => (Zdiv_eucl_POS a' b) + | (NEG a') (POS _) => + let (q,r) = (Zdiv_eucl_POS a' b) in + Cases r of + | ZERO => `(-q,0)` + | _ => `(-(q+1),b-r)` + end + | (NEG a') (NEG b') => + let (q,r) = (Zdiv_eucl_POS a' (POS b')) in `(q,-r)` + | (POS a') (NEG b') => + let (q,r) = (Zdiv_eucl_POS a' (POS b')) in + Cases r of + | ZERO => `(-q,0)` + | _ => `(-(q+1),b+r)` + end + end. + + +(** Division and modulo are projections of [Zdiv_eucl] *) + +Definition Zdiv [a,b:Z] : Z := let (q,_) = (Zdiv_eucl a b) in q. + +Definition Zmod [a,b:Z] : Z := let (_,r) = (Zdiv_eucl a b) in r. + +(* Tests: + +Eval Compute in `(Zdiv_eucl 7 3)`. + +Eval Compute in `(Zdiv_eucl (-7) 3)`. + +Eval Compute in `(Zdiv_eucl 7 (-3))`. + +Eval Compute in `(Zdiv_eucl (-7) (-3))`. + +*) + + +(** + + Main division theorem. + + First a lemma for positive + +*) + +Lemma Z_div_mod_POS : (b:Z)`b > 0` -> (a:positive) + let (q,r)=(Zdiv_eucl_POS a b) in `(POS a) = b*q + r`/\`0<=r 0` -> + let (q,r) = (Zdiv_eucl a b) in `a = b*q + r` /\ `0<=r 0` -> (a:Z) + { qr:Z*Z | let (q,r)=qr in `a=b*q+r` /\ `0 <= r < b` }. +Proof. +Intros b Hb a. +Exists (Zdiv_eucl a b). +Exact (Z_div_mod a b Hb). +Qed. + +Implicits Zdiv_eucl_exist. + +Theorem Zdiv_eucl_extended : (b:Z)`b <> 0` -> (a:Z) + { qr:Z*Z | let (q,r)=qr in `a=b*q+r` /\ `0 <= r < |b|` }. +Proof. +Intros b Hb a. +Elim (Z_le_gt_dec `0` b);Intro Hb'. +Cut `b>0`;[Intro Hb''|Omega]. +Rewrite Zabs_eq;[Apply Zdiv_eucl_exist;Assumption|Assumption]. +Cut `-b>0`;[Intro Hb''|Omega]. +Elim (Zdiv_eucl_exist Hb'' a);Intros qr. +Elim qr;Intros q r Hqr. +Exists (pair ? ? `-q` r). +Elim Hqr;Intros. +Split. +Rewrite <- Zmult_Zopp_left;Assumption. +Rewrite Zabs_non_eq;[Assumption|Omega]. +Qed. + +Implicits Zdiv_eucl_extended. + +(** Auxiliary lemmas about [Zdiv] and [Zmod] *) + +Lemma Z_div_mod_eq : (a,b:Z)`b > 0` -> `a = b * (Zdiv a b) + (Zmod a b)`. +Proof. +Unfold Zdiv Zmod. +Intros a b Hb. +Generalize (Z_div_mod a b Hb). +Case (Zdiv_eucl); Tauto. +Save. + +Lemma Z_mod_lt : (a,b:Z)`b > 0` -> `0 <= (Zmod a b) < b`. +Proof. +Unfold Zmod. +Intros a b Hb. +Generalize (Z_div_mod a b Hb). +Case (Zdiv_eucl a b); Tauto. +Save. + +Lemma Z_div_POS_ge0 : (b:Z)(a:positive) + let (q,_) = (Zdiv_eucl_POS a b) in `q >= 0`. +Proof. +Induction a; Unfold Zdiv_eucl_POS; Fold Zdiv_eucl_POS. +Intro p; Case (Zdiv_eucl_POS p b). +Intros; Case (Zgt_bool b `2*z0+1`); Intros; Omega. +Intro p; Case (Zdiv_eucl_POS p b). +Intros; Case (Zgt_bool b `2*z0`); Intros; Omega. +Case (Zge_bool b `2`); Simpl; Omega. +Save. + +Lemma Z_div_ge0 : (a,b:Z)`b > 0` -> `a >= 0` -> `(Zdiv a b) >= 0`. +Proof. +Intros a b Hb; Unfold Zdiv Zdiv_eucl; Case a; Simpl; Intros. +Case b; Simpl; Trivial. +Generalize Hb; Case b; Try Trivial. +Auto with zarith. +Intros p0 Hp0; Generalize (Z_div_POS_ge0 (POS p0) p). +Case (Zdiv_eucl_POS p (POS p0)); Simpl; Tauto. +Intros; Discriminate. +Elim H; Trivial. +Save. + +Lemma Z_div_lt : (a,b:Z)`b >= 2` -> `a > 0` -> `(Zdiv a b) < a`. +Proof. +Intros. Cut `b > 0`; [Intro Hb | Omega]. +Generalize (Z_div_mod a b Hb). +Cut `a >= 0`; [Intro Ha | Omega]. +Generalize (Z_div_ge0 a b Hb Ha). +Unfold Zdiv; Case (Zdiv_eucl a b); Intros q r H1 [H2 H3]. +Cut `a >= 2*q` -> `q < a`; [ Intro h; Apply h; Clear h | Intros; Omega ]. +Apply Zge_trans with `b*q`. +Omega. +Auto with zarith. +Save. + +(** Syntax *) + +V7only[ +Grammar znatural expr2 : constr := + expr_div [ expr2($p) "/" expr2($c) ] -> [ (Zdiv $p $c) ] +| expr_mod [ expr2($p) "%" expr2($c) ] -> [ (Zmod $p $c) ] +. + +Syntax constr + level 6: + Zdiv [ (Zdiv $n1 $n2) ] + -> [ [ "`"(ZEXPR $n1):E "/" [0 0] (ZEXPR $n2):L "`"] ] + | Zmod [ (Zmod $n1 $n2) ] + -> [ [ "`"(ZEXPR $n1):E "%" [0 0] (ZEXPR $n2):L "`"] ] + | Zdiv_inside + [ << (ZEXPR <<(Zdiv $n1 $n2)>>) >> ] + -> [ (ZEXPR $n1):E "/" [0 0] (ZEXPR $n2):L ] + | Zmod_inside + [ << (ZEXPR <<(Zmod $n1 $n2)>>) >> ] + -> [ (ZEXPR $n1):E " %" [1 0] (ZEXPR $n2):L ] +. +]. + + +Infix 3 "/" Zdiv (no associativity) : Z_scope V8only. +Infix 3 "mod" Zmod (no associativity) : Z_scope. + +(** Other lemmas (now using the syntax for [Zdiv] and [Zmod]). *) + +Lemma Z_div_ge : (a,b,c:Z)`c > 0`->`a >= b`->`a/c >= b/c`. +Proof. +Intros a b c cPos aGeb. +Generalize (Z_div_mod_eq a c cPos). +Generalize (Z_mod_lt a c cPos). +Generalize (Z_div_mod_eq b c cPos). +Generalize (Z_mod_lt b c cPos). +Intros. +Elim (Z_ge_lt_dec `a/c` `b/c`); Trivial. +Intro. +Absurd `b-a >= 1`. +Omega. +Rewrite -> H0. +Rewrite -> H2. +Assert `c*(b/c)+b % c-(c*(a/c)+a % c) = c*(b/c - a/c) + b % c - a % c`. +Ring. +Rewrite H3. +Assert `c*(b/c-a/c) >= c*1`. +Apply Zge_Zmult_pos_left. +Omega. +Omega. +Assert `c*1=c`. +Ring. +Omega. +Save. + +Lemma Z_mod_plus : (a,b,c:Z)`c > 0`->`(a+b*c) % c = a % c`. +Proof. +Intros a b c cPos. +Generalize (Z_div_mod_eq a c cPos). +Generalize (Z_mod_lt a c cPos). +Generalize (Z_div_mod_eq `a+b*c` c cPos). +Generalize (Z_mod_lt `a+b*c` c cPos). +Intros. + +Assert `(a+b*c) % c - a % c = c*(b+a/c - (a+b*c)/c)`. +Replace `(a+b*c) % c` with `a+b*c - c*((a+b*c)/c)`. +Replace `a % c` with `a - c*(a/c)`. +Ring. +Omega. +Omega. +LetTac q := `b+a/c-(a+b*c)/c`. +Apply (Zcase_sign q); Intros. +Assert `c*q=0`. +Rewrite H4; Ring. +Rewrite H5 in H3. +Omega. + +Assert `c*q >= c`. +Pattern 2 c; Replace c with `c*1`. +Apply Zge_Zmult_pos_left; Omega. +Ring. +Omega. + +Assert `c*q <= -c`. +Replace `-c` with `c*(-1)`. +Apply Zle_Zmult_pos_left; Omega. +Ring. +Omega. +Save. + +Lemma Z_div_plus : (a,b,c:Z)`c > 0`->`(a+b*c)/c = a/c+b`. +Proof. +Intros a b c cPos. +Generalize (Z_div_mod_eq a c cPos). +Generalize (Z_mod_lt a c cPos). +Generalize (Z_div_mod_eq `a+b*c` c cPos). +Generalize (Z_mod_lt `a+b*c` c cPos). +Intros. +Apply Zmult_reg_left with c. Omega. +Replace `c*((a+b*c)/c)` with `a+b*c-(a+b*c) % c`. +Rewrite (Z_mod_plus a b c cPos). +Pattern 1 a; Rewrite H2. +Ring. +Pattern 1 `a+b*c`; Rewrite H0. +Ring. +Save. + +Lemma Z_div_mult : (a,b:Z)`b > 0`->`(a*b)/b = a`. +Intros; Replace `a*b` with `0+a*b`; Auto. +Rewrite Z_div_plus; Auto. +Save. + +Lemma Z_mult_div_ge : (a,b:Z)`b>0`->`b*(a/b) <= a`. +Proof. +Intros a b bPos. +Generalize (Z_div_mod_eq `a` ? bPos); Intros. +Generalize (Z_mod_lt `a` ? bPos); Intros. +Pattern 2 a; Rewrite H. +Omega. +Save. + +Lemma Z_mod_same : (a:Z)`a>0`->`a % a=0`. +Proof. +Intros a aPos. +Generalize (Z_mod_plus `0` `1` a aPos). +Replace `0+1*a` with `a`. +Intros. +Rewrite H. +Compute. +Trivial. +Ring. +Save. + +Lemma Z_div_same : (a:Z)`a>0`->`a/a=1`. +Proof. +Intros a aPos. +Generalize (Z_div_plus `0` `1` a aPos). +Replace `0+1*a` with `a`. +Intros. +Rewrite H. +Compute. +Trivial. +Ring. +Save. + +Lemma Z_div_exact_1 : (a,b:Z)`b>0` -> `a = b*(a/b)` -> `a%b = 0`. +Intros a b Hb; Generalize (Z_div_mod a b Hb); Unfold Zmod Zdiv. +Case (Zdiv_eucl a b); Intros q r; Omega. +Save. + +Lemma Z_div_exact_2 : (a,b:Z)`b>0` -> `a%b = 0` -> `a = b*(a/b)`. +Intros a b Hb; Generalize (Z_div_mod a b Hb); Unfold Zmod Zdiv. +Case (Zdiv_eucl a b); Intros q r; Omega. +Save. + +Lemma Z_mod_zero_opp : (a,b:Z)`b>0` -> `a%b = 0` -> `(-a)%b = 0`. +Intros a b Hb. +Intros. +Rewrite Z_div_exact_2 with a b; Auto. +Replace `-(b*(a/b))` with `0+(-(a/b))*b`. +Rewrite Z_mod_plus; Auto. +Ring. +Save. + diff --git a/theories7/ZArith/Zeven.v b/theories7/ZArith/Zeven.v new file mode 100644 index 00000000..04b3ec09 --- /dev/null +++ b/theories7/ZArith/Zeven.v @@ -0,0 +1,184 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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. + +Definition 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) ]. +Defined. + +Definition 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) ]. +Defined. + +Definition 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) ]. +Defined. + +Lemma Zeven_not_Zodd : (z:Z)(Zeven z) -> ~(Zodd z). +Proof. + Intro z; NewDestruct z; [ Idtac | NewDestruct p | NewDestruct p ]; Compute; Trivial. +Qed. + +Lemma Zodd_not_Zeven : (z:Z)(Zodd z) -> ~(Zeven z). +Proof. + Intro z; NewDestruct z; [ Idtac | NewDestruct p | NewDestruct p ]; Compute; Trivial. +Qed. + +Lemma Zeven_Sn : (z:Z)(Zodd z) -> (Zeven (Zs z)). +Proof. + Intro z; NewDestruct z; Unfold Zs; [ Idtac | NewDestruct p | NewDestruct p ]; Simpl; Trivial. + Unfold double_moins_un; Case p; Simpl; Auto. +Qed. + +Lemma Zodd_Sn : (z:Z)(Zeven z) -> (Zodd (Zs z)). +Proof. + Intro z; NewDestruct z; Unfold Zs; [ Idtac | NewDestruct p | NewDestruct p ]; Simpl; Trivial. + Unfold double_moins_un; Case p; Simpl; Auto. +Qed. + +Lemma Zeven_pred : (z:Z)(Zodd z) -> (Zeven (Zpred z)). +Proof. + Intro z; NewDestruct z; Unfold Zpred; [ Idtac | NewDestruct p | NewDestruct p ]; Simpl; Trivial. + Unfold double_moins_un; Case p; Simpl; Auto. +Qed. + +Lemma Zodd_pred : (z:Z)(Zeven z) -> (Zodd (Zpred z)). +Proof. + Intro z; NewDestruct z; Unfold Zpred; [ Idtac | NewDestruct p | NewDestruct p ]; Simpl; Trivial. + Unfold double_moins_un; Case p; Simpl; Auto. +Qed. + +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 := + [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. +Intro x; NewDestruct x. +Auto with arith. +NewDestruct p; Auto with arith. +Intros. Absurd (Zeven (POS (xI p))); Red; Auto with arith. +Intros. Absurd (Zeven `1`); Red; Auto with arith. +NewDestruct p; Auto with arith. +Intros. Absurd (Zeven (NEG (xI p))); Red; Auto with arith. +Intros. Absurd (Zeven `-1`); Red; Auto with arith. +Qed. + +Lemma Zodd_div2 : (x:Z) `x >= 0` -> (Zodd x) -> `x = 2*(Zdiv2 x)+1`. +Proof. +Intro x; NewDestruct x. +Intros. Absurd (Zodd `0`); Red; Auto with arith. +NewDestruct p; Auto with arith. +Intros. Absurd (Zodd (POS (xO p))); Red; Auto with arith. +Intros. Absurd `(NEG p) >= 0`; Red; Auto with arith. +Qed. + +Lemma Zodd_div2_neg : (x:Z) `x <= 0` -> (Zodd x) -> `x = 2*(Zdiv2 x)-1`. +Proof. +Intro x; NewDestruct x. +Intros. Absurd (Zodd `0`); Red; Auto with arith. +Intros. Absurd `(NEG p) >= 0`; Red; Auto with arith. +NewDestruct p; Auto with arith. +Intros. Absurd (Zodd (NEG (xO p))); Red; Auto with arith. +Qed. + +Lemma Z_modulo_2 : (x:Z) { y:Z | `x=2*y` }+{ y:Z | `x=2*y+1` }. +Proof. +Intros x. +Elim (Zeven_odd_dec x); Intro. +Left. Split with (Zdiv2 x). Exact (Zeven_div2 x a). +Right. Generalize b; Clear b; Case x. +Intro b; Inversion b. +Intro p; Split with (Zdiv2 (POS p)). Apply (Zodd_div2 (POS p)); Trivial. +Unfold Zge Zcompare; Simpl; Discriminate. +Intro p; Split with (Zdiv2 (Zpred (NEG p))). +Pattern 1 (NEG p); Rewrite (Zs_pred (NEG p)). +Pattern 1 (Zpred (NEG p)); Rewrite (Zeven_div2 (Zpred (NEG p))). +Reflexivity. +Apply Zeven_pred; Assumption. +Qed. + +Lemma Zsplit2 : (x:Z) { p : Z*Z | let (x1,x2)=p in (`x=x1+x2` /\ (x1=x2 \/ `x2=x1+1`)) }. +Proof. +Intros x. +Elim (Z_modulo_2 x); Intros (y,Hy); Rewrite Zmult_sym in Hy; Rewrite <- Zplus_Zmult_2 in Hy. +Exists (y,y); Split. +Assumption. +Left; Reflexivity. +Exists (y,`y+1`); Split. +Rewrite Zplus_assoc; Assumption. +Right; Reflexivity. +Qed. diff --git a/theories7/ZArith/Zhints.v b/theories7/ZArith/Zhints.v new file mode 100644 index 00000000..01860d18 --- /dev/null +++ b/theories7/ZArith/Zhints.v @@ -0,0 +1,387 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* `(Zs n) = (Zs m)` *) + + (* Lemmas ending by Zgt *) + Zgt_n_S (* :(n,m:Z)`m > n`->`(Zs m) > (Zs n)` *) + Zgt_Sn_n (* :(n:Z)`(Zs n) > n` *) + POS_gt_ZERO (* :(p:positive)`(POS p) > 0` *) + Zgt_reg_l (* :(n,m,p:Z)`n > m`->`p+n > p+m` *) + Zgt_reg_r (* :(n,m,p:Z)`n > m`->`n+p > m+p` *) + + (* Lemmas ending by Zlt *) + Zlt_n_Sn (* :(n:Z)`n < (Zs n)` *) + Zlt_n_S (* :(n,m:Z)`n < m`->`(Zs n) < (Zs m)` *) + Zlt_pred_n_n (* :(n:Z)`(Zpred n) < n` *) + Zlt_reg_l (* :(n,m,p:Z)`n < m`->`p+n < p+m` *) + Zlt_reg_r (* :(n,m,p:Z)`n < m`->`n+p < m+p` *) + + (* Lemmas ending by Zle *) + ZERO_le_inj (* :(n:nat)`0 <= (inject_nat n)` *) + ZERO_le_POS (* :(p:positive)`0 <= (POS p)` *) + Zle_n (* :(n:Z)`n <= n` *) + Zle_n_Sn (* :(n:Z)`n <= (Zs n)` *) + Zle_n_S (* :(n,m:Z)`m <= n`->`(Zs m) <= (Zs n)` *) + Zle_pred_n (* :(n:Z)`(Zpred n) <= n` *) + Zle_min_l (* :(n,m:Z)`(Zmin n m) <= n` *) + Zle_min_r (* :(n,m:Z)`(Zmin n m) <= m` *) + Zle_reg_l (* :(n,m,p:Z)`n <= m`->`p+n <= p+m` *) + Zle_reg_r (* :(a,b,c:Z)`a <= b`->`a+c <= b+c` *) + Zabs_pos (* :(x:Z)`0 <= |x|` *) + + (* B) Irreversible simplification lemmas : Probably to be declared as *) + (* hints, when no other simplification is possible *) + + (* Lemmas ending by eq *) + Z_eq_mult (* :(x,y:Z)`y = 0`->`y*x = 0` *) + Zplus_simpl (* :(n,m,p,q:Z)`n = m`->`p = q`->`n+p = m+q` *) + + (* Lemmas ending by Zge *) + Zge_Zmult_pos_right (* :(a,b,c:Z)`a >= b`->`c >= 0`->`a*c >= b*c` *) + Zge_Zmult_pos_left (* :(a,b,c:Z)`a >= b`->`c >= 0`->`c*a >= c*b` *) + Zge_Zmult_pos_compat (* : + (a,b,c,d:Z)`a >= c`->`b >= d`->`c >= 0`->`d >= 0`->`a*b >= c*d` *) + + (* Lemmas ending by Zlt *) + Zgt_ZERO_mult (* :(a,b:Z)`a > 0`->`b > 0`->`a*b > 0` *) + Zlt_S (* :(n,m:Z)`n < m`->`n < (Zs m)` *) + + (* Lemmas ending by Zle *) + Zle_ZERO_mult (* :(x,y:Z)`0 <= x`->`0 <= y`->`0 <= x*y` *) + Zle_Zmult_pos_right (* :(a,b,c:Z)`a <= b`->`0 <= c`->`a*c <= b*c` *) + Zle_Zmult_pos_left (* :(a,b,c:Z)`a <= b`->`0 <= c`->`c*a <= c*b` *) + OMEGA2 (* :(x,y:Z)`0 <= x`->`0 <= y`->`0 <= x+y` *) + Zle_le_S (* :(x,y:Z)`x <= y`->`x <= (Zs y)` *) + Zle_plus_plus (* :(n,m,p,q:Z)`n <= m`->`p <= q`->`n+p <= m+q` *) + +: zarith. + +(**********************************************************************) +(* Reversible lemmas relating operators *) +(* Probably to be declared as hints but need to define precedences *) + +(* A) Conversion between comparisons/predicates and arithmetic operators + +(* Lemmas ending by eq *) +Zegal_left: (x,y:Z)`x = y`->`x+(-y) = 0` +Zabs_eq: (x:Z)`0 <= x`->`|x| = x` +Zeven_div2: (x:Z)(Zeven x)->`x = 2*(Zdiv2 x)` +Zodd_div2: (x:Z)`x >= 0`->(Zodd x)->`x = 2*(Zdiv2 x)+1` + +(* Lemmas ending by Zgt *) +Zgt_left_rev: (x,y:Z)`x+(-y) > 0`->`x > y` +Zgt_left_gt: (x,y:Z)`x > y`->`x+(-y) > 0` + +(* Lemmas ending by Zlt *) +Zlt_left_rev: (x,y:Z)`0 < y+(-x)`->`x < y` +Zlt_left_lt: (x,y:Z)`x < y`->`0 < y+(-x)` +Zlt_O_minus_lt: (n,m:Z)`0 < n-m`->`m < n` + +(* Lemmas ending by Zle *) +Zle_left: (x,y:Z)`x <= y`->`0 <= y+(-x)` +Zle_left_rev: (x,y:Z)`0 <= y+(-x)`->`x <= y` +Zlt_left: (x,y:Z)`x < y`->`0 <= y+(-1)+(-x)` +Zge_left: (x,y:Z)`x >= y`->`0 <= x+(-y)` +Zgt_left: (x,y:Z)`x > y`->`0 <= x+(-1)+(-y)` + +(* B) Conversion between nat comparisons and Z comparisons *) + +(* Lemmas ending by eq *) +inj_eq: (x,y:nat)x=y->`(inject_nat x) = (inject_nat y)` + +(* Lemmas ending by Zge *) +inj_ge: (x,y:nat)(ge x y)->`(inject_nat x) >= (inject_nat y)` + +(* Lemmas ending by Zgt *) +inj_gt: (x,y:nat)(gt x y)->`(inject_nat x) > (inject_nat y)` + +(* Lemmas ending by Zlt *) +inj_lt: (x,y:nat)(lt x y)->`(inject_nat x) < (inject_nat y)` + +(* Lemmas ending by Zle *) +inj_le: (x,y:nat)(le x y)->`(inject_nat x) <= (inject_nat y)` + +(* C) Conversion between comparisons *) + +(* Lemmas ending by Zge *) +not_Zlt: (x,y:Z)~`x < y`->`x >= y` +Zle_ge: (m,n:Z)`m <= n`->`n >= m` + +(* Lemmas ending by Zgt *) +Zle_gt_S: (n,p:Z)`n <= p`->`(Zs p) > n` +not_Zle: (x,y:Z)~`x <= y`->`x > y` +Zlt_gt: (m,n:Z)`m < n`->`n > m` +Zle_S_gt: (n,m:Z)`(Zs n) <= m`->`m > n` + +(* Lemmas ending by Zlt *) +not_Zge: (x,y:Z)~`x >= y`->`x < y` +Zgt_lt: (m,n:Z)`m > n`->`n < m` +Zle_lt_n_Sm: (n,m:Z)`n <= m`->`n < (Zs m)` + +(* Lemmas ending by Zle *) +Zlt_ZERO_pred_le_ZERO: (x:Z)`0 < x`->`0 <= (Zpred x)` +not_Zgt: (x,y:Z)~`x > y`->`x <= y` +Zgt_le_S: (n,p:Z)`p > n`->`(Zs n) <= p` +Zgt_S_le: (n,p:Z)`(Zs p) > n`->`n <= p` +Zge_le: (m,n:Z)`m >= n`->`n <= m` +Zlt_le_S: (n,p:Z)`n < p`->`(Zs n) <= p` +Zlt_n_Sm_le: (n,m:Z)`n < (Zs m)`->`n <= m` +Zlt_le_weak: (n,m:Z)`n < m`->`n <= m` +Zle_refl: (n,m:Z)`n = m`->`n <= m` + +(* D) Irreversible simplification involving several comparaisons, *) +(* useful with clear precedences *) + +(* Lemmas ending by Zlt *) +Zlt_le_reg :(a,b,c,d:Z)`a < b`->`c <= d`->`a+c < b+d` +Zle_lt_reg : (a,b,c,d:Z)`a <= b`->`c < d`->`a+c < b+d` + +(* D) What is decreasing here ? *) + +(* Lemmas ending by eq *) +Zplus_minus: (n,m,p:Z)`n = m+p`->`p = n-m` + +(* Lemmas ending by Zgt *) +Zgt_pred: (n,p:Z)`p > (Zs n)`->`(Zpred p) > n` + +(* Lemmas ending by Zlt *) +Zlt_pred: (n,p:Z)`(Zs n) < p`->`n < (Zpred p)` + +*) + +(**********************************************************************) +(* Useful Bottom-up lemmas *) + +(* A) Bottom-up simplification: should be used + +(* Lemmas ending by eq *) +Zeq_add_S: (n,m:Z)`(Zs n) = (Zs m)`->`n = m` +Zsimpl_plus_l: (n,m,p:Z)`n+m = n+p`->`m = p` +Zplus_unit_left: (n,m:Z)`n+0 = m`->`n = m` +Zplus_unit_right: (n,m:Z)`n = m+0`->`n = m` + +(* Lemmas ending by Zgt *) +Zsimpl_gt_plus_l: (n,m,p:Z)`p+n > p+m`->`n > m` +Zsimpl_gt_plus_r: (n,m,p:Z)`n+p > m+p`->`n > m` +Zgt_S_n: (n,p:Z)`(Zs p) > (Zs n)`->`p > n` + +(* Lemmas ending by Zlt *) +Zsimpl_lt_plus_l: (n,m,p:Z)`p+n < p+m`->`n < m` +Zsimpl_lt_plus_r: (n,m,p:Z)`n+p < m+p`->`n < m` +Zlt_S_n: (n,m:Z)`(Zs n) < (Zs m)`->`n < m` + +(* Lemmas ending by Zle *) +Zsimpl_le_plus_l: (p,n,m:Z)`p+n <= p+m`->`n <= m` +Zsimpl_le_plus_r: (p,n,m:Z)`n+p <= m+p`->`n <= m` +Zle_S_n: (n,m:Z)`(Zs m) <= (Zs n)`->`m <= n` + +(* B) Bottom-up irreversible (syntactic) simplification *) + +(* Lemmas ending by Zle *) +Zle_trans_S: (n,m:Z)`(Zs n) <= m`->`n <= m` + +(* C) Other unclearly simplifying lemmas *) + +(* Lemmas ending by Zeq *) +Zmult_eq: (x,y:Z)`x <> 0`->`y*x = 0`->`y = 0` + +(* Lemmas ending by Zgt *) +Zmult_gt: (x,y:Z)`x > 0`->`x*y > 0`->`y > 0` + +(* Lemmas ending by Zlt *) +pZmult_lt: (x,y:Z)`x > 0`->`0 < y*x`->`0 < y` + +(* Lemmas ending by Zle *) +Zmult_le: (x,y:Z)`x > 0`->`0 <= y*x`->`0 <= y` +OMEGA1: (x,y:Z)`x = y`->`0 <= x`->`0 <= y` +*) + +(**********************************************************************) +(* Irreversible lemmas with meta-variables *) +(* To be used by EAuto + +Hints Immediate +(* Lemmas ending by eq *) +Zle_antisym: (n,m:Z)`n <= m`->`m <= n`->`n = m` + +(* Lemmas ending by Zge *) +Zge_trans: (n,m,p:Z)`n >= m`->`m >= p`->`n >= p` + +(* Lemmas ending by Zgt *) +Zgt_trans: (n,m,p:Z)`n > m`->`m > p`->`n > p` +Zgt_trans_S: (n,m,p:Z)`(Zs n) > m`->`m > p`->`n > p` +Zle_gt_trans: (n,m,p:Z)`m <= n`->`m > p`->`n > p` +Zgt_le_trans: (n,m,p:Z)`n > m`->`p <= m`->`n > p` + +(* Lemmas ending by Zlt *) +Zlt_trans: (n,m,p:Z)`n < m`->`m < p`->`n < p` +Zlt_le_trans: (n,m,p:Z)`n < m`->`m <= p`->`n < p` +Zle_lt_trans: (n,m,p:Z)`n <= m`->`m < p`->`n < p` + +(* Lemmas ending by Zle *) +Zle_trans: (n,m,p:Z)`n <= m`->`m <= p`->`n <= p` +*) + +(**********************************************************************) +(* Unclear or too specific lemmas *) +(* Not to be used ?? *) + +(* A) Irreversible and too specific (not enough regular) + +(* Lemmas ending by Zle *) +Zle_mult: (x,y:Z)`x > 0`->`0 <= y`->`0 <= y*x` +Zle_mult_approx: (x,y,z:Z)`x > 0`->`z > 0`->`0 <= y`->`0 <= y*x+z` +OMEGA6: (x,y,z:Z)`0 <= x`->`y = 0`->`0 <= x+y*z` +OMEGA7: (x,y,z,t:Z)`z > 0`->`t > 0`->`0 <= x`->`0 <= y`->`0 <= x*z+y*t` + + +(* B) Expansion and too specific ? *) + +(* Lemmas ending by Zge *) +Zge_mult_simpl: (a,b,c:Z)`c > 0`->`a*c >= b*c`->`a >= b` + +(* Lemmas ending by Zgt *) +Zgt_mult_simpl: (a,b,c:Z)`c > 0`->`a*c > b*c`->`a > b` +Zgt_square_simpl: (x,y:Z)`x >= 0`->`y >= 0`->`x*x > y*y`->`x > y` + +(* Lemmas ending by Zle *) +Zle_mult_simpl: (a,b,c:Z)`c > 0`->`a*c <= b*c`->`a <= b` +Zmult_le_approx: (x,y,z:Z)`x > 0`->`x > z`->`0 <= y*x+z`->`0 <= y` + +(* C) Reversible but too specific ? *) + +(* Lemmas ending by Zlt *) +Zlt_minus: (n,m:Z)`0 < m`->`n-m < n` +*) + +(**********************************************************************) +(* Lemmas to be used as rewrite rules *) +(* but can also be used as hints + +(* Left-to-right simplification lemmas (a symbol disappears) *) + +Zcompare_n_S: (n,m:Z)(Zcompare (Zs n) (Zs m))=(Zcompare n m) +Zmin_n_n: (n:Z)`(Zmin n n) = n` +Zmult_1_n: (n:Z)`1*n = n` +Zmult_n_1: (n:Z)`n*1 = n` +Zminus_plus: (n,m:Z)`n+m-n = m` +Zle_plus_minus: (n,m:Z)`n+(m-n) = m` +Zopp_Zopp: (x:Z)`(-(-x)) = x` +Zero_left: (x:Z)`0+x = x` +Zero_right: (x:Z)`x+0 = x` +Zplus_inverse_r: (x:Z)`x+(-x) = 0` +Zplus_inverse_l: (x:Z)`(-x)+x = 0` +Zopp_intro: (x,y:Z)`(-x) = (-y)`->`x = y` +Zmult_one: (x:Z)`1*x = x` +Zero_mult_left: (x:Z)`0*x = 0` +Zero_mult_right: (x:Z)`x*0 = 0` +Zmult_Zopp_Zopp: (x,y:Z)`(-x)*(-y) = x*y` + +(* Right-to-left simplification lemmas (a symbol disappears) *) + +Zpred_Sn: (m:Z)`m = (Zpred (Zs m))` +Zs_pred: (n:Z)`n = (Zs (Zpred n))` +Zplus_n_O: (n:Z)`n = n+0` +Zmult_n_O: (n:Z)`0 = n*0` +Zminus_n_O: (n:Z)`n = n-0` +Zminus_n_n: (n:Z)`0 = n-n` +Zred_factor6: (x:Z)`x = x+0` +Zred_factor0: (x:Z)`x = x*1` + +(* Unclear orientation (no symbol disappears) *) + +Zplus_n_Sm: (n,m:Z)`(Zs (n+m)) = n+(Zs m)` +Zmult_n_Sm: (n,m:Z)`n*m+n = n*(Zs m)` +Zmin_SS: (n,m:Z)`(Zs (Zmin n m)) = (Zmin (Zs n) (Zs m))` +Zplus_assoc_l: (n,m,p:Z)`n+(m+p) = n+m+p` +Zplus_assoc_r: (n,m,p:Z)`n+m+p = n+(m+p)` +Zplus_permute: (n,m,p:Z)`n+(m+p) = m+(n+p)` +Zplus_Snm_nSm: (n,m:Z)`(Zs n)+m = n+(Zs m)` +Zminus_plus_simpl: (n,m,p:Z)`n-m = p+n-(p+m)` +Zminus_Sn_m: (n,m:Z)`(Zs (n-m)) = (Zs n)-m` +Zmult_plus_distr_l: (n,m,p:Z)`(n+m)*p = n*p+m*p` +Zmult_minus_distr: (n,m,p:Z)`(n-m)*p = n*p-m*p` +Zmult_assoc_r: (n,m,p:Z)`n*m*p = n*(m*p)` +Zmult_assoc_l: (n,m,p:Z)`n*(m*p) = n*m*p` +Zmult_permute: (n,m,p:Z)`n*(m*p) = m*(n*p)` +Zmult_Sm_n: (n,m:Z)`n*m+m = (Zs n)*m` +Zmult_Zplus_distr: (x,y,z:Z)`x*(y+z) = x*y+x*z` +Zmult_plus_distr: (n,m,p:Z)`(n+m)*p = n*p+m*p` +Zopp_Zplus: (x,y:Z)`(-(x+y)) = (-x)+(-y)` +Zplus_sym: (x,y:Z)`x+y = y+x` +Zplus_assoc: (x,y,z:Z)`x+(y+z) = x+y+z` +Zmult_sym: (x,y:Z)`x*y = y*x` +Zmult_assoc: (x,y,z:Z)`x*(y*z) = x*y*z` +Zopp_Zmult: (x,y:Z)`(-x)*y = (-(x*y))` +Zplus_S_n: (x,y:Z)`(Zs x)+y = (Zs (x+y))` +Zopp_one: (x:Z)`(-x) = x*(-1)` +Zopp_Zmult_r: (x,y:Z)`(-(x*y)) = x*(-y)` +Zmult_Zopp_left: (x,y:Z)`(-x)*y = x*(-y)` +Zopp_Zmult_l: (x,y:Z)`(-(x*y)) = (-x)*y` +Zred_factor1: (x:Z)`x+x = x*2` +Zred_factor2: (x,y:Z)`x+x*y = x*(1+y)` +Zred_factor3: (x,y:Z)`x*y+x = x*(1+y)` +Zred_factor4: (x,y,z:Z)`x*y+x*z = x*(y+z)` +Zminus_Zplus_compatible: (x,y,n:Z)`x+n-(y+n) = x-y` +Zmin_plus: (x,y,n:Z)`(Zmin (x+n) (y+n)) = (Zmin x y)+n` + +(* nat <-> Z *) +inj_S: (y:nat)`(inject_nat (S y)) = (Zs (inject_nat y))` +inj_plus: (x,y:nat)`(inject_nat (plus x y)) = (inject_nat x)+(inject_nat y)` +inj_mult: (x,y:nat)`(inject_nat (mult x y)) = (inject_nat x)*(inject_nat y)` +inj_minus1: + (x,y:nat)(le y x)->`(inject_nat (minus x y)) = (inject_nat x)-(inject_nat y)` +inj_minus2: (x,y:nat)(gt y x)->`(inject_nat (minus x y)) = 0` + +(* Too specific ? *) +Zred_factor5: (x,y:Z)`x*0+y = y` +*) + +(*i*) diff --git a/theories7/ZArith/Zlogarithm.v b/theories7/ZArith/Zlogarithm.v new file mode 100644 index 00000000..dc850738 --- /dev/null +++ b/theories7/ZArith/Zlogarithm.v @@ -0,0 +1,272 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* `0` (* 1 *) + | (xO q) => (Zs (log_inf q)) (* 2n *) + | (xI q) => (Zs (log_inf q)) (* 2n+1 *) + end. +Fixpoint log_sup [p:positive] : Z := + Cases p of + xH => `0` (* 1 *) + | (xO n) => (Zs (log_sup n)) (* 2n *) + | (xI n) => (Zs (Zs (log_inf n))) (* 2n+1 *) + end. + +Hints Unfold log_inf log_sup. + +(** Then we give the specifications of [log_inf] and [log_sup] + and prove their validity *) + +(*i Hints Resolve ZERO_le_S : zarith. i*) +Hints Resolve Zle_trans : zarith. + +Theorem log_inf_correct : (x:positive) ` 0 <= (log_inf x)` /\ + ` (two_p (log_inf x)) <= (POS x) < (two_p (Zs (log_inf x)))`. +Induction x; Intros; Simpl; +[ Elim H; Intros Hp HR; Clear H; Split; + [ Auto with zarith + | Conditional (Apply Zle_le_S; Trivial) Rewrite two_p_S with x:=(Zs (log_inf p)); + Conditional Trivial Rewrite two_p_S; + Conditional Trivial Rewrite two_p_S in HR; + Rewrite (POS_xI p); Omega ] +| Elim H; Intros Hp HR; Clear H; Split; + [ Auto with zarith + | Conditional (Apply Zle_le_S; Trivial) Rewrite two_p_S with x:=(Zs (log_inf p)); + Conditional Trivial Rewrite two_p_S; + Conditional Trivial Rewrite two_p_S in HR; + Rewrite (POS_xO p); Omega ] +| Unfold two_power_pos; Unfold shift_pos; Simpl; Omega +]. +Qed. + +Definition log_inf_correct1 := + [p:positive](proj1 ? ? (log_inf_correct p)). +Definition log_inf_correct2 := + [p:positive](proj2 ? ? (log_inf_correct p)). + +Opaque log_inf_correct1 log_inf_correct2. + +Hints Resolve log_inf_correct1 log_inf_correct2 : zarith. + +Lemma log_sup_correct1 : (p:positive)` 0 <= (log_sup p)`. +Induction p; Intros; Simpl; Auto with zarith. +Qed. + +(** For every [p], either [p] is a power of two and [(log_inf p)=(log_sup p)] + either [(log_sup p)=(log_inf p)+1] *) + +Theorem log_sup_log_inf : (p:positive) + IF (POS p)=(two_p (log_inf p)) + then (POS p)=(two_p (log_sup p)) + else ` (log_sup p)=(Zs (log_inf p))`. + +Induction p; Intros; +[ Elim H; Right; Simpl; + Rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0)); + Rewrite POS_xI; Unfold Zs; Omega +| Elim H; Clear H; Intro Hif; + [ Left; Simpl; + Rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0)); + Rewrite (two_p_S (log_sup p0) (log_sup_correct1 p0)); + Rewrite <- (proj1 ? ? Hif); Rewrite <- (proj2 ? ? Hif); + Auto + | Right; Simpl; + Rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0)); + Rewrite POS_xO; Unfold Zs; Omega ] +| Left; Auto ]. +Qed. + +Theorem log_sup_correct2 : (x:positive) + ` (two_p (Zpred (log_sup x))) < (POS x) <= (two_p (log_sup x))`. + +Intro. +Elim (log_sup_log_inf x). +(* x is a power of two and [log_sup = log_inf] *) +Intros (E1,E2); Rewrite E2. +Split ; [ Apply two_p_pred; Apply log_sup_correct1 | Apply Zle_n ]. +Intros (E1,E2); Rewrite E2. +Rewrite <- (Zpred_Sn (log_inf x)). +Generalize (log_inf_correct2 x); Omega. +Qed. + +Lemma log_inf_le_log_sup : + (p:positive) `(log_inf p) <= (log_sup p)`. +Induction p; Simpl; Intros; Omega. +Qed. + +Lemma log_sup_le_Slog_inf : + (p:positive) `(log_sup p) <= (Zs (log_inf p))`. +Induction p; Simpl; Intros; Omega. +Qed. + +(** Now it's possible to specify and build the [Log] rounded to the nearest *) + +Fixpoint log_near[x:positive] : Z := + Cases x of + xH => `0` + | (xO xH) => `1` + | (xI xH) => `2` + | (xO y) => (Zs (log_near y)) + | (xI y) => (Zs (log_near y)) + end. + +Theorem log_near_correct1 : (p:positive)` 0 <= (log_near p)`. +Induction p; Simpl; Intros; +[Elim p0; Auto with zarith | Elim p0; Auto with zarith | Trivial with zarith ]. +Intros; Apply Zle_le_S. +Generalize H0; Elim p1; Intros; Simpl; + [ Assumption | Assumption | Apply ZERO_le_POS ]. +Intros; Apply Zle_le_S. +Generalize H0; Elim p1; Intros; Simpl; + [ Assumption | Assumption | Apply ZERO_le_POS ]. +Qed. + +Theorem log_near_correct2: (p:positive) + (log_near p)=(log_inf p) +\/(log_near p)=(log_sup p). +Induction p. +Intros p0 [Einf|Esup]. +Simpl. Rewrite Einf. +Case p0; [Left | Left | Right]; Reflexivity. +Simpl; Rewrite Esup. +Elim (log_sup_log_inf p0). +Generalize (log_inf_le_log_sup p0). +Generalize (log_sup_le_Slog_inf p0). +Case p0; Auto with zarith. +Intros; Omega. +Case p0; Intros; Auto with zarith. +Intros p0 [Einf|Esup]. +Simpl. +Repeat Rewrite Einf. +Case p0; Intros; Auto with zarith. +Simpl. +Repeat Rewrite Esup. +Case p0; Intros; Auto with zarith. +Auto. +Qed. + +(*i****************** +Theorem log_near_correct: (p:positive) + `| (two_p (log_near p)) - (POS p) | <= (POS p)-(two_p (log_inf p))` + /\`| (two_p (log_near p)) - (POS p) | <= (two_p (log_sup p))-(POS p)`. +Intro. +Induction p. +Intros p0 [(Einf1,Einf2)|(Esup1,Esup2)]. +Unfold log_near log_inf log_sup. Fold log_near log_inf log_sup. +Rewrite Einf1. +Repeat Rewrite two_p_S. +Case p0; [Left | Left | Right]. + +Split. +Simpl. +Rewrite E1; Case p0; Try Reflexivity. +Compute. +Unfold log_near; Fold log_near. +Unfold log_inf; Fold log_inf. +Repeat Rewrite E1. +Split. +**********************************i*) + +End Log_pos. + +Section divers. + +(** Number of significative digits. *) + +Definition N_digits := + [x:Z]Cases x of + (POS p) => (log_inf p) + | (NEG p) => (log_inf p) + | ZERO => `0` + end. + +Lemma ZERO_le_N_digits : (x:Z) ` 0 <= (N_digits x)`. +Induction x; Simpl; +[ Apply Zle_n +| Exact log_inf_correct1 +| Exact log_inf_correct1]. +Qed. + +Lemma log_inf_shift_nat : + (n:nat)(log_inf (shift_nat n xH))=(inject_nat n). +Induction n; Intros; +[ Try Trivial +| Rewrite -> inj_S; Rewrite <- H; Reflexivity]. +Qed. + +Lemma log_sup_shift_nat : + (n:nat)(log_sup (shift_nat n xH))=(inject_nat n). +Induction n; Intros; +[ Try Trivial +| Rewrite -> inj_S; Rewrite <- H; Reflexivity]. +Qed. + +(** [Is_power p] means that p is a power of two *) +Fixpoint Is_power[p:positive] : Prop := + Cases p of + xH => True + | (xO q) => (Is_power q) + | (xI q) => False + end. + +Lemma Is_power_correct : + (p:positive) (Is_power p) <-> (Ex [y:nat](p=(shift_nat y xH))). + +Split; +[ Elim p; + [ Simpl; Tauto + | Simpl; Intros; Generalize (H H0); Intro H1; Elim H1; Intros y0 Hy0; + Exists (S y0); Rewrite Hy0; Reflexivity + | Intro; Exists O; Reflexivity] +| Intros; Elim H; Intros; Rewrite -> H0; Elim x; Intros; Simpl; Trivial]. +Qed. + +Lemma Is_power_or : (p:positive) (Is_power p)\/~(Is_power p). +Induction p; +[ Intros; Right; Simpl; Tauto +| Intros; Elim H; + [ Intros; Left; Simpl; Exact H0 + | Intros; Right; Simpl; Exact H0] +| Left; Simpl; Trivial]. +Qed. + +End divers. + + + + + + + diff --git a/theories7/ZArith/Zmin.v b/theories7/ZArith/Zmin.v new file mode 100644 index 00000000..753fe461 --- /dev/null +++ b/theories7/ZArith/Zmin.v @@ -0,0 +1,102 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Cases (Zcompare n m) of + EGAL => n + | INFERIEUR => n + | SUPERIEUR => m + end. + +(** Properties of minimum on binary integer numbers *) + +Lemma Zmin_SS : (n,m:Z)((Zs (Zmin n m))=(Zmin (Zs n) (Zs m))). +Proof. +Intros n m;Unfold Zmin; Rewrite (Zcompare_n_S n m); +(ElimCompare 'n 'm);Intros E;Rewrite E;Auto with arith. +Qed. + +Lemma Zle_min_l : (n,m:Z)(Zle (Zmin n m) n). +Proof. +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 ]. +Qed. + +Lemma Zle_min_r : (n,m:Z)(Zle (Zmin n m) m). +Proof. +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 ]. +Qed. + +Lemma Zmin_case : (n,m:Z)(P:Z->Set)(P n)->(P m)->(P (Zmin n m)). +Proof. +Intros n m P H1 H2; Unfold Zmin; Case (Zcompare n m);Auto with arith. +Qed. + +Lemma Zmin_or : (n,m:Z)(Zmin n m)=n \/ (Zmin n m)=m. +Proof. +Unfold Zmin; Intros; Elim (Zcompare n m); Auto. +Qed. + +Lemma Zmin_n_n : (n:Z) (Zmin n n)=n. +Proof. +Unfold Zmin; Intros; Elim (Zcompare n n); Auto. +Qed. + +Lemma Zmin_plus : + (x,y,n:Z)(Zmin (Zplus x n) (Zplus y n))=(Zplus (Zmin x y) n). +Proof. +Intros x y n; Unfold Zmin. +Rewrite (Zplus_sym x n); +Rewrite (Zplus_sym y n); +Rewrite (Zcompare_Zplus_compatible x y n). +Case (Zcompare x y); Apply Zplus_sym. +Qed. + +(**********************************************************************) +(** Maximum of two binary integer numbers *) +V7only [ (* From Zdivides *) ]. + +Definition Zmax := + [a, b : ?] Cases (Zcompare a b) of INFERIEUR => b | _ => a end. + +(** Properties of maximum on binary integer numbers *) + +Tactic Definition CaseEq name := +Generalize (refl_equal ? name); Pattern -1 name; Case name. + +Theorem Zmax1: (a, b : ?) (Zle a (Zmax a b)). +Proof. +Intros a b; Unfold Zmax; (CaseEq '(Zcompare a b)); Simpl; Auto with zarith. +Unfold Zle; Intros H; Rewrite H; Red; Intros; Discriminate. +Qed. + +Theorem Zmax2: (a, b : ?) (Zle b (Zmax a b)). +Proof. +Intros a b; Unfold Zmax; (CaseEq '(Zcompare a b)); Simpl; Auto with zarith. +Intros H; + (Case (Zle_or_lt b a); Auto; Unfold Zlt; Rewrite H; Intros; Discriminate). +Intros H; + (Case (Zle_or_lt b a); Auto; Unfold Zlt; Rewrite H; Intros; Discriminate). +Qed. + diff --git a/theories7/ZArith/Zmisc.v b/theories7/ZArith/Zmisc.v new file mode 100644 index 00000000..bd89ec66 --- /dev/null +++ b/theories7/ZArith/Zmisc.v @@ -0,0 +1,188 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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)). +Proof. +Induction n; +[ Simpl; Auto with arith +| Intros; Simpl; Apply f_equal with f:=f; Apply H +]. +Qed. + +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). +Proof. +Intro n; NewInduction n as [p H|p H|]; +[ 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 +]. +Qed. + +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)). +Proof. +Intros n m; 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. +Qed. + +(** 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)). +Proof. +Induction n; Intros; +[ Trivial with arith +| Simpl; Apply H0 with x:=(iter_nat n0 A f x); Apply H; Trivial with arith]. +Qed. + +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)). +Proof. +Intros; Rewrite iter_convert; Apply iter_nat_invariant; Trivial with arith. +Qed. + +V7only [ +(* Compatibility *) +Require Zbool. +Require Zeven. +Require Zabs. +Require Zmin. +Notation rename := rename. +Notation POS_xI := POS_xI. +Notation POS_xO := POS_xO. +Notation NEG_xI := NEG_xI. +Notation NEG_xO := NEG_xO. +Notation POS_add := POS_add. +Notation NEG_add := NEG_add. +Notation Zle_cases := Zle_cases. +Notation Zlt_cases := Zlt_cases. +Notation Zge_cases := Zge_cases. +Notation Zgt_cases := Zgt_cases. +Notation POS_gt_ZERO := POS_gt_ZERO. +Notation ZERO_le_POS := ZERO_le_POS. +Notation Zlt_ZERO_pred_le_ZERO := Zlt_ZERO_pred_le_ZERO. +Notation NEG_lt_ZERO := NEG_lt_ZERO. +Notation Zeven_not_Zodd := Zeven_not_Zodd. +Notation Zodd_not_Zeven := Zodd_not_Zeven. +Notation Zeven_Sn := Zeven_Sn. +Notation Zodd_Sn := Zodd_Sn. +Notation Zeven_pred := Zeven_pred. +Notation Zodd_pred := Zodd_pred. +Notation Zeven_div2 := Zeven_div2. +Notation Zodd_div2 := Zodd_div2. +Notation Zodd_div2_neg := Zodd_div2_neg. +Notation Z_modulo_2 := Z_modulo_2. +Notation Zsplit2 := Zsplit2. +Notation Zminus_Zplus_compatible := Zminus_Zplus_compatible. +Notation Zcompare_egal_dec := Zcompare_egal_dec. +Notation Zcompare_elim := Zcompare_elim. +Notation Zcompare_x_x := Zcompare_x_x. +Notation Zlt_not_eq := Zlt_not_eq. +Notation Zcompare_eq_case := Zcompare_eq_case. +Notation Zle_Zcompare := Zle_Zcompare. +Notation Zlt_Zcompare := Zlt_Zcompare. +Notation Zge_Zcompare := Zge_Zcompare. +Notation Zgt_Zcompare := Zgt_Zcompare. +Notation Zmin_plus := Zmin_plus. +Notation absolu_lt := absolu_lt. +Notation Zle_bool_imp_le := Zle_bool_imp_le. +Notation Zle_imp_le_bool := Zle_imp_le_bool. +Notation Zle_bool_refl := Zle_bool_refl. +Notation Zle_bool_antisym := Zle_bool_antisym. +Notation Zle_bool_trans := Zle_bool_trans. +Notation Zle_bool_plus_mono := Zle_bool_plus_mono. +Notation Zone_pos := Zone_pos. +Notation Zone_min_pos := Zone_min_pos. +Notation Zle_is_le_bool := Zle_is_le_bool. +Notation Zge_is_le_bool := Zge_is_le_bool. +Notation Zlt_is_le_bool := Zlt_is_le_bool. +Notation Zgt_is_le_bool := Zgt_is_le_bool. +Notation Zle_plus_swap := Zle_plus_swap. +Notation Zge_iff_le := Zge_iff_le. +Notation Zlt_plus_swap := Zlt_plus_swap. +Notation Zgt_iff_lt := Zgt_iff_lt. +Notation Zeq_plus_swap := Zeq_plus_swap. +(* Definitions *) +Notation entier_of_Z := entier_of_Z. +Notation Z_of_entier := Z_of_entier. +Notation Zle_bool := Zle_bool. +Notation Zge_bool := Zge_bool. +Notation Zlt_bool := Zlt_bool. +Notation Zgt_bool := Zgt_bool. +Notation Zeq_bool := Zeq_bool. +Notation Zneq_bool := Zneq_bool. +Notation Zeven := Zeven. +Notation Zodd := Zodd. +Notation Zeven_bool := Zeven_bool. +Notation Zodd_bool := Zodd_bool. +Notation Zeven_odd_dec := Zeven_odd_dec. +Notation Zeven_dec := Zeven_dec. +Notation Zodd_dec := Zodd_dec. +Notation Zdiv2_pos := Zdiv2_pos. +Notation Zdiv2 := Zdiv2. +Notation Zle_bool_total := Zle_bool_total. +Export Zbool. +Export Zeven. +Export Zabs. +Export Zmin. +Export Zorder. +Export Zcompare. +]. diff --git a/theories7/ZArith/Znat.v b/theories7/ZArith/Znat.v new file mode 100644 index 00000000..99d1422f --- /dev/null +++ b/theories7/ZArith/Znat.v @@ -0,0 +1,138 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* inj_S; Rewrite <- Zmult_Sm_n; + Rewrite <- H;Rewrite <- inj_plus; Simpl; Rewrite plus_sym; Trivial with arith]. +Qed. + +Theorem inj_neq: + (x,y:nat) (neq x y) -> (Zne (inject_nat x) (inject_nat y)). +Proof. +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]. +Qed. + +Theorem inj_le: + (x,y:nat) (le x y) -> (Zle (inject_nat x) (inject_nat y)). +Proof. +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]]. +Qed. + +Theorem inj_lt: (x,y:nat) (lt x y) -> (Zlt (inject_nat x) (inject_nat y)). +Proof. +Intros x y H; Apply Zgt_lt; Apply Zle_S_gt; Rewrite <- inj_S; Apply inj_le; +Exact H. +Qed. + +Theorem inj_gt: (x,y:nat) (gt x y) -> (Zgt (inject_nat x) (inject_nat y)). +Proof. +Intros x y H; Apply Zlt_gt; Apply inj_lt; Exact H. +Qed. + +Theorem inj_ge: (x,y:nat) (ge x y) -> (Zge (inject_nat x) (inject_nat y)). +Proof. +Intros x y H; Apply Zle_ge; Apply inj_le; Apply H. +Qed. + +Theorem inj_eq: (x,y:nat) x=y -> (inject_nat x) = (inject_nat y). +Proof. +Intros x y H; Rewrite H; Trivial with arith. +Qed. + +Theorem intro_Z : + (x:nat) (EX y:Z | (inject_nat x)=y /\ + (Zle ZERO (Zplus (Zmult y (POS xH)) ZERO))). +Proof. +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 ]. +Qed. + +Theorem inj_minus1 : + (x,y:nat) (le y x) -> + (inject_nat (minus x y)) = (Zminus (inject_nat x) (inject_nat y)). +Proof. +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. +Qed. + +Theorem inj_minus2: (x,y:nat) (gt y x) -> (inject_nat (minus x y)) = ZERO. +Proof. +Intros x y H; Rewrite inj_minus_aux; [ Trivial with arith | Apply gt_not_le; Assumption]. +Qed. + +V7only [ (* From Zdivides *) ]. +Theorem POS_inject: (x : positive) (POS x) = (inject_nat (convert x)). +Proof. +Intros x; Elim x; Simpl; Auto. +Intros p H; Rewrite ZL6. +Apply f_equal with f := POS. +Apply convert_intro. +Rewrite bij1; Unfold convert; Simpl. +Rewrite ZL6; Auto. +Intros p H; Unfold convert; Simpl. +Rewrite ZL6; Simpl. +Rewrite inj_plus; Repeat Rewrite <- H. +Rewrite POS_xO; Simpl; Rewrite add_x_x; Reflexivity. +Qed. + diff --git a/theories7/ZArith/Znumtheory.v b/theories7/ZArith/Znumtheory.v new file mode 100644 index 00000000..b8e5f300 --- /dev/null +++ b/theories7/ZArith/Znumtheory.v @@ -0,0 +1,629 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (Zdivide a b). + +(** Syntax for divisibility *) + +Notation "( a | b )" := (Zdivide a b) + (at level 0, a,b at level 10) : Z_scope + V8only "( a | b )" (at level 0). + +(** Results concerning divisibility*) + +Lemma Zdivide_refl : (a:Z) (a|a). +Proof. +Intros; Apply Zdivide_intro with `1`; Ring. +Save. + +Lemma Zone_divide : (a:Z) (1|a). +Proof. +Intros; Apply Zdivide_intro with `a`; Ring. +Save. + +Lemma Zdivide_0 : (a:Z) (a|0). +Proof. +Intros; Apply Zdivide_intro with `0`; Ring. +Save. + +Hints Resolve Zdivide_refl Zone_divide Zdivide_0 : zarith. + +Lemma Zdivide_mult_left : (a,b,c:Z) (a|b) -> (`c*a`|`c*b`). +Proof. +Induction 1; Intros; Apply Zdivide_intro with q. +Rewrite H0; Ring. +Save. + +Lemma Zdivide_mult_right : (a,b,c:Z) (a|b) -> (`a*c`|`b*c`). +Proof. +Intros a b c; Rewrite (Zmult_sym a c); Rewrite (Zmult_sym b c). +Apply Zdivide_mult_left; Trivial. +Save. + +Hints Resolve Zdivide_mult_left Zdivide_mult_right : zarith. + +Lemma Zdivide_plus : (a,b,c:Z) (a|b) -> (a|c) -> (a|`b+c`). +Proof. +Induction 1; Intros q Hq; Induction 1; Intros q' Hq'. +Apply Zdivide_intro with `q+q'`. +Rewrite Hq; Rewrite Hq'; Ring. +Save. + +Lemma Zdivide_opp : (a,b:Z) (a|b) -> (a|`-b`). +Proof. +Induction 1; Intros; Apply Zdivide_intro with `-q`. +Rewrite H0; Ring. +Save. + +Lemma Zdivide_opp_rev : (a,b:Z) (a|`-b`) -> (a| b). +Proof. +Intros; Replace b with `-(-b)`. Apply Zdivide_opp; Trivial. Ring. +Save. + +Lemma Zdivide_opp_left : (a,b:Z) (a|b) -> (`-a`|b). +Proof. +Induction 1; Intros; Apply Zdivide_intro with `-q`. +Rewrite H0; Ring. +Save. + +Lemma Zdivide_opp_left_rev : (a,b:Z) (`-a`|b) -> (a|b). +Proof. +Intros; Replace a with `-(-a)`. Apply Zdivide_opp_left; Trivial. Ring. +Save. + +Lemma Zdivide_minus : (a,b,c:Z) (a|b) -> (a|c) -> (a|`b-c`). +Proof. +Induction 1; Intros q Hq; Induction 1; Intros q' Hq'. +Apply Zdivide_intro with `q-q'`. +Rewrite Hq; Rewrite Hq'; Ring. +Save. + +Lemma Zdivide_left : (a,b,c:Z) (a|b) -> (a|`b*c`). +Proof. +Induction 1; Intros q Hq; Apply Zdivide_intro with `q*c`. +Rewrite Hq; Ring. +Save. + +Lemma Zdivide_right : (a,b,c:Z) (a|c) -> (a|`b*c`). +Proof. +Induction 1; Intros q Hq; Apply Zdivide_intro with `q*b`. +Rewrite Hq; Ring. +Save. + +Lemma Zdivide_a_ab : (a,b:Z) (a|`a*b`). +Proof. +Intros; Apply Zdivide_intro with b; Ring. +Save. + +Lemma Zdivide_a_ba : (a,b:Z) (a|`b*a`). +Proof. +Intros; Apply Zdivide_intro with b; Ring. +Save. + +Hints Resolve Zdivide_plus Zdivide_opp Zdivide_opp_rev + Zdivide_opp_left Zdivide_opp_left_rev + Zdivide_minus Zdivide_left Zdivide_right + Zdivide_a_ab Zdivide_a_ba : zarith. + +(** Auxiliary result. *) + +Lemma Zmult_one : + (x,y:Z) `x>=0` -> `x*y=1` -> `x=1`. +Proof. +Intros x y H H0; NewDestruct (Zmult_1_inversion_l ? ? H0) as [Hpos|Hneg]. + Assumption. + Rewrite Hneg in H; Simpl in H. + Contradiction (Zle_not_lt `0` `-1`). + Apply Zge_le; Assumption. + Apply NEG_lt_ZERO. +Save. + +(** Only [1] and [-1] divide [1]. *) + +Lemma Zdivide_1 : (x:Z) (x|1) -> `x=1` \/ `x=-1`. +Proof. +Induction 1; Intros. +Elim (Z_lt_ge_dec `0` x); [Left|Right]. +Apply Zmult_one with q; Auto with zarith; Rewrite H0; Ring. +Assert `(-x) = 1`; Auto with zarith. +Apply Zmult_one with (-q); Auto with zarith; Rewrite H0; Ring. +Save. + +(** If [a] divides [b] and [b] divides [a] then [a] is [b] or [-b]. *) + +Lemma Zdivide_antisym : (a,b:Z) (a|b) -> (b|a) -> `a=b` \/ `a=-b`. +Proof. +Induction 1; Intros. +Inversion H1. +Rewrite H0 in H2; Clear H H1. +Case (Z_zerop a); Intro. +Left; Rewrite H0; Rewrite e; Ring. +Assert Hqq0: `q0*q = 1`. +Apply Zmult_reg_left with a. +Assumption. +Ring. +Pattern 2 a; Rewrite H2; Ring. +Assert (q|1). +Rewrite <- Hqq0; Auto with zarith. +Elim (Zdivide_1 q H); Intros. +Rewrite H1 in H0; Left; Omega. +Rewrite H1 in H0; Right; Omega. +Save. + +(** If [a] divides [b] and [b<>0] then [|a| <= |b|]. *) + +Lemma Zdivide_bounds : (a,b:Z) (a|b) -> `b<>0` -> `|a| <= |b|`. +Proof. +Induction 1; Intros. +Assert `|b|=|q|*|a|`. + Subst; Apply Zabs_Zmult. +Rewrite H2. +Assert H3 := (Zabs_pos q). +Assert H4 := (Zabs_pos a). +Assert `|q|*|a|>=1*|a|`; Auto with zarith. +Apply Zge_Zmult_pos_compat; Auto with zarith. +Elim (Z_lt_ge_dec `|q|` `1`); [ Intros | Auto with zarith ]. +Assert `|q|=0`. + Omega. +Assert `q=0`. + Rewrite <- (Zabs_Zsgn q). +Rewrite H5; Auto with zarith. +Subst q; Omega. +Save. + +(** * Greatest common divisor (gcd). *) + +(** There is no unicity of the gcd; hence we define the predicate [gcd a b d] + expressing that [d] is a gcd of [a] and [b]. + (We show later that the [gcd] is actually unique if we discard its sign.) *) + +Inductive gcd [a,b,d:Z] : Prop := + gcd_intro : + (d|a) -> (d|b) -> ((x:Z) (x|a) -> (x|b) -> (x|d)) -> (gcd a b d). + +(** Trivial properties of [gcd] *) + +Lemma gcd_sym : (a,b,d:Z)(gcd a b d) -> (gcd b a d). +Proof. +Induction 1; Constructor; Intuition. +Save. + +Lemma gcd_0 : (a:Z)(gcd a `0` a). +Proof. +Constructor; Auto with zarith. +Save. + +Lemma gcd_minus :(a,b,d:Z)(gcd a `-b` d) -> (gcd b a d). +Proof. +Induction 1; Constructor; Intuition. +Save. + +Lemma gcd_opp :(a,b,d:Z)(gcd a b d) -> (gcd b a `-d`). +Proof. +Induction 1; Constructor; Intuition. +Save. + +Hints Resolve gcd_sym gcd_0 gcd_minus gcd_opp : zarith. + +(** * Extended Euclid algorithm. *) + +(** Euclid's algorithm to compute the [gcd] mainly relies on + the following property. *) + +Lemma gcd_for_euclid : + (a,b,d,q:Z) (gcd b `a-q*b` d) -> (gcd a b d). +Proof. +Induction 1; Constructor; Intuition. +Replace a with `a-q*b+q*b`. Auto with zarith. Ring. +Save. + +Lemma gcd_for_euclid2 : + (b,d,q,r:Z) (gcd r b d) -> (gcd b `b*q+r` d). +Proof. +Induction 1; Constructor; Intuition. +Apply H2; Auto. +Replace r with `b*q+r-b*q`. Auto with zarith. Ring. +Save. + +(** We implement the extended version of Euclid's algorithm, + i.e. the one computing Bezout's coefficients as it computes + the [gcd]. We follow the algorithm given in Knuth's + "Art of Computer Programming", vol 2, page 325. *) + +Section extended_euclid_algorithm. + +Variable a,b : Z. + +(** The specification of Euclid's algorithm is the existence of + [u], [v] and [d] such that [ua+vb=d] and [(gcd a b d)]. *) + +Inductive Euclid : Set := + Euclid_intro : + (u,v,d:Z) `u*a+v*b=d` -> (gcd a b d) -> Euclid. + +(** The recursive part of Euclid's algorithm uses well-founded + recursion of non-negative integers. It maintains 6 integers + [u1,u2,u3,v1,v2,v3] such that the following invariant holds: + [u1*a+u2*b=u3] and [v1*a+v2*b=v3] and [gcd(u2,v3)=gcd(a,b)]. + *) + +Lemma euclid_rec : + (v3:Z) `0 <= v3` -> (u1,u2,u3,v1,v2:Z) `u1*a+u2*b=u3` -> `v1*a+v2*b=v3` -> + ((d:Z)(gcd u3 v3 d) -> (gcd a b d)) -> Euclid. +Proof. +Intros v3 Hv3; Generalize Hv3; Pattern v3. +Apply Z_lt_rec. +Clear v3 Hv3; Intros. +Elim (Z_zerop x); Intro. +Apply Euclid_intro with u:=u1 v:=u2 d:=u3. +Assumption. +Apply H2. +Rewrite a0; Auto with zarith. +LetTac q := (Zdiv u3 x). +Assert Hq: `0 <= u3-q*x < x`. +Replace `u3-q*x` with `u3%x`. +Apply Z_mod_lt; Omega. +Assert xpos : `x > 0`. Omega. +Generalize (Z_div_mod_eq u3 x xpos). +Unfold q. +Intro eq; Pattern 2 u3; Rewrite eq; Ring. +Apply (H `u3-q*x` Hq (proj1 ? ? Hq) v1 v2 x `u1-q*v1` `u2-q*v2`). +Tauto. +Replace `(u1-q*v1)*a+(u2-q*v2)*b` with `(u1*a+u2*b)-q*(v1*a+v2*b)`. +Rewrite H0; Rewrite H1; Trivial. +Ring. +Intros; Apply H2. +Apply gcd_for_euclid with q; Assumption. +Assumption. +Save. + +(** We get Euclid's algorithm by applying [euclid_rec] on + [1,0,a,0,1,b] when [b>=0] and [1,0,a,0,-1,-b] when [b<0]. *) + +Lemma euclid : Euclid. +Proof. +Case (Z_le_gt_dec `0` b); Intro. +Intros; Apply euclid_rec with u1:=`1` u2:=`0` u3:=a + v1:=`0` v2:=`1` v3:=b; +Auto with zarith; Ring. +Intros; Apply euclid_rec with u1:=`1` u2:=`0` u3:=a + v1:=`0` v2:=`-1` v3:=`-b`; +Auto with zarith; Try Ring. +Save. + +End extended_euclid_algorithm. + +Theorem gcd_uniqueness_apart_sign : + (a,b,d,d':Z) (gcd a b d) -> (gcd a b d') -> `d = d'` \/ `d = -d'`. +Proof. +Induction 1. +Intros H1 H2 H3; Induction 1; Intros. +Generalize (H3 d' H4 H5); Intro Hd'd. +Generalize (H6 d H1 H2); Intro Hdd'. +Exact (Zdivide_antisym d d' Hdd' Hd'd). +Save. + +(** * Bezout's coefficients *) + +Inductive Bezout [a,b,d:Z] : Prop := + Bezout_intro : (u,v:Z) `u*a + v*b = d` -> (Bezout a b d). + +(** Existence of Bezout's coefficients for the [gcd] of [a] and [b] *) + +Lemma gcd_bezout : (a,b,d:Z) (gcd a b d) -> (Bezout a b d). +Proof. +Intros a b d Hgcd. +Elim (euclid a b); Intros u v d0 e g. +Generalize (gcd_uniqueness_apart_sign a b d d0 Hgcd g). +Intro H; Elim H; Clear H; Intros. +Apply Bezout_intro with u v. +Rewrite H; Assumption. +Apply Bezout_intro with `-u` `-v`. +Rewrite H; Rewrite <- e; Ring. +Save. + +(** gcd of [ca] and [cb] is [c gcd(a,b)]. *) + +Lemma gcd_mult : (a,b,c,d:Z) (gcd a b d) -> (gcd `c*a` `c*b` `c*d`). +Proof. +Intros a b c d; Induction 1; Constructor; Intuition. +Elim (gcd_bezout a b d H); Intros. +Elim H3; Intros. +Elim H4; Intros. +Apply Zdivide_intro with `u*q+v*q0`. +Rewrite <- H5. +Replace `c*(u*a+v*b)` with `u*(c*a)+v*(c*b)`. +Rewrite H6; Rewrite H7; Ring. +Ring. +Save. + +(** We could obtain a [Zgcd] function via [euclid]. But we propose + here a more direct version of a [Zgcd], with better extraction + (no bezout coeffs). *) + +Definition Zgcd_pos : (a:Z)`0<=a` -> (b:Z) + { g:Z | `0<=a` -> (gcd a b g) /\ `g>=0` }. +Proof. +Intros a Ha. +Apply (Z_lt_rec [a:Z](b:Z) { g:Z | `0<=a` -> (gcd a b g) /\`g>=0` }); Try Assumption. +Intro x; Case x. +Intros _ b; Exists (Zabs b). + Elim (Z_le_lt_eq_dec ? ? (Zabs_pos b)). + Intros H0; Split. + Apply Zabs_ind. + Intros; Apply gcd_sym; Apply gcd_0; Auto. + Intros; Apply gcd_opp; Apply gcd_0; Auto. + Auto with zarith. + + Intros H0; Rewrite <- H0. + Rewrite <- (Zabs_Zsgn b); Rewrite <- H0; Simpl. + Split; [Apply gcd_0|Idtac];Auto with zarith. + +Intros p Hrec b. +Generalize (Z_div_mod b (POS p)). +Case (Zdiv_eucl b (POS p)); Intros q r Hqr. +Elim Hqr; Clear Hqr; Intros; Auto with zarith. +Elim (Hrec r H0 (POS p)); Intros g Hgkl. +Inversion_clear H0. +Elim (Hgkl H1); Clear Hgkl; Intros H3 H4. +Exists g; Intros. +Split; Auto. +Rewrite H. +Apply gcd_for_euclid2; Auto. + +Intros p Hrec b. +Exists `0`; Intros. +Elim H; Auto. +Defined. + +Definition Zgcd_spec : (a,b:Z){ g : Z | (gcd a b g) /\ `g>=0` }. +Proof. +Intros a; Case (Z_gt_le_dec `0` a). +Intros; Assert `0 <= -a`. +Omega. +Elim (Zgcd_pos `-a` H b); Intros g Hgkl. +Exists g. +Intuition. +Intros Ha b; Elim (Zgcd_pos a Ha b); Intros g; Exists g; Intuition. +Defined. + +Definition Zgcd := [a,b:Z](let (g,_) = (Zgcd_spec a b) in g). + +Lemma Zgcd_is_pos : (a,b:Z)`(Zgcd a b) >=0`. +Intros a b; Unfold Zgcd; Case (Zgcd_spec a b); Tauto. +Qed. + +Lemma Zgcd_is_gcd : (a,b:Z)(gcd a b (Zgcd a b)). +Intros a b; Unfold Zgcd; Case (Zgcd_spec a b); Tauto. +Qed. + +(** * Relative primality *) + +Definition rel_prime [a,b:Z] : Prop := (gcd a b `1`). + +(** Bezout's theorem: [a] and [b] are relatively prime if and + only if there exist [u] and [v] such that [ua+vb = 1]. *) + +Lemma rel_prime_bezout : + (a,b:Z) (rel_prime a b) -> (Bezout a b `1`). +Proof. +Intros a b; Exact (gcd_bezout a b `1`). +Save. + +Lemma bezout_rel_prime : + (a,b:Z) (Bezout a b `1`) -> (rel_prime a b). +Proof. +Induction 1; Constructor; Auto with zarith. +Intros. Rewrite <- H0; Auto with zarith. +Save. + +(** Gauss's theorem: if [a] divides [bc] and if [a] and [b] are + relatively prime, then [a] divides [c]. *) + +Theorem Gauss : (a,b,c:Z) (a |`b*c`) -> (rel_prime a b) -> (a | c). +Proof. +Intros. Elim (rel_prime_bezout a b H0); Intros. +Replace c with `c*1`; [ Idtac | Ring ]. +Rewrite <- H1. +Replace `c*(u*a+v*b)` with `(c*u)*a + v*(b*c)`; [ EAuto with zarith | Ring ]. +Save. + +(** If [a] is relatively prime to [b] and [c], then it is to [bc] *) + +Lemma rel_prime_mult : + (a,b,c:Z) (rel_prime a b) -> (rel_prime a c) -> (rel_prime a `b*c`). +Proof. +Intros a b c Hb Hc. +Elim (rel_prime_bezout a b Hb); Intros. +Elim (rel_prime_bezout a c Hc); Intros. +Apply bezout_rel_prime. +Apply Bezout_intro with u:=`u*u0*a+v0*c*u+u0*v*b` v:=`v*v0`. +Rewrite <- H. +Replace `u*a+v*b` with `(u*a+v*b) * 1`; [ Idtac | Ring ]. +Rewrite <- H0. +Ring. +Save. + +Lemma rel_prime_cross_prod : + (a,b,c,d:Z) (rel_prime a b) -> (rel_prime c d) -> `b>0` -> `d>0` -> + `a*d = b*c` -> (a=c /\ b=d). +Proof. +Intros a b c d; Intros. +Elim (Zdivide_antisym b d). +Split; Auto with zarith. +Rewrite H4 in H3. +Rewrite Zmult_sym in H3. +Apply Zmult_reg_left with d; Auto with zarith. +Intros; Omega. +Apply Gauss with a. +Rewrite H3. +Auto with zarith. +Red; Auto with zarith. +Apply Gauss with c. +Rewrite Zmult_sym. +Rewrite <- H3. +Auto with zarith. +Red; Auto with zarith. +Save. + +(** After factorization by a gcd, the original numbers are relatively prime. *) + +Lemma gcd_rel_prime : + (a,b,g:Z)`b>0` -> `g>=0`-> (gcd a b g) -> (rel_prime `a/g` `b/g`). +Intros a b g; Intros. +Assert `g <> 0`. + Intro. + Elim H1; Intros. + Elim H4; Intros. + Rewrite H2 in H6; Subst b; Omega. +Unfold rel_prime. +Elim (Zgcd_spec `a/g` `b/g`); Intros g' (H3,H4). +Assert H5 := (gcd_mult ? ? g ? H3). +Rewrite <- Z_div_exact_2 in H5; Auto with zarith. +Rewrite <- Z_div_exact_2 in H5; Auto with zarith. +Elim (gcd_uniqueness_apart_sign ? ? ? ? H1 H5). +Intros; Rewrite (!Zmult_reg_left `1` g' g); Auto with zarith. +Intros; Rewrite (!Zmult_reg_left `1` `-g'` g); Auto with zarith. +Pattern 1 g; Rewrite H6; Ring. + +Elim H1; Intros. +Elim H7; Intros. +Rewrite H9. +Replace `q*g` with `0+q*g`. +Rewrite Z_mod_plus. +Compute; Auto. +Omega. +Ring. + +Elim H1; Intros. +Elim H6; Intros. +Rewrite H9. +Replace `q*g` with `0+q*g`. +Rewrite Z_mod_plus. +Compute; Auto. +Omega. +Ring. +Save. + +(** * Primality *) + +Inductive prime [p:Z] : Prop := + prime_intro : + `1 < p` -> ((n:Z) `1 <= n < p` -> (rel_prime n p)) -> (prime p). + +(** The sole divisors of a prime number [p] are [-1], [1], [p] and [-p]. *) + +Lemma prime_divisors : + (p:Z) (prime p) -> + (a:Z) (a|p) -> `a = -1` \/ `a = 1` \/ a = p \/ `a = -p`. +Proof. +Induction 1; Intros. +Assert `a = (-p)`\/`-p (a:Z) ~ (p|a) -> (rel_prime p a). +Proof. +Induction 1; Intros. +Constructor; Intuition. +Elim (prime_divisors p H x H3); Intuition; Subst; Auto with zarith. +Absurd (p | a); Auto with zarith. +Absurd (p | a); Intuition. +Save. + +Hints Resolve prime_rel_prime : zarith. + +(** [Zdivide] can be expressed using [Zmod]. *) + +Lemma Zmod_Zdivide : (a,b:Z) `b>0` -> `a%b = 0` -> (b|a). +Intros a b H H0. +Apply Zdivide_intro with `(a/b)`. +Pattern 1 a; Rewrite (Z_div_mod_eq a b H). +Rewrite H0; Ring. +Save. + +Lemma Zdivide_Zmod : (a,b:Z) `b>0` -> (b|a) -> `a%b = 0`. +Intros a b; Destruct 2; Intros; Subst. +Change `q*b` with `0+q*b`. +Rewrite Z_mod_plus; Auto. +Save. + +(** [Zdivide] is hence decidable *) + +Lemma Zdivide_dec : (a,b:Z) { (a|b) } + { ~ (a|b) }. +Proof. +Intros a b; Elim (Ztrichotomy_inf a `0`). +(* a<0 *) +Intros H; Elim H; Intros. +Case (Z_eq_dec `b%(-a)` `0`). +Left; Apply Zdivide_opp_left_rev; Apply Zmod_Zdivide; Auto with zarith. +Intro H1; Right; Intro; Elim H1; Apply Zdivide_Zmod; Auto with zarith. +(* a=0 *) +Case (Z_eq_dec b `0`); Intro. +Left; Subst; Auto with zarith. +Right; Subst; Intro H0; Inversion H0; Omega. +(* a>0 *) +Intro H; Case (Z_eq_dec `b%a` `0`). +Left; Apply Zmod_Zdivide; Auto with zarith. +Intro H1; Right; Intro; Elim H1; Apply Zdivide_Zmod; Auto with zarith. +Save. + +(** If a prime [p] divides [ab] then it divides either [a] or [b] *) + +Lemma prime_mult : + (p:Z) (prime p) -> (a,b:Z) (p | `a*b`) -> (p | a) \/ (p | b). +Proof. +Intro p; Induction 1; Intros. +Case (Zdivide_dec p a); Intuition. +Right; Apply Gauss with a; Auto with zarith. +Save. + + diff --git a/theories7/ZArith/Zorder.v b/theories7/ZArith/Zorder.v new file mode 100644 index 00000000..d49a0800 --- /dev/null +++ b/theories7/ZArith/Zorder.v @@ -0,0 +1,969 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* n`}. +Proof. +Unfold Zgt Zlt; Intros m n; Assert H:=(refl_equal ? (Zcompare m n)). + LetTac x := (Zcompare m n) in 2 H Goal. + NewDestruct x; + [Left; Right;Rewrite Zcompare_EGAL_eq with 1:=H + | Left; Left + | Right ]; Reflexivity. +Qed. + +Theorem Ztrichotomy : (m,n:Z) `mn`. +Proof. + Intros m n; NewDestruct (Ztrichotomy_inf m n) as [[Hlt|Heq]|Hgt]; + [Left | Right; Left |Right; Right]; Assumption. +Qed. + +(**********************************************************************) +(** Decidability of equality and order on Z *) + +Theorem dec_eq: (x,y:Z) (decidable (x=y)). +Proof. +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]. +Qed. + +Theorem dec_Zne: (x,y:Z) (decidable (Zne x y)). +Proof. +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]]. +Qed. + +Theorem dec_Zle: (x,y:Z) (decidable `x<=y`). +Proof. +Intros x y; Unfold decidable Zle ; Elim (Zcompare x y); [ + Left; Discriminate + | Left; Discriminate + | Right; Unfold not ; Intros H; Apply H; Trivial with arith]. +Qed. + +Theorem dec_Zgt: (x,y:Z) (decidable `x>y`). +Proof. +Intros x y; Unfold decidable Zgt ; Elim (Zcompare x y); + [ Right; Discriminate | Right; Discriminate | Auto with arith]. +Qed. + +Theorem dec_Zge: (x,y:Z) (decidable `x>=y`). +Proof. +Intros x y; Unfold decidable Zge ; Elim (Zcompare x y); [ + Left; Discriminate +| Right; Unfold not ; Intros H; Apply H; Trivial with arith +| Left; Discriminate]. +Qed. + +Theorem dec_Zlt: (x,y:Z) (decidable `x `xn` -> `n `n>m`. +Proof. +Unfold Zgt Zlt ;Intros m n H; Elim (Zcompare_ANTISYM n m); Auto with arith. +Qed. + +Lemma Zge_le : (m,n:Z) `m>=n` -> `n<=m`. +Proof. +Intros m n; Change ~`m ~`n>m`; +Unfold not; Intros H1 H2; Apply H1; Apply Zgt_lt; Assumption. +Qed. + +Lemma Zle_ge : (m,n:Z) `m<=n` -> `n>=m`. +Proof. +Intros m n; Change ~`m>n`-> ~`n ~`n>m`. +Proof. +Trivial. +Qed. + +Lemma Zgt_not_le : (n,m:Z)`n>m` -> ~`n<=m`. +Proof. +Intros n m H1 H2; Apply H2; Assumption. +Qed. + +Lemma Zle_not_lt : (n,m:Z)`n<=m` -> ~`m ~`m<=n`. +Proof. +Intros n m H1 H2. +Apply Zle_not_lt with m n; Assumption. +Qed. + +Lemma not_Zge : (x,y:Z) ~`x>=y` -> `x `x>=y`. +Proof. +Unfold Zlt Zge; Auto with arith. +Qed. + +Lemma not_Zgt : (x,y:Z)~`x>y` -> `x<=y`. +Proof. +Trivial. +Qed. + +Lemma not_Zle : (x,y:Z) ~`x<=y` -> `x>y`. +Proof. +Unfold Zle Zgt ; Intros x y H; Apply dec_not_not; + [ Exact (dec_Zgt x y) | Assumption]. +Qed. + +Lemma Zge_iff_le : (x,y:Z) `x>=y` <-> `y<=x`. +Proof. + Intros x y; Intros. Split. Intro. Apply Zge_le. Assumption. + Intro. Apply Zle_ge. Assumption. +Qed. + +Lemma Zgt_iff_lt : (x,y:Z) `x>y` <-> `y `n<=m`. +Proof. +Intros; Rewrite H; Apply Zle_n. +Qed. + +Hints Resolve Zle_n : zarith. + +(** Antisymmetry *) + +Lemma Zle_antisym : (n,m:Z)`n<=m`->`m<=n`->n=m. +Proof. +Intros n m H1 H2; NewDestruct (Ztrichotomy n m) as [Hlt|[Heq|Hgt]]. + Absurd `m>n`; [ Apply Zle_not_gt | Apply Zlt_gt]; Assumption. + Assumption. + Absurd `n>m`; [ Apply Zle_not_gt | Idtac]; Assumption. +Qed. + +(** Asymmetry *) + +Lemma Zgt_not_sym : (n,m:Z)`n>m` -> ~`m>n`. +Proof. +Unfold Zgt ;Intros n m H; Elim (Zcompare_ANTISYM n m); Intros H1 H2; +Rewrite -> H1; [ Discriminate | Assumption ]. +Qed. + +Lemma Zlt_not_sym : (n,m:Z)`n ~`mn`. Apply Zlt_gt; Assumption. +Assert H3: `n>m`. Apply Zlt_gt; Assumption. +Apply Zgt_not_sym with m n; Assumption. +Qed. + +(** Irreflexivity *) + +Lemma Zgt_antirefl : (n:Z)~`n>n`. +Proof. +Intros n H; Apply (Zgt_not_sym n n H H). +Qed. + +Lemma Zlt_n_n : (n:Z)~`n ~x=y. +Proof. +Unfold not; Intros x y H H0. +Rewrite H0 in H. +Apply (Zlt_n_n ? H). +Qed. + +(** Large = strict or equal *) + +Lemma Zlt_le_weak : (n,m:Z)`n`n<=m`. +Proof. +Intros n m Hlt; Apply not_Zgt; Apply Zgt_not_sym; Apply Zlt_gt; Assumption. +Qed. + +Lemma Zle_lt_or_eq : (n,m:Z)`n<=m`->(`nm`; [Apply Zle_not_gt|Idtac]; Assumption ]. +Qed. + +(** Dichotomy *) + +Lemma Zle_or_lt : (n,m:Z)`n<=m`\/`mm`->`m>p`->`n>p`. +Proof. +Exact Zcompare_trans_SUPERIEUR. +Qed. + +Lemma Zlt_trans : (n,m,p:Z)`n`m`n`m>p`->`n>p`. +Proof. +Intros n m p H1 H2; NewDestruct (Zle_lt_or_eq m n H1) as [Hlt|Heq]; [ + Apply Zgt_trans with m; [Apply Zlt_gt; Assumption | Assumption ] +| Rewrite <- Heq; Assumption ]. +Qed. + +Lemma Zgt_le_trans : (n,m,p:Z)`n>m`->`p<=m`->`n>p`. +Proof. +Intros n m p H1 H2; NewDestruct (Zle_lt_or_eq p m H2) as [Hlt|Heq]; [ + Apply Zgt_trans with m; [Assumption|Apply Zlt_gt; Assumption] +| Rewrite Heq; Assumption ]. +Qed. + +Lemma Zlt_le_trans : (n,m,p:Z)`n`m<=p`->`n`m`n`m<=p`->`n<=p`. +Proof. +Intros n m p H1 H2; Apply not_Zgt. +Intro Hgt; Apply Zle_not_gt with n m. Assumption. +Exact (Zgt_le_trans n p m Hgt H2). +Qed. + +Lemma Zge_trans : (n, m, p : Z) `n>=m` -> `m>=p` -> `n>=p`. +Proof. +Intros n m p H1 H2. +Apply Zle_ge. +Apply Zle_trans with m; Apply Zge_le; Trivial. +Qed. + +Hints Resolve Zle_trans : zarith. + +(** Compatibility of successor wrt to order *) + +Lemma Zle_n_S : (n,m:Z) `m<=n` -> `(Zs m)<=(Zs n)`. +Proof. +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. +Qed. + +Lemma Zgt_n_S : (n,m:Z)`m>n` -> `(Zs m)>(Zs n)`. +Proof. +Unfold Zgt; Intros n m H; Rewrite Zcompare_n_S; Auto with arith. +Qed. + +Lemma Zlt_n_S : (n,m:Z)`n`(Zs n)<(Zs m)`. +Proof. +Intros n m H;Apply Zgt_lt;Apply Zgt_n_S;Apply Zlt_gt; Assumption. +Qed. + +Hints Resolve Zle_n_S : zarith. + +(** Simplification of successor wrt to order *) + +Lemma Zgt_S_n : (n,p:Z)`(Zs p)>(Zs n)`->`p>n`. +Proof. +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. +Qed. + +Lemma Zle_S_n : (n,m:Z) `(Zs m)<=(Zs n)` -> `m<=n`. +Proof. +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. +Qed. + +Lemma Zlt_S_n : (n,m:Z)`(Zs n)<(Zs m)`->`nm`->`p+n>p+m`. +Proof. +Unfold Zgt; Intros n m p H; Rewrite (Zcompare_Zplus_compatible n m p); +Assumption. +Qed. + +Lemma Zgt_reg_r : (n,m,p:Z)`n>m`->`n+p>m+p`. +Proof. +Intros n m p H; Rewrite (Zplus_sym n p); Rewrite (Zplus_sym m p); Apply Zgt_reg_l; Trivial. +Qed. + +Lemma Zle_reg_l : (n,m,p:Z)`n<=m`->`p+n<=p+m`. +Proof. +Intros n m p; Unfold Zle not ;Intros H1 H2;Apply H1; +Rewrite <- (Zcompare_Zplus_compatible n m p); Assumption. +Qed. + +Lemma Zle_reg_r : (n,m,p:Z) `n<=m`->`n+p<=m+p`. +Proof. +Intros a b c;Do 2 Rewrite [n:Z](Zplus_sym n c); Exact (Zle_reg_l a b c). +Qed. + +Lemma Zlt_reg_l : (n,m,p:Z)`n`p+n`n+p`c<=d`->`a+c`c`a+c(Zle p q)->`n+p<=m+q`. +Proof. +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 ]. +Qed. + +V7only [Set Implicit Arguments.]. + +Lemma Zlt_Zplus : (x1,x2,y1,y2:Z)`x1 < x2` -> `y1 < y2` -> `x1 + y1 < x2 + y2`. +Intros; Apply Zle_lt_reg. Apply Zlt_le_weak; Assumption. Assumption. +Qed. + +V7only [Unset Implicit Arguments.]. + +(** Compatibility of addition wrt to being positive *) + +Lemma Zle_0_plus : (x,y:Z) `0<=x` -> `0<=y` -> `0<=x+y`. +Proof. +Intros x y H1 H2;Rewrite <- (Zero_left ZERO); Apply Zle_plus_plus; Assumption. +Qed. + +(** Simplification of addition wrt to order *) + +Lemma Zsimpl_gt_plus_l : (n,m,p:Z)`p+n>p+m`->`n>m`. +Proof. +Unfold Zgt; Intros n m p H; + Rewrite <- (Zcompare_Zplus_compatible n m p); Assumption. +Qed. + +Lemma Zsimpl_gt_plus_r : (n,m,p:Z)`n+p>m+p`->`n>m`. +Proof. +Intros n m p H; Apply Zsimpl_gt_plus_l with p. +Rewrite (Zplus_sym p n); Rewrite (Zplus_sym p m); Trivial. +Qed. + +Lemma Zsimpl_le_plus_l : (n,m,p:Z)`p+n<=p+m`->`n<=m`. +Proof. +Intros n m p; Unfold Zle not ;Intros H1 H2;Apply H1; +Rewrite (Zcompare_Zplus_compatible n m p); Assumption. +Qed. + +Lemma Zsimpl_le_plus_r : (n,m,p:Z)`n+p<=m+p`->`n<=m`. +Proof. +Intros n m p H; Apply Zsimpl_le_plus_l with p. +Rewrite (Zplus_sym p n); Rewrite (Zplus_sym p m); Trivial. +Qed. + +Lemma Zsimpl_lt_plus_l : (n,m,p:Z)`p+n`n`nn`. +Proof. +Exact Zcompare_Zs_SUPERIEUR. +Qed. + +Lemma Zle_Sn_n : (n:Z)~`(Zs n)<=n`. +Proof. +Intros n; Apply Zgt_not_le; Apply Zgt_Sn_n. +Qed. + +Lemma Zlt_n_Sn : (n:Z)`n<(Zs n)`. +Proof. +Intro n; Apply Zgt_lt; Apply Zgt_Sn_n. +Qed. + +Lemma Zlt_pred_n_n : (n:Z)`(Zpred n)n`->`(Zs n)<=p`. +Proof. +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]. +Qed. + +Lemma Zle_gt_S : (n,p:Z)`n<=p`->`(Zs p)>n`. +Proof. +Intros n p H; Apply Zgt_le_trans with p. + Apply Zgt_Sn_n. + Assumption. +Qed. + +Lemma Zle_lt_n_Sm : (n,m:Z)`n<=m`->`n<(Zs m)`. +Proof. +Intros n m H; Apply Zgt_lt; Apply Zle_gt_S; Assumption. +Qed. + +Lemma Zlt_le_S : (n,p:Z)`n`(Zs n)<=p`. +Proof. +Intros n p H; Apply Zgt_le_S; Apply Zlt_gt; Assumption. +Qed. + +Lemma Zgt_S_le : (n,p:Z)`(Zs p)>n`->`n<=p`. +Proof. +Intros n p H;Apply Zle_S_n; Apply Zgt_le_S; Assumption. +Qed. + +Lemma Zlt_n_Sm_le : (n,m:Z)`n<(Zs m)`->`n<=m`. +Proof. +Intros n m H; Apply Zgt_S_le; Apply Zlt_gt; Assumption. +Qed. + +Lemma Zle_S_gt : (n,m:Z) `(Zs n)<=m` -> `m>n`. +Proof. +Intros n m H;Apply Zle_gt_trans with m:=(Zs n); + [ Assumption | Apply Zgt_Sn_n ]. +Qed. + +(** Weakening order *) + +Lemma Zle_n_Sn : (n:Z)`n<=(Zs n)`. +Proof. +Intros n; Apply Zgt_S_le;Apply Zgt_trans with m:=(Zs n) ;Apply Zgt_Sn_n. +Qed. + +Hints Resolve Zle_n_Sn : zarith. + +Lemma Zle_pred_n : (n:Z)`(Zpred n)<=n`. +Proof. +Intros n;Pattern 2 n ;Rewrite Zs_pred; Apply Zle_n_Sn. +Qed. + +Lemma Zlt_S : (n,m:Z)`n`n<(Zs m)`. +Intros n m H;Apply Zgt_lt; Apply Zgt_trans with m:=m; [ + Apply Zgt_Sn_n +| Apply Zlt_gt; Assumption ]. +Qed. + +Lemma Zle_le_S : (x,y:Z)`x<=y`->`x<=(Zs y)`. +Proof. +Intros x y H. +Apply Zle_trans with y; Trivial with zarith. +Qed. + +Lemma Zle_trans_S : (n,m:Z)`(Zs n)<=m`->`n<=m`. +Proof. +Intros n m H;Apply Zle_trans with m:=(Zs n); [ Apply Zle_n_Sn | Assumption ]. +Qed. + +Hints Resolve Zle_le_S : zarith. + +(** Relating order wrt successor and order wrt predecessor *) + +Lemma Zgt_pred : (n,p:Z)`p>(Zs n)`->`(Zpred p)>n`. +Proof. +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. +Qed. + +Lemma Zlt_pred : (n,p:Z)`(Zs n)`n<(Zpred p)`. +Proof. +Intros n p H;Apply Zlt_S_n; Rewrite <- Zs_pred; Assumption. +Qed. + +(** Relating strict order and large order on positive *) + +Lemma Zlt_ZERO_pred_le_ZERO : (n:Z) `0 `0<=(Zpred n)`. +Intros x H. +Rewrite (Zs_pred x) in H. +Apply Zgt_S_le. +Apply Zlt_gt. +Assumption. +Qed. + +V7only [Set Implicit Arguments.]. + +Lemma Zgt0_le_pred : (y:Z) `y > 0` -> `0 <= (Zpred y)`. +Intros; Apply Zlt_ZERO_pred_le_ZERO; Apply Zgt_lt. Assumption. +Qed. + +V7only [Unset Implicit Arguments.]. + +(** Special cases of ordered integers *) + +V7only [ (* Relevance confirmed from Zdivides *) ]. +Lemma Z_O_1: `0<1`. +Proof. +Change `0<(Zs 0)`. Apply Zlt_n_Sn. +Qed. + +Lemma Zle_0_1: `0<=1`. +Proof. +Change `0<=(Zs 0)`. Apply Zle_n_Sn. +Qed. + +V7only [ (* Relevance confirmed from Zdivides *) ]. +Lemma Zle_NEG_POS: (p,q:positive) `(NEG p)<=(POS q)`. +Proof. +Intros p; Red; Simpl; Red; Intros H; Discriminate. +Qed. + +Lemma POS_gt_ZERO : (p:positive) `(POS p)>0`. +Unfold Zgt; Trivial. +Qed. + + (* weaker but useful (in [Zpower] for instance) *) +Lemma ZERO_le_POS : (p:positive) `0<=(POS p)`. +Intro; Unfold Zle; Discriminate. +Qed. + +Lemma NEG_lt_ZERO : (p:positive)`(NEG p)<0`. +Unfold Zlt; Trivial. +Qed. + +Lemma ZERO_le_inj : + (n:nat) `0 <= (inject_nat n)`. +Induction n; Simpl; Intros; +[ Apply Zle_n +| Unfold Zle; Simpl; Discriminate]. +Qed. + +Hints Immediate Zle_refl : zarith. + +(** Transitivity using successor *) + +Lemma Zgt_trans_S : (n,m,p:Z)`(Zs n)>m`->`m>p`->`n>p`. +Proof. +Intros n m p H1 H2;Apply Zle_gt_trans with m:=m; + [ Apply Zgt_S_le; Assumption | Assumption ]. +Qed. + +(** Derived lemma *) + +Lemma Zgt_S : (n,m:Z)`(Zs n)>m`->(`n>m`\/(m=n)). +Proof. +Intros n m H. +Assert Hle : `m<=n`. + Apply Zgt_S_le; Assumption. +NewDestruct (Zle_lt_or_eq ? ? Hle) as [Hlt|Heq]. + Left; Apply Zlt_gt; Assumption. + Right; Assumption. +Qed. + +(** Compatibility of multiplication by a positive wrt to order *) + +V7only [Set Implicit Arguments.]. + +Lemma Zle_Zmult_pos_right : (a,b,c : Z) `a<=b` -> `0<=c` -> `a*c<=b*c`. +Proof. +Intros a b c H H0; NewDestruct c. + Do 2 Rewrite Zero_mult_right; Assumption. + Rewrite (Zmult_sym a); Rewrite (Zmult_sym b). + Unfold Zle; Rewrite Zcompare_Zmult_compatible; Assumption. + Unfold Zle in H0; Contradiction H0; Reflexivity. +Qed. + +Lemma Zle_Zmult_pos_left : (a,b,c : Z) `a<=b` -> `0<=c` -> `c*a<=c*b`. +Proof. +Intros a b c H1 H2; Rewrite (Zmult_sym c a);Rewrite (Zmult_sym c b). +Apply Zle_Zmult_pos_right; Trivial. +Qed. + +V7only [ (* Relevance confirmed from Zextensions *) ]. +Lemma Zmult_lt_compat_r : (x,y,z:Z)`0 `x < y` -> `x*z < y*z`. +Proof. +Intros x y z H H0; NewDestruct z. + Contradiction (Zlt_n_n `0`). + Rewrite (Zmult_sym x); Rewrite (Zmult_sym y). + Unfold Zlt; Rewrite Zcompare_Zmult_compatible; Assumption. + Discriminate H. +Save. + +Lemma Zgt_Zmult_right : (x,y,z:Z)`z>0` -> `x > y` -> `x*z > y*z`. +Proof. +Intros x y z; Intros; Apply Zlt_gt; Apply Zmult_lt_compat_r; + Apply Zgt_lt; Assumption. +Qed. + +Lemma Zlt_Zmult_right : (x,y,z:Z)`z>0` -> `x < y` -> `x*z < y*z`. +Proof. +Intros x y z; Intros; Apply Zmult_lt_compat_r; + [Apply Zgt_lt; Assumption | Assumption]. +Qed. + +Lemma Zle_Zmult_right : (x,y,z:Z)`z>0` -> `x <= y` -> `x*z <= y*z`. +Proof. +Intros x y z Hz Hxy. +Elim (Zle_lt_or_eq x y Hxy). +Intros; Apply Zlt_le_weak. +Apply Zlt_Zmult_right; Trivial. +Intros; Apply Zle_refl. +Rewrite H; Trivial. +Qed. + +V7only [ (* Relevance confirmed from Zextensions *) ]. +Lemma Zmult_lt_0_le_compat_r : (x,y,z:Z)`0 < z`->`x <= y`->`x*z <= y*z`. +Proof. +Intros x y z; Intros; Apply Zle_Zmult_right; Try Apply Zlt_gt; Assumption. +Qed. + +Lemma Zlt_Zmult_left : (x,y,z:Z)`z>0` -> `x < y` -> `z*x < z*y`. +Proof. +Intros x y z; Intros. +Rewrite (Zmult_sym z x); Rewrite (Zmult_sym z y); +Apply Zlt_Zmult_right; Assumption. +Qed. + +V7only [ (* Relevance confirmed from Zextensions *) ]. +Lemma Zmult_lt_compat_l : (x,y,z:Z)`0 `x < y` -> `z*x < z*y`. +Proof. +Intros x y z; Intros. +Rewrite (Zmult_sym z x); Rewrite (Zmult_sym z y); +Apply Zlt_Zmult_right; Try Apply Zlt_gt; Assumption. +Save. + +Lemma Zgt_Zmult_left : (x,y,z:Z)`z>0` -> `x > y` -> `z*x > z*y`. +Proof. +Intros x y z; Intros; +Rewrite (Zmult_sym z x); Rewrite (Zmult_sym z y); +Apply Zgt_Zmult_right; Assumption. +Qed. + +Lemma Zge_Zmult_pos_right : (a,b,c : Z) `a>=b` -> `c>=0` -> `a*c>=b*c`. +Proof. +Intros a b c H1 H2; Apply Zle_ge. +Apply Zle_Zmult_pos_right; Apply Zge_le; Trivial. +Qed. + +Lemma Zge_Zmult_pos_left : (a,b,c : Z) `a>=b` -> `c>=0` -> `c*a>=c*b`. +Proof. +Intros a b c H1 H2; Apply Zle_ge. +Apply Zle_Zmult_pos_left; Apply Zge_le; Trivial. +Qed. + +Lemma Zge_Zmult_pos_compat : + (a,b,c,d : Z) `a>=c` -> `b>=d` -> `c>=0` -> `d>=0` -> `a*b>=c*d`. +Proof. +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. +Qed. + +V7only [ (* Relevance confirmed from Zextensions *) ]. +Lemma Zmult_le_compat: (a, b, c, d : Z) + `a<=c` -> `b<=d` -> `0<=a` -> `0<=b` -> `a*b<=c*d`. +Proof. +Intros a b c d H0 H1 H2 H3. +Apply Zle_trans with (Zmult c b). +Apply Zle_Zmult_pos_right; Assumption. +Apply Zle_Zmult_pos_left. +Assumption. +Apply Zle_trans with a; Assumption. +Qed. + +(** Simplification of multiplication by a positive wrt to being positive *) + +Lemma Zlt_Zmult_right2 : (x,y,z:Z)`z>0` -> `x*z < y*z` -> `x < y`. +Proof. +Intros x y z; Intros; NewDestruct z. + Contradiction (Zgt_antirefl `0`). + Rewrite (Zmult_sym x) in H0; Rewrite (Zmult_sym y) in H0. + Unfold Zlt in H0; Rewrite Zcompare_Zmult_compatible in H0; Assumption. + Discriminate H. +Qed. + +V7only [ (* Relevance confirmed from Zextensions *) ]. +Lemma Zmult_lt_reg_r : (a, b, c : Z) `0 `a*c `a0`->`a*c<=b*c`->`a<=b`. +Proof. +Intros x y z Hz Hxy. +Elim (Zle_lt_or_eq `x*z` `y*z` Hxy). +Intros; Apply Zlt_le_weak. +Apply Zlt_Zmult_right2 with z; Trivial. +Intros; Apply Zle_refl. +Apply Zmult_reg_right with z. + Intro. Rewrite H0 in Hz. Contradiction (Zgt_antirefl `0`). +Assumption. +Qed. +V7only [Notation Zle_Zmult_right2 := Zle_mult_simpl. +(* Zle_Zmult_right2 : (x,y,z:Z)`z>0` -> `x*z <= y*z` -> `x <= y`. *) +]. + +V7only [ (* Relevance confirmed from Zextensions *) ]. +Lemma Zmult_lt_0_le_reg_r: (x,y,z:Z)`0 `x*z <= y*z`->`x <= y`. +Intros x y z; Intros ; Apply Zle_mult_simpl with z. +Try Apply Zlt_gt; Assumption. +Assumption. +Qed. + +V7only [Unset Implicit Arguments.]. + +Lemma Zge_mult_simpl : (a,b,c:Z) `c>0`->`a*c>=b*c`->`a>=b`. +Intros a b c H1 H2; Apply Zle_ge; Apply Zle_mult_simpl with c; Trivial. +Apply Zge_le; Trivial. +Qed. + +Lemma Zgt_mult_simpl : (a,b,c:Z) `c>0`->`a*c>b*c`->`a>b`. +Intros a b c H1 H2; Apply Zlt_gt; Apply Zlt_Zmult_right2 with c; Trivial. +Apply Zgt_lt; Trivial. +Qed. + + +(** Compatibility of multiplication by a positive wrt to being positive *) + +Lemma Zle_ZERO_mult : (x,y:Z) `0<=x` -> `0<=y` -> `0<=x*y`. +Proof. +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. +Qed. + +Lemma Zgt_ZERO_mult: (a,b:Z) `a>0`->`b>0`->`a*b>0`. +Proof. +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. +Qed. + +V7only [ (* Relevance confirmed from Zextensions *) ]. +Lemma Zmult_lt_O_compat : (a, b : Z) `0 `0 `00` -> `0<=y` -> `0<=(Zmult y x)`. +Proof. +Intros x y H1 H2; Apply Zle_ZERO_mult; Trivial. +Apply Zlt_le_weak; Apply Zgt_lt; Trivial. +Qed. + +(** Simplification of multiplication by a positive wrt to being positive *) + +Lemma Zmult_le: (x,y:Z) `x>0` -> `0<=(Zmult y x)` -> `0<=y`. +Proof. +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]. +Qed. + +Lemma Zmult_lt: (x,y:Z) `x>0` -> `0 `0 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]. +Qed. + +V7only [ (* Relevance confirmed from Zextensions *) ]. +Lemma Zmult_lt_0_reg_r : (x,y:Z)`0 < x`->`0 < y*x`->`0 < y`. +Proof. +Intros x y; Intros; EApply Zmult_lt with x ; Try Apply Zlt_gt; Assumption. +Qed. + +Lemma Zmult_gt: (x,y:Z) `x>0` -> `x*y>0` -> `y>0`. +Proof. +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. +Qed. + +(** Simplification of square wrt order *) + +Lemma Zgt_square_simpl: (x, y : Z) `x>=0` -> `y>=0` -> `x*x>y*y` -> `x>y`. +Proof. +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. + +Lemma Zlt_square_simpl: (x,y:Z) `0<=x` -> `0<=y` -> `y*y `y `x<=y-z`. +Proof. + Intros x y z; Intros. Split. Intro. Rewrite <- (Zero_right x). Rewrite <- (Zplus_inverse_r z). + Rewrite Zplus_assoc_l. Exact (Zle_reg_r ? ? ? H). + Intro. Rewrite <- (Zero_right y). Rewrite <- (Zplus_inverse_l z). Rewrite Zplus_assoc_l. + Apply Zle_reg_r. Assumption. +Qed. + +Lemma Zlt_plus_swap : (x,y,z:Z) `x+z `x `x=y-z`. +Proof. +Intros x y z; Intros. Split. Intro. Apply Zplus_minus. Symmetry. Rewrite Zplus_sym. + Assumption. +Intro. Rewrite H. Unfold Zminus. Rewrite Zplus_assoc_r. + Rewrite Zplus_inverse_l. Apply Zero_right. +Qed. + +Lemma Zlt_minus : (n,m:Z)`0`n-m`mnat] and [Zmult : Z->Z] *) + +Lemma Zpower_nat_is_exp : + (n,m:nat)(z:Z) + `(Zpower_nat z (plus n m)) = (Zpower_nat z n)*(Zpower_nat z m)`. + +Intros; Elim n; +[ Simpl; Elim (Zpower_nat z m); Auto with zarith +| Unfold Zpower_nat; Intros; Simpl; Rewrite H; + Apply Zmult_assoc]. +Qed. + +(** [Zpower_pos z n] is the n-th power of [z] when [n] is an binary + integer (type [positive]) and [z] a signed integer (type [Z]) *) + +Definition Zpower_pos := + [z:Z][n:positive] (iter_pos n Z ([x:Z]`z * x`) `1`). + +(** This theorem shows that powers of unary and binary integers + are the same thing, modulo the function convert : [positive -> nat] *) + +Theorem Zpower_pos_nat : + (z:Z)(p:positive)(Zpower_pos z p) = (Zpower_nat z (convert p)). + +Intros; Unfold Zpower_pos; Unfold Zpower_nat; Apply iter_convert. +Qed. + +(** Using the theorem [Zpower_pos_nat] and the lemma [Zpower_nat_is_exp] we + deduce that the function [[n:positive](Zpower_pos z n)] is a morphism + for [add : positive->positive] and [Zmult : Z->Z] *) + +Theorem Zpower_pos_is_exp : + (n,m:positive)(z:Z) + ` (Zpower_pos z (add n m)) = (Zpower_pos z n)*(Zpower_pos z m)`. + +Intros. +Rewrite -> (Zpower_pos_nat z n). +Rewrite -> (Zpower_pos_nat z m). +Rewrite -> (Zpower_pos_nat z (add n m)). +Rewrite -> (convert_add n m). +Apply Zpower_nat_is_exp. +Qed. + +Definition Zpower := + [x,y:Z]Cases y of + (POS p) => (Zpower_pos x p) + | ZERO => `1` + | (NEG p) => `0` + end. + +V8Infix "^" Zpower : Z_scope. + +Hints Immediate Zpower_nat_is_exp : zarith. +Hints Immediate Zpower_pos_is_exp : zarith. +Hints Unfold Zpower_pos : zarith. +Hints Unfold Zpower_nat : zarith. + +Lemma Zpower_exp : (x:Z)(n,m:Z) + `n >= 0` -> `m >= 0` -> `(Zpower x (n+m))=(Zpower x n)*(Zpower x m)`. +NewDestruct n; NewDestruct m; Auto with zarith. +Simpl; Intros; Apply Zred_factor0. +Simpl; Auto with zarith. +Intros; Compute in H0; Absurd INFERIEUR=INFERIEUR; Auto with zarith. +Intros; Compute in H0; Absurd INFERIEUR=INFERIEUR; Auto with zarith. +Qed. + +End section1. + +(* Exporting notation "^" *) + +V8Infix "^" Zpower : Z_scope. + +Hints Immediate Zpower_nat_is_exp : zarith. +Hints Immediate Zpower_pos_is_exp : zarith. +Hints Unfold Zpower_pos : zarith. +Hints Unfold Zpower_nat : zarith. + +Section Powers_of_2. + +(** For the powers of two, that will be widely used, a more direct + calculus is possible. We will also prove some properties such + as [(x:positive) x < 2^x] that are true for all integers bigger + than 2 but more difficult to prove and useless. *) + +(** [shift n m] computes [2^n * m], or [m] shifted by [n] positions *) + +Definition shift_nat := + [n:nat][z:positive](iter_nat n positive xO z). +Definition shift_pos := + [n:positive][z:positive](iter_pos n positive xO z). +Definition shift := + [n:Z][z:positive] + Cases n of + ZERO => z + | (POS p) => (iter_pos p positive xO z) + | (NEG p) => z + end. + +Definition two_power_nat := [n:nat] (POS (shift_nat n xH)). +Definition two_power_pos := [x:positive] (POS (shift_pos x xH)). + +Lemma two_power_nat_S : + (n:nat)` (two_power_nat (S n)) = 2*(two_power_nat n)`. +Intro; Simpl; Apply refl_equal. +Qed. + +Lemma shift_nat_plus : + (n,m:nat)(x:positive) + (shift_nat (plus n m) x)=(shift_nat n (shift_nat m x)). + +Intros; Unfold shift_nat; Apply iter_nat_plus. +Qed. + +Theorem shift_nat_correct : + (n:nat)(x:positive)(POS (shift_nat n x))=`(Zpower_nat 2 n)*(POS x)`. + +Unfold shift_nat; Induction n; +[ Simpl; Trivial with zarith +| Intros; Replace (Zpower_nat `2` (S n0)) with `2 * (Zpower_nat 2 n0)`; +[ Rewrite <- Zmult_assoc; Rewrite <- (H x); Simpl; Reflexivity +| Auto with zarith ] +]. +Qed. + +Theorem two_power_nat_correct : + (n:nat)(two_power_nat n)=(Zpower_nat `2` n). + +Intro n. +Unfold two_power_nat. +Rewrite -> (shift_nat_correct n). +Omega. +Qed. + +(** Second we show that [two_power_pos] and [two_power_nat] are the same *) +Lemma shift_pos_nat : (p:positive)(x:positive) + (shift_pos p x)=(shift_nat (convert p) x). + +Unfold shift_pos. +Unfold shift_nat. +Intros; Apply iter_convert. +Qed. + +Lemma two_power_pos_nat : + (p:positive) (two_power_pos p)=(two_power_nat (convert p)). + +Intro; Unfold two_power_pos; Unfold two_power_nat. +Apply f_equal with f:=POS. +Apply shift_pos_nat. +Qed. + +(** Then we deduce that [two_power_pos] is also correct *) + +Theorem shift_pos_correct : + (p,x:positive) ` (POS (shift_pos p x)) = (Zpower_pos 2 p) * (POS x)`. + +Intros. +Rewrite -> (shift_pos_nat p x). +Rewrite -> (Zpower_pos_nat `2` p). +Apply shift_nat_correct. +Qed. + +Theorem two_power_pos_correct : + (x:positive) (two_power_pos x)=(Zpower_pos `2` x). + +Intro. +Rewrite -> two_power_pos_nat. +Rewrite -> Zpower_pos_nat. +Apply two_power_nat_correct. +Qed. + +(** Some consequences *) + +Theorem two_power_pos_is_exp : + (x,y:positive) (two_power_pos (add x y)) + =(Zmult (two_power_pos x) (two_power_pos y)). +Intros. +Rewrite -> (two_power_pos_correct (add x y)). +Rewrite -> (two_power_pos_correct x). +Rewrite -> (two_power_pos_correct y). +Apply Zpower_pos_is_exp. +Qed. + +(** The exponentiation [z -> 2^z] for [z] a signed integer. + For convenience, we assume that [2^z = 0] for all [z < 0] + We could also define a inductive type [Log_result] with + 3 contructors [ Zero | Pos positive -> | minus_infty] + but it's more complexe and not so useful. *) + +Definition two_p := + [x:Z]Cases x of + ZERO => `1` + | (POS y) => (two_power_pos y) + | (NEG y) => `0` + end. + +Theorem two_p_is_exp : + (x,y:Z) ` 0 <= x` -> ` 0 <= y` -> + ` (two_p (x+y)) = (two_p x)*(two_p y)`. +Induction x; +[ Induction y; Simpl; Auto with zarith +| Induction y; + [ Unfold two_p; Rewrite -> (Zmult_sym (two_power_pos p) `1`); + Rewrite -> (Zmult_one (two_power_pos p)); Auto with zarith + | Unfold Zplus; Unfold two_p; + Intros; Apply two_power_pos_is_exp + | Intros; Unfold Zle in H0; Unfold Zcompare in H0; + Absurd SUPERIEUR=SUPERIEUR; Trivial with zarith + ] +| Induction y; + [ Simpl; Auto with zarith + | Intros; Unfold Zle in H; Unfold Zcompare in H; + Absurd (SUPERIEUR=SUPERIEUR); Trivial with zarith + | Intros; Unfold Zle in H; Unfold Zcompare in H; + Absurd (SUPERIEUR=SUPERIEUR); Trivial with zarith + ] +]. +Qed. + +Lemma two_p_gt_ZERO : (x:Z) ` 0 <= x` -> ` (two_p x) > 0`. +Induction x; Intros; +[ Simpl; Omega +| Simpl; Unfold two_power_pos; Apply POS_gt_ZERO +| Absurd ` 0 <= (NEG p)`; + [ Simpl; Unfold Zle; Unfold Zcompare; + Do 2 Unfold not; Auto with zarith + | Assumption ] +]. +Qed. + +Lemma two_p_S : (x:Z) ` 0 <= x` -> + `(two_p (Zs x)) = 2 * (two_p x)`. +Intros; Unfold Zs. +Rewrite (two_p_is_exp x `1` H (ZERO_le_POS xH)). +Apply Zmult_sym. +Qed. + +Lemma two_p_pred : + (x:Z)` 0 <= x` -> ` (two_p (Zpred x)) < (two_p x)`. +Intros; Apply natlike_ind +with P:=[x:Z]` (two_p (Zpred x)) < (two_p x)`; +[ Simpl; Unfold Zlt; Auto with zarith +| Intros; Elim (Zle_lt_or_eq `0` x0 H0); + [ Intros; + Replace (two_p (Zpred (Zs x0))) + with (two_p (Zs (Zpred x0))); + [ Rewrite -> (two_p_S (Zpred x0)); + [ Rewrite -> (two_p_S x0); + [ Omega + | Assumption] + | Apply Zlt_ZERO_pred_le_ZERO; Assumption] + | Rewrite <- (Zs_pred x0); Rewrite <- (Zpred_Sn x0); Trivial with zarith] + | Intro Hx0; Rewrite <- Hx0; Simpl; Unfold Zlt; Auto with zarith] +| Assumption]. +Qed. + +Lemma Zlt_lt_double : (x,y:Z) ` 0 <= x < y` -> ` x < 2*y`. +Intros; Omega. Qed. + +End Powers_of_2. + +Hints Resolve two_p_gt_ZERO : zarith. +Hints Immediate two_p_pred two_p_S : zarith. + +Section power_div_with_rest. + +(** Division by a power of two. + To [n:Z] and [p:positive], [q],[r] are associated such that + [n = 2^p.q + r] and [0 <= r < 2^p] *) + +(** Invariant: [d*q + r = d'*q + r /\ d' = 2*d /\ 0<= r < d /\ 0 <= r' < d'] *) +Definition Zdiv_rest_aux := + [qrd:(Z*Z)*Z] + let (qr,d)=qrd in let (q,r)=qr in + (Cases q of + ZERO => ` (0, r)` + | (POS xH) => ` (0, d + r)` + | (POS (xI n)) => ` ((POS n), d + r)` + | (POS (xO n)) => ` ((POS n), r)` + | (NEG xH) => ` (-1, d + r)` + | (NEG (xI n)) => ` ((NEG n) - 1, d + r)` + | (NEG (xO n)) => ` ((NEG n), r)` + end, ` 2*d`). + +Definition Zdiv_rest := + [x:Z][p:positive]let (qr,d)=(iter_pos p ? Zdiv_rest_aux ((x,`0`),`1`)) in qr. + +Lemma Zdiv_rest_correct1 : + (x:Z)(p:positive) + let (qr,d)=(iter_pos p ? Zdiv_rest_aux ((x,`0`),`1`)) in d=(two_power_pos p). + +Intros x p; +Rewrite (iter_convert p ? Zdiv_rest_aux ((x,`0`),`1`)); +Rewrite (two_power_pos_nat p); +Elim (convert p); Simpl; +[ Trivial with zarith +| Intro n; Rewrite (two_power_nat_S n); + Unfold 2 Zdiv_rest_aux; + Elim (iter_nat n (Z*Z)*Z Zdiv_rest_aux ((x,`0`),`1`)); + NewDestruct a; Intros; Apply f_equal with f:=[z:Z]`2*z`; Assumption ]. +Qed. + +Lemma Zdiv_rest_correct2 : + (x:Z)(p:positive) + let (qr,d)=(iter_pos p ? Zdiv_rest_aux ((x,`0`),`1`)) in + let (q,r)=qr in + ` x=q*d + r` /\ ` 0 <= r < d`. + +Intros; Apply iter_pos_invariant with + f:=Zdiv_rest_aux + Inv:=[qrd:(Z*Z)*Z]let (qr,d)=qrd in let (q,r)=qr in + ` x=q*d + r` /\ ` 0 <= r < d`; +[ Intro x0; Elim x0; Intro y0; Elim y0; + Intros q r d; Unfold Zdiv_rest_aux; + Elim q; + [ Omega + | NewDestruct p0; + [ Rewrite POS_xI; Intro; Elim H; Intros; Split; + [ Rewrite H0; Rewrite Zplus_assoc; + Rewrite Zmult_plus_distr_l; + Rewrite Zmult_1_n; Rewrite Zmult_assoc; + Rewrite (Zmult_sym (POS p0) `2`); Apply refl_equal + | Omega ] + | Rewrite POS_xO; Intro; Elim H; Intros; Split; + [ Rewrite H0; + Rewrite Zmult_assoc; Rewrite (Zmult_sym (POS p0) `2`); + Apply refl_equal + | Omega ] + | Omega ] + | NewDestruct p0; + [ Rewrite NEG_xI; Unfold Zminus; Intro; Elim H; Intros; Split; + [ Rewrite H0; Rewrite Zplus_assoc; + Apply f_equal with f:=[z:Z]`z+r`; + Do 2 (Rewrite Zmult_plus_distr_l); + Rewrite Zmult_assoc; + Rewrite (Zmult_sym (NEG p0) `2`); + Rewrite <- Zplus_assoc; + Apply f_equal with f:=[z:Z]`2 * (NEG p0) * d + z`; + Omega + | Omega ] + | Rewrite NEG_xO; Unfold Zminus; Intro; Elim H; Intros; Split; + [ Rewrite H0; + Rewrite Zmult_assoc; Rewrite (Zmult_sym (NEG p0) `2`); + Apply refl_equal + | Omega ] + | Omega ] ] +| Omega]. +Qed. + +Inductive Set Zdiv_rest_proofs[x:Z; p:positive] := + Zdiv_rest_proof : (q:Z)(r:Z) + `x = q * (two_power_pos p) + r` + -> `0 <= r` + -> `r < (two_power_pos p)` + -> (Zdiv_rest_proofs x p). + +Lemma Zdiv_rest_correct : + (x:Z)(p:positive)(Zdiv_rest_proofs x p). +Intros x p. +Generalize (Zdiv_rest_correct1 x p); Generalize (Zdiv_rest_correct2 x p). +Elim (iter_pos p (Z*Z)*Z Zdiv_rest_aux ((x,`0`),`1`)). +Induction a. +Intros. +Elim H; Intros H1 H2; Clear H. +Rewrite -> H0 in H1; Rewrite -> H0 in H2; +Elim H2; Intros; +Apply Zdiv_rest_proof with q:=a0 r:=b; Assumption. +Qed. + +End power_div_with_rest. diff --git a/theories7/ZArith/Zsqrt.v b/theories7/ZArith/Zsqrt.v new file mode 100644 index 00000000..72a2e9cf --- /dev/null +++ b/theories7/ZArith/Zsqrt.v @@ -0,0 +1,136 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + (Match ?1 With + | [[xH]] -> Fail + | _ -> Rewrite (POS_xI ?1)) + | [|- [(POS (xO ?1))]] -> + (Match ?1 With + | [[xH]] -> Fail + | _ -> Rewrite (POS_xO ?1)). + +Inductive sqrt_data [n : Z] : Set := + c_sqrt: (s, r :Z)`n=s*s+r`->`0<=r<=2*s`->(sqrt_data n) . + +Definition sqrtrempos: (p : positive) (sqrt_data (POS p)). +Refine (Fix sqrtrempos { + sqrtrempos [p : positive] : (sqrt_data (POS p)) := + <[p : ?] (sqrt_data (POS p))> Cases p of + xH => (c_sqrt `1` `1` `0` ? ?) + | (xO xH) => (c_sqrt `2` `1` `1` ? ?) + | (xI xH) => (c_sqrt `3` `1` `2` ? ?) + | (xO (xO p')) => + Cases (sqrtrempos p') of + (c_sqrt s' r' Heq Hint) => + Cases (Z_le_gt_dec `4*s'+1` `4*r'`) of + (left Hle) => + (c_sqrt (POS (xO (xO p'))) `2*s'+1` `4*r'-(4*s'+1)` ? ?) + | (right Hgt) => + (c_sqrt (POS (xO (xO p'))) `2*s'` `4*r'` ? ?) + end + end + | (xO (xI p')) => + Cases (sqrtrempos p') of + (c_sqrt s' r' Heq Hint) => + Cases + (Z_le_gt_dec `4*s'+1` `4*r'+2`) of + (left Hle) => + (c_sqrt + (POS (xO (xI p'))) `2*s'+1` `4*r'+2-(4*s'+1)` ? ?) + | (right Hgt) => + (c_sqrt (POS (xO (xI p'))) `2*s'` `4*r'+2` ? ?) + end + end + | (xI (xO p')) => + Cases (sqrtrempos p') of + (c_sqrt s' r' Heq Hint) => + Cases + (Z_le_gt_dec `4*s'+1` `4*r'+1`) of + (left Hle) => + (c_sqrt + (POS (xI (xO p'))) `2*s'+1` `4*r'+1-(4*s'+1)` ? ?) + | (right Hgt) => + (c_sqrt (POS (xI (xO p'))) `2*s'` `4*r'+1` ? ?) + end + end + | (xI (xI p')) => + Cases (sqrtrempos p') of + (c_sqrt s' r' Heq Hint) => + Cases + (Z_le_gt_dec `4*s'+1` `4*r'+3`) of + (left Hle) => + (c_sqrt + (POS (xI (xI p'))) `2*s'+1` `4*r'+3-(4*s'+1)` ? ?) + | (right Hgt) => + (c_sqrt (POS (xI (xI p'))) `2*s'` `4*r'+3` ? ?) + end + end + end + }); Clear sqrtrempos; Repeat compute_POS; + Try (Try Rewrite Heq; Ring; Fail); Try Omega. +Defined. + +(** Define with integer input, but with a strong (readable) specification. *) +Definition Zsqrt : (x:Z)`0<=x`->{s:Z & {r:Z | x=`s*s+r` /\ `s*s<=x<(s+1)*(s+1)`}}. +Refine [x] + <[x:Z]`0<=x`->{s:Z & {r:Z | x=`s*s+r` /\ `s*s<=x<(s+1)*(s+1)`}}>Cases x of + (POS p) => [h]Cases (sqrtrempos p) of + (c_sqrt s r Heq Hint) => + (existS ? [s:Z]{r:Z | `(POS p)=s*s+r` /\ + `s*s<=(POS p)<(s+1)*(s+1)`} + s + (exist Z [r:Z]((POS p)=`s*s+r` /\ `s*s<=(POS p)<(s+1)*(s+1)`) + r ?)) + end + | (NEG p) => [h](False_rec + {s:Z & {r:Z | + (NEG p)=`s*s+r` /\ `s*s<=(NEG p)<(s+1)*(s+1)`}} + (h (refl_equal ? SUPERIEUR))) + | ZERO => [h](existS ? [s:Z]{r:Z | `0=s*s+r` /\ `s*s<=0<(s+1)*(s+1)`} + `0` (exist Z [r:Z](`0=0*0+r`/\`0*0<=0<(0+1)*(0+1)`) + `0` ?)) + end;Try Omega. +Split;[Omega|Rewrite Heq;Ring `(s+1)*(s+1)`;Omega]. +Defined. + +(** Define a function of type Z->Z that computes the integer square root, + but only for positive numbers, and 0 for others. *) +Definition Zsqrt_plain : Z->Z := + [x]Cases x of + (POS p)=>Cases (Zsqrt (POS p) (ZERO_le_POS p)) of (existS s _) => s end + |(NEG p)=>`0` + |ZERO=>`0` + end. + +(** A basic theorem about Zsqrt_plain *) +Theorem Zsqrt_interval :(x:Z)`0<=x`-> + `(Zsqrt_plain x)*(Zsqrt_plain x)<= x < ((Zsqrt_plain x)+1)*((Zsqrt_plain x)+1)`. +Intros x;Case x. +Unfold Zsqrt_plain;Omega. +Intros p;Unfold Zsqrt_plain;Case (Zsqrt (POS p) (ZERO_le_POS p)). +Intros s (r,(Heq,Hint)) Hle;Assumption. +Intros p Hle;Elim Hle;Auto. +Qed. + + diff --git a/theories7/ZArith/Zsyntax.v b/theories7/ZArith/Zsyntax.v new file mode 100644 index 00000000..3c7f3a57 --- /dev/null +++ b/theories7/ZArith/Zsyntax.v @@ -0,0 +1,278 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* [$id] + +with number := + +with negnumber := + +with formula : constr := + form_expr [ expr($p) ] -> [$p] +(*| form_eq [ expr($p) "=" expr($c) ] -> [ (eq Z $p $c) ]*) +| form_eq [ expr($p) "=" expr($c) ] -> [ (Coq.Init.Logic.eq ? $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_eq_eq [ expr($p) "=" expr($c) "=" expr($c1) ] + -> [ (Coq.Init.Logic.eq ? $p $c)/\(Coq.Init.Logic.eq ? $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) ] -> [ ~(Coq.Init.Logic.eq Z $p $c) ]*) +| form_neq [ expr($p) "<>" expr($c) ] -> [ ~(Coq.Init.Logic.eq ? $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) ] +| expr_meta [ zmeta($m) ] -> [ $m ] + +with zmeta := +| rimpl [ "?" ] -> [ ? ] +| rmeta0 [ "?" "0" ] -> [ ?0 ] +| rmeta1 [ "?" "1" ] -> [ ?1 ] +| rmeta2 [ "?" "2" ] -> [ ?2 ] +| rmeta3 [ "?" "3" ] -> [ ?3 ] +| rmeta4 [ "?" "4" ] -> [ ?4 ] +| rmeta5 [ "?" "5" ] -> [ ?5 ] + +with application : constr := + apply [ application($p) expr($c1) ] -> [ ($p $c1) ] +| apply_inject_nat [ "inject_nat" constr:constr($c1) ] -> [ (inject_nat $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 [ "`" prim:bigint($c) "`" ] -> [ 'Z: $c ' ]. + +(* The symbols "`" "`" must be printed just once at the top of the expressions, + 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), which is printed like \$subexpr + 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: + Zle [ (Zle $n1 $n2) ] -> + [[ "`" (ZEXPR $n1) [1 0] "<= " (ZEXPR $n2) "`"]] + | Zlt [ (Zlt $n1 $n2) ] -> + [[ "`" (ZEXPR $n1) [1 0] "< " (ZEXPR $n2) "`" ]] + | Zge [ (Zge $n1 $n2) ] -> + [[ "`" (ZEXPR $n1) [1 0] ">= " (ZEXPR $n2) "`" ]] + | Zgt [ (Zgt $n1 $n2) ] -> + [[ "`" (ZEXPR $n1) [1 0] "> " (ZEXPR $n2) "`" ]] + | Zcompare [<<(Zcompare $n1 $n2)>>] -> + [[ "`" (ZEXPR $n1) [1 0] "?= " (ZEXPR $n2) "`" ]] + | Zeq [ (eq Z $n1 $n2) ] -> + [[ "`" (ZEXPR $n1) [1 0] "= " (ZEXPR $n2)"`"]] + | Zneq [ ~(eq Z $n1 $n2) ] -> + [[ "`" (ZEXPR $n1) [1 0] "<> " (ZEXPR $n2) "`"]] + | Zle_Zle [ (Zle $n1 $n2)/\(Zle $n2 $n3) ] -> + [[ "`" (ZEXPR $n1) [1 0] "<= " (ZEXPR $n2) + [1 0] "<= " (ZEXPR $n3) "`"]] + | Zle_Zlt [ (Zle $n1 $n2)/\(Zlt $n2 $n3) ] -> + [[ "`" (ZEXPR $n1) [1 0] "<= " (ZEXPR $n2) + [1 0] "< " (ZEXPR $n3) "`"]] + | Zlt_Zle [ (Zlt $n1 $n2)/\(Zle $n2 $n3) ] -> + [[ "`" (ZEXPR $n1) [1 0] "< " (ZEXPR $n2) + [1 0] "<= " (ZEXPR $n3) "`"]] + | Zlt_Zlt [ (Zlt $n1 $n2)/\(Zlt $n2 $n3) ] -> + [[ "`" (ZEXPR $n1) [1 0] "< " (ZEXPR $n2) + [1 0] "< " (ZEXPR $n3) "`"]] + | ZZero_v7 [ ZERO ] -> [ "`0`" ] + | ZPos_v7 [ (POS $r) ] -> [$r:"positive_printer":9] + | ZNeg_v7 [ (NEG $r) ] -> [$r:"negative_printer":9] + ; + + level 7: + Zplus [ (Zplus $n1 $n2) ] + -> [ [ "`" (ZEXPR $n1):E "+" [0 0] (ZEXPR $n2):L "`"] ] + | Zminus [ (Zminus $n1 $n2) ] + -> [ [ "`" (ZEXPR $n1):E "-" [0 0] (ZEXPR $n2):L "`"] ] + ; + + level 6: + Zmult [ (Zmult $n1 $n2) ] + -> [ [ "`" (ZEXPR $n1):E "*" [0 0] (ZEXPR $n2):L "`"] ] + ; + + level 8: + Zopp [ (Zopp $n1) ] -> [ [ "`" "-" (ZEXPR $n1):E "`"] ] + | Zopp_POS [ (Zopp (POS $r)) ] -> + [ [ "`(" "Zopp" [1 0] $r:"positive_printer_inside" ")`"] ] + | Zopp_ZERO [ (Zopp ZERO) ] -> [ [ "`(" "Zopp" [1 0] "0" ")`"] ] + | Zopp_NEG [ (Zopp (NEG $r)) ] -> + [ [ "`(" "Zopp" [1 0] "(" $r:"negative_printer_inside" "))`"] ] + ; + + level 4: + Zabs [ (Zabs $n1) ] -> [ [ "`|" (ZEXPR $n1):E "|`"] ] + ; + + level 0: + escape_inside [ << (ZEXPR $r) >> ] -> [ "[" $r:E "]" ] + ; + + level 4: + Zappl_inside [ << (ZEXPR (APPLIST $h ($LIST $t))) >> ] + -> [ [ "("(ZEXPR $h):E [1 0] (ZAPPLINSIDETAIL ($LIST $t)):E ")"] ] + | Zappl_inject_nat [ << (ZEXPR (APPLIST <> $n)) >> ] + -> [ [ "(inject_nat" [1 1] $n:L ")"] ] + | Zappl_inside_tail [ << (ZAPPLINSIDETAIL $h ($LIST $t)) >> ] + -> [(ZEXPR $h):E [1 0] (ZAPPLINSIDETAIL ($LIST $t)):E] + | Zappl_inside_one [ << (ZAPPLINSIDETAIL $e) >> ] ->[(ZEXPR $e):E] + | pair_inside [ << (ZEXPR <<(pair $s1 $s2 $z1 $z2)>>) >> ] + -> [ [ "("(ZEXPR $z1):E "," [1 0] (ZEXPR $z2):E ")"] ] + ; + + level 3: + var_inside [ << (ZEXPR ($VAR $i)) >> ] -> [$i] + | secvar_inside [ << (ZEXPR (SECVAR $i)) >> ] -> [(SECVAR $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) ] + + | O_inside [ << (ZEXPR << O >>) >> ] -> [ "O" ] (* To shunt Arith printer *) + + (* Added by JCF, 9/3/98; updated HH, 11/9/01 *) + | implicit_head_inside [ << (ZEXPR (APPLISTEXPL ($LIST $c))) >> ] + -> [ (APPLIST ($LIST $c)) ] + | implicit_arg_inside [ << (ZEXPR (EXPL "!" $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))>>) >> ] -> + [ [ "Zopp" [1 0] $r:"positive_printer_inside" ] ] + | Zopp_ZERO_inside [ << (ZEXPR <<(Zopp ZERO)>>) >> ] -> + [ [ "Zopp" [1 0] "0"] ] + | Zopp_NEG_inside [ << (ZEXPR <<(Zopp (NEG $r))>>) >> ] -> + [ [ "Zopp" [1 0] $r:"negative_printer_inside" ] ] + ; + + level 4: + Zabs_inside [ << (ZEXPR <<(Zabs $n1)>>) >> ] -> [ "|" (ZEXPR $n1) "|"] + ; + + level 0: + ZZero_inside [ << (ZEXPR <>) >> ] -> ["0"] + | ZPos_inside [ << (ZEXPR <<(POS $p)>>) >>] -> + [$p:"positive_printer_inside":9] + | ZNeg_inside [ << (ZEXPR <<(NEG $p)>>) >>] -> + [$p:"negative_printer_inside":9] +. +]. + +V7only[ +(* For parsing/printing based on scopes *) +Module Z_scope. + +Infix LEFTA 4 "+" Zplus : Z_scope. +Infix LEFTA 4 "-" Zminus : Z_scope. +Infix LEFTA 3 "*" Zmult : Z_scope. +Notation "- x" := (Zopp x) (at level 0): Z_scope V8only. +Infix NONA 5 "<=" Zle : Z_scope. +Infix NONA 5 "<" Zlt : Z_scope. +Infix NONA 5 ">=" Zge : Z_scope. +Infix NONA 5 ">" Zgt : Z_scope. +Infix NONA 5 "?=" Zcompare : Z_scope. +Notation "x <= y <= z" := (Zle x y)/\(Zle y z) + (at level 5, y at level 4):Z_scope + V8only (at level 70, y at next level). +Notation "x <= y < z" := (Zle x y)/\(Zlt y z) + (at level 5, y at level 4):Z_scope + V8only (at level 70, y at next level). +Notation "x < y < z" := (Zlt x y)/\(Zlt y z) + (at level 5, y at level 4):Z_scope + V8only (at level 70, y at next level). +Notation "x < y <= z" := (Zlt x y)/\(Zle y z) + (at level 5, y at level 4):Z_scope + V8only (at level 70, y at next level). +Notation "x = y = z" := x=y/\y=z : Z_scope + V8only (at level 70, y at next level). + +(* Now a polymorphic notation +Notation "x <> y" := ~(eq Z x y) (at level 5, no associativity) : Z_scope. +*) + +(* Notation "| x |" (Zabs x) : Z_scope.(* "|" conflicts with THENS *)*) + +(* Overwrite the printing of "`x = y`" *) +Syntax constr level 0: + Zeq [ (eq Z $n1 $n2) ] -> [[ $n1 [1 0] "= " $n2 ]]. + +Open Scope Z_scope. + +End Z_scope. +]. diff --git a/theories7/ZArith/Zwf.v b/theories7/ZArith/Zwf.v new file mode 100644 index 00000000..c2e6ca2a --- /dev/null +++ b/theories7/ZArith/Zwf.v @@ -0,0 +1,96 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (Acc Z (Zwf c) a). +Clear a; Induction n; Intros. +(** n= 0 *) +Case H; Intros. +Case (lt_n_O (f a)); Auto. +Apply Acc_intro; Unfold Zwf; Intros. +Assert False;Omega Orelse Contradiction. +(** inductive case *) +Case H0; Clear H0; Intro; Auto. +Apply Acc_intro; Intros. +Apply H. +Unfold Zwf in H1. +Case (Zle_or_lt c y); Intro; Auto with zarith. +Left. +Red in H0. +Apply lt_le_trans with (f a); Auto with arith. +Unfold f. +Apply absolu_lt; Omega. +Apply (H (S (f a))); Auto. +Save. + +End wf_proof. + +Hints Resolve Zwf_well_founded : datatypes v62. + + +(** We also define the other family of relations: + + [x (Zwf_up c) y] iff [y < x <= c] + *) + +Definition Zwf_up := [c:Z][x,y:Z] `y < x <= c`. + +(** and we prove that [(Zwf_up c)] is well founded *) + +Section wf_proof_up. + +Variable c : Z. + +(** The proof of well-foundness is classic: we do the proof by induction + on a measure in nat, which is here [|c-x|] *) + +Local f := [z:Z](absolu (Zminus c z)). + +Lemma Zwf_up_well_founded : (well_founded Z (Zwf_up c)). +Proof. +Apply well_founded_lt_compat with f:=f. +Unfold Zwf_up f. +Intros. +Apply absolu_lt. +Unfold Zminus. Split. +Apply Zle_left; Intuition. +Apply Zlt_reg_l; Unfold Zlt; Rewrite <- Zcompare_Zopp; Intuition. +Save. + +End wf_proof_up. + +Hints Resolve Zwf_up_well_founded : datatypes v62. diff --git a/theories7/ZArith/auxiliary.v b/theories7/ZArith/auxiliary.v new file mode 100644 index 00000000..8db2c852 --- /dev/null +++ b/theories7/ZArith/auxiliary.v @@ -0,0 +1,219 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (Zne (Zplus x (Zopp y)) ZERO). +Proof. +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. +Qed. + +Theorem Zegal_left : (x,y:Z) (x=y) -> (Zplus x (Zopp y)) = ZERO. +Proof. +Intros x y H; +Apply (Zsimpl_plus_l y);Rewrite -> Zplus_permute; +Rewrite -> Zplus_inverse_r;Do 2 Rewrite -> Zero_right;Assumption. +Qed. + +Theorem Zle_left : (x,y:Z) (Zle x y) -> (Zle ZERO (Zplus y (Zopp x))). +Proof. +Intros x y H; Replace ZERO with (Zplus x (Zopp x)). +Apply Zle_reg_r; Trivial. +Apply Zplus_inverse_r. +Qed. + +Theorem Zle_left_rev : (x,y:Z) (Zle ZERO (Zplus y (Zopp x))) + -> (Zle x y). +Proof. +Intros x y H; Apply Zsimpl_le_plus_r with (Zopp x). +Rewrite Zplus_inverse_r; Trivial. +Qed. + +Theorem Zlt_left_rev : (x,y:Z) (Zlt ZERO (Zplus y (Zopp x))) + -> (Zlt x y). +Proof. +Intros x y H; Apply Zsimpl_lt_plus_r with (Zopp x). +Rewrite Zplus_inverse_r; Trivial. +Qed. + +Theorem Zlt_left : + (x,y:Z) (Zlt x y) -> (Zle ZERO (Zplus (Zplus y (NEG xH)) (Zopp x))). +Proof. +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. +Qed. + +Theorem Zlt_left_lt : + (x,y:Z) (Zlt x y) -> (Zlt ZERO (Zplus y (Zopp x))). +Proof. +Intros x y H; Replace ZERO with (Zplus x (Zopp x)). +Apply Zlt_reg_r; Trivial. +Apply Zplus_inverse_r. +Qed. + +Theorem Zge_left : (x,y:Z) (Zge x y) -> (Zle ZERO (Zplus x (Zopp y))). +Proof. +Intros x y H; Apply Zle_left; Apply Zge_le; Assumption. +Qed. + +Theorem Zgt_left : + (x,y:Z) (Zgt x y) -> (Zle ZERO (Zplus (Zplus x (NEG xH)) (Zopp y))). +Proof. +Intros x y H; Apply Zlt_left; Apply Zgt_lt; Assumption. +Qed. + +Theorem Zgt_left_gt : + (x,y:Z) (Zgt x y) -> (Zgt (Zplus x (Zopp y)) ZERO). +Proof. +Intros x y H; Replace ZERO with (Zplus y (Zopp y)). +Apply Zgt_reg_r; Trivial. +Apply Zplus_inverse_r. +Qed. + +Theorem Zgt_left_rev : (x,y:Z) (Zgt (Zplus x (Zopp y)) ZERO) + -> (Zgt x y). +Proof. +Intros x y H; Apply Zsimpl_gt_plus_r with (Zopp y). +Rewrite Zplus_inverse_r; Trivial. +Qed. + +(**********************************************************************) +(** Factorization lemmas *) + +Theorem Zred_factor0 : (x:Z) x = (Zmult x (POS xH)). +Intro x; Rewrite (Zmult_n_1 x); Reflexivity. +Qed. + +Theorem Zred_factor1 : (x:Z) (Zplus x x) = (Zmult x (POS (xO xH))). +Proof. +Exact Zplus_Zmult_2. +Qed. + +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. +Qed. + +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. +Qed. +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. +Qed. + +Theorem Zred_factor5 : (x,y:Z) (Zplus (Zmult x ZERO) y) = y. + +Intros x y; Rewrite <- Zmult_n_O;Auto with arith. +Qed. + +Theorem Zred_factor6 : (x:Z) x = (Zplus x ZERO). + +Intro; Rewrite Zero_right; Trivial with arith. +Qed. + +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]. +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 with x; [ + Assumption + | Apply Zle_lt_trans with 1:=H3 ; Rewrite <- Zmult_Sm_n; + Apply Zlt_reg_l; Apply Zgt_lt; Assumption]. + +Qed. + +V7only [ +(* Compatibility *) +Require Znat. +Require Zcompare. +Notation neq := neq. +Notation Zne := Zne. +Notation OMEGA2 := Zle_0_plus. +Notation add_un_Zs := add_un_Zs. +Notation inj_S := inj_S. +Notation Zplus_S_n := Zplus_S_n. +Notation inj_plus := inj_plus. +Notation inj_mult := inj_mult. +Notation inj_neq := inj_neq. +Notation inj_le := inj_le. +Notation inj_lt := inj_lt. +Notation inj_gt := inj_gt. +Notation inj_ge := inj_ge. +Notation inj_eq := inj_eq. +Notation intro_Z := intro_Z. +Notation inj_minus1 := inj_minus1. +Notation inj_minus2 := inj_minus2. +Notation dec_eq := dec_eq. +Notation dec_Zne := dec_Zne. +Notation dec_Zle := dec_Zle. +Notation dec_Zgt := dec_Zgt. +Notation dec_Zge := dec_Zge. +Notation dec_Zlt := dec_Zlt. +Notation dec_eq_nat := dec_eq_nat. +Notation not_Zge := not_Zge. +Notation not_Zlt := not_Zlt. +Notation not_Zle := not_Zle. +Notation not_Zgt := not_Zgt. +Notation not_Zeq := not_Zeq. +Notation Zopp_one := Zopp_one. +Notation Zopp_Zmult_r := Zopp_Zmult_r. +Notation Zmult_Zopp_left := Zmult_Zopp_left. +Notation Zopp_Zmult_l := Zopp_Zmult_l. +Notation Zcompare_Zplus_compatible2 := Zcompare_Zplus_compatible2. +Notation Zcompare_Zmult_compatible := Zcompare_Zmult_compatible. +Notation Zmult_eq := Zmult_eq. +Notation Z_eq_mult := Z_eq_mult. +Notation Zmult_le := Zmult_le. +Notation Zle_ZERO_mult := Zle_ZERO_mult. +Notation Zgt_ZERO_mult := Zgt_ZERO_mult. +Notation Zle_mult := Zle_mult. +Notation Zmult_lt := Zmult_lt. +Notation Zmult_gt := Zmult_gt. +Notation Zle_Zmult_pos_right := Zle_Zmult_pos_right. +Notation Zle_Zmult_pos_left := Zle_Zmult_pos_left. +Notation Zge_Zmult_pos_right := Zge_Zmult_pos_right. +Notation Zge_Zmult_pos_left := Zge_Zmult_pos_left. +Notation Zge_Zmult_pos_compat := Zge_Zmult_pos_compat. +Notation Zle_mult_simpl := Zle_mult_simpl. +Notation Zge_mult_simpl := Zge_mult_simpl. +Notation Zgt_mult_simpl := Zgt_mult_simpl. +Notation Zgt_square_simpl := Zgt_square_simpl. +]. diff --git a/theories7/ZArith/fast_integer.v b/theories7/ZArith/fast_integer.v new file mode 100644 index 00000000..7e3fe306 --- /dev/null +++ b/theories7/ZArith/fast_integer.v @@ -0,0 +1,191 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* positive;y:positive](times x y). +Notation times1_convert := + [x,y:positive;_:positive->positive](times_convert x y). + +Notation Z := Z. +Notation POS := POS. +Notation NEG := NEG. +Notation ZERO := ZERO. +Notation Zero_left := Zero_left. +Notation Zopp_Zopp := Zopp_Zopp. +Notation Zero_right := Zero_right. +Notation Zplus_inverse_r := Zplus_inverse_r. +Notation Zopp_Zplus := Zopp_Zplus. +Notation Zplus_sym := Zplus_sym. +Notation Zplus_inverse_l := Zplus_inverse_l. +Notation Zopp_intro := Zopp_intro. +Notation Zopp_NEG := Zopp_NEG. +Notation weak_assoc := weak_assoc. +Notation Zplus_assoc := Zplus_assoc. +Notation Zplus_simpl := Zplus_simpl. +Notation Zmult_sym := Zmult_sym. +Notation Zmult_assoc := Zmult_assoc. +Notation Zmult_one := Zmult_one. +Notation lt_mult_left := lt_mult_left. (* Mult*) +Notation Zero_mult_left := Zero_mult_left. +Notation Zero_mult_right := Zero_mult_right. +Notation Zopp_Zmult := Zopp_Zmult. +Notation Zmult_Zopp_Zopp := Zmult_Zopp_Zopp. +Notation weak_Zmult_plus_distr_r := weak_Zmult_plus_distr_r. +Notation Zmult_plus_distr_r := Zmult_plus_distr_r. +Notation Zcompare_EGAL := Zcompare_EGAL. +Notation Zcompare_ANTISYM := Zcompare_ANTISYM. +Notation le_minus := le_minus. +Notation Zcompare_Zopp := Zcompare_Zopp. +Notation weaken_Zcompare_Zplus_compatible := weaken_Zcompare_Zplus_compatible. +Notation weak_Zcompare_Zplus_compatible := weak_Zcompare_Zplus_compatible. +Notation Zcompare_Zplus_compatible := Zcompare_Zplus_compatible. +Notation Zcompare_trans_SUPERIEUR := Zcompare_trans_SUPERIEUR. +Notation SUPERIEUR_POS := SUPERIEUR_POS. +Export Datatypes. +Export BinPos. +Export BinNat. +Export BinInt. +Export Zcompare. +Export Mult. +]. diff --git a/theories7/ZArith/zarith_aux.v b/theories7/ZArith/zarith_aux.v new file mode 100644 index 00000000..cd67d46b --- /dev/null +++ b/theories7/ZArith/zarith_aux.v @@ -0,0 +1,163 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(*