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.

Local Open Scope program_scope.

Section Well_founded.
  Variable A : Type.
  Variable R : A -> A -> Prop.
  Hypothesis Rwf : well_founded R.

  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) : 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).


  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_sub (`y) (Acc_inv r (proj2_sig y))) = Fix_F_sub x r.

  Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F_sub x r = Fix_F_sub x s.

  Lemma Fix_eq : forall x:A, Fix_sub x = F_sub x (fun (y:A|R y x) => Fix_sub (proj1_sig y)).

  Lemma fix_sub_eq :
    forall x : A,
      Fix_sub x =
      let f_sub := F_sub in
        f_sub x (fun (y : A | R y x) => Fix_sub (`y)).

End Well_founded.

Extraction Inline Fix_F_sub Fix_sub.

Set Implicit Arguments.

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.

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 _ 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
        appcontext 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.

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_sub A R Rwf P F_sub y).

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.