Stream: Coq devs & plugin devs

Topic: Is `Printing Existential Instances` broken?


view this post on Zulip Jason Gross (Jan 12 2022 at 03:15):

Is there a way to deactivate the printing of evar instances? Unset Printing Existential Instances worked in Coq 8.4, but since Coq 8.5 it seems to only impact the display of evars in the with part of displaying existentials...

view this post on Zulip Gaëtan Gilbert (Jan 12 2022 at 09:34):

it's off by default

Goal nat -> exists x, x = 0.
intros n.
eexists.
(* goal: ?x = 0 *)
Set Printing Existential Instances.
(* goal: ?x@{n:=n} = 0 *)

view this post on Zulip Pierre-Marie Pédrot (Jan 12 2022 at 09:41):

What's the problem with that?

view this post on Zulip Jason Gross (Jan 12 2022 at 20:50):

I want to disable the verbosity of things like:

Goal forall x y : nat, x = y -> exists n : nat, n = n.
  intros; eexists.
  subst.
  (* ?n@{x:=y; y:=y} = ?n@{x:=y; y:=y} *)

view this post on Zulip Guillaume Melquiond (Jan 12 2022 at 21:27):

I feel like Coq is right to display the long form here, since the variable assignment is ambiguous and the incorrect lambda-term might be created after unification. I suppose Coq could use a more compact notation to show that substituting n with a term containing y is a bad idea.

view this post on Zulip Jason Gross (Jan 24 2022 at 15:03):

I agree that Coq is right to display it by default, but I want an option to disable it in cases where the substituted term is enormous and irrelevant to the proof I'm doing (for example because the evar is of type nat and the substituted variable is a proof of some non-singleton Prop)


Last updated: Feb 05 2023 at 22:03 UTC