good way to prove existence of records containing proofs? · Coq users

I need to prove something about a record with some fields that are proofs, generated through a goal of the form ∃ T : myRecordType, P T with eexists {| ...|}.Unshelve.

The proofs in the record are huge, so my new goal P {| ... |} is illegible. Can I hide the proofs, or is there a better way to do this kind of proof?

Michael Soegtrop (Oct 05 2021 at 13:08):

A common method is to use an identity function where the argument is declared implicit, so that it is not shown unless "implict arguments" are on. E.g. VST has this definition:

Definition abbreviate {A:Type} (x:A) := x.
Arguments abbreviate {A} {x}.

(which could be made shorter by writing {x:A}right away). I think there are also tricks with printing only notations, but I tend to use the above method. The downside of the above method is that you actually modify your terms by inserting the id function. But this can also be an advantage, because it gives you control over what you want to see and what not.

Gaëtan Gilbert (Oct 05 2021 at 13:10):

you can try using abstract or transparent_abstract in the proof goals
you can set some implicit arguments on the constructor of your record and Unset Printing Records:

Record XX := { a : nat; b : nat; c : nat }.
Arguments Build_XX _ {_} _.
Unset Printing Records.
Check @Build_XX 0 1 2.
(* Build_XX 0 2 *)
(* imagine that 1 is a big term *)

you can use an identity function with implicit arguments to hide a term (Michael also suggested this while I was typing)

Record XX := { a : nat; b : nat; c : nat }.

Definition hide {A a} : A := a.

Lemma bla : exists x : XX, x = x.
Proof.
  unshelve eexists {| a := _; b := @hide _ _; c := _ |}.
  - exact 0.
  - exact 1.
  - exact 2.
  - (* goal is {| a := 0; b := hide; c := 2 |} = {| a := 0; b := hide; c := 2 |} *)

Paolo Giarrusso (Oct 05 2021 at 13:27):

for a local Unset Printing Records there's also Add Printing Constructor XX.

Paolo Giarrusso (Oct 05 2021 at 13:29):

And abstract or similar is arguably better in many scenarios, especially if your proof is proof-irrelevant, since it hides proof terms from computation, which helps for both information hiding and performance.

Paolo Giarrusso (Oct 05 2021 at 13:30):

otherwise your clients might depend on the implementation details of, say, a tactic-generated proof, or might end up trying to run it

Jonas Oberhauser (Oct 05 2021 at 13:41):

That's neat, thanks! A follow up question: it seems that abstract only works on the tactic that solves the goal, but I have to do some intros etc. before that, which appears then in the generated proof term. With abstract ( whole ; proof ; here) I can avoid that, but it's obviously not so nice. Is there a way to tell Coq "start a new local lemma here" at the beginning of the proof instead of just in the final step?

Paolo Giarrusso (Oct 05 2021 at 14:00):

not quite, but I often prefer Program to abstract, tho I first flip almost all settings:

Unset Program Cases.
(* Insert tweaks from stdpp here: https://gitlab.mpi-sws.org/iris/stdpp#side-effects *)
Program Definition bla : exists x : XX, x = x := {| a := _; b := @hide _ _; c := _ |}.
Next Obligation. ... Qed.
Next Obligation. ... Qed.

Stream: Coq users

Topic: good way to prove existence of records containing proofs?