proving trivial facts about types

Stream: new members

[Joseph Corneli]

I can #check ff but can I prove ff : bool or similar facts?

Let's see:

-- works
example (ff : bool) := tt
example (ff : bool) := ff

-- breaks
example (1 : ℕ) := (1 : ℕ)

-- breaks
theorem ff_is_a_bool : (ff : bool) := (↥ff : Prop)

Oh dear, I am confused again.

[Reid Barton]

The typing relation is not something you can prove or really talk about at all internal to the system.

[Reid Barton]

In logic terminology it's a judgment, not a proposition.

[Joseph Corneli]

I guess I can say tautological things like "every bool is a bool"...

theorem t (x : bool) : bool := x

[Joseph Corneli]

but it's interesting, these type judgments don't live in the hierarchy of types?

[Joseph Corneli]

In general, a judgment may be any inductively definable assertion in the metatheory.

So is Lean's metatheory accessible somewhere?

[Reid Barton]

Metatheory here means whatever logical framework you are using to define and reason about the formal system (Lean in this case).

[Reid Barton]

For example, it can just be ordinary informal mathematics.

[Reid Barton]

For example, you could prove a "unique typing" theorem like "if e : t1 and e : t2 [are derivable judgments], then t1 = t2 [is a derivable judgment]".

[Reid Barton]

that's a theorem you would prove in an ordinary math paper, probably using induction on the ordinary natural numbers and so on

[Reid Barton]

I should add that encoding "ff is a bool" as a judgment ff : bool is part of what it means to use type theory as a foundation. In a system based on set theory, for example, ff would be represented by some set and bool would be represented by some other set and ff ∈ bool would be a proposition that you could prove.

[Reid Barton]

https://github.com/digama0/lean-type-theory/releases is Mario's paper on the theory of Lean in particular, though it doesn't have much in the way of background material

[Kevin Buzzard]

I guess I can say tautological things like "every bool is a bool"...

theorem t (x : bool) : bool := x

That's not a theorem. That's a definition of a function t from bool to bool; you can check the type of t to see this. Theorems are terms whose type is Prop.

[Kevin Buzzard]

PS if you write ```lean rather than just ``` then you get cool syntax highlighting :-)