Library Coq.Program.Wf
Reformulation of the Wf module using subsets where possible, providing
the support for Program's treatment of well-founded definitions.
Reasoning about well-founded fixpoints on measures.
Section Measure_well_founded.
Variables T M:
Type.
Variable R:
M -> M -> Prop.
Hypothesis wf:
well_founded R.
Variable m:
T -> M.
Definition MR (
x y:
T):
Prop :=
R (
m x) (
m y).
Lemma measure_wf:
well_founded MR.
End Measure_well_founded.
Hint Resolve measure_wf :
core.
Section Fix_rects.
Variable A:
Type.
Variable P:
A -> Type.
Variable R :
A -> A -> Prop.
Variable Rwf :
well_founded R.
Variable f:
forall (
x :
A),
(forall y:
{ y: A | R y x },
P (
proj1_sig y)
) -> P x.
Lemma F_unfold x r:
Fix_F_sub A R P f x r =
f (
fun y =>
Fix_F_sub A R P f (
proj1_sig y) (
Acc_inv r (
proj2_sig y))).
Lemma Fix_F_sub_rect
(
Q:
forall x,
P x -> Type)
(
inv:
forall x:
A,
(forall (
y:
A) (
H:
R y x) (
a:
Acc R y),
Q y (
Fix_F_sub A R P f y a)
) ->
forall (
a:
Acc R x),
Q x (
f (
fun y:
{y: A | R y x} =>
Fix_F_sub A R P f (
proj1_sig y) (
Acc_inv a (
proj2_sig y)))))
:
forall x a,
Q _ (
Fix_F_sub A R P f x a).
Hypothesis equiv_lowers:
forall x0 (
g h:
forall x:
{y: A | R y x0},
P (
proj1_sig x)),
(forall x p p',
g (
exist (
fun y:
A =>
R y x0)
x p)
= h (
exist (
fun y =>
R y x0)
x p')
) ->
f g = f h.
Lemma eq_Fix_F_sub x (
a a':
Acc R x):
Fix_F_sub A R P f x a =
Fix_F_sub A R P f x a'.
Lemma Fix_sub_rect
(
Q:
forall x,
P x -> Type)
(
inv:
forall
(
x:
A)
(
H:
forall (
y:
A),
R y x -> Q y (
Fix_sub A R Rwf P f y))
(
a:
Acc R x),
Q x (
f (
fun y:
{y: A | R y x} =>
Fix_sub A R Rwf P f (
proj1_sig y))))
:
forall x,
Q _ (
Fix_sub A R Rwf P f x).
End Fix_rects.
Tactic to fold a definition based on Fix_measure_sub.
Ltac fold_sub f :=
match goal with
| [ |- ?
T ] =>
match T with
context C [ @
Fix_sub _ _ _ _ _ ?
arg ] =>
let app :=
context C [
f arg ]
in
change app
end
end.
This module provides the fixpoint equation provided one assumes
functional extensionality.
The two following lemmas allow to unfold a well-founded fixpoint definition without
restriction using the functional extensionality axiom.
For a function defined with Program using a well-founded order.
Tactic to unfold once a definition based on Fix_sub.
Ltac unfold_sub f fargs :=
set (
call:=
fargs) ;
unfold f in call ;
unfold call ;
clear call ;
rewrite fix_sub_eq_ext ;
repeat fold_sub f ;
simpl proj1_sig.
End WfExtensionality.