The Coq mailing list

[Armaël Guéneau <armael.gueneau AT ens-lyon.fr>]

Thank you for the replies. I've opened an issue to keep track of this:
https://github.com/coq/coq/issues/6723

Cheers,
Armaël

On 07/02/2018 14:47, Robbert Krebbers wrote:
> +1 for more a more clever desugaring.
> 
> See also https://github.com/coq/coq/issues/5701
> 
> On 02/07/2018 01:46 PM, Matthieu Sozeau wrote:
>> Hi,
>>
>> It think it would be rather hopeless to try and invert the projections at
>> pretty printing time to everyone’s contentment. However, it might be
>> possible to use a more clever desugarring that let-binds the projections
>> (potentially with specific constants to avoid simpl reducing them but
>> still
>> allowing unification to succeed) and invert those.
>> Cheers,
>> — Matthieu
>> Le mer. 7 févr. 2018 à 13:26, Armaël Guéneau
>> <armael.gueneau AT ens-lyon.fr>
>>  a
>> écrit :
>>
>>> Hi everyone,
>>>
>>> I am facing an issue related to the use of "fun '(_,_) => ..." with
>>> primitive projections. It works well when writing goals & lemmas, but
>>> at pretty-printing time, only the desugared version is printed, which
>>> quickly gets unreadable. I'm wondering if other people have already
>>> faced this issue, and if there's a known workaround to improve the
>>> pretty-printing -- or if I should maybe open a feature request on
>>> Coq's issue tracker.
>>>
>>>
>>>
>>> Here follows a more detailed description of the issue.
>>>
>>> Let's assume for the sake of the example a predicate on functions of
>>> type "A -> nat", and a compatibility lemma about P and +, which holds
>>> for any A.
>>>
>>>    Parameter P : forall A, (A -> nat) -> Prop.
>>>    Hypothesis P_add : forall A f g,
>>>      P A f -> P A g -> P A (fun x => f x + g x).
>>>
>>> Now consider the following goal, where A is (nat * nat):
>>>
>>>    Goal P (nat * nat) (fun '(x,y) => x + y).
>>>      Fail apply P_add.
>>>
>>> With the standard pairs, I cannot call "apply P_add" -- the goal does
>>> not unify with the conclusion of the lemma, since (fun '(x,y) => x +
>>> y) is sugar for (fun p => let (x,y) := p in x + y). One solution would
>>> be to restate the goal as:
>>>
>>>    Goal P (nat * nat) (fun p => (fst p) + (snd p)).
>>>      apply P_add
>>>
>>> which I find inconvienient; I like being able to give names to the
>>> components of the tuple, especially with bigger arities (where one
>>> would have to instead write (fst (fst p)) and such).
>>>
>>>
>>> Matthieu Sozeau pointed out to me that an other solution is to use
>>> primitive projections: this way, one can still use the "fun '(x,y) =>
>>> ..." sugar, which gets desugared to uses of fst and snd.
>>>
>>>    Set Primitive Projections.
>>>    Unset Printing Primitive Projection Compatibility.
>>>    (* required for projections to actually be displayed *)
>>>
>>>    Record myprod A B := mypair { myfst : A; mysnd : B }.
>>>
>>>    Arguments mypair {A B} _ _.
>>>    Arguments myfst {A B} _.
>>>    Arguments mysnd {A B} _.
>>>
>>>    Notation "x ** y" := (myprod x y) (at level 80): type_scope.
>>>    Notation "( x , y , .. , z )" := (mypair .. (mypair x y) .. z).
>>>
>>>    Goal P (nat ** nat) (fun '(x,y) => x + y).
>>>      apply P_add.
>>>
>>> This works, which is nice. (fun '(x,y) => x + y) is desugared to (fun
>>> pat : nat ** nat => (myfst pat) + (mysnd pat)), and P_add can be
>>> applied directly.
>>>
>>> However, this desugaring is made apparent to the user: when proving
>>> the goal, the user works with the desugared version of the goal &
>>> hypothesis. This quickly gets unreadable in my opinion: there's a
>>> "pat" variable that I cannot name, the names "x" and "y" are lost, and
>>> with tuples of arity > 2, they are replaced by nested projections (eg
>>> (fst (fst pat))) which I find really hard to keep track of.
>>>
>>> I'm wondering if someone already faced this issue.
>>> If there is no workaround for now, could one think of a better
>>> pretty-printer? I'm thinking of attaching to a "fun" the fact that it
>>> comes from a "fun '(_,_) => ..." sugar, along with information about
>>> the user-provided names; and then trying to pretty-print the
>>> fun+projections using the "fun '(_,_) => ..." sugar and the user
>>> names.
>>>
>>> If this seems a reasonable proposal I could submit a feature request
>>> on Coq's issue tracker.
>>>
>>>
>>> Cheers, and thanks for reading,
>>> Armaël
>>>
>>