# 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.

Module WfExtensionality.

Require Import FunctionalExtensionality.

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.

Program Lemma fix_sub_measure_eq_ext :
forall (A : Type) (f : A -> nat) (P : A -> Type)
(F_sub : forall x : A, (forall (y : A | f y < f x), P y) -> P x),
forall x : A,
Fix_measure_sub A f P F_sub x =
F_sub x (fun (y : A | f y < f x) => Fix_measure_sub A f P F_sub y).

Tactic to unfold once a definition based on Fix_measure_sub.

Ltac unfold_sub f fargs :=
set (call:=fargs) ; unfold f in call ; unfold call ; clear call ;
rewrite fix_sub_measure_eq_ext ; repeat fold_sub fargs ; simpl proj1_sig.

End WfExtensionality.