Library Coq.Wellfounded.Inverse_Image
Author: Bruno Barras
Section
Inverse_Image
.
Variables
A
B
:
Type
.
Variable
R
:
B
->
B
->
Prop
.
Variable
f
:
A
->
B
.
Let
Rof
(
x
y
:
A
) :
Prop
:=
R
(
f
x
) (
f
y
).
Remark
Acc_lemma
:
forall
y
:
B
,
Acc
R
y
->
forall
x
:
A
,
y
=
f
x
->
Acc
Rof
x
.
Lemma
Acc_inverse_image
:
forall
x
:
A
,
Acc
R
(
f
x
) ->
Acc
Rof
x
.
Theorem
wf_inverse_image
:
well_founded
R
->
well_founded
Rof
.
Variable
F
:
A
->
B
->
Prop
.
Let
RoF
(
x
y
:
A
) :
Prop
:=
exists2
b
:
B
,
F
x
b
&
(
forall
c
:
B
,
F
y
c
->
R
b
c
)
.
Lemma
Acc_inverse_rel
:
forall
b
:
B
,
Acc
R
b
->
forall
x
:
A
,
F
x
b
->
Acc
RoF
x
.
Theorem
wf_inverse_rel
:
well_founded
R
->
well_founded
RoF
.
End
Inverse_Image
.