Library Coq.Init.Wf
This module proves the validity of
- well-founded recursion (also known as course of values)
- well-founded induction
from a well-founded ordering on a given set
Well-founded induction principle on Prop
The accessibility predicate is defined to be non-informative (Acc_rect is automatically defined because Acc is a singleton type)
A relation is well-founded if every element is accessible
Well-founded induction on Set and Prop
Hypothesis Rwf :
well_founded.
Theorem well_founded_induction_type :
forall P:
A -> Type,
(forall x:
A,
(forall y:
A,
R y x -> P y) -> P x) -> forall a:
A,
P a.
Theorem well_founded_induction :
forall P:
A -> Set,
(forall x:
A,
(forall y:
A,
R y x -> P y) -> P x) -> forall a:
A,
P a.
Theorem well_founded_ind :
forall P:
A -> Prop,
(forall x:
A,
(forall y:
A,
R y x -> P y) -> P x) -> forall a:
A,
P a.
Well-founded fixpoints
Proof that well_founded_induction satisfies the fixpoint equation.
It requires an extra property of the functional
Well-founded fixpoints over pairs
Section Well_founded_2.
Variables A B :
Type.
Variable R :
A * B -> A * B -> Prop.
Variable P :
A -> B -> Type.
Section FixPoint_2.
Variable
F :
forall (
x:
A) (
x':
B),
(forall (
y:
A) (
y':
B),
R (y, y') (x, x') -> P y y') -> P x x'.
Fixpoint Fix_F_2 (
x:
A) (
x':
B) (
a:
Acc R (x, x')) :
P x x' :=
F
(
fun (
y:
A) (
y':
B) (
h:
R (y, y') (x, x')) =>
Fix_F_2 (
x:=
y) (
x':=
y') (
Acc_inv a (y,y') h)).
End FixPoint_2.
Hypothesis Rwf :
well_founded R.
Theorem well_founded_induction_type_2 :
(forall (
x:
A) (
x':
B),
(forall (
y:
A) (
y':
B),
R (y, y') (x, x') -> P y y') -> P x x') ->
forall (
a:
A) (
b:
B),
P a b.
End Well_founded_2.
Notation Acc_iter :=
Fix_F (
only parsing).
Notation Acc_iter_2 :=
Fix_F_2 (
only parsing).
Section Acc_generator.
Variable A :
Type.
Variable R :
A -> A -> Prop.
Fixpoint Acc_intro_generator n (
wf :
well_founded R) :=
match n with
|
O =>
wf
|
S n =>
fun x =>
Acc_intro x (
fun y _ =>
Acc_intro_generator n (
Acc_intro_generator n wf)
y)
end.
End Acc_generator.