How do I use instances in proofs? · Coq users

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.
  *)

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):

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):

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?