## Stream: Coq users

### Topic: ✔ Dependent Pattern Match -- Unification

#### 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.
``````

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

#### 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
*)
``````

#### 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.

#### 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!

#### 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

#### 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.

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

• "which occurrences" is deduced from the annotations of `match ... in ... return`
• for this specific match, `y` occurs once in the goal, and the annotations ask Coq to replace that single occurrence

#### 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`.

#### 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

#### Notification Bot (Nov 02 2022 at 04:06):

Jacob Salzberg has marked this topic as resolved.

Last updated: Jun 24 2024 at 01:01 UTC