Formalizing Dependent Type Theory

Stream: general

[Viliam Vadocz]

How would one go about formalizing something like this?
image.png

I am following Introduction to Homotopy Type Theory by Egbert Rijke (https://arxiv.org/abs/2212.11082) and in it they suggest that "The more ambitious student may even try to formalize the solutions of some of the exercises in a computer proof assistant." I wonder how this is done, since I want to try and learn Lean by reading the book and trying to formalize the exercises.

Lean already uses dependent types, but trying something like this does not work:

variable (A A' : Type)
variable (a : A)

axiom eq: A = A'

example: (a : A') := by
  rw [eq] at a
  sorry

I thought maybe instead I need to define dependent types inside Lean (e.g. create types for the Context, Judgements, write axioms for the inference rules), but this did not feel right. For example, nowhere do I define that future types that I add may depend only on the previously added elements. I also have no clue how to actually make the axioms work.

inductive Context where
  | empty
  | comma (Γ : Context) (element: Value) (type: Type)

inductive Judgement where
  | type (Γ : Context) (A: Type)
  | equal_types (Γ : Context) (A : Type) (B : Type)
  | element (Γ : Context) (a : Value)
  | equal_elements (Γ : Context) (a : Value) (b : Value)


variable (Γ : Context)
variable (x₁ x₂ : Value)
variable (A₁ A₂ : Type)

def formation₁: (Judgement.type (Context.comma Γ x₁ A₁) A₂) → (Judgement.type Γ A₁)

I would appreciate some help with how to get started with formalizing dependent type theory for the purpose of verifying my solutions to exercises in the book.

[Mario Carneiro]

Viliam Vadocz said:

Lean already uses dependent types, but trying something like this does not work:

variable (A A' : Type)
variable (a : A)

axiom eq: A = A'

example: (a : A') := by
  rw [eq] at a
  sorry

This definitely works, you just have the syntax a bit off.

variable (A A' : Type)
variable (a : A)

variable (eq: A = A')

example: A' := by
  rw [← eq]
  exact a

But you are right that this is somewhat of a cheat, and a proper formalization would need to define contexts and all the rest.

[Mario Carneiro]

Here's a basic formalization of the four judgments you mention:

inductive Term where
  | zero

inductive Ty where
  | nat

inductive Context where
  | empty
  | comma (Γ : Context) (element: Term) (type: Ty)

mutual
inductive IsType : Context → Ty → Prop
  | nat (Γ) : IsType Γ .nat

inductive HasType : Context → Term → Ty → Prop
  | zero (Γ) : HasType Γ .zero .nat
  | conv {Γ a A A'} : TyEq Γ A A' → HasType Γ a A → HasType Γ a A'

inductive TyEq : Context → Ty → Ty → Prop
  | rfl (Γ A) : TyEq Γ A A

inductive TermEq : Context → Term → Term → Prop
  | rfl (Γ a) : TermEq Γ a a
end

The axiom in question is the HasType.conv constructor.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Another thing to mention is that some of the exercises in Egbert's book will presumably need the axioms of HoTT, which Lean does not support. So it might be more workable to use Cubical Agda, for example, as the proof assistant in which you formalize your solutions.

[Chris Henson]

Have you worked much with formalizations of the simply typed lambda calculus before? If not, I would personally start there, using resources like this Software Foundations chapter and Part 2 of Programming Language Foundations in Agda as examples. These take two approaches that are a good starting point for formalizing a lambda calculus. Then once that feels comfortable, go back and add the dependent type aspect.

[Viliam Vadocz]

Mario Carneiro said:

This definitely works, you just have the syntax a bit off.

Wow, nice to see that I was not too far off.

Mario Carneiro said:

Here's a basic formalization of the four judgments you mention

Did you just come up with this or is this already predefined in some library?

[Viliam Vadocz]

Wojciech Nawrocki said:

Another thing to mention is that some of the exercises in Egbert's book will presumably need the axioms of HoTT, which Lean does not support. So it might be more workable to use Cubical Agda, for example, as the proof assistant in which you formalize your solutions.

Even if we define the context, judgements, etc. ourselves like @Mario Carneiro did above?

[Mario Carneiro]

This is a WIP formalization of a somewhat toy dependent type theory (with a very non-toy semantic interpretation), and this is a formalization of lean's type theory judgment, which is probably way overkill for solving homework questions but should give you some hints at how this kind of thing can scale up

[Mario Carneiro]

Viliam Vadocz said:

Mario Carneiro said:

Here's a basic formalization of the four judgments you mention

Did you just come up with this or is this already predefined in some library?

I just made it up, guided by the two DTT formalizations I just mentioned

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Viliam Vadocz said:

Wojciech Nawrocki said:

Another thing to mention is that some of the exercises in Egbert's book will presumably need the axioms of HoTT, which Lean does not support. So it might be more workable to use Cubical Agda, for example, as the proof assistant in which you formalize your solutions.

Even if we define the context, judgements, etc. ourselves like Mario Carneiro did above?

That would be a bit like first defining ZFC before learning to do arithmetic. It's not really the point, unless you are very interested in foundational details. Proof assistants such as Cubical Agda or agda-unimath already give you all the tools you need to prove things in HoTT, and using those is almost certainly what Egbert means by that sentence. In particular, you shouldn't have to first define HoTT by defining contexts, judgments, the language of types, etc.

[Viliam Vadocz]

Chris Henson said:

Have you worked much with formalizations of the simply typed lambda calculus before?

I have not. I have started learning Lean a few months ago by reading the Theorem Proving in Lean 4 book, but I have not have much practice, so I thought that while I read this other book I might as well get some practice.

[Mario Carneiro]

I strongly agree with Wojciech, formalizing DTT is not a beginner level project

[Mario Carneiro]

Using it can be

[Viliam Vadocz]

Mario Carneiro said:

Using it can be

By that you mean the first approach by using the dependent type system built into Lean?

[Mario Carneiro]

At least up until you need HoTT axioms, you can do this kind of investigation in lean, using something similar to the first code block I gave. But note that if you want to handle defeq correctly, it's not actually a hypothesis you can have, it's something the proof assistant figures out on its own.

[Mario Carneiro]

The conversion rule is how this typechecks for example:

def x : Nat := 0

example : (fun x : Type => x) Nat := x

because |- (fun x : Type => x) Nat ≡ Nat

[Chris Henson]

I also agree with Mario and Wojciech about this being a tough beginning project. I consider myself an advanced beginner (I've been using various proof assistants for a couple years) and am just now feeling comfortable working on formalizing some lambda calculi. It is certainly not impossible and I recommend the resources I linked above, but there are many tricky details.

[Viliam Vadocz]

In past projects I have found that trying something difficult early on is helpful in motivating future learning. It gives a goal which frames what I read in the future. All becomes a tool to chip away at the mountain.

I would prefer to practice with what the book is teaching, which is doing the derivations myself. I'll see how far I get using Mario's example above, and if I get stuck, I will try Chris's recommendation of formalizing a simply typed lambda calculus.

[Viliam Vadocz]

Thanks for the quick and insightful replies everyone.