diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-05 13:57:03 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-05 13:57:03 +0000 |
commit | 0f325db9852325d558a0a8ca49cf8da52b1774e1 (patch) | |
tree | 85968c4aedef698211a03497b61f069bc3305aa1 | |
parent | 52afa10317195c2aa24a802c624043f4bfd3ef4c (diff) |
principes de récurrences plus efficaces pour l'extraction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4309 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | theories/ZArith/Wf_Z.v | 99 |
1 files changed, 29 insertions, 70 deletions
diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v index c303b6fe7..56f8485da 100644 --- a/theories/ZArith/Wf_Z.v +++ b/theories/ZArith/Wf_Z.v @@ -124,26 +124,22 @@ Intros; Apply inject_nat_set; | Assumption]. Qed. -Section natlike_rec2. +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=(Zpred b)`. +Local R := [a,b:Z]`0<=a`/\`a<b`. Local R_wf : (well_founded Z R). Proof. LetTac f := [z]Cases z of (POS p) => (convert p) | ZERO => O | (NEG _) => O end. Apply well_founded_lt_compat with f. -Unfold R f. -Intros x y; Case x. -Intuition; Rewrite (Zs_pred y); Rewrite <- H1; Simpl; Apply compare_convert_O. -Case y; Intuition; Try Solve [ Simpl in H2; Inversion H2 ]. -Assert (POS p) = (POS (add_un p0)). - Rewrite add_un_Zs; Rewrite H2; Auto with zarith. -Inversion_clear H0; Unfold convert; Rewrite convert_add_un. -Change 1 (positive_to_nat p0 (1)) with (plus (0) (positive_to_nat p0 (1))). -Apply lt_reg_r; Auto. -Intuition; Elim H1; Simpl; Trivial. +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`) -> @@ -158,11 +154,12 @@ Apply Zlt_ZERO_pred_le_ZERO; Unfold Zlt; Simpl; Trivial. Rewrite Zs_pred. Apply Hrec. Auto. -Apply X; Unfold R; Intuition. +Apply X; Auto; Unfold R; Intuition; Apply Zlt_pred_n_n. Intros; Elim H; Simpl; Trivial. Qed. -(** variant using [Zpred] instead of [Zs] *) +(** A variant of the previous using [Zpred] instead of [Zs]. *) + Lemma natlike_rec3 : (P:Z->Type)(P `0`) -> ((z:Z)`0<z` -> (P (Zpred z)) -> (P z)) -> (z:Z)`0<=z` -> (P z). Proof. @@ -170,72 +167,34 @@ 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; Simpl; Trivial. +Unfold Zlt; Trivial. Assert `0<=(Zpred (POS p))`. Apply Zlt_ZERO_pred_le_ZERO; Unfold Zlt; Simpl; Trivial. -Apply X; Unfold R; Intuition. +Apply X; Auto; Unfold R; Intuition; Apply Zlt_pred_n_n. Intros; Elim H; Simpl; Trivial. Qed. -End natlike_rec2. +(** A more general induction principal using [Zlt]. *) -Lemma Z_lt_induction : - (P:Z->Prop) - ((x:Z)((y:Z)`0 <= y < x`->(P y))->(P x)) - -> (x:Z)`0 <= x`->(P x). +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 H x Hx. -Cut (x:Z)`0 <= x`->(y:Z)`0 <= y < x`->(P y). -Intro. -Apply (H0 (Zs x)). -Auto with zarith. +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. +Ground. +Unfold Zle Zcompare in H; Elim H; Auto. +Defined. -Split; [ Assumption | Exact (Zlt_n_Sn x) ]. - -Intros x0 Hx0; Generalize Hx0; Pattern x0; Apply natlike_ind. -Intros. -Absurd `0 <= 0`; Try Assumption. -Apply Zgt_not_le. -Apply Zgt_le_trans with m:=y. -Apply Zlt_gt. -Intuition. Intuition. - -Intros. Apply H. Intros. -Apply (H1 H0). -Split; [ Intuition | Idtac ]. -Apply Zlt_le_trans with y. Intuition. -Apply Zgt_S_le. Apply Zlt_gt. Intuition. - -Assumption. -Qed. - -Lemma Z_lt_rec : - (P:Z->Set) +Lemma Z_lt_induction : + (P:Z->Prop) ((x:Z)((y:Z)`0 <= y < x`->(P y))->(P x)) -> (x:Z)`0 <= x`->(P x). Proof. -Intros P H x Hx. -Cut (x:Z)`0 <= x`->(y:Z)`0 <= y < x`->(P y). -Intro. -Apply (H0 (Zs x)). -Auto with zarith. - -Split; [ Assumption | Exact (Zlt_n_Sn x) ]. - -Intros x0 Hx0; Generalize Hx0; Pattern x0; Apply natlike_rec2. -Intros. -Absurd `0 <= 0`; Try Assumption. -Apply Zgt_not_le. -Apply Zgt_le_trans with m:=y. -Apply Zlt_gt. -Intuition. Intuition. - -Intros. Apply H. Intros. -Apply (H1 H0). -Split; [ Intuition | Idtac ]. -Apply Zlt_le_trans with y. Intuition. -Apply Zgt_S_le. Apply Zlt_gt. Intuition. - -Assumption. +Exact Z_lt_rec. Qed. +End Efficient_Rec. |