Stream: Coq users

Topic: How do I use instances in proofs?


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Ignat Insarov (Jun 20 2021 at 15:24):

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

view this post on Zulip Ignat Insarov (Jun 20 2021 at 15:24):

Why are they introduced like that in the first place?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Ignat Insarov (Jun 20 2021 at 15:44):

It even inlines the class dictionary.

view this post on Zulip 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.

view this post on Zulip Ignat Insarov (Jun 27 2021 at 18:23):

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

view this post on Zulip Gaëtan Gilbert (Jun 27 2021 at 18:26):

decode_encode

view this post on Zulip Ignat Insarov (Jun 27 2021 at 20:52):

Thanks!


Last updated: Jan 27 2023 at 01:03 UTC