The Coq mailing list

[Feró <ferenc.tamasi AT gmail.com>]

`apply f_equal3' does what you want

On Sun, May 19, 2013 at 4:02 AM, Math Prover 
<mathprover AT gmail.com>
 wrote:
> Hi,
>
>   I have a rather simplistic question (and will not take offense at an
> response of the form "read section X.Y.Z of the manual").
>
>   I want to know if there is a way to automatically generate lemmas of the
> form simp_lem.
>
>   The way this happens in my work flow is:
>
>
> ### Problem
>
> (1) I define some Record class Foo.
> (2) In writing a proof, I have something like:
>
>   Hypothesis: ...
>   ====================
>   Goal: Build_Foo a1 a2 a3 = Build_Foo b1 b2 b3
>
> (3) Now, I want to using one command, change my state to something with 3
> goals:
>   Hypothesis: ...
>   ====================
>   Main Goal: a1 = b1
>   --------------
>   Next Goal: a2 = b2
>   --------------
>   Next Goal: a3 = b3
>
>
> ### Current Solution
>
> The only way I currently know how to solve this problem is by manually
> defining "simp_lem" and typing in "apply simp_lem."
>
>
> ### Desired Solution
>
> I would be able to type in something like:
>
>   apply Record_Constructor_Break(Foo)
>
> and have it auto generate the lemma and apply it.
>
>
> ### Relation to Macros
>
> I like lisp macros. One possible way to do this would be if Coq had
> something like Macros; and if so, I'd be able to write
> Record_Constructor_Break once, and it'd work for all Records by generating
> the proof on the fly by examining the structure of the Records.
>
>
> ### Actual Question:
>
> (1) What is the best way to do the above?
>
> (2) Does Coq have anything like Macros?
>
> (3) If Coq does not have Macros, for the above problem, can I somehow still
> build it using Program/Refine?
>
> Thanks!
>
>
> ==== Code ====
>
> Require Import CpdtTactics.
>
> Inductive Foo1 :=
>   | Foo1_1 : nat -> Foo1
>   | Foo1_2 : nat -> nat -> Foo1
>   | Foo1_3 : nat -> nat -> nat -> Foo1 .
>
> Inductive Foo2 :=
>   | Foo2_1 : nat -> Foo2
>   | Foo2_2 : nat -> Foo2
>   | Foo2_3 : nat -> Foo2.
>
> Inductive Foo3 := Foo3_1 | Foo3_2 | Foo3_3.
>
>
> Record Foo : Set := {
>   foo1 : Foo1;
>   foo2 : Foo2;
>   foo3 : Foo3 }.
>
> Lemma simp_lem:
>   forall f1 f2 f3 g1 g2 g3,
>     f1 = g1 ->
>     f2 = g2 ->
>     f3 = g3 ->
>     Build_Foo f1 f2 f3 = Build_Foo g1 g2 g3.
>     crush. Qed.
>
> (* now, in other parts, of my proof, I can use "apply simp_lem" *)
>



-- 
Give me liberty or give me cash!