Library Coq.Wellfounded.Well_Ordering
Author: Cristina Cornes. From: Constructing Recursion Operators in Type Theory L. Paulson JSC (1986) 2, 325-355
Require
Import
Eqdep
.
Section
WellOrdering
.
Variable
A
:
Type
.
Variable
B
:
A
->
Type
.
Inductive
WO
:
Type
:=
sup
:
forall
(
a
:
A
) (
f
:
B
a
->
WO
),
WO
.
Inductive
le_WO
:
WO
->
WO
->
Prop
:=
le_sup
:
forall
(
a
:
A
) (
f
:
B
a
->
WO
) (
v
:
B
a
),
le_WO
(
f
v
) (
sup
a
f
).
Theorem
wf_WO
:
well_founded
le_WO
.
End
WellOrdering
.
Section
Characterisation_wf_relations
.
Wellfounded relations are the inverse image of wellordering types
Variable
A
:
Type
.
Variable
leA
:
A
->
A
->
Prop
.
Definition
B
(
a
:
A
) :=
{
x
:
A
|
leA
x
a
}
.
Definition
wof
:
well_founded
leA
->
A
->
WO
A
B
.
End
Characterisation_wf_relations
.