The Coq mailing list

[Gregory Malecha <gmalecha AT cs.harvard.edu>]

You'll need to do something a little bit more powerful than this since Coq's structural recursion checker supports deep pattern matching. So at the very least you would need to do recursion on the transitive closure of the accessible relation.

Out of curiosity, why do you want to do this?

On Tue, Feb 3, 2015 at 4:29 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

Is there a plugin (or ltac, or partial work) on turning functions defined with [fix] into functions defined with [Fix], automatically, together with a(n automatic) proof of pointwise equality between the original function and the new function?

For example, I am looking for something that, given [fold_right], produces:

Require Import Coq.Lists.List Coq.Init.Wf.

Inductive listR {A : Type} : list A -> list A -> Prop :=

| cons1 : forall (x : A) (xs : list A), @listR A xs (x :: xs).

Definition listR_wf {A : Type} : well_founded (@listR A).

Proof.

  intro x.

  induction x; constructor; intros y H; inversion_clear H; eauto with nocore.

Qed. 

Definition fold_right' A B (f : B -> A -> A) (a0 : A) : list B -> A :=

  let fold_right'' (x : list B) (rec : forall y : list B, listR y x -> A)

      := match x return (forall y : list B, listR y x -> A) -> A with

           | nil => fun _ => a0

           | b :: t => fun rec => f b (rec t (@cons1 _ _ _))

         end rec in

  Fix (@listR_wf B) (fun _ => A) fold_right''.

                         

Lemma fold_right'_correct A B f a0 ls : @fold_right' A B f a0 ls = @fold_right A B f a0 ls.

Proof.

  induction ls; unfold fold_right'; simpl; rewrite Fix_eq; trivial;

  try solve [ match goal with

            | [ IH : _ |- _ ] => rewrite <- IH; reflexivity

          end

        | intro x; destruct x; intros; trivial;

          match goal with

            | [ H : _ |- _ ] => rewrite H; reflexivity

          end ].

Qed.

The construction I'm imagining is as follows:

1. Construct an inductive definition of the well-founded structural less-than relation, with one constructor for each recursive argument appearing in any constructor of the inductive type of the structural argument of the fixpoint

2. Construct the type of the well-foundedness theorem, and inhabit that type (the tactic above might be enough to prove all such well-foundedness theorems)

3. Extract the body of the fixpoint, and convert it into a let-expanded form using [Fix] like the one above

4. Construct the type of the correctness theorem, and prove it (the tactic I gave above might, again, be enough, in general)

Does such a plugin/ltac exist?  (Bonus points for supporting [fix] with multiple arguments, mutual [fix]es, nested [fix]es.)

Thanks,

Jason

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/