| 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.
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.