diff options
Diffstat (limited to 'theories/Arith/Wf_nat.v')
-rw-r--r--[-rwxr-xr-x] | theories/Arith/Wf_nat.v | 200 |
1 files changed, 103 insertions, 97 deletions
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index 8bf237b5..11fcd161 100755..100644 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Wf_nat.v,v 1.16.2.1 2004/07/16 19:31:01 herbelin Exp $ i*) +(*i $Id: Wf_nat.v 9341 2006-11-06 13:08:10Z notin $ i*) (** Well-founded relations and natural numbers *) @@ -18,7 +18,7 @@ Implicit Types m n p : nat. Section Well_founded_Nat. -Variable A : Set. +Variable A : Type. Variable f : A -> nat. Definition ltof (a b:A) := f a < f b. @@ -26,72 +26,77 @@ Definition gtof (a b:A) := f b > f a. Theorem well_founded_ltof : well_founded ltof. Proof. -red in |- *. -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 in |- *; intros b ltfafb. -apply IHn. -apply lt_le_trans with (f a); auto with arith. -Qed. + red in |- *. + 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 in |- *; intros b ltfafb. + apply IHn. + apply lt_le_trans with (f a); auto with arith. +Defined. Theorem well_founded_gtof : well_founded gtof. -Proof well_founded_ltof. +Proof. + exact well_founded_ltof. +Defined. (** It is possible to directly prove the induction principle going back to primitive recursion on natural numbers ([induction_ltof1]) or to use the previous lemmas to extract a program with a fixpoint ([induction_ltof2]) -the ML-like program for [induction_ltof1] is : [[ +the ML-like program for [induction_ltof1] is : +[[ let induction_ltof1 F a = indrec ((f a)+1) a where rec indrec = function 0 -> (function a -> error) |(S m) -> (function a -> (F a (function y -> indrec y m)));; ]] -the ML-like program for [induction_ltof2] is : [[ +the ML-like program for [induction_ltof2] is : +[[ let induction_ltof2 F a = indrec a where rec indrec a = F a indrec;; -]] *) +]] +*) 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. + 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 in |- *; intros b ltfafb. -apply IHn. -apply lt_le_trans with (f a); auto with arith. + 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 in |- *; intros b ltfafb. + apply IHn. + apply lt_le_trans with (f a); auto with arith. Defined. Theorem induction_gtof1 : - forall P:A -> Set, - (forall x:A, (forall y:A, gtof y x -> P y) -> P x) -> forall a:A, P a. + forall P:A -> Set, + (forall x:A, (forall y:A, gtof y x -> P y) -> P x) -> forall a:A, P a. Proof. -exact induction_ltof1. + exact induction_ltof1. Defined. Theorem induction_ltof2 : - forall P:A -> Set, - (forall x:A, (forall y:A, ltof y x -> P y) -> P x) -> forall a:A, P a. + forall P:A -> Set, + (forall x:A, (forall y:A, ltof y x -> P y) -> P x) -> forall a:A, P a. Proof. -exact (well_founded_induction well_founded_ltof). + exact (well_founded_induction well_founded_ltof). Defined. Theorem induction_gtof2 : - forall P:A -> Set, - (forall x:A, (forall y:A, gtof y x -> P y) -> P x) -> forall a:A, P a. + forall P:A -> Set, + (forall x:A, (forall y:A, gtof y x -> P y) -> P x) -> forall a:A, P a. Proof. -exact induction_ltof2. + exact induction_ltof2. Defined. (** If a relation [R] is compatible with [lt] i.e. if [x R y => f(x) < f(y)] @@ -103,104 +108,105 @@ Hypothesis H_compat : forall x y:A, R x y -> f x < f y. Theorem well_founded_lt_compat : well_founded R. Proof. -red in |- *. -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. -Qed. + red in |- *. + 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. Lemma lt_wf : well_founded lt. -Proof well_founded_ltof nat (fun m => m). +Proof. + exact (well_founded_ltof nat (fun m => m)). +Defined. Lemma lt_wf_rec1 : - forall n (P:nat -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n. + forall n (P:nat -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n. Proof. -exact - (fun p (P:nat -> Set) (F:forall n, (forall m, m < n -> P m) -> P n) => - induction_ltof1 nat (fun m => m) P F p). + exact (fun p P F => induction_ltof1 nat (fun m => m) P F p). Defined. Lemma lt_wf_rec : - forall n (P:nat -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n. + forall n (P:nat -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n. Proof. -exact - (fun p (P:nat -> Set) (F:forall n, (forall m, m < n -> P m) -> P n) => - induction_ltof2 nat (fun m => m) P F p). + exact (fun p P F => induction_ltof2 nat (fun m => m) P F p). Defined. Lemma lt_wf_ind : - forall n (P:nat -> Prop), (forall n, (forall m, m < n -> P m) -> P n) -> P n. -intro p; intros; elim (lt_wf p); auto with arith. + forall n (P:nat -> Prop), (forall n, (forall m, m < n -> P m) -> P n) -> P n. +Proof. + intro p; intros; elim (lt_wf p); auto with arith. Qed. Lemma gt_wf_rec : - forall n (P:nat -> Set), (forall n, (forall m, n > m -> P m) -> P n) -> P n. + forall n (P:nat -> Set), (forall n, (forall m, n > m -> P m) -> P n) -> P n. Proof. -exact lt_wf_rec. + exact lt_wf_rec. Defined. Lemma gt_wf_ind : - forall n (P:nat -> Prop), (forall n, (forall m, n > m -> P m) -> P n) -> P n. + forall n (P:nat -> Prop), (forall n, (forall m, n > m -> P m) -> P n) -> P n. Proof lt_wf_ind. Lemma lt_wf_double_rec : forall P:nat -> nat -> Set, (forall n m, - (forall p (q:nat), p < n -> P p q) -> - (forall p, p < m -> P n p) -> P n m) -> forall n m, P n m. -intros P Hrec p; pattern p in |- *; apply lt_wf_rec. -intros n H q; pattern q in |- *; apply lt_wf_rec; auto with arith. + (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; pattern p in |- *; apply lt_wf_rec. + intros n H q; pattern q in |- *; apply lt_wf_rec; auto with arith. Defined. Lemma lt_wf_double_ind : - forall P:nat -> nat -> Prop, - (forall n m, + forall P:nat -> nat -> Prop, + (forall n m, (forall p (q:nat), p < n -> P p q) -> (forall p, p < m -> P n p) -> P n m) -> forall n m, P n m. -intros P Hrec p; pattern p in |- *; apply lt_wf_ind. -intros n H q; pattern q in |- *; apply lt_wf_ind; auto with arith. +Proof. + intros P Hrec p; pattern p in |- *; apply lt_wf_ind. + intros n H q; pattern q in |- *; apply lt_wf_ind; auto with arith. Qed. Hint Resolve lt_wf: arith. Hint Resolve well_founded_lt_compat: arith. Section LT_WF_REL. -Variable A : Set. -Variable R : A -> A -> Prop. - -(* Relational form of inversion *) -Variable F : A -> nat -> Prop. -Definition inv_lt_rel x y := - exists2 n : _, F x n & (forall m, F y m -> n < m). - -Hypothesis F_compat : forall x y:A, R x y -> inv_lt_rel x y. -Remark acc_lt_rel : forall x:A, (exists n : _, F x n) -> Acc R x. -intros x [n fxn]; generalize x fxn; clear x fxn. -pattern n in |- *; apply lt_wf_ind; intros. -constructor; intros. -case (F_compat y x); trivial; intros. -apply (H x0); auto. -Qed. - -Theorem well_founded_inv_lt_rel_compat : well_founded R. -constructor; intros. -case (F_compat y a); trivial; intros. -apply acc_lt_rel; trivial. -exists x; trivial. -Qed. - + Variable A : Set. + Variable R : A -> A -> Prop. + + (* Relational form of inversion *) + Variable F : A -> nat -> Prop. + Definition inv_lt_rel x y := exists2 n, F x n & (forall m, F y m -> n < m). + + Hypothesis F_compat : forall x y:A, R x y -> inv_lt_rel x y. + Remark acc_lt_rel : forall x:A, (exists n, F x n) -> Acc R x. + Proof. + intros x [n fxn]; generalize dependent x. + pattern n in |- *; apply lt_wf_ind; intros. + constructor; intros. + destruct (F_compat y x) as (x0,H1,H2); trivial. + apply (H x0); auto. + Qed. + + Theorem well_founded_inv_lt_rel_compat : well_founded R. + Proof. + constructor; intros. + case (F_compat y a); trivial; intros. + apply acc_lt_rel; trivial. + exists x; trivial. + Qed. 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). -intros; apply (well_founded_inv_lt_rel_compat A (inv_lt_rel A F) F); trivial. -Qed.
\ No newline at end of file + forall (A:Set) (F:A -> nat -> Prop), well_founded (inv_lt_rel A F). + intros; apply (well_founded_inv_lt_rel_compat A (inv_lt_rel A F) F); trivial. +Qed. |