# Library Coq.Arith.Wf_nat

``` ```
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 : Type. 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. Defined. Theorem well_founded_gtof : well_founded gtof. 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 :
``` 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. Defined. End Well_founded_Nat. Lemma lt_wf : well_founded lt. 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. Proof.   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. Proof.   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. 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. 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, 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 (q:nat), 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_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.   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. ```
``` ```