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 p
s 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 y
s 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 z
s 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.
p = MyEq.refl x
then it follows that the type ofp
andMyEq.refl x
are equal, thereforeMyEq a x y = MyEq a x x
, hencex = y
by looking at the last argument. Similar reasoning applied toq
yieldsx = z
. But you are probably asking: what is the algorithm that allows Lean to figure ths out, yes? $\endgroup$