Type theory of Lean

Stream: general

[Mario Carneiro]

I just delivered my master's thesis on lean's type theory, and the talk was recorded: https://www.youtube.com/watch?v=3sKrSNhSxik . It builds up the motivation for all the complexity in DTT, so if you have a basic understanding of how proof judgments are presented you should be able to follow it. The repo with the full thesis is https://github.com/digama0/lean-type-theory/releases .

[Rob Lewis]

Congrats!

[Patrick Massot]

http://phdcomics.com/comics/archive.php?comicid=590

[Patrick Massot]

Who would have believed to see this before Lean 4?

[Wojciech Nawrocki]

Congrats!

[Wojciech Nawrocki]

f == g -> x == y -> f x == g y is unprovable

Oops, so that's why I couldn't do it when I tried recently. Do you know if this is consistent as an added axiom?

[Kevin Buzzard]

Don't add axioms! It's not really how Lean works, and support for them is poor. If you need it, add a variable. But people in general try to avoid heq completely. Why do you think you need it at all?

[Wojciech Nawrocki]

I agree that adding axioms is probably undesirable, but it would be interesting to see whether this one is consistent with Lean from a purely type-theoretical point of view

[Mario Carneiro]

It's consistent, because it follows from injectivity of pi

[Simon Hudon]

Are you saying that adding injectivity of pi is sufficient to prove it? Is there a down side to having that axiom?

[Mario Carneiro]

One downside, as Carlo mentioned to me, is that it breaks the types-as-sets model, and the types-as-cardinalities model

[Mario Carneiro]

plus axioms always have computation / canonicity troubles

[Mario Carneiro]

axiom pi_injective₁ {α : Sort*} {β : α → Type*} {α' : Sort*} {β' : α' → Type*}
  (H : (Π a, β a) = (Π a, β' a)) : α = α'

axiom pi_injective₂ {α : Sort*} {β β' : α → Type*}
  (H : (Π a, β a) = (Π a, β' a)) (a) : β a = β' a

theorem heq_congr {α : Sort*} {β : α → Type*} {α' : Sort*} {β' : α' → Type*}
  {f : Π a, β a} {g : Π a, β' a} {x : α} {y : α'}
  (h₁ : f == g) (h₂ : x == y) : f x == g y :=
begin
  cases pi_injective₁ (type_eq_of_heq h₁),
  cases (funext $ pi_injective₂ (type_eq_of_heq h₁) : β = β'),
  cases h₁, cases h₂, refl
end

[Patrick Massot]

Who would have believed to see this before Lean 4?

That was a very narrow win...

[Simon Hudon]

Do you have a release date for Lean 4?

[Patrick Massot]

We didn't need a release to see it

[Wojciech Nawrocki]

What about functional extensionality over heq? I think it doesn't hold in pure CiC, but maybe it's provable in Lean's theory (or in Lean+pi_injective)? Something like

axiom heq_funext {α β: Type u} {A: α → Type v} {B: β → Type v}
  (f: Π a: α, A a) (g: Π b: β, B b)
  : α = β → (∀ (a: α) (b: β), a == b → f a == g b) → f == g

[Reid Barton]

This looks provable in Lean

[Reid Barton]

Here is my unoptimized proof

lemma heq_funext {α β: Type u} {A: α → Type v} {B: β → Type v}
  (f: Π a: α, A a) (g: Π b: β, B b)
  : α = β → (∀ (a: α) (b: β), a == b → f a == g b) → f == g :=
begin
  rintro rfl h,
  have : A = B,
  { apply funext,
    intro a,
    apply type_eq_of_heq (h a a heq.rfl) },
  subst this,
  apply heq_of_eq,
  apply funext,
  intro a,
  apply eq_of_heq (h a a heq.rfl)
end

[Wojciech Nawrocki]

Thanks!

[Chris Hughes]

Golfed

lemma heq_funext {α β: Type u} {A: α → Type v} {B: β → Type v}
  (f: Π a: α, A a) (g: Π b: β, B b)
  : α = β → (∀ (a: α) (b: β), a == b → f a == g b) → f == g :=
function.hfunext

[Wojciech Nawrocki]

:smiley: I was looking for this in heq parts of the library

[Chris Hughes]

Alternatively

lemma heq_funext {α β: Type u} {A: α → Type v} {B: β → Type v}
  (f: Π a: α, A a) (g: Π b: β, B b)
  : α = β → (∀ (a: α) (b: β), a == b → f a == g b) → f == g :=
by library_search

[Kevin Buzzard]

library_search is still not my first instinct with these sorts of things, and it probably should be. Sometimes I think "probably I need import mathlib for the search to work".

[Kevin Buzzard]

Of course, Chris' triumph should be seen within the context of the hours of pain he had when trying to deal with heq last year.

[Juho Kupiainen]

@Mario Carneiro Can the types of Lean be regarded as sets in some usual sense? I mean, in mathlib the module (vector space) axioms are defined by saying that the "add" and "scalar multiplication" functions are Lean functions. If I'm formalizing math that was originally defined with set theory, as a lot of math has been, can I just replace all sets with types? Or should I define set theory inside Lean in some particular way first.

[Yaël Dillies]

No, in general the sets you're not set operations (union, intersection... but not cartesian product or sum) with should be types.

[Juho Kupiainen]

I feel it would be useful to have a guide for how to formalize math that was previously defined in set theory.

[Reid Barton]

The one line summary is Type = set, set = subset.

[Yaël Dillies]

i think it's hard to get too specific, but really the main guidance what Reid just said.

[Mario Carneiro]

(I don't have anything to add for the general situation, Reid is right)

[Patrick Massot]

Juho Kupiainen said:

I feel it would be useful to have a guide for how to formalize math that was previously defined in set theory.

The main trick is to realize you are lying to yourself. The math you are thinking of have not been "previously defined in set theory". They have been defined outside of any formal foundation. However they are usually expressed using a vocabulary that is inspired by set theory, but this is a very superficial connection with set theory. When using Lean you can mostly ignore foundational details (unless you want to formalize computer science). You'll get used to it very quickly.

[Kevin Buzzard]

In particular, "A ring is a set equipped with an addition, a multiplication..." is what we say, "A ring is a collection of stuff equipped with an addition..." is what we mean, and "A ring is a type equipped with..." is what we say in Lean, but it's all the same thing.