The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sat, 18 May 2013 19:02:26 -0700,
Math Prover 
<mathprover AT gmail.com>
 a écrit :

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


The path I would take would be to use the "f_equal" tactic.
BUT in this case it may or may not work, depending whether there is
some dependency in the parameters type, that is

Record Foo : Type :=
Build_Foo { a : nat
          ; b : nat
          ; c : nat
          }.

will not raise any problem, but

Record Foo : Type :=
Build_Foo { a : nat
          ; b : nat
          ; c : a < b
          }.

will.
There is also a (lot less) annoying stuff with such a way to do (but
anyway any common tactic leading to your point (3) will have) is
that you cannot share proofs in parallel branches. That is:

with

Build_Foo a b (a + b) = Build_Foo c d (c + d)

you will be asked to prove

1. a = c
2. b = d
3. a + b = c + d

but in 3. you will not have access of your previous proofs (1. and 2.),
so you will probably have to redo these proofs in the 3. goal.
A trick is to design your proofs so that you assert the common used
subproofs before applying f_equal.

In this case, that would be:

assert (Hac : a = c).
<do your proof>
assert (Hbd : b = d).
<do your proof>
f_equal.
(* case 1. *)
exact Hac.
(* case 2. *)
exact Hbd.
(* case 3. *)
rewrite Hab, Hcd; reflexivity.

Note that in this sketch, you have a shorter proof by directly
rewriting Hac and Hbd and then use reflexivity, but I gave this
example simply to explain my idea.

Note also that f_equal is clever enough not to make you do identity
proofs. That is in the following goal:

Build_Foo a1 b c1 = Build_Foo a2 b c2

you will be asked to prove (a1 = a2) and (c1 = c2), but not (b = b).

> ### 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.

There is the Ltac language, but I really don't like it as it is rather
awkward and does not give access to the full ast of Coq. ("I don't
like" does not mean "I don't use", just that I would prefer to have
some better one.) If you have not read about Ltac, do it, as you can
still do a lot of things with it (and also read all the tactics of the
reference manual, there are not all usefull, and many are variants of
others, but you may find some subset of tactics which you may find
usefull).

> 
> 
> ### Actual Question:
> 
> (1) What is the best way to do the above?

f_equal as far as there are not type dependencies between fields.
Else things are a lot more complex, and I have no general solution.

> 
> (2) Does Coq have anything like Macros?

Yes, Ltac, and the proof structure stuff (ie. ';', '(, )' and '[, |,
]'). But it may not be as powerfull as you may wish (you cannot get the
number of constructors of an inductive type for instance).

> 
> (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" *)

Well, in this case, f_equal seems to be definetely what you want.