Library Coq.Arith.Wf_nat
Well-founded relations and natural numbers
Require Import PeanoNat.
Local Open 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.
Register well_founded_ltof as num.nat.well_founded_ltof.
Theorem well_founded_gtof : well_founded gtof.
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 F a =
let rec indrec n k =
match n with
| O -> error
| S m -> F k (indrec m)
in indrec (f a + 1) a
the ML-like program for induction_ltof2 is :
let induction_ltof2 F a = indrec a
where rec indrec a = F a indrec;;
let induction_ltof1 f F a =
let rec indrec n k =
match n with
| O -> error
| S m -> F k (indrec m)
in indrec (f a + 1) a
let induction_ltof2 F a = indrec a
where rec indrec a = F a indrec;;
Theorem induction_ltof1 :
forall P:A -> Type,
(forall x:A, (forall y:A, ltof y x -> P y) -> P x) -> forall a:A, P a.
Theorem induction_gtof1 :
forall P:A -> Type,
(forall x:A, (forall y:A, gtof y x -> P y) -> P x) -> forall a:A, P a.
Theorem induction_ltof2 :
forall P:A -> Type,
(forall x:A, (forall y:A, ltof y x -> P y) -> P x) -> forall a:A, P a.
Theorem induction_gtof2 :
forall P:A -> Type,
(forall x:A, (forall y:A, gtof y x -> P y) -> P x) -> forall a:A, P a.
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.
End Well_founded_Nat.
Lemma lt_wf : well_founded lt.
Lemma lt_wf_rect1 :
forall n (P:nat -> Type), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
Lemma lt_wf_rect :
forall n (P:nat -> Type), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
Lemma lt_wf_rec1 :
forall n (P:nat -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
Lemma lt_wf_rec :
forall n (P:nat -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
Lemma lt_wf_ind :
forall n (P:nat -> Prop), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
Lemma gt_wf_rect :
forall n (P:nat -> Type), (forall n, (forall m, n > m -> P m) -> P n) -> P n.
Lemma gt_wf_rec :
forall n (P:nat -> Set), (forall n, (forall m, n > m -> P m) -> P n) -> P n.
Lemma gt_wf_ind :
forall n (P:nat -> Prop), (forall n, (forall m, n > m -> P m) -> P n) -> P n.
Lemma lt_wf_double_rect :
forall P:nat -> nat -> Type,
(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.
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.
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.
#[global]
Hint Resolve lt_wf: arith.
#[global]
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.
Theorem well_founded_inv_lt_rel_compat : well_founded R.
End LT_WF_REL.
Lemma well_founded_inv_rel_inv_lt_rel (A:Set) (F:A -> nat -> Prop) :
well_founded (inv_lt_rel A F).
A constructive proof that any non empty decidable subset of
natural numbers has a least element
Set Implicit Arguments.
Require Import Compare_dec.
Require Import Decidable.
Definition has_unique_least_element (A:Type) (R:A->A->Prop) (P:A->Prop) :=
exists! x, P x /\ forall x', P x' -> R x x'.
Lemma dec_inh_nat_subset_has_unique_least_element :
forall P:nat->Prop, (forall n, P n \/ ~ P n) ->
(exists n, P n) -> has_unique_least_element le P.
Unset Implicit Arguments.
Notation iter_nat n A f x := (nat_rect (fun _ => A) x (fun _ => f) n) (only parsing).
Require Import Le Lt.