diff options
Diffstat (limited to 'theories/Arith')
| -rw-r--r-- | theories/Arith/Wf_nat.v | 93 |
1 files changed, 52 insertions, 41 deletions
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index dd22d493e..b55451233 100644 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -24,16 +24,16 @@ Definition gtof (a b:A) := f b > f a. Theorem well_founded_ltof : well_founded ltof. Proof. -(* forall n (a : A), f a < n -> Acc ltof a *) - - intro a; assert (H: f a <= f a) by trivial with arith. - set (n:=f a) in H at 2. clearbody n. (* - remember (f a) in H at 2. as n. - revert H. generalize (f a) at 2 as n; intros n. revert a. *) induction n in a, H |- *; apply Acc_intro; -(* induction (f a) in a, H at 2 |- *; apply Acc_intro; *) - intros b ltfafb; unfold ltof in ltfafb. - - inversion H as [H0|]. rewrite H0 in ltfafb. inversion ltfafb. - - apply IHn. apply le_S_n, lt_le_trans with (f a); assumption. + red. + cut (forall n (a:A), f a < n -> Acc ltof a). + intros H a; apply (H (S (f a))); auto with arith. + induction n. + intros; absurd (f a < 0); auto with arith. + intros a ltSma. + apply Acc_intro. + unfold ltof; intros b ltfafb. + apply IHn. + apply lt_le_trans with (f a); auto with arith. Defined. Theorem well_founded_gtof : well_founded gtof. @@ -67,11 +67,15 @@ Theorem induction_ltof1 : forall P:A -> Set, (forall x:A, (forall y:A, ltof y x -> P y) -> P x) -> forall a:A, P a. Proof. - intros P F a; assert (H : f a < S (f a)) by trivial with arith. - induction (S (f a)) in a, H |- *. - - absurd (f a < 0); auto with arith. - - apply F. intros b ltfafb. apply IHn, le_S_n. - induction H; auto using Le.le_n_S. + intros P F; cut (forall n (a:A), f a < n -> P a). + intros H a; apply (H (S (f a))); auto with arith. + induction n. + intros; absurd (f a < 0); auto with arith. + intros a ltSma. + apply F. + unfold ltof; intros b ltfafb. + apply IHn. + apply lt_le_trans with (f a); auto with arith. Defined. Theorem induction_gtof1 : @@ -104,12 +108,16 @@ Hypothesis H_compat : forall x y:A, R x y -> f x < f y. Theorem well_founded_lt_compat : well_founded R. Proof. - intros a; assert (H : f a < S (f a)) by trivial with arith. - induction (S (f a)) in a, H |- *. - - absurd (f a < 0); auto with arith. - - apply Acc_intro. intros b ltfafb. apply IHn, le_S_n. - apply H_compat in ltfafb. - induction H; auto using Le.le_n_S. + red. + cut (forall n (a:A), f a < n -> Acc R a). + intros H a; apply (H (S (f a))); auto with arith. + induction n. + intros; absurd (f a < 0); auto with arith. + intros a ltSma. + apply Acc_intro. + intros b ltfafb. + apply IHn. + apply lt_le_trans with (f a); auto with arith. Defined. End Well_founded_Nat. @@ -153,7 +161,8 @@ Lemma lt_wf_double_rec : (forall p q, p < n -> P p q) -> (forall p, p < m -> P n p) -> P n m) -> forall n m, P n m. Proof. - intros P Hrec p. destruct p using lt_wf_ind, m using lt_wf_ind. auto. + intros P Hrec p; pattern p; apply lt_wf_rec. + intros n H q; pattern q; apply lt_wf_rec; auto with arith. Defined. Lemma lt_wf_double_ind : @@ -190,7 +199,7 @@ Section LT_WF_REL. Theorem well_founded_inv_lt_rel_compat : well_founded R. Proof. constructor; intros. - destruct (F_compat y a); trivial. + case (F_compat y a); trivial; intros. apply acc_lt_rel; trivial. exists x; trivial. Qed. @@ -222,27 +231,29 @@ Proof. assert (forall n, (exists n', n'<n /\ P n' /\ forall n'', P n'' -> n'<=n'') \/(forall n', P n' -> n<=n')). - { induction n. - - right. intros n' Hn'. apply le_O_n. - - destruct IHn. - + left; destruct H as (n', (Hlt', HPn')). - exists n'; split. - * apply lt_S; assumption. - * assumption. - + destruct (Pdec n). - * left; exists n; split. - apply lt_n_Sn. - split; assumption. - * right. - intros n' Hltn'. - destruct (le_lt_eq_dec n n') as [Hltn| ->]. - apply H; assumption. - assumption. - destruct H0 as []; assumption. } + induction n. + right. + intros n' Hn'. + apply le_O_n. + destruct IHn. + left; destruct H as (n', (Hlt', HPn')). + exists n'; split. + apply lt_S; assumption. + assumption. + destruct (Pdec n). + left; exists n; split. + apply lt_n_Sn. + split; assumption. + right. + intros n' Hltn'. + destruct (le_lt_eq_dec n n') as [Hltn|Heqn]. + apply H; assumption. + assumption. + destruct H0. + rewrite Heqn; assumption. destruct (H n0) as [(n,(Hltn,(Hmin,Huniqn)))|]; [exists n | exists n0]; repeat split; assumption || intros n' (HPn',Hminn'); apply le_antisym; auto. - Qed. Unset Implicit Arguments. |