diff options
Diffstat (limited to 'theories/Arith/Wf_nat.v')
| -rw-r--r-- | theories/Arith/Wf_nat.v | 93 |
1 files changed, 35 insertions, 58 deletions
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index 8cd195f8..64764830 100644 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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,34 +221,20 @@ 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. -Notation iter_nat := @nat_iter (only parsing). -Notation iter_nat_plus := @nat_iter_plus (only parsing). -Notation iter_nat_invariant := @nat_iter_invariant (only parsing). +Notation iter_nat n A f x := (nat_rect (fun _ => A) x (fun _ => f) n) (only parsing). |