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

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

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

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.

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!

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

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.

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

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`

.

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

Jacob Salzberg has marked this topic as resolved.

Last updated: Oct 05 2023 at 02:01 UTC