## 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: Jun 17 2024 at 22:01 UTC