diff options
Diffstat (limited to 'theories/Arith/Wf_nat.v')
| -rwxr-xr-x | theories/Arith/Wf_nat.v | 206 |
1 files changed, 206 insertions, 0 deletions
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v new file mode 100755 index 00000000..8bf237b5 --- /dev/null +++ b/theories/Arith/Wf_nat.v @@ -0,0 +1,206 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * 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*) + +(** Well-founded relations and natural numbers *) + +Require Import Lt. + +Open Local Scope nat_scope. + +Implicit Types m n p : nat. + +Section Well_founded_Nat. + +Variable A : Set. + +Variable f : A -> nat. +Definition ltof (a b:A) := f a < f b. +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. + +Theorem well_founded_gtof : well_founded gtof. +Proof well_founded_ltof. + +(** 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 : [[ + 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 : [[ + 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. +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. +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. +Proof. +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. +Proof. +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. +Proof. +exact induction_ltof2. +Defined. + +(** If a relation [R] is compatible with [lt] i.e. if [x R y => f(x) < f(y)] + then [R] is well-founded. *) + +Variable R : A -> A -> Prop. + +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. + +End Well_founded_Nat. + +Lemma lt_wf : well_founded lt. +Proof well_founded_ltof nat (fun m => m). + +Lemma lt_wf_rec1 : + 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). +Defined. + +Lemma lt_wf_rec : + 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). +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. +Qed. + +Lemma gt_wf_rec : + forall n (P:nat -> Set), (forall n, (forall m, n > m -> P m) -> P n) -> P n. +Proof. +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. +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. +Defined. + +Lemma lt_wf_double_ind : + 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. +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. + + +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 |