Stream: Coq users

Topic: How to put proofs inside values?


view this post on Zulip Ignat Insarov (Jun 20 2021 at 13:30):

Examples:

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Ignat Insarov (Jun 20 2021 at 13:53):

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

view this post on Zulip 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

view this post on Zulip 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: Jan 27 2023 at 00:03 UTC