Library Coq.Arith.Wf_nat
Well-founded relations and natural numbers
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;;
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.
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.
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.
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.
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_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_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_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.
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.
Theorem well_founded_inv_lt_rel_compat :
well_founded R.
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).
A constructive proof that any non empty decidable subset of
natural numbers has a least element
nth iteration of the function f