Library Coq.Program.Wf
Reformulation of the Wf module using subsets where possible, providing
the support for Program's treatment of well-founded definitions.
Require Import Coq.Init.Wf.
Require Import Coq.Program.Utils.
Require Import ProofIrrelevance.
Open Local Scope program_scope.
Implicit Arguments Acc_inv [
A R x y].
Section Well_founded.
Variable A :
Type.
Variable R :
A ->
A ->
Prop.
Hypothesis Rwf :
well_founded R.
Section Acc.
Variable P :
A ->
Type.
Variable F_sub :
forall x:A, (
forall y: {
y :
A |
R y x },
P (
proj1_sig y)) ->
P x.
Fixpoint Fix_F_sub (
x :
A) (
r :
Acc R x) {
struct r} :
P x :=
F_sub x (
fun y: {
y :
A |
R y x} =>
Fix_F_sub (
proj1_sig y)
(
Acc_inv r (
proj2_sig y))).
Definition Fix_sub (
x :
A) :=
Fix_F_sub x (
Rwf x).
End Acc.
Section FixPoint.
Variable P :
A ->
Type.
Variable F_sub :
forall x:A, (
forall y: {
y :
A |
R y x },
P (
proj1_sig y)) ->
P x.
Notation Fix_F := (
Fix_F_sub P F_sub) (
only parsing).
Definition Fix (
x:A) :=
Fix_F_sub P F_sub x (
Rwf x).
Hypothesis
F_ext :
forall (
x:A) (
f g:forall
y:{y:A |
R y x},
P (`
y)),
(
forall (
y :
A |
R y x),
f y =
g y) ->
F_sub x f =
F_sub x g.
Lemma Fix_F_eq :
forall (
x:A) (
r:Acc
R x),
F_sub x (
fun (
y:A|R
y x) =>
Fix_F (`
y) (
Acc_inv r (
proj2_sig y))) =
Fix_F x r.
Lemma Fix_F_inv :
forall (
x:A) (
r s:Acc
R x),
Fix_F x r =
Fix_F x s.
Lemma Fix_eq :
forall x:A,
Fix x =
F_sub x (
fun (
y:A|R
y x) =>
Fix (
proj1_sig y)).
Lemma fix_sub_eq :
forall x :
A,
Fix_sub P F_sub x =
let f_sub :=
F_sub in
f_sub x (
fun (
y :
A |
R y x) =>
Fix (`
y)).
End FixPoint.
End Well_founded.
Extraction Inline Fix_F_sub Fix_sub.
Require Import Wf_nat.
Require Import Lt.
Section Well_founded_measure.
Variable A :
Type.
Variable m :
A ->
nat.
Section Acc.
Variable P :
A ->
Type.
Variable F_sub :
forall x:A, (
forall y: {
y :
A |
m y <
m x },
P (
proj1_sig y)) ->
P x.
Program Fixpoint Fix_measure_F_sub (
x :
A) (
r :
Acc lt (
m x)) {
struct r} :
P x :=
F_sub x (
fun (
y :
A |
m y <
m x) =>
Fix_measure_F_sub y
(@
Acc_inv _ _ _ r (
m y) (
proj2_sig y))).
Definition Fix_measure_sub (
x :
A) :=
Fix_measure_F_sub x (
lt_wf (
m x)).
End Acc.
Section FixPoint.
Variable P :
A ->
Type.
Program Variable F_sub :
forall x:A, (
forall (
y :
A |
m y <
m x),
P y) ->
P x.
Notation Fix_F := (
Fix_measure_F_sub P F_sub) (
only parsing).
Definition Fix_measure (
x:A) :=
Fix_measure_F_sub P F_sub x (
lt_wf (
m x)).
Hypothesis
F_ext :
forall (
x:A) (
f g:forall
y : {
y :
A |
m y <
m x},
P (`
y)),
(
forall y : {
y :
A |
m y <
m x},
f y =
g y) ->
F_sub x f =
F_sub x g.
Program Lemma Fix_measure_F_eq :
forall (
x:A) (
r:Acc
lt (
m x)),
F_sub x (
fun (
y:A |
m y <
m x) =>
Fix_F y (
Acc_inv r (
proj2_sig y))) =
Fix_F x r.
Lemma Fix_measure_F_inv :
forall (
x:A) (
r s:Acc
lt (
m x)),
Fix_F x r =
Fix_F x s.
Lemma Fix_measure_eq :
forall x:A,
Fix_measure x =
F_sub x (
fun (
y:{y:A|
m y <
m x}) =>
Fix_measure (
proj1_sig y)).
Lemma fix_measure_sub_eq :
forall x :
A,
Fix_measure_sub P F_sub x =
let f_sub :=
F_sub in
f_sub x (
fun (
y :
A |
m y <
m x) =>
Fix_measure (`
y)).
End FixPoint.
End Well_founded_measure.
Extraction Inline Fix_measure_F_sub Fix_measure_sub.
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.
Section Fix_measure_rects.
Variable A:
Type.
Variable m:
A ->
nat.
Variable P:
A ->
Type.
Variable f:
forall (
x :
A), (
forall y: {
y:
A |
m y <
m x },
P (
proj1_sig y)) ->
P x.
Lemma F_unfold x r:
Fix_measure_F_sub A m P f x r =
f (
fun y =>
Fix_measure_F_sub A m P f (
proj1_sig y) (
Acc_inv r (
proj2_sig y))).
Lemma Fix_measure_F_sub_rect
(
Q:
forall x,
P x ->
Type)
(
inv:
forall x:
A,
(
forall (
y:
A) (
H:
MR lt m y x) (
a:
Acc lt (
m y)),
Q y (
Fix_measure_F_sub A m P f y a)) ->
forall (
a:
Acc lt (
m x)),
Q x (
f (
fun y: {
y:
A |
m y <
m x} =>
Fix_measure_F_sub A m P f (
proj1_sig y) (
Acc_inv a (
proj2_sig y)))))
:
forall x a,
Q _ (
Fix_measure_F_sub A m P f x a).
Hypothesis equiv_lowers:
forall x0 (
g h:
forall x: {
y:
A |
m y <
m x0},
P (
proj1_sig x)),
(
forall x p p',
g (
exist (
fun y:
A =>
m y <
m x0)
x p) =
h (
exist _ x p')) ->
f g =
f h.
Lemma eq_Fix_measure_F_sub x (
a a':
Acc lt (
m x)):
Fix_measure_F_sub A m P f x a =
Fix_measure_F_sub A m P f x a'.
Lemma Fix_measure_sub_rect
(
Q:
forall x,
P x ->
Type)
(
inv:
forall
(
x:
A)
(
H:
forall (
y:
A),
MR lt m y x ->
Q y (
Fix_measure_sub A m P f y))
(
a:
Acc lt (
m x)),
Q x (
f (
fun y: {
y:
A |
m y <
m x} =>
Fix_measure_sub A m P f (
proj1_sig y))))
:
forall x,
Q _ (
Fix_measure_sub A m P f x).
End Fix_measure_rects.
Tactic to fold a definition based on Fix_measure_sub.
Ltac fold_sub f :=
match goal with
| [ |- ?T ] =>
match T with
appcontext C [ @
Fix_measure_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.
Program Lemma fix_sub_eq_ext :
forall (
A :
Type) (
R :
A ->
A ->
Prop) (
Rwf :
well_founded R)
(
P :
A ->
Type)
(
F_sub :
forall x :
A, (
forall (
y :
A |
R y x),
P y) ->
P x),
forall x :
A,
Fix_sub A R Rwf P F_sub x =
F_sub x (
fun (
y :
A |
R y x) =>
Fix A R Rwf P F_sub y).
For a function defined with Program using a measure.
Tactic to unfold once a definition based on Fix_measure_sub.