From 3c3dd85abc893f5eb428a878a4bc86ff53327e3a Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 12 Nov 2003 19:19:12 +0000 Subject: Ajout lemmes; independance vis a vis noms variables liees git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4871 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/ZArith/Wf_Z.v | 26 ++++---- theories/ZArith/ZArith_dec.v | 123 ++++++++++++++++++++++++++++++++++-- theories/ZArith/Zabs.v | 79 ++++++++++++++++++------ theories/ZArith/Zeven.v | 22 +++---- theories/ZArith/Zmin.v | 32 +++++++++- theories/ZArith/Zmisc.v | 144 +++---------------------------------------- 6 files changed, 240 insertions(+), 186 deletions(-) diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v index 452855a116..4d11f92b04 100644 --- a/theories/ZArith/Wf_Z.v +++ b/theories/ZArith/Wf_Z.v @@ -8,12 +8,12 @@ (*i $Id$ i*) -Require fast_integer. +Require BinInt. +Require Zcompare. Require Zorder. -Require zarith_aux. -Require auxiliary. -Require Zsyntax. +Require Znat. Require Zmisc. +Require Zsyntax. Require Wf_nat. V7only [Import Z_scope.]. Open Local Scope Z_scope. @@ -38,7 +38,7 @@ Open Local Scope Z_scope. Lemma inject_nat_complete : (x:Z)`0 <= x` -> (EX n:nat | x=(inject_nat n)). -NewDestruct x; Intros; +Intro x; NewDestruct x; Intros; [ Exists O; Auto with arith | Specialize (ZL4 p); Intros Hp; Elim Hp; Intros; Exists (S x); Intros; Simpl; @@ -53,18 +53,18 @@ NewDestruct x; Intros; Qed. Lemma ZL4_inf: (y:positive) { h:nat | (convert y)=(S h) }. -Induction y; [ - Intros p H;Elim H; Intros x H1; Exists (plus (S x) (S x)); +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 -| Intros p H1;Elim H1;Intros x H2; Exists (plus x (S x)); Unfold convert; +| 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)) }. -NewDestruct x; Intros; +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; @@ -81,7 +81,7 @@ Qed. Lemma inject_nat_prop : (P:Z->Prop)((n:nat)(P (inject_nat n))) -> (x:Z) `0 <= x` -> (P x). -Intros. +Intros P H x H0. Specialize (inject_nat_complete x H0). Intros Hn; Elim Hn; Intros. Rewrite -> H1; Apply H. @@ -90,7 +90,7 @@ Qed. Lemma inject_nat_set : (P:Z->Set)((n:nat)(P (inject_nat n))) -> (x:Z) `0 <= x` -> (P x). -Intros. +Intros P H x H0. Specialize (inject_nat_complete_inf x H0). Intros Hn; Elim Hn; Intros. Rewrite -> p; Apply H. @@ -106,7 +106,7 @@ 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; Apply inject_nat_prop; +Intros P H H0 x H1; Apply inject_nat_prop; [ Induction n; [ Simpl; Assumption | Intros; Rewrite -> (inj_S n0); @@ -117,7 +117,7 @@ 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; Apply inject_nat_set; +Intros P H H0 x H1; Apply inject_nat_set; [ Induction n; [ Simpl; Assumption | Intros; Rewrite -> (inj_S n0); diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v index 5507acdb29..e8f83fe1a1 100644 --- a/theories/ZArith/ZArith_dec.v +++ b/theories/ZArith/ZArith_dec.v @@ -10,10 +10,9 @@ Require Sumbool. -Require fast_integer. +Require BinInt. Require Zorder. -Require zarith_aux. -Require auxiliary. +Require Zcompare. Require Zsyntax. V7only [Import Z_scope.]. Open Local Scope Z_scope. @@ -35,11 +34,12 @@ 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. @@ -50,6 +50,8 @@ 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. @@ -91,6 +93,15 @@ 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. @@ -108,7 +119,6 @@ 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. @@ -118,9 +128,110 @@ 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. diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v index d3d3efac11..a4968b4187 100644 --- a/theories/ZArith/Zabs.v +++ b/theories/ZArith/Zabs.v @@ -10,7 +10,8 @@ (** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) Require Arith. -Require fast_integer. +Require BinPos. +Require BinInt. Require Zorder. V7only [Import nat_scope.]. @@ -20,33 +21,84 @@ Open Local Scope Z_scope. (** Properties of absolute value *) Lemma Zabs_eq : (x:Z) (Zle ZERO x) -> (Zabs x)=x. -NewDestruct x; Auto with arith. +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. -NewDestruct x; Auto with arith. +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. + +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. -NewDestruct x;Auto with arith. +Intro x; NewDestruct x;Auto with arith. Defined. Lemma Zabs_pos : (x:Z)(Zle ZERO (Zabs x)). -NewDestruct x;Auto with arith; Compute; Intros H;Inversion H. +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. -NewDestruct x; Rewrite Zmult_sym; Auto with arith. +Intro x; NewDestruct x; Rewrite Zmult_sym; Auto with arith. Qed. Lemma Zabs_Zsgn: (x:Z)(Zmult (Zabs x) (Zsgn x))=x. Proof. -NewDestruct x; Rewrite Zmult_sym; Auto with arith. +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 *) @@ -70,16 +122,3 @@ Compute. Intro H0. Discriminate H0. Intuition. Intros. Absurd (Zle ZERO (NEG p)). Compute. Auto with arith. Intuition. Qed. - -Lemma Zlt_minus : (n,m:Z)(Zlt ZERO m)->(Zlt (Zminus n m) n). -Proof. -Intros n m H; Apply Zsimpl_lt_plus_l with p:=m; Rewrite Zle_plus_minus; -Pattern 1 n ;Rewrite <- (Zero_right n); Rewrite (Zplus_sym m n); -Apply Zlt_reg_l; Assumption. -Qed. - -Lemma Zlt_O_minus_lt : (n,m:Z)(Zlt ZERO (Zminus n m))->(Zlt m n). -Proof. -Intros n m H; Apply Zsimpl_lt_plus_l with p:=(Zopp m); Rewrite Zplus_inverse_l; -Rewrite Zplus_sym;Exact H. -Qed. diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v index 38cefa520f..e22dc20f65 100644 --- a/theories/ZArith/Zeven.v +++ b/theories/ZArith/Zeven.v @@ -8,11 +8,11 @@ (*i $Id$ i*) -Require fast_integer. +Require BinInt. Require Zsyntax. (**********************************************************************) -(** Even and odd predicates on Z, division by 2 on Z *) +(** About parity: even and odd predicates on Z, division by 2 on Z *) (**********************************************************************) (** [Zeven], [Zodd], [Zdiv2] and their related properties *) @@ -78,35 +78,35 @@ Defined. Lemma Zeven_not_Zodd : (z:Z)(Zeven z) -> ~(Zodd z). Proof. - NewDestruct z; [ Idtac | NewDestruct p | NewDestruct p ]; Compute; Trivial. + Intro z; NewDestruct z; [ Idtac | NewDestruct p | NewDestruct p ]; Compute; Trivial. Qed. Lemma Zodd_not_Zeven : (z:Z)(Zodd z) -> ~(Zeven z). Proof. - NewDestruct z; [ Idtac | NewDestruct p | NewDestruct p ]; Compute; Trivial. + Intro z; NewDestruct z; [ Idtac | NewDestruct p | NewDestruct p ]; Compute; Trivial. Qed. Lemma Zeven_Sn : (z:Z)(Zodd z) -> (Zeven (Zs z)). Proof. - NewDestruct z; Unfold Zs; [ Idtac | NewDestruct p | NewDestruct p ]; Simpl; Trivial. + 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. - NewDestruct z; Unfold Zs; [ Idtac | NewDestruct p | NewDestruct p ]; Simpl; Trivial. + 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. - NewDestruct z; Unfold Zpred; [ Idtac | NewDestruct p | NewDestruct p ]; Simpl; Trivial. + 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. - NewDestruct z; Unfold Zpred; [ Idtac | NewDestruct p | NewDestruct p ]; Simpl; Trivial. + Intro z; NewDestruct z; Unfold Zpred; [ Idtac | NewDestruct p | NewDestruct p ]; Simpl; Trivial. Unfold double_moins_un; Case p; Simpl; Auto. Qed. @@ -127,7 +127,7 @@ Definition Zdiv2 := Lemma Zeven_div2 : (x:Z) (Zeven x) -> `x = 2*(Zdiv2 x)`. Proof. -NewDestruct x. +Intro x; NewDestruct x. Auto with arith. NewDestruct p; Auto with arith. Intros. Absurd (Zeven (POS (xI p))); Red; Auto with arith. @@ -139,7 +139,7 @@ Qed. Lemma Zodd_div2 : (x:Z) `x >= 0` -> (Zodd x) -> `x = 2*(Zdiv2 x)+1`. Proof. -NewDestruct x. +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. @@ -148,7 +148,7 @@ Qed. Lemma Zodd_div2_neg : (x:Z) `x <= 0` -> (Zodd x) -> `x = 2*(Zdiv2 x)-1`. Proof. -NewDestruct x. +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. diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v index b09299466d..01192c3bce 100644 --- a/theories/ZArith/Zmin.v +++ b/theories/ZArith/Zmin.v @@ -10,7 +10,8 @@ (** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) Require Arith. -Require fast_integer. +Require BinInt. +Require Zcompare. Require Zorder. Open Local Scope Z_scope. @@ -65,10 +66,37 @@ Qed. Lemma Zmin_plus : (x,y,n:Z)(Zmin (Zplus x n) (Zplus y n))=(Zplus (Zmin x y) n). Proof. -Intros; Unfold Zmin. +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/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v index d6d5cd3d3c..42f4618578 100644 --- a/theories/ZArith/Zmisc.v +++ b/theories/ZArith/Zmisc.v @@ -8,140 +8,14 @@ (*i $Id$ i*) -Require fast_integer. -Require zarith_aux. -Require auxiliary. +Require BinInt. +Require Zcompare. +Require Zorder. Require Zsyntax. Require Bool. V7only [Import Z_scope.]. Open Local Scope Z_scope. -(**********************************************************************) -(** Boolean comparisons of binary integers *) - -Definition Zle_bool := - [x,y:Z]Cases `x ?= y` of SUPERIEUR => 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. 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. 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. 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. 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. 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. - (**********************************************************************) (** Iterators *) @@ -171,7 +45,7 @@ Definition iter := 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 @@ -180,8 +54,8 @@ 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). - -Induction n; +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; @@ -197,8 +71,8 @@ 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)). - -Intros. +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). @@ -212,6 +86,7 @@ Qed. 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]. @@ -220,6 +95,7 @@ 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. -- cgit v1.2.3