Stream: Coq users

Topic: Typeclass resolution without impacting the proof term


view this post on Zulip Armaël Guéneau (Jul 30 2020 at 14:45):

If I have a goal of type nat, and I want to derive through typeclass resolution an instance of ThisNat n where ThisNat is a class and n a concrete nat, then use n to prove the goal.
Is there a way to do that using Ltac so that the resulting proof term is exactly n, without any trace of the type class resolution or trace of ThisNat?

view this post on Zulip Enrico Tassi (Jul 30 2020 at 15:01):

Class Foo (n : nat).
Instance xxx : Foo 3. Defined.
Definition ooF n (_ : Foo n) := n.

Goal nat.
let solution := eval cbv in (ooF _ _) in exact solution.
Show Proof.

view this post on Zulip Armaël Guéneau (Jul 30 2020 at 15:02):

Right. I guess I wanted to avoid ooF appearing in the proof term. But now I'm not sure it's very important

view this post on Zulip Armaël Guéneau (Jul 30 2020 at 15:03):

Ah wait nvm, didn't see the second part

view this post on Zulip Armaël Guéneau (Jul 30 2020 at 15:04):

thanks!


Last updated: Feb 06 2023 at 13:03 UTC