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
Section FixPoint.
Variable P :
A ->
Type.
Variable F :
forall x:A, (
forall y:A,
R y x ->
P y) ->
P x.
Fixpoint Fix_F (
x:A) (
a:Acc
x) {
struct a} :
P x :=
F (
fun (
y:A) (
h:R
y x) =>
Fix_F (
Acc_inv a h)).
Scheme Acc_inv_dep :=
Induction for Acc Sort Prop.
Lemma Fix_F_eq :
forall (
x:A) (
r:Acc
x),
F (
fun (
y:A) (
p:R
y x) =>
Fix_F (
x:=y) (
Acc_inv r p)) =
Fix_F (
x:=x)
r.
Definition Fix (
x:A) :=
Fix_F (
Rwf x).
Proof that well_founded_induction satisfies the fixpoint equation.
It requires an extra property of the functional
Hypothesis
F_ext :
forall (
x:A) (
f g:forall
y:A,
R y x ->
P y),
(
forall (
y:A) (
p:R
y x),
f y p =
g y p) ->
F f =
F g.
Lemma Fix_F_inv :
forall (
x:A) (
r s:Acc
x),
Fix_F r =
Fix_F s.
Lemma Fix_eq :
forall x:A,
Fix x =
F (
fun (
y:A) (
p:R
y x) =>
Fix y).
End FixPoint.
End Well_founded.
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')) {
struct a} :
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).