How does Lean figure out that these variables are equal?

Question

This code type checks:

inductive MyEq (a : Type) : a -> a -> Type where
  | myRefl (x : a) : MyEq a x x

def concat (p : MyEq a x y) (q : MyEq a y z) : MyEq a x z :=
  match p, q with
  | MyEq.myRefl x, MyEq.myRefl x => MyEq.myRefl x

But why? Each instance of MyEq.myRefl x on the last line seems to have the wrong type for its context: the expected types are MyEq a x y, MyEq a y z, and MyEq a x z, but the type is MyEq a x x in all three cases.

But any slight modification of this code fails to type check, for example

def concat (p : MyEq a x y) (q : MyEq a y z) : MyEq a x z :=
  match p, q with
  | MyEq.myRefl y, MyEq.myRefl y => MyEq.myRefl y

or

def concat (p : MyEq a x y) (q : MyEq a y z) : MyEq a x z := p

or

def concat (p : MyEq a x y) (q : MyEq a y z) : MyEq a x z :=
  match p, q with
  | MyEq.myRefl w, MyEq.myRefl x => MyEq.myRefl x

where w here is meant to be a variable introduced by pattern matching.

I know that, by the elimination rule of the identity type, a function with the same type as concat should be able to be defined. And I'm assuming that Lean somehow generates a corresponding elimination rule for this type based on the inductive statement. But I don't understand why concat is able to be defined by this specific code, which seems nonsensical to me.

Specifically what I would like to know is:

1. Why does Lean accept the first code? Is it some kind of "syntax sugar", where Lean goes above and beyond and automatically figures out that x, y, and z are equal? If so then is there a simpler way of writing this that doesn't rely on the interpreter being smart?

2. Why aren't the other three examples I give valid?

Answer 1

While I probably can't go into the nitty gritty of Lean's code, I think I can explain why what Lean is doing is natural given the recursion rule for equality and that its behavior is predictable and understandable.

Simple inductive type

Let's start with a simple inductive type and a simple recursive construction:

inductive MyContainer (a : Type) : Type where
  | myConst (x : a) (y : a) : MyContainer a

def foo (p : MyContainer a) (f : a -> b): MyContainer b :=
  match p with
  | MyContainer.myConst x y => MyContainer.myConst (f x) (f y)

Here x and y are both acting as variables and can be replaced with anything, including banana. Also, it is helpful to look at the recursor for MyContainer. It is the axiom/rule that does all the work when you want to prove anything about MyContainer.

#print MyContainer.rec
-- recursor MyContainer.rec.{u} : 
--   {a : Type} →
--   {motive : MyContainer a → Sort u} → 
--   ((x y : a) → motive (MyContainer.myConst x y)) → 
--   (t : MyContainer a) → motive t

There is a lot going on here, but the important bit is that to use recursion on MyContainer, one is trying to construct a motive which is just the output Type/Prop/Sort (which may or may not be dependent on the input). One also needs to (obviously) supply an input object t : MyContainer which is the thing you are recursing over. Finally, one needs to supply a way to construct an object of the output motive from the input, but note in this case it is not from the input t itself, but from the x and y inside t, which makes sense since t : MyContainer a is uniquely specified by its inner x and y.

match ... with is just semantic sugar and abstraction around rec. To see what is going on, let's use pp.all:

set_option pp.all true
#print foo
-- def foo : {a b : Type} → MyContainer a → (a → b) → MyContainer b :=
--   fun {a b : Type} (p : MyContainer a) (f : a → b) =>
--     @foo.match_1.{1}
--       a
--       (fun (p : MyContainer a) => MyContainer b)
--       p
--       fun (x y : a) => @MyContainer.myConst b (f x) (f y)

You can look up the automatically generated definition foo.match_1 yourself, but basically it has a similar type to MyContainer.rec. And we supply it the same sort of objects:

• The motive is fun (p : MyContainer a) => MyContainer b, so the output of the match is MyContainer b.
• The input: p.
• The function constructed by the match is fun (x : a) => @MyContainer.myConst b (f x).

To really see more of what match is doing, let's look at a slightly different construction where p is used more than once. To do that let's just define a trivial relation

def R (t : T) := t = t

Now, here is half a construction:

def foo' (p : MyContainer a) (h : R p) (f : a -> b): MyContainer b :=
  match p with
  | MyContainer.myConst x y => _

If we hover over the _ we get this goal:

a b: Type
p: MyContainer a
f: a → b
x y: a
h: R (MyContainer.myConst x y)
⊢ MyContainer b

Notice all ps are replaced with MyContainer.myConst x y, including our h. The one exception to this is the original p we gave as input to the match statement. This is also apparent in the generated code for foo' (after we finish writing the code same as before):

-- def foo' : {a b : Type} → (p : MyContainer a) → @R.{1} (MyContainer a) p → (a → b) → MyContainer b :=
--   fun {a b : Type} (p : MyContainer a) (h : @R.{1} (MyContainer a) p) (f : a → b) =>
--     @foo'.match_1.{1}
--       a
--       (fun (p : MyContainer a) (h : @R.{1} (MyContainer a) p) => MyContainer b)
--       p
--       h
--       fun (x y : a) (h : @R.{1} (MyContainer a) (@MyContainer.myConst a x y)) => @MyContainer.myConst b (f x) (f y)

Notice h is now an input just like p and factors into the motive and the function that match is constructing.

Dependent Inductive Type

Now let's look at what happens if we have a dependent type whose type parameters and inner values align:

inductive MyDepContainer (a : Type) : a -> Type where
  | myConst (x : a) (y : a) : MyDepContainer a x

Now the recursor (where I replaced a variable name to make it more readable) looks similar but a bit different :

#print MyDepContainer.rec
-- recursor MyDepContainer.rec.{u} :
--   {a : Type} →
--   {x : a} →
--   {motive : MyDepContainer a x → Sort u} →
--   ((y : a) → motive (MyDepContainer.myConst a x y)) →
--   (t : MyDepContainer a x) → motive t

The big difference from before is that the function we are constructing is of type ((y : a) → motive (MyDepContainer.myConst a x y)). Why do we only have the y input and not the x input? Well, we don't need x because we already have x to specify the type of t. There is nothing we discover about x by looking inside t.

We use a match on MyDepContainer as follows.

def bar (p : MyDepContainer a x) (f : a -> b): MyDepContainer b (f x) :=
  match p with
  | MyDepContainer.myConst x y => MyDepContainer.myConst (f x) (f y)

While y could be replaced with anything, x cannot be anything but x. Lean knows this, and we could even just write _ in place of the first x and in place of (f x), which also can't be anything but f x.

This is apparent when printing the code for bar:

set_option pp.all true
#print bar
-- def bar : {a : Type} → {x : a} → {b : Type} → MyDepContainer a x → (f : a → b) → MyDepContainer b (f x) :=
--   fun {a : Type} {x : a} {b : Type} (p : MyDepContainer a x) (f : a → b) =>
--     @bar.match_1.{1}
--       a
--       x
--       (fun (p : MyDepContainer a x) => MyDepContainer b (f x))
--       p
--       fun (y : a) => @MyDepContainer.myConst b (f x) (f y)

Again, the function we are constructing which gets applied to p doesn't need to know anything about x.

Identity types

Finally, we can get to your type MyEq, which is an identity type. (As an aside, I assume you are familiar at least a little homotopy type theory since you constructed the main object of interest in that field, but if not, see section 1.12 of the HoTT book for more on recursion and induction for this type.) The recursor for MyEq is as follows (where I replaced some of the variable names to make it more readable):

recursor MyEq.rec.{u} :
  {a : Type} →
  {x : a} →
  {motive : (y : a) → MyEq a x y → Sort u} →
  motive x (MyEq.myRefl x) → 
  {y : a} → 
  (t : MyEq a x y) → 
  motive y t

Now we have two inputs y and t : MyEq a x y to the recursor (and to the motive). Just like the previous example, we don't need x to construct an element of the motive, but now we don't need y either since it is also a parameter to the type. But here is is especially important that our motive can be dependent on y. In the end we want to construct something that depends on our input y (and sometimes on the path t). Let's call the motive P. Then we are trying to construct an element (or proof) of P y t. But the function we are constructing is not of that form. To construct and element/proof of P y t it is enough to give a construction of an element of P x (MyEq.myRefl x). This makes sense if you think of your type as the equality type x = y.

Okay, here is a simple example:

def baz (p : MyEq a x y) (f : a -> b) : MyEq b (f x) (f y) :=
  match p with
  | MyEq.myRefl x => MyEq.myRefl (f x)

Again, we can't supply anything else but x as input. Let's look at the function details:

-- def baz : {a : Type} → {x y : a} → {b : Type} → MyEq a x y → (f : a → b) → MyEq b (f x) (f y) :=
--   fun {a : Type} {x y : a} {b : Type} (p : MyEq a x y) (f : a → b) =>
--     @baz.match_1.{1}
--       a
--       x
--       (fun (y : a) (p : MyEq a x y) => MyEq b (f x) (f y))
--       y
--       p
--       fun (_ : Unit) => @MyEq.myRefl b (f x)

So per the discussion above, the function we are trying to convey with this match has to have type of the motive x (myEq.myRefl x), which in this case is MyEq b (f x) (f x), that is where y is replaced with x.

To better see this in action, let's look at on more example which is closer to your example:

def baz2 (p : MyEq a x y) (q : MyEq a y z) (f : a -> b) : MyEq b (f x) (f z) :=
  match p with
  | MyEq.myRefl x => _

I have only filled in half the proof for the moment. But if you hover over the _, it will tell you what you have to fill in:

a: Type
x y z: a
b: Type
p: MyEq a x y
f: a → b
q: MyEq a x z
⊢ MyEq b (f x) (f z)

All the ys have been replaced with x except for y and p which are the official inputs to the match statement, so q now has type q: MyEq a x z. (This is similar to what we saw with the simple inductive type example.) Therefore, if we nest our match one more level, we have to use MyEq.myRefl x for q since that now matches the type of q:

def baz2 (p : MyEq a x y) (q : MyEq a y z) (f : a -> b) : MyEq b (f x) (f z) :=
  match p with
  | MyEq.myRefl x =>
    match q with
    | MyEq.myRefl x => _

Again, what we need to show is

a: Type
x y z: a
b: Type
p: MyEq a x y
f: a → b
q: MyEq a x z
⊢ MyEq b (f x) (f x)

where now all zs have been replaced with x except z and q which are inputs to our function.

And finally, your match is just basically sugar for nested matches. You can start to see now what is going on.