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?

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.

Thanks! `unfold countable.decode, countable.encode.`

converts it into `decode`

and `encode`

! Why does it though?

Why are they introduced like that in the first place?

I notice that `decode`

and `encode`

in the goal only become `countable.decode`

and `countable.encode`

after I destruct `aCountable`

.

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

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

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.

It even inlines the class dictionary.

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.

Then how do I get the proof that `decode`

retracts `encode`

from out of said instance?

`decode_encode`

Thanks!

Last updated: Jun 14 2024 at 19:02 UTC