The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

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