The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/19/2015 06:06 AM, Soegtrop, Michael wrote:
> Dear Coq Users,
>
> using Jonathan Leivant's ideas on the split tactic, I created a tactic which produces for simple 
> enumeration style inductive types a list of all values (see attached Coq script). It works fine, 
> just the returned "proof term" contains some unnecessary overhead (a function 
> definition which is never used). I wonder if there is a way to modify the tactic such that the 
> resulting "proof term" is just the list, without the overhead.

I don't think this is possible in 8.4, as you can't simplify a proof 
term built tactically while being "inside" of it, and there does not 
seem to be any way short of defining a function in proof mode to get an 
external handle on something built tactically.  In 8.5, it is easily 
done by building the proof term in a $(...)$ construct, then using eval 
compute on that prior to using it as the body of the function.

It is unfortunate that you can't move easily to 8.5, as it sounds like 
what you are trying to achieve is done most easily in 8.5.  For 
instance, see my posting on Dec 20, 2014 titled "using $(...)$ and admit 
to analyze tactic results" - which shows a way in 8.5 to generate a term 
containing the constructor information for an arbitrary inductive type.  
I omitted the printed result from that posting, assuming any interested 
parties would try it in a trunk version for themselves.  Here it is:

(forall f : foo 1, f = Foo1 -> True,
forall (f : foo 2) (b : bool), f = Foo2 b -> True,
forall f : foo 3, f = Foo3 -> True,
forall (f : foo 4) (n : nat) (f0 : foo n), f = Foo4 n f0 -> True)

based on analyzing the inductive type:

Inductive foo : nat -> Set :=
| Foo1 : foo 1
| Foo2(b : bool) : foo 2
| Foo3 : foo 3
| Foo4(n : nat)(f : foo n) : foo 4.

-- Jonathan