Library Stdlib.Program.WfExtensionality

Reformulation of the Wf module using subsets where possible, providing the support for Program's treatment of well-founded definitions.

From Stdlib.Init Require Import Wf.
From Stdlib.Program Require Import Utils.
From Stdlib.Program Require Import Wf.

Local Open Scope program_scope.

This module provides the fixpoint equation provided one assumes functional extensionality.

From Stdlib.Logic Require Import FunctionalExtensionality.

Module WfExtensionality.

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