The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

It would be nice to add support for Ralf's wish to the Derive mechanism. 
I have opened https://coq.inria.fr/bugs/show_bug.cgi?id=4594 for this wish.

On 02/25/2016 07:14 AM, Arnaud Spiwack wrote:
> Hi Robbert,
>
> Indeed. I retract my implied claim that it may have been used to save a
> few keystrokes.
>
> On 25 February 2016 at 00:29, Robbert Krebbers
> <mailinglists AT robbertkrebbers.nl
> <mailto:mailinglists AT robbertkrebbers.nl>>
>  wrote:
>
>     Hi Arnaud,
>
>     For Ralf's purpose the generated term should be Opaque. As far as I
>     see, one can only control the opacity of the equality lemma. So, given:
>
>        Derive f SuchThat (f = λ x : nat, 10) As foo.
>
>     One can control whether foo is Opaque by ending the proof with
>     Qed/Defined, but not whether f is Opaque.
>
>     Robbert
>
>     On 02/24/2016 09:15 PM, Arnaud Spiwack wrote:
>
>         See also :
>         
> https://coq.inria.fr/distrib/current/refman/Reference-Manual033.html#hevea_command305
>
>         (syntax subject to changes by the time of next release)
>
>         On 24 February 2016 at 14:57, Jacques-Henri Jourdan
>         
> <jacques-henri.jourdan AT inria.fr
>         
> <mailto:jacques-henri.jourdan AT inria.fr>
>         
> <mailto:jacques-henri.jourdan AT inria.fr
>         
> <mailto:jacques-henri.jourdan AT inria.fr>>>
>         wrote:
>
>              Le 24/02/2016 14:51, Ralf Jung a écrit :
>              > Hi,
>              >
>              >> Oh, but you also want the equality lemma.
>              > Right :)
>              >
>              >> Then you can do something like:
>              >>
>              >> Definition x : nat := 1.
>              >>
>              >> Definition x_aux : { x':_ & x' = x }.
>              >>   exact (existT _ _ eq_refl). Qed.
>              >> Definition x_sealed := projT1 x_aux.
>              >> Definition x_sealed_eq : x_sealed = x := projT2 x_aux.
>              >>
>              >> Which is, I admit, not ideal from a syntactic point of
>         view. However,
>              >> note that the type and definition of x appear only once.
>              > Thanks, this indeed looks nicer than using modules!
>              >
>              > Unfortunately, if the type of x is more complicated, this
>         loses all the
>              > information about implicit arguments: If some arguments
>         of "x" were made
>              > implicit by putting them in "{...}", these are all
>         explicit for
>              > x_sealed. So the type has to be repeated, or at least the
>         implicitness
>              > information has to be declared again with Arguments.
>
>              Well, you don't really need x, so you don't need to give this
>              information twice. But yes, you have to repeat the
>         information about
>              implicitness of arguments.
>
>               > Kind regards,
>               > Ralf