How to reason about the proof for Eq.symm?

Stream: new members

[Matthias Geier]

I guess this is a valid proof for the symmetry of equality:

example (h : a = b) : b = a :=
  h ▸ rfl

I don't understand the operator ▸ yet, so I thought I try something that's easier to understand for me:

example (h : a = b) : b = a :=
  match h with
  | rfl => rfl

This in turn should be more or less the same as this:

example (h : a = b) : b = a :=
  match h with
  | Eq.refl a => Eq.refl a

Now comes my question: how can I understand how and why exactly this type-checks?

The input type is a = b, I'm matching with something that expects type a = a and the return type is b = a. Of course, ultimately, all those are the same type, but how does the compiler know?

It's not as easy as all those are equivalent, because if I replace Eq.refl a with Eq.refl b in either position (or both), this ceases to be accepted by Lean.

The reason why I'm asking is that I tried to create my own Eq type (as a learning exercise):

inductive MyEq : α → α → Prop where
  | refl (a : α) : MyEq a a

@[match_pattern] def my_rfl {a : α} : Eq a a := Eq.refl a

With this, I can re-write the proof, and this type-checks:

example (h : MyEq a b) : MyEq b a :=
  match h with
  | MyEq.refl a => MyEq.refl a

However, this doesn't work:

example (h : MyEq a b) : MyEq b a :=
  match h with
  | my_rfl => my_rfl

I tried it with an without @[match_pattern], which causes two different errors:

Type mismatch
  my_rfl
has type
  ?m.7 = ?m.7
but is expected to have type
  MyEq a b

Type mismatch
  my_rfl
has type
  MyEq a b
but is expected to have type
  MyEq b a

Did I make a mistake in my MyEq type?
Or is there something else going on that I'm not aware of?

[Kenny Lau]

Matthias Geier said:

how can I understand how and why exactly this type-checks

you can always #print out the proof:

theorem foo {α : Type} {a b : α} (h : a = b) : b = a :=
  h ▸ rfl

set_option pp.notation false
set_option pp.explicit true
-- set_option pp.all true
#print foo

[Kenny Lau]

Lean is not magic, every notation is required to unfold via 100 layers to an actual Lean expression that the kernel typechecks

[Robin Arnez]

However, this doesn't work:

-@[match_pattern] def my_rfl {a : α} : Eq a a := Eq.refl a
+@[match_pattern] def my_rfl {a : α} : MyEq a a := MyEq.refl a

[Matthias Geier]

Thanks for the hint with #print, that's very helpful!

Any yes, silly me, I should have used MyEq instead of Eq! with this (and with @[match_pattern]) now it works!

However this still leaves my original question: how does the compiler resolve the types a = b, a = a and b = a?

[Kenny Lau]

you're asking a very broad question here, there are many steps and i don't know which step you're referring to

[Matthias Geier]

Fair enough. I guess I can narrow it down to 2 questions:

• why does the pattern Eq.refl a accept a term of type a = b (even though it should be a = a)?
• why is it OK that the match statement returns a term of type a = a, but the return type of the function is supposed to be b = a?

(and I know that those all mean the same thing, but how does the compiler know?)

[Kenny Lau]

the concept here is inductive types

[Kenny Lau]

https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html

[Kenny Lau]

Eq has one constructor, so it comes with the "axiom" that the only way to ever make Eq is by calling the constructor

[Kenny Lau]

the compiler or whatever part of lean, it sees that a and b are both free variables

[Kenny Lau]

so when you do matching it says ok these are free variables so let's specialise their values to c because of the constructor Eq.refl c

[Kenny Lau]

by the philosophy that propositions are types, consider instead the following:

def emphasiseZero (n : Nat) : Nat :=
  match n with
  | Nat.zero => 0
  | Nat.succ m => 37

[Kenny Lau]

Nat is similarly an inductive type, with two constructors

[Kenny Lau]

so the compiler sees that n is a free variable and it freely assumes that it is formed from either one of the two constructors

[Kenny Lau]

for a more concrete answer, have a look at the following outputs:

#check Nat.rec
#check Eq.rec

[Kenny Lau]

convince yourself that Nat.rec is the "recursion" that everyone knows

[Kenny Lau]

try to connect it to the definition of Nat as an inductive type with two constructors

[Kenny Lau]

and then convince yourself that Eq.rec follows the exact same logic

[Matthias Geier]

I was hoping I could understand this without having to understand Eq.rec. This is something that's too much for my abilities right now ...

But coming back to your mention of MyEq c: I realized that I was probably re-using the name a for two different things ... but then I saw that this doesn't compile:

example (h : a = b) : b = a :=
  match h with
  | Eq.refl c => Eq.refl c

It says "Unknown identifier c".

[Kenny Lau]

I see, it seems like the first argument is actually anchored in the matching principle

[Kenny Lau]

as in, only b is free there, and the matcher substitutes it with the value of the left hand side

[Kenny Lau]

example {a b : Nat} (h : 4 + b = a) : a = 4 + b :=
  match h with
  | Eq.refl _ => _

example {a b : Nat} (h : a = 4 + b) : a = 4 + b :=
  match h with
  | Eq.refl _ => _

[Kenny Lau]

for more context, compare these two examples, and try to put stuff in the underscores, and you'll find out that only (4+b) works for the first example and only a works for the second example, which means that it anchors the LHS and destructs the RHS

[Robin Arnez]

If you print out the match, you'll see that it has pulled in b into the match:

def test (h : a = b) : b = a :=
  match b, h with
  | .(a), Eq.refl a => Eq.refl a

In other words, Eq.refl a type-checks in this place because it has also match b to be a

[Robin Arnez]

You can also do this the other way around yourself, although Lean seems to always pull in the second one by default:

def test (h : a = b) : b = a :=
  match a, h with
  | .(b), Eq.refl b => Eq.refl b

[Kenny Lau]

also ignore the "free" stuff i said, that has basically nothing to do with it

[Robin Arnez]

You can also introduce a new variable by matching on all variables:

def test (h : a = b) : b = a :=
  match a, b, h with
  | .(c), c, Eq.refl c => Eq.refl c

[Kenny Lau]

what is .()?

[Robin Arnez]

That's a so-called inaccessible pattern, which is used when the value within the .() is determined by typing

[Matthias Geier]

Wow, thanks! That's a lot to wrap my head around ... I'll play around with this to see if it clarifies the situation for me.

[Robin Arnez]

e.g. the .(c) is forced by the typing of Eq.refl c

[Aaron Liu]

Kenny Lau said:

I see, it seems like the first argument is actually anchored in the matching principle

The first argument is a parameter and the second argument is an index

Example of a parameter: the n in Fin n
Example of an index: the n in Fin2 n