Stream: Coq users

Topic: Opaque Definition from proofterm


view this post on Zulip Fabian Kunze (Nov 16 2020 at 09:40):

What's a way to declare a lemma by giving a proof term such that the lemma is Opaque, without giving the type of t explicitly?
This fails, as Lemma expects a type:

 Definition SpecT__step := projT2 SpecT__step'.

This fails, although I think I read about this somewhere, but maybe it was a Coq Improvement proposal:

#[opaque]
Definition SpecT__step := projT2 SpecT__step'.

view this post on Zulip Théo Zimmermann (Nov 16 2020 at 09:41):

Indeed, it is coq/ceps#42.

view this post on Zulip Théo Zimmermann (Nov 16 2020 at 09:42):

There is no way to solve your problem and this was precisely the problem that gave rise to this CEP.

view this post on Zulip Fabian Kunze (Nov 16 2020 at 10:00):

Thanks Theo. Ok, then live with this approximation, as the ting I project out of is Qed.-opaque:

 Definition SpecT := projT2 SpecT'.
 Opaque SpecT__step.

view this post on Zulip Théo Zimmermann (Nov 16 2020 at 10:29):

Actually, here is a possible (complicated) workaround. Example where I define an opaque bar of value 0 without ever providing its type:

Definition foo := 0.
Definition bar : (ltac:(let t := type of foo in exact t)).
exact foo.
Qed.

view this post on Zulip Fabian Kunze (Nov 16 2020 at 10:30):

Oh, right, everything is possible in a world with inline-ltac :)


Last updated: Jan 29 2023 at 05:03 UTC