Zulip Chat Archive

Stream: new members

Topic: proving trivial facts about types


view this post on Zulip Joseph Corneli (Jan 24 2019 at 13:57):

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.

view this post on Zulip Reid Barton (Jan 24 2019 at 14:06):

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

view this post on Zulip Reid Barton (Jan 24 2019 at 14:06):

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

view this post on Zulip Joseph Corneli (Jan 24 2019 at 14:08):

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

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

view this post on Zulip Joseph Corneli (Jan 24 2019 at 14:10):

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

view this post on Zulip Joseph Corneli (Jan 24 2019 at 14:13):

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

So is Lean's metatheory accessible somewhere?

view this post on Zulip Reid Barton (Jan 24 2019 at 14:17):

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

view this post on Zulip Reid Barton (Jan 24 2019 at 14:17):

For example, it can just be ordinary informal mathematics.

view this post on Zulip Reid Barton (Jan 24 2019 at 14:21):

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

view this post on Zulip Reid Barton (Jan 24 2019 at 14:22):

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

view this post on Zulip Reid Barton (Jan 24 2019 at 14:44):

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.

view this post on Zulip Reid Barton (Jan 24 2019 at 14:48):

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

view this post on Zulip Kevin Buzzard (Jan 24 2019 at 15:20):

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.

view this post on Zulip Kevin Buzzard (Jan 24 2019 at 15:21):

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


Last updated: May 11 2021 at 00:31 UTC