Stream: Coq users

Topic: Controlling printing of patters in binders


view this post on Zulip MackieLoeffel (Jun 05 2023 at 07:55):

Hi, I am very confused by how the printing of patterns in binders works. Can someone explain why the same term is printed in two different ways in the following example?

  Axiom get_tuple : forall (T : (nat * nat * nat) -> Prop), Prop.
  Goal get_tuple (fun '(x1, x2, x3) => x1 = 0).
  Proof.
    Set Printing All.
    (* Copy term from goal: *)
    pose (get_tuple
    (fun pat : prod (prod nat nat) nat =>
     match pat return Prop with
     | pair p _ => match p return Prop with
                   | pair x1 _ => @eq nat x1 O
                   end
     end)).
    (* The body of P and the goal print identical now. *)
    Unset Printing All.
    (* But now they print differently. What is going on? *)
  Abort.

view this post on Zulip Gaëtan Gilbert (Jun 05 2023 at 08:01):

matches remember how they were generated ('(pattern), (_, _) tuple, if or plain match) and use the same way to print

Additionally "plain match" can be overriden by some options depending on the type,
for instance prod is in the https://coq.github.io/doc/master/refman/language/extensions/match.html#printing-matching-on-irrefutable-patterns table so by default matches on prod get printed as let (_, ..., _) := ...

view this post on Zulip MackieLoeffel (Jun 05 2023 at 08:09):

I see, thanks for the explanation. Is there a way to copy this information from one constr to another using Ltac or Ltac2?

view this post on Zulip Gaëtan Gilbert (Jun 05 2023 at 09:22):

in ltac2 there's the Constr.Unsafe.case type which contains that info
do take care that a value of that type is specific to the inductive that is matched on

view this post on Zulip MackieLoeffel (Jun 05 2023 at 13:35):

I think that works for my use case, thanks!


Last updated: Jun 13 2024 at 19:02 UTC