The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Jason,

  Many of these ingredients are part of the Equations plugin. There is a Derive Subterm which builds the subterm relation and its proof of well-foundedness and the transformation part starts from a different syntax but could be adapted to start from a restricted subset of existing Coq terms. I believe it would be easy to show extensional equality of the two functions given that you'd have the graph and defining equations of the translated version available (which hide the fixpoint unfolding theorem for you). The system handles inductive families, fix on multiple arguments and deep pattern-matching but not nested or mutual inductives currently.

Best,

-- Matthieu

Le mercredi 4 février 2015, Gregory Malecha <gmalecha AT cs.harvard.edu> a écrit :

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

On Tue, Feb 3, 2015 at 7:35 PM, Gregory Malecha <gmalecha AT cs.harvard.edu> wrote:

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.

Sure, bonus points for supporting deep structural recursion too.  But I want an automatic way of doing it for naive structural recursion, first.  (And perhaps there's a generic proof that well_founded R -> well_founded (transitive closure of R)?)

There is: https://github.com/coq-ext-lib/coq-ext-lib/blob/master/theories/Recur/Relation.v#L11 

 

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

It might be a useful thing to have as part of the Fiat pipeline, of compiling math -> (computational) Gallina -> Facade -> Cito -> Bedrock IL.  In particular, it would mean that I don't need to do this manually for a few fixpoints I'm interested in compiling.

 

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/

--

gregory malecha

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

--