diff options
Diffstat (limited to 'theories/Arith/Wf_nat.v')
-rw-r--r-- | theories/Arith/Wf_nat.v | 87 |
1 files changed, 33 insertions, 54 deletions
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index 05be5e1a3..2cb7c3c09 100644 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -8,7 +8,7 @@ (** Well-founded relations and natural numbers *) -Require Import Lt. +Require Import PeanoNat Lt. Local Open Scope nat_scope. @@ -24,16 +24,12 @@ Definition gtof (a b:A) := f b > f a. Theorem well_founded_ltof : well_founded ltof. Proof. - 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. + assert (H : forall n (a:A), f a < n -> Acc ltof a). + { induction n. + - intros; absurd (f a < 0); auto with arith. + - intros a Ha. apply Acc_intro. unfold ltof at 1. intros b Hb. + apply IHn. apply Nat.lt_le_trans with (f a); auto with arith. } + intros a. apply (H (S (f a))). auto with arith. Defined. Theorem well_founded_gtof : well_founded gtof. @@ -67,15 +63,13 @@ 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; 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. + intros P F. + assert (H : forall n (a:A), f a < n -> P a). + { induction n. + - intros; absurd (f a < 0); auto with arith. + - intros a Ha. apply F. unfold ltof. intros b Hb. + apply IHn. apply Nat.lt_le_trans with (f a); auto with arith. } + intros a. apply (H (S (f a))). auto with arith. Defined. Theorem induction_gtof1 : @@ -108,16 +102,12 @@ Hypothesis H_compat : forall x y:A, R x y -> f x < f y. Theorem well_founded_lt_compat : well_founded R. Proof. - 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. + assert (H : forall n (a:A), f a < n -> Acc R a). + { induction n. + - intros; absurd (f a < 0); auto with arith. + - intros a Ha. apply Acc_intro. intros b Hb. + apply IHn. apply Nat.lt_le_trans with (f a); auto with arith. } + intros a. apply (H (S (f a))). auto with arith. Defined. End Well_founded_Nat. @@ -208,6 +198,7 @@ End LT_WF_REL. Lemma well_founded_inv_rel_inv_lt_rel : forall (A:Set) (F:A -> nat -> Prop), well_founded (inv_lt_rel A F). +Proof. intros; apply (well_founded_inv_lt_rel_compat A (inv_lt_rel A F) F); trivial. Qed. @@ -230,30 +221,18 @@ Proof. intros P Pdec (n0,HPn0). 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|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. + \/ (forall n', P n' -> n<=n')). + { induction n. + - right. intros. apply Nat.le_0_l. + - destruct IHn as [(n' & IH1 & IH2)|IH]. + + left. exists n'; auto with arith. + + destruct (Pdec n) as [HP|HP]. + * left. exists n; auto with arith. + * right. intros n' Hn'. + apply Nat.le_neq; split; auto. intros <-. auto. } + destruct (H n0) as [(n & H1 & H2 & H3)|H0]; [exists n | exists n0]; + repeat split; trivial; + intros n' (HPn',Hn'); apply Nat.le_antisymm; auto. Qed. Unset Implicit Arguments. |