Two silly questions

Stream: Berkeley Lean Seminar

[Rahul Dalal]

What is the difference between passing in something like "function \< a b \> " and just doing "function a b"

Related to this, what exactly is rintro \<a b\> doing? What does it mean when one of those is replaced with rfl?

[Kevin Buzzard]

\<a, b\> is one term, and a b is two.

[Kevin Buzzard]

Sometimes you want to deal with the type of natural numbers less than $n$. In Lean this is the "canonical set of size $n$" and it's denoted fin n.

[Kevin Buzzard]

A term of type fin n is two things: a natural number $m$, and a proof that $m<n$. The way I thought about such a concept for decades was that $m$ was a number and the proof that $m<n$ was a proof, and that numbers and proofs were entirely different things. An interesting consequence of doing maths in Type theory rather than set theory is that $m$ is a term, and a proof that $m<n$ is also a term.

[Kevin Buzzard]

So a term of type fin n is a package of data, consisting both of m and the proof that m<n. In particular if a : fin n then a is not a natural number.

[Kevin Buzzard]

So given that a is some kind of package of data, one has to know how to get to m and the proof.

[Kevin Buzzard]

To figure out how to do this, we need to look at the definition of fin n by typing something like #check fin and then right clicking on fin and peeking at the definition. We find that fin n is defined to be a structure, which means an inductive type with one constructor.

[Kevin Buzzard]

structure fin (n : nat) :=
(val : nat)
(is_lt : val < n)

[Kevin Buzzard]

So if a : fin n then a.val will be the $m$ above, and a.is_lt will be the proof that it's less than $n$.

[Kevin Buzzard]

example : ∀ (x : fin 10), ∃ m, m < 10 :=
begin
  sorry
end

In this example, the claim is that for every x of type fin 10 we can find an m such that m<10. Note that m=x won't do, because x isn't a natural number, despite the fact that sometimes people will refer to $x$ as "a natural number less than 10". It's not that, it's a term of type fin 10 so it's a pair.

[Kevin Buzzard]

import tactic -- I always do this

example : ∀ (x : fin 10), ∃ m, m < 10 :=
begin
  intro x,
  /-
  x : fin 10
  ⊢ ∃ (m : ℕ), m < 10
  -/
  use x.val,
  /-
  x : fin 10
  ⊢ x.val < 10
  -/
  exact x.is_lt
end

[Kevin Buzzard]

The natural number we use is x.val, and the proof it satisfies the right thing is x.is_lt.

[Kevin Buzzard]

Another way of getting the terms out of a structure is to use the cases command.

import tactic -- I always do this

example : ∀ (x : fin 10), ∃ m, m < 10 :=
begin
  intro x,
  cases x with m hm,
  /-
  m : ℕ,
  hm : m < 10
  ⊢ ∃ (m : ℕ), m < 10
  -/
  use m,
  exact hm
end

[Kevin Buzzard]

cases is a core Lean tactic. Sometimes structures are fancier objects though, with 3 or more fields, or fields containing other structures, and so the rcases tactic was born, which can take more complex structures apart. For this the standard cases syntax of just listing variable names wasn't powerful enough, so they started with these pointy brackets.

import tactic -- I always do this

example : ∀ (x : fin 10), ∃ m, m < 10 :=
begin
  intro x,
  rcases x with ⟨m, hm⟩,
  use m,
  exact hm
end

[Kevin Buzzard]

intro, rcases was such a common idiom that rintro was born:

example : ∀ (x : fin 10), ∃ m, m < 10 :=
begin
  rintro ⟨m, hm⟩,
  use m,
  exact hm
end

[Kevin Buzzard]

This introduces x and then instantly takes it apart into its pieces.

[Kevin Buzzard]

Here's a silly structure:

import tactic -- I always do this

structure silly :=
(n : ℕ)
(b : bool)
(m : ℕ)
(h : n < 37)
(hmn : m = n)

example : ∀ x : silly, x.m < 37 :=
begin
  sorry
end

[Kevin Buzzard]

To make a term of type silly you need to supply two naturals, a boolean, a proof that the two naturals are equal, and a proof that one of the naturals is less than 37.

[Rahul Dalal]

Thank you!

[Kevin Buzzard]

Using our rintro skills we can solve this example as follows:

example : ∀ x : silly, x.m < 37 :=
begin
  rintro ⟨n, b, m, h, hnm⟩,
  -- goal is now a mess
  dsimp,
  /-
  n : ℕ,
  b : bool,
  m : ℕ,
  h : n < 37,
  hnm : m = n
  ⊢ m < 37
  -/
  rw hnm,
  -- ⊢ n < 37
  exact h,
end

[Kevin Buzzard]

(dsimp simplifies {m := blah, ... }.m to blah)

[Kevin Buzzard]

But rintro has got one more trick up its sleeve -- instead of rintroing hnm we can put rfl instead, which just means "define one side to be the other side".

[Kevin Buzzard]

example : ∀ x : silly, x.m < 37 :=
begin
  rintro ⟨_, b, m, h, rfl⟩,
  -- h is now a proof of m<37!
  exact h,
end

[Kevin Buzzard]

tactic#rintro

[Rahul Dalal]

So practically, you can put rfl in any spot where the corresponding term is an equality or equivalence and it will apply this to everything other term you are creating in the rintro?

[Kevin Buzzard]

I'm not sure about an equivalence but yes an equality

[Kevin Buzzard]

It will look to see if one side or the other is a bare variable, and if one of them is then it will basically just sub in its value everywhere

[Kevin Buzzard]

What it's actually doing is cases h if h : a = b!

[Kevin Buzzard]

Because = is not a primitive notion in type theory, it's notation for eq which is an inductive type with one constructor, just like silly

[Kevin Buzzard]

eq a b is an inductive type with one constructor, refl a which is a term of type eq a a (note I just corrected a bad typo here)

[Kevin Buzzard]

If you work out the recursor for that type, it's the principle that if you know P(a) and you know that a=b, you can deduce P(b)

[Kevin Buzzard]

Ie it's the fact that you can substitute in an equality

[Kevin Buzzard]

This is the basic principle behind the rewrite tactic

[Rahul Dalal]

ok, thanks again!