The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Jonathan,

It looks like I should give 8.5 a try and see if the other things I need work 
out of the box.  Are there 8.5 prerelease versions which passed a reasonable 
set of regression test or should I just use the git trunk version?

Best regards,

Michael


-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Jonathan Leivent
Sent: Monday, January 19, 2015 4:39 PM
To: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] Simplification of terms generated with tactics


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