Stream: Coq users

Topic: ✔ Dependent Pattern Match -- Unification


view this post on Zulip Jacob Salzberg (Nov 01 2022 at 23:27):

Hi,

In the following example, in the second eq_refl, is x unified with y? Otherwise, I'm very confused as to how it can type the second eq_refl with y = x.

Section coqusers.
  Variables x y z : Type.

  Definition symm' : eq x y -> eq y x :=
    (fun H1 : eq x y => match H1 in (_ = y) return (y = x) with | eq_refl => eq_refl end).

  Print symm.

End coqusers.

view this post on Zulip Jacob Salzberg (Nov 01 2022 at 23:33):

(This is a proof generated by applying case on the hypothesis and then exact. I'm not interested in how the dependent mattern match is itself generated; instead i'm wondering what the mechanism behind typing eq_refl with : y = x is.)

view this post on Zulip Paolo Giarrusso (Nov 01 2022 at 23:39):

no, x and y remain distinct normal forms so they're not unifiable, and Check (eq_refl : x = y). still fails. The trick does not modify how unification behave; it changes the goal instead:

  Definition symm' : eq x y -> eq y x.
  refine (fun H1 : eq x y => match H1 in (_ = y) return (y = x) with | eq_refl => _ end).
    Fail Check (eq_refl : x = y).
    Eval cbv in x.
    Eval cbv in y.
    Show.
(* Output:

The command has indeed failed with message:
In environment
x, y, z : Type
H1 : x = y
The term "eq_refl" has type "x = x" while it is expected to have type
"x = y" (cannot unify "x" and "y").
     = x
     : Type
     = y
     : Type
1 goal

  x, y, z : Type
  H1 : x = y
  ============================
  x = x
*)

view this post on Zulip Paolo Giarrusso (Nov 01 2022 at 23:47):

IOW, the match does not tell Coq "let y be unifiable with x in the body". Rather, it replaces y by x in the goal when you do the match.

view this post on Zulip Paolo Giarrusso (Nov 01 2022 at 23:49):

since H1 : y = x is not part of the goal, it keeps its type, and we can use it to see that x and y still do not unify:

    Fail apply H1.
(*
The command has indeed failed with message:
In environment
x, y, z : Type
H1 : x = y
Unable to unify "x = y" with "x = x".
*)

This applies not just to the scrutinee but to all hypotheses!

view this post on Zulip Jacob Salzberg (Nov 01 2022 at 23:56):

Paolo Giarrusso said:

IOW, the match does not tell Coq "let y be unifiable with x in the body". Rather, it replaces y by x in the goal when you do the match.

I really appreciate your patience in explaining this to me.

I'm confused as to how the dependent pattern match can transform something of type x = x to something about y = x. Is it because in the context you have both (eq_refl : x x) and (eq_refl: x y) for the first witness?

My mental model/mental approximation of how case works is it takes k1, k2, ..., kn as, the proof obligations of each of the cases of the inductive type, and transforms them to a witness of the goal...

then does (match IndT with | Case1 => k1 | ... | CaseN => kn end)
and then within the context where k1, ..., kn are returned, how come our obligation here would be only to prove x = x? Is it because the types are equal in the environment, deduced from the two possible types of the equality witness?

Thanks

view this post on Zulip Paolo Giarrusso (Nov 02 2022 at 00:20):

First, do you have an environment that lets you step through the proof? If not, that's the first thing you should fix.

My mental model/mental approximation of how case works is it takes k1, k2, ..., kn as, the proof obligations of each of the cases of the inductive type, and transforms them to a witness of the goal...

You are describing a _forward_ proof, but typing here proceeds backwards: match transforms the goal y = x into a goal x = x.

how come our obligation here would be only to prove x = x? Is it because the types are equal in the environment, deduced from the two possible types of the equality witness?

Again, no. You keep asking if this is about unification, and I keep answering no. Since this is the 3rd time, let me be absolutely clear: Coq does not record that x and y are definitionally equal/unifiable/convertible. Coq only picks some occurrences of y in the goal and replaces those specific ones by x, as a consequence of nothing other than the match typing rule and the definition of the eq datatype.

For a proper explanation, chapter 8 of Chlipala's book, available at http://adam.chlipala.net/cpdt/html/MoreDep.html, might be helpful.

view this post on Zulip Paolo Giarrusso (Nov 02 2022 at 00:22):

Coq only picks some occurrences of y in the goal and replaces those specific ones by x,

Clarification:

view this post on Zulip Paolo Giarrusso (Nov 02 2022 at 00:27):

one reason I insist this is not a definitional equality is because in this goal you _can_ write set (w := y). to bind a _new_ variable w that is definitionally equal to y. And this is shown in the context as w:= y : Type! On the other hand, the context does _not_ have a binding saying y := x : Type — and that would be the only way to have a local variable y be convertible with another local variable x.

view this post on Zulip Paolo Giarrusso (Nov 02 2022 at 00:32):

^^ I hope the above helps a bit. Googling "convoy pattern" might also help — I've read https://jamesrwilcox.com/dep-destruct.html a long while ago

view this post on Zulip Notification Bot (Nov 02 2022 at 04:06):

Jacob Salzberg has marked this topic as resolved.


Last updated: Jan 28 2023 at 07:30 UTC