coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert"

From: Enrico Tassi <enrico.tassi AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert"
Date: Wed, 21 Jan 2015 20:55:21 +0100

On Wed, Jan 21, 2015 at 10:21:20AM +0000, Soegtrop, Michael wrote:
> Dear George,
>
> splendid, the “have @f : type_of_f” tactic works like a charm! Even
> simplification of proof terms with compute works.

Thanks for testing, these relatively new features of the ssreflect proof
language are not yet systematically used in the mathematical components
library that is the main test suite we use to find bugs and regressions.

I'm particularly interested in your experience, since I did fight quite
a bit with the proof terms produced by ssreflect. With have @ they
become visible, so their shape (and not only their type) matters.

Are there still "random" eta expansions? Anything else looking ugly or
just odd? Which tactics are you using to build them?

Best,
--
Enrico Tassi

[Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert", Soegtrop, Michael, 01/20/2015
- Re: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert", Arnaud Spiwack, 01/20/2015
  - RE: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert", Soegtrop, Michael, 01/20/2015
    - Re: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert", Pierre-Marie Pédrot, 01/20/2015
      - Re: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert", Arnaud Spiwack, 01/20/2015
        
        RE: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert", Georges Gonthier, 01/20/2015
        
        RE: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert", Soegtrop, Michael, 01/21/2015
        
        Re: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert", Enrico Tassi, 01/21/2015