## Stream: Coq users

### Topic: How do I use instances in proofs?

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

Example:

``````Goal ∀ type (anEqDecision: EqDecision type) (aCountable: Countable type) (x: type)
, decode (encode x) = Some x.
intros. destruct aCountable.
(*
type : Type
anEqDecision : EqDecision type
encode : type → positive
decode : positive → option type
decode_encode : ∀ x : type, decode (encode x) = Some x
x : type
============================
countable.decode (countable.encode x) = Some x
*)
rewrite (decode_encode x).
(*
Error: Found no subterm matching "decode (encode x)" in the current goal.
*)
``````

If I rewrite the other way, I can use reflexivity:

``````Goal ∀ type (anEqDecision: EqDecision type) (aCountable: Countable type) (x: type)
, decode (encode x) = Some x.
intros. destruct aCountable.
rewrite <- (decode_encode x).
(*
type : Type
anEqDecision : EqDecision type
encode : type → positive
decode : positive → option type
decode_encode : ∀ x : type, decode (encode x) = Some x
x : type
============================
countable.decode (countable.encode x) = decode (encode x)
*)
reflexivity. Qed.
``````

So, apparently Coq knows that `countable.decode` = `decode` and `countable.encode` = `encode`? What is going on here? How can I rewrite it the way I want?

#### Li-yao (Jun 20 2021 at 15:12):

Try simplifying the goal before rewriting (`cbn`, maybe after `unfold countable.decode` if it does nothing). Rewriting pretty much requires expressions to match exactly, whereas `reflexivity` reduces the two sides so it can equate more terms.

#### Ignat Insarov (Jun 20 2021 at 15:24):

Thanks! `unfold countable.decode, countable.encode.` converts it into `decode` and `encode`! Why does it though?

#### Ignat Insarov (Jun 20 2021 at 15:24):

Why are they introduced like that in the first place?

#### Ignat Insarov (Jun 20 2021 at 15:25):

I notice that `decode` and `encode` in the goal only become `countable.decode` and `countable.encode` after I destruct `aCountable`.

#### Ignat Insarov (Jun 20 2021 at 15:26):

Only for me to unfold them back. Coq is trying to make my life harder for no reason?

#### Gaëtan Gilbert (Jun 20 2021 at 15:37):

Before you destruct, `countable.encode` can be shortened to `encode`, but after that would refer to the local context so a more precise name is printed
Do `Set Printing All` before and after your destruct and reduction to see what happens

#### Ignat Insarov (Jun 20 2021 at 15:43):

Oh, I see. Before `destruct aCountable.`, it is `@decode type anEqDecision aCountable`, so it refers to `aCountable`. After `destruct aCountable.`, there is no more `aCountable.` so it becomes complicated.

#### Ignat Insarov (Jun 20 2021 at 15:44):

It even inlines the class dictionary.

#### Paolo Giarrusso (Jun 27 2021 at 17:47):

I think this problem would disappear if you avoid destructing the typeclass instance; I don't think stdpp (or its main client Iris) ever do that.

#### Ignat Insarov (Jun 27 2021 at 18:23):

Then how do I get the proof that `decode` retracts `encode` from out of said instance?

#### Gaëtan Gilbert (Jun 27 2021 at 18:26):

`decode_encode`

#### Ignat Insarov (Jun 27 2021 at 20:52):

Thanks!

Last updated: Sep 23 2023 at 14:01 UTC