Understanding refl

Stream: new members

[Morten Brodersen]

I am trying to truly understand the fundamentals of proving using type theory. In the following code I have implemented my own equivalence relation and are proving a few things with and without using tactics. That seems to work. However the rec_on function (used in meq.symmetry_2) is a bit magical to me. I can get it to do what I want, by following the types, but it isn't clear to me why it works?

namespace my_eq

inductive meq {a : Type} : a → a → Prop
| refl {x : a} : meq x x

--private def refl := @meq.refl

def meq.symmetry {a : Type} {x y : a} : meq x y → meq y x :=
begin intro h, cases h, apply h end

def meq.symmetry_2 {a : Type} {x y : a} (exy : meq x y) : meq y x :=
  meq.rec_on exy (λ {x : a}, meq.refl)

def meq.transitive {a : Type} {x y z : a} : meq x y → meq y z → meq x z :=
begin intro h1, intro h2, cases h1, cases h2, apply h1 end

def meq.left {a : Type} {x y z : a} (exz : meq x z) (eyz : meq y z) : meq x y :=
  let ezy := meq.symmetry eyz in
    meq.transitive exz ezy

def meq.right {a : Type} {x y z : a} (exy : meq x y) (exz : meq x z) : meq y z :=
  let eyx := meq.symmetry exy in
    meq.transitive eyx exz

end my_eq

[Mario Carneiro]

meq is an indexed inductive type which is true only when the two indices are the same. (That is, it's another way to write =.) The eliminator for this type says that any property C x y is true for all x, y such that meq x y if C x x is true for all x. In normal parlance we would call this the substitution property of equality: if x = y and P x is true then P y is as well. So proving symmetry is as simple as "recursion on equality": we know meq x y so we can assume x and y are the same; thus we are proving meq x x and meq.refl works

[Morten Brodersen]

Thanks Mario! Much appreciated.

[Morten Brodersen]

OK here is how far I get reasoning about meq.rec_on:

Starting with the type signature:

meq.rec_on : meq ?M_3 ?M_4 → (Π {x : ?M_1}, ?M_2 x x) → ?M_2 ?M_3 ?M_4

and substituting to match the required end type (meq y x) and arbitrary type A:

meq.rec_on : meq y x → (Π {x : A}, meq x x) → meq y x

we still require (meq y x) to prove (meq y x). Which we obviously don't have?

[Morten Brodersen]

(deleted)

[Eric Wieser]

You filled in ?M_2 backwards

[Eric Wieser]

#check @meq.rec_on is more insightful as it doesn't show the ?s

[Mario Carneiro]

Here ?M_2 is being assigned (\lam y x, meq x y). Note that when you plug in y, x to this you get meq x y which is the goal, and when you plug in x, x as in the minor premise you get meq x x which is the thing we can prove by refl

[Morten Brodersen]

I don't think so? I tried both manually and using the editor to auto swap. Here is what I substitute:

meq.rec_on :
  Π {a : Type}
    {C : a → a → Sort u_1}
    {ᾰ ᾰ_1 : a},
    meq ᾰ ᾰ_1 → (Π {x : a}, C x x) → C ᾰ ᾰ_1

C   -> meq
ᾰ   -> y
ᾰ_1 -> x

meq.rec_on :
  Π {a : Type}
    {meq : a → a → Sort u_1}
    {y x : a},
    meq y x → (Π {x : a}, meq x x) → meq y x

[Mario Carneiro]

You don't want to assign C := meq because that doesn't get you anywhere, as you point out

[Mario Carneiro]

the trick is to use C := \lam y x, meq x y instead

[Mario Carneiro]

because then C y x, which is what you want to show, works out to meq x y which is actually the goal

[Mario Carneiro]

lean will work backwards from the goal to figure out what C should be

[Morten Brodersen]

OK that makes sense. What confuses me is the (C x x). It doesn't allow you to use two different args? In other words, you can't do (C y x)?

[Mario Carneiro]

Note that it's an argument, so being more restrictive there is to your advantage

[Mario Carneiro]

it's saying you only have to prove C x x rather than C x y for all x, y

[Mario Carneiro]

in particular, if it wasn't then you wouldn't be able to finish the proof by refl

[Mario Carneiro]

You can always use additional arguments beyond the listed ones, like say some other variable a, by using a choice for C that contains a free occurrence of a

[Mario Carneiro]

you can even choose not to generalize some of the arguments in the goal, for example you could take C := \lam _ _, meq x y instead

[Mario Carneiro]

that would be silly though because in that case C x x is meq x y so you won't have made any progress in the proof

[Morten Brodersen]

But (C x x) is (\lam y x, meq x y) x x = (\lam x, meq x x) x = (meq x x) and not (meq x y)?

[Mario Carneiro]

I mean if you set C to \lam _ _, meq x y, then C x x = (\lam _ _, meq x y) x x = meq x y

[Mario Carneiro]

by underscores I mean an ignored argument, i.e. this is a constant function

[Morten Brodersen]

Ahhhhh! I get it now. Because x and y is part of the lambda context so it can be accessed in C.

[Morten Brodersen]

Sorry that was exactly what you were saying by using _ _ :-) Thanks Mario this has been really helpful! Looking forward to reading your thesis.

[Mario Carneiro]

they are both available in the "outer context", and now C is giving you two more arguments to play with. By choosing whether to use them or not you decide how the goal is generalized

[Morten Brodersen]

Yep exactly I get it now :-) Excellent!

[Mario Carneiro]

by the way, you can see the specific arguments lean used by

set_option pp.all true
#print meq.symmetry_2

[Mario Carneiro]

  @my_eq.meq.rec_on.{0} a (λ (_x _x_1 : a), @my_eq.meq a _x_1 _x) x y exy (λ {x : a}, @my_eq.meq.refl a x)

[Mario Carneiro]

this part -> (λ (_x _x_1 : a), @my_eq.meq a _x_1 _x) is what I wrote as \lam y x, meq x y earlier

[Morten Brodersen]

Yep. I fully understand it now Mario. I write functional compilers for a living but forgot about the lambda environment and mixing up x with x where I shouldn't.