Zulip Chat Archive

Stream: general

Topic: Type theory of Lean


view this post on Zulip Mario Carneiro (Apr 22 2019 at 17:05):

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 .

view this post on Zulip Rob Lewis (Apr 22 2019 at 17:13):

Congrats!

view this post on Zulip Patrick Massot (Apr 22 2019 at 17:41):

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

view this post on Zulip Patrick Massot (Apr 22 2019 at 17:44):

Who would have believed to see this before Lean 4?

view this post on Zulip Wojciech Nawrocki (Apr 23 2019 at 13:41):

Congrats!

view this post on Zulip Wojciech Nawrocki (Apr 23 2019 at 15:13):

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?

view this post on Zulip Kevin Buzzard (Apr 23 2019 at 17:48):

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?

view this post on Zulip Wojciech Nawrocki (Apr 24 2019 at 12:15):

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

view this post on Zulip Mario Carneiro (Apr 25 2019 at 01:29):

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

view this post on Zulip Simon Hudon (Apr 25 2019 at 01:34):

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

view this post on Zulip Mario Carneiro (Apr 25 2019 at 04:02):

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

view this post on Zulip Mario Carneiro (Apr 25 2019 at 04:03):

plus axioms always have computation / canonicity troubles

view this post on Zulip Mario Carneiro (Apr 25 2019 at 04:11):

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

view this post on Zulip Patrick Massot (Apr 25 2019 at 15:23):

Who would have believed to see this before Lean 4?

That was a very narrow win...

view this post on Zulip Simon Hudon (Apr 25 2019 at 15:49):

Do you have a release date for Lean 4?

view this post on Zulip Patrick Massot (Apr 25 2019 at 15:50):

We didn't need a release to see it

view this post on Zulip Wojciech Nawrocki (Jun 13 2019 at 15:16):

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

view this post on Zulip Reid Barton (Jun 13 2019 at 15:22):

This looks provable in Lean

view this post on Zulip Reid Barton (Jun 13 2019 at 15:27):

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

view this post on Zulip Wojciech Nawrocki (Jun 13 2019 at 15:38):

Thanks!

view this post on Zulip Chris Hughes (Jun 13 2019 at 15:39):

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

view this post on Zulip Wojciech Nawrocki (Jun 13 2019 at 15:41):

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

view this post on Zulip Chris Hughes (Jun 13 2019 at 15:43):

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

view this post on Zulip Kevin Buzzard (Jun 13 2019 at 15:58):

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".

view this post on Zulip Kevin Buzzard (Jun 13 2019 at 15:59):

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.


Last updated: May 16 2021 at 05:21 UTC