Term Mode

Stream: new members

[Brandon Sisler]

Hello all, I was wondering if there was any resource that could help me learn term mode. All of the reading I have as of now has to do with tactic mode and as a result, term mode is rather mysterious to me. Anyway, let me know what there is out there!

[Arien Malec]

Theorem Proving in Lean's first two chapters. It's really important to read those chapters carefully. but it also might be helpful to understand what the tactics do and how they translate behind the scenes to constructive proofs, as well as what some of the Lean symbols translate to at the level of functions (or "dependent type arrows"), structures and inductive types.

I found it steep going, but it was really helpful to understand the underlying types the theorem is "asking for" and how to construct that type from the ground up; sometimes that involves looking behind the syntactic sugar that Lean provides to see what's going on under the hood, because that's what I really need to provide.

As examples, if you want to prove an implication, you need to remember that an implication a → b is just a function, so my constructive proof is going to provide a function that takes a and gives up a b; behind the scenes ¬a is a → false so you also need a function. Even the fancy stuff in Lean is just sugar over functions, structures and inductive types. a = b? Equality is an inductive type. a ↔ b? The biconditional is a structure. a ∨ b? Or is an inductive type. And is a structure. Quantifiers? forall is a function. Exists is an inductive type.

And the chapters of TPIL explain this, but it's one thing to read it, and another to really understand that when TPIL says that it builds the entire edifice on top of functions (or "dependent type arrows"), structures and inductive types, it means it.

[Martin Dvořák]

Before you dive into the term mode (for proofs of propositions), do you know how typed lambda calculus works (for manipulating data), for example as it is done in Haskell (which is a very similar programming language)?

[Kevin Buzzard]

Just as a datapoint: I didn't know anything about Haskell or lambda calculus, and I learnt everything I needed to know about term mode from Theorem Proving In Lean itself, I didn't ever read any references or anything else.