Stream: Coq users

Topic: How to put proofs inside values?

Ignat Insarov (Jun 20 2021 at 13:30):

Examples:

• A value of a Σ type must have a proof inside: exist Odd 1 …. How can I put a proof there without giving it a name?
• An instance of [Countable] is a record that contains two functions and a proof that one retracts the other. How do I write that proof in?

I know that I can write the proof separately and assign it to a name with a Theorem or a Lemma. But it would be cumbersome. Is there a way to do it inline?

[Countable]: https://plv.mpi-sws.org/coqdoc/stdpp/stdpp.base.html#lab9

Ignat Insarov (Jun 20 2021 at 13:37):

I also know that I can use ltac:(…) to put some Ltac inline, but it is awkward. Is it the only way?

Ignat Insarov (Jun 20 2021 at 13:40):

Awkward because I cannot see the context and without seeing the context I find it hard to build a suitable Ltac snippet.

Gaëtan Gilbert (Jun 20 2021 at 13:50):

ltac just builds terms
you can Print your definition or theorem to see what ltac produced
eg

Lemma foo_countable : Countable foo.
Proof. some ltac. Qed.
Print foo_countable.

the print will say something like (* foo_countable = {| encode := ...; decode := ...; decode_encode := ... |} *)
if you do Definition foo_countable_alt := {| encode := ...; decode := ...; decode_encode := ... |} it will work too

Ignat Insarov (Jun 20 2021 at 13:53):

What do these fancy "{| … |}" braces do?

Gaëtan Gilbert (Jun 20 2021 at 14:01):

it's record syntax
if you Set Printing All to disable the sugared printing it will be something like @Build_Countable foo ... ... ... instead

Ignat Insarov (Jun 20 2021 at 14:14):

Oh, I see. I was lost between the notation for defining record types and record values.

Last updated: Oct 03 2023 at 19:01 UTC