The Coq mailing list

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

Dear George,

 

splendid, the “have @f : type_of_f”  tactic works like a charm! Even simplification of proof terms with compute works.

 

Thanks & best regards,

 

Michael

 

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Georges Gonthier
Sent: Tuesday, January 20, 2015 7:01 PM
To: coq-club AT inria.fr
Subject: RE: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert"

 

  As was pointed out, the new proof engine was already in 8.4, but the its new functionalities were not exposed in Ltac.

The current Coq 8.4 release of Ssreflect does use them, however. In particular the tactic “have @f: type_of_f.” does exactly what you want.

Ssreflect also supports (via the [: Pf1 Pf2] pattern) abstracting part of the term of f (see the manual).

  Enjoy,

Georges

 

From: arnaud.spiwack AT gmail.com [mailto:arnaud.spiwack AT gmail.com] On Behalf Of Arnaud Spiwack
Sent: 20 January 2015 16:03
To: Coq Club
Subject: Re: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert"

 

I'm not sure you would learn much by digging up my commits as Pierre-Marie suggests. But the bottom-line is that the proof given to a goal has always been a regular Coq term but the interactive proof mechanism was built in a way which made it unable to retrieve such a proof. I wrote a completely new mechanism which, among other things, support the feature you need (it's often called dependent subgoals). This new implementation was already partially part of the v8.4, but it's been only completed in v8.5.

 

On 20 January 2015 at 15:15, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

On 20/01/2015 14:59, Soegtrop, Michael wrote:
> quite intriguing! So if I got you right, in 8.4 I cannot access the
> value of a tactic generated term inside a proof, only its type? This is
> unexpected since I can access the value after the proof is finished, if
> I end it with Defined rather than Qed. I wonder what makes it impossible
> to access it inside of the proof.

Short answer: the legacy proof engine.
Long answer: get a look at the merging of the branch of Arnaud in the
git repo.

> 1.       switch to 8.5 and try to fix ssreflect
>
> 2.       switch to 8.5 and try to port the ssreflect libraries I want to
> mainstream Coq
>
> 3.       stay with 8.4

If I am not mistaken, there is a 8.5-compatible version of ssreflect
already. We use it for testing. I do not know where it is officially
downloadable, but you should find it in the coq-contribs repo at least.

PMP