The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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)?)

 

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/