Intuitionistic Type Theory Proofs

Stream: general

[Billy Price]

Hi there,

I'm doing a project on topos theory and proof-assistants, and I would like to write some proofs about intuitionistic type theory as presented in Lambek and Scott "Introduction to Higher Order Logic", specifically I'm proving that its associated category is a topos. The sequent-tree-proofs are laborious to organise and write out by hand. Would Lean be an appropriate tool for this?

I essentially want to define Term's inductively, and then create and work with sequents of the form "p |--_X q", where |--_X is entailment with a subscript set X of variables, and p,q are Terms with free variables all in X. I am imagining then implementing the rules of deduction as axioms like this, "axiom rule : A -> B" where A and B are entailment expressions as before.

I am unsure how I should marry Lean's existing type theory with the one I'm modelling. Should I endeavour to completely separate them? For example, one rule is "(r|--_X p & q) iff (r|--_X p) and (r|--_X q)", in which case I imagine I should write my own conjuction for the use of "&" and use the existing "and" and "iff" in Lean's library.

[Reid Barton]

This sounds like approximately the right approach except that, instead of using axiom, make "p |--_X q" an inductive Prop with the rules of deduction as constructors.

[Reid Barton]

Or maybe a type rather than a prop depending on what you want to do with it

[Patrick Massot]

https://flypitch.github.io/ is probably useful as an example of embedding other theories into Lean.

[Billy Price]

Something like this? I'm still new to lean and I'm 100% certain this is wrong.
"inductive entails (X : set) (p : Term) (q: Term)
| self_entail : entails X p p
"

[Kevin Buzzard]

```lean at the top of your code and ``` at the bottom to quote it with syntax highlighting

[Andrew Ashworth]

On top of Flypitch, there is also https://softwarefoundations.cis.upenn.edu/plf-current/Types.html#lab174, which shows something related but not quite (also it's in Coq, so you have to translate syntax)

[Billy Price]

Patrick Massot said:

https://flypitch.github.io/ is probably useful as an example of embedding other theories into Lean.

Is their use of the unicode \entails a defined notation or is that already part of lean?

[Patrick Massot]

@Floris van Doorn @Jesse Michael Han

[Jesse Michael Han]

we define our own notion of provability for first-order logic, see fol.lean in the Flypitch repo

[Floris van Doorn]

Provability is defined in the repository:

inductive prf : set (formula L) → formula L → Type u
| axm     {Γ A} (h : A ∈ Γ) : prf Γ A
| impI    {Γ : set $ formula L} {A B} (h : prf (insert A Γ) B) : prf Γ (A ⟹ B)
| impE    {Γ} (A) {B} (h₁ : prf Γ (A ⟹ B)) (h₂ : prf Γ A) : prf Γ B
| falsumE {Γ : set $ formula L} {A} (h : prf (insert ∼A Γ) ⊥) : prf Γ A
| allI    {Γ A} (h : prf (lift_formula1 '' Γ) A) : prf Γ (∀' A)
| allE₂   {Γ} A t (h : prf Γ (∀' A)) : prf Γ (A[t // 0])
| ref     (Γ t) : prf Γ (t ≃ t)
| subst₂  {Γ} (s t f) (h₁ : prf Γ (s ≃ t)) (h₂ : prf Γ (f[s // 0])) : prf Γ (f[t // 0])

https://github.com/flypitch/flypitch/blob/master/src/fol.lean#L816

This is all done on top of our internal definition of formula of first-order logic.
Here prf Γ A stands for Γ ⊢ A. So for example impE states that if Γ ⊢ A ⟹ B and Γ ⊢ A then Γ ⊢ B. Some of the other rules are a bit more tricky to decipher, this is because we're using de Bruijn indices for formulas. More details can be found in the two papers we wrote about it: https://flypitch.github.io/papers/

[Billy Price]

I'm trying to write the inductive definition of a Formula in my type theory, in which every Type has a powerset type. One of the Formulas is of the form "a \in \alpha", where A is a type, a : A, and \alpha : PA. However Lean is not happy when I try to define this constructor on the last line - "universe level of type_of(arg #1) of 'TypeTheory.Formula.elem' is too big for the corresponding inductive datatype"

structure PowerSet (A : Type) : Type

inductive Formula : Type
| var : ℕ → Formula
| top : Formula
| bot : Formula
| and : Formula → Formula → Formula
| or  : Formula → Formula → Formula
| imp : Formula → Formula → Formula
| elem {A : Type} : A → (PowerSet A) → Formula

I imagine its because I've defined a lot of things to be of type Type, but I don't really understand where things should live. Those things being: the types of my theory (instances of A in my code above), the powersets of those types (same level as normal types?), and Formulas.

[Donald Sebastian Leung]

Perhaps try adding the type parameter A to Formula itself, i.e. inductive Formula (A : Type) : Type

[Billy Price]

Okay cool, I'd like to know why that worked, but also it seems like now every constructor of Formula now depends on this type, which I don't think I want.

[Mario Carneiro]

More precisely, this makes it so that there is only one type over which elem can work

[Mario Carneiro]

You can make Formula live in Type 1 and then it will work, but the better question is what you intend to do with an uncountable number of formulas

[Mario Carneiro]

I think you need some constraints on what types are supposed to exist in your type theory

[Billy Price]

Why would it be uncountable? Surely the fact that it's defined inductively only gives me countably many?

[Kenny Lau]

elem x is different for each x : Type

[Kenny Lau]

what does PowerSet A do?

[Kenny Lau]

it has no constructor so there can be no instances of it...

[Mario Carneiro]

actually it's a structure so there is one for each A

[Billy Price]

I am ambivalent to what PowerSet A is, just that it's also a type in the same way that A is

[Mario Carneiro]

but the problem is that A can be anything

[Kenny Lau]

I claim that PowerSet A -> false for all A

[Mario Carneiro]

that's false, PowerSet A ~= unit

[Kenny Lau]

I don't understand structures

[Billy Price]

Yeah okay, well here's my updated attempt (doesn't compile)

inductive type : Type 1
| prod : type → type → type
| pow  : type → type

inductive Formula : Type 1
| top : Formula
| bot : Formula
| and : Formula → Formula → Formula
| or  : Formula → Formula → Formula
| imp : Formula → Formula → Formula
| elem {A : type} : A → (type.pow A) → Formula

[Mario Carneiro]

@Billy Price What I think you want is an inductive type declaring the valid types of your theory. At minimum, it should include PowerSet and some fixed collection of base types

[Kenny Lau]

PowerSet.rec : Π {A : Type} {C : PowerSet A → Sort u_1}, C PowerSet.mk → Π (n : PowerSet A), C n

[Kenny Lau]

now I can claim that type -> false

[Billy Price]

This is the Type theory I am trying to model in Lean. http://therisingsea.org/notes/ch2018-lecture9.pdf

[Mario Carneiro]

@Kenny Lau A structure is like an inductive type with one constructor and many arguments. So it is basically a product of all the fields, and the 0-ary case is unit

[Kenny Lau]

structure PowerSet (A : Type) : Type

inductive Formula : Type 1
| var : ℕ → Formula
| top : Formula
| bot : Formula
| and : Formula → Formula → Formula
| or  : Formula → Formula → Formula
| imp : Formula → Formula → Formula
| elem {A : Type} : A → (PowerSet A) → Formula

[Kenny Lau]

I'm not sure if this is the intended interpretation

[Kenny Lau]

@Mario Carneiro I see

[Mario Carneiro]

Here's an easy fix:

inductive type : Type
| prod : type → type → type
| pow  : type → type

inductive Formula : Type
| top : Formula
| bot : Formula
| and : Formula → Formula → Formula
| or  : Formula → Formula → Formula
| imp : Formula → Formula → Formula
| elem {A : type} : ℕ → ℕ → Formula

[Mario Carneiro]

The problem is that you don't have a grammar of terms that can inhabit a type

[Mario Carneiro]

here I'm just assuming they are numbered variables, and the type checking is separate

[Mario Carneiro]

Also, type is empty

[Mario Carneiro]

Here's a more well typed version

inductive type : Type
| prod : type → type → type
| pow  : type → type

def term : type → Type
| (type.prod a b) := term a × term b
| (type.pow a) := term a → Prop

inductive Formula : Type
| top : Formula
| bot : Formula
| and : Formula → Formula → Formula
| or  : Formula → Formula → Formula
| imp : Formula → Formula → Formula
| elem {A : type} : term A → term (type.pow A) → Formula

but it's still not good because there are too many elements of term (type.pow a)

[Billy Price]

Yeah I need to add Unit and Omega, where Omega is interpreted as the type of propositions. At the moment I was modelling Omega with Formula, without explicitly calling it a type, maybe I should try that

[Kenny Lau]

I don't think the intended meaning is "1 is a Type, Ω is a Type, AxB is a type for each A and B, PA is a type for each A, and this is all there is to it"

[Kenny Lau]

i.e. I don't agree with the use of inductive

[Mario Carneiro]

The problem is that this is going to turn into an inductive-recursive type if you aren't careful

[Mario Carneiro]

because the definition of term depends on formula and vice versa

[Billy Price]

@Kenny Lau Would it not be possible to inject the semantics of each of these types later on?

[Mario Carneiro]

When I look at the lecture notes you linked, I see a description of a structure, a system of constraints that defines a "type system", not an inductive type enumerating all possible terms

[Kenny Lau]

inductive type : Type
| one | Omega | prod (A B : type) | pow (A : type)

inductive term : type → Type
| prod : Π A B : type, term A → term B → term (type.prod A B)
| elem : Π A : type, term A → term (type.pow A) → term type.Omega
-- what is b3?
| and : term type.Omega → term type.Omega → term type.Omega
| or : term type.Omega → term type.Omega → term type.Omega
| imp : term type.Omega → term type.Omega → term type.Omega
-- what is b5??

[Kenny Lau]

@Mario Carneiro and then I looked deeper, and they defined "Pure type theory" to be basically the inductive thing

[Kenny Lau]

I'm not sure how to formalize "a variable x of type A"

[Kenny Lau]

which is required in b3 and b5

[Kenny Lau]

but here's b2 formalized @Billy Price

[Mario Carneiro]

A variable of type A would be a constructor | var {A : type} : nat -> term A

[Billy Price]

Awesome, thanks. For the variables, I just need them to act such that I can substitute terms of the type that the variable is associated to.

[Kenny Lau]

inductive type : Type
| one | Omega | prod (A B : type) | pow (A : type)

inductive term : type → Type
| prod : Π A B : type, term A → term B → term (type.prod A B)
| elem : Π A : type, term A → term (type.pow A) → term type.Omega
| sep : Π A : type, term type.Omega → ℕ → term (type.pow A)
| and : term type.Omega → term type.Omega → term type.Omega
| or : term type.Omega → term type.Omega → term type.Omega
| imp : term type.Omega → term type.Omega → term type.Omega
| all : Π A : type, term type.Omega → ℕ → term type.Omega
| ex : Π A : type, term type.Omega → ℕ → term type.Omega

[Kenny Lau]

how does this look

[Mario Carneiro]

If you use de bruijn variables you don't need the index on sep,all,ex

[Mario Carneiro]

and you are still missing var

[Mario Carneiro]

also star,true,false

[Kenny Lau]

inductive type : Type
| one | Omega | prod (A B : type) | pow (A : type)

inductive term : type → Type
| var : Π A : type, ℕ → term A
| star : term type.one
| true : term type.Omega
| false : term type.Omega
| prod : Π A B : type, term A → term B → term (type.prod A B)
| elem : Π A : type, term A → term (type.pow A) → term type.Omega
| sep : Π A : type, term type.Omega → ℕ → term (type.pow A)
| and : term type.Omega → term type.Omega → term type.Omega
| or : term type.Omega → term type.Omega → term type.Omega
| imp : term type.Omega → term type.Omega → term type.Omega
| all : Π A : type, term type.Omega → ℕ → term type.Omega
| ex : Π A : type, term type.Omega → ℕ → term type.Omega

[Kenny Lau]

what do you mean by use de Bruijn variables?

[Mario Carneiro]

that is, binders are defined so that all variable numbers shift up by one and variable number 0 becomes the newly introduced variable

[Billy Price]

same question from me, and I'm also curious how in Lean I could go about "actually substituting terms" in either of these cases.

[Mario Carneiro]

You have to define subst by recursion

[Mario Carneiro]

This is as opposed to named variables where you say "variable k is bound now" and all other variable names stay the same (and variable k outside the binder is not accessible from inside the binder)

[Mario Carneiro]

here it makes just as much sense to use string as nat for the names of variables, but you need to know that there is a way to get fresh variables when you need them

[Kenny Lau]

inductive type : Type
| one | Omega | prod (A B : type) | pow (A : type)

inductive term : type → Type
| var : Π A : type, ℕ → term A
| star : term type.one
| true : term type.Omega
| false : term type.Omega
| prod : Π A B : type, term A → term B → term (type.prod A B)
| elem : Π A : type, term A → term (type.pow A) → term type.Omega
| sep : Π A : type, term type.Omega → ℕ → term (type.pow A)
| and : term type.Omega → term type.Omega → term type.Omega
| or : term type.Omega → term type.Omega → term type.Omega
| imp : term type.Omega → term type.Omega → term type.Omega
| all : Π A : type, term type.Omega → ℕ → term type.Omega
| ex : Π A : type, term type.Omega → ℕ → term type.Omega

def FV : Π {A : type}, term A → finset ℕ
| _ (term.var A n) := {n}
| _ term.star := ∅
| _ term.true := ∅
| _ term.false := ∅
| _ (term.prod A B a b) := FV a ∪ FV b
| _ (term.elem A a α) := FV a ∪ FV α
| _ (term.sep A a n) := (FV a).erase n
| _ (term.and p q) := FV p ∪ FV q
| _ (term.or p q) := FV p ∪ FV q
| _ (term.imp p q) := FV p ∪ FV q
| _ (term.all A φ n) := (FV φ).erase n
| _ (term.ex A φ n) := (FV φ).erase n

[Mario Carneiro]

yep

[Kenny Lau]

this doesn't use de Bruijn though

[Mario Carneiro]

no

[Mario Carneiro]

this is the named variables approach

[Mario Carneiro]

The other major issue with named variables is that alpha equivalence is a thing

[Kenny Lau]

do I just remove the N if I want to use de Bruijn?

[Kenny Lau]

inductive type : Type
| one | Omega | prod (A B : type) | pow (A : type)

inductive term : type → Type
| var : Π A : type, ℕ → term A
| star : term type.one
| true : term type.Omega
| false : term type.Omega
| prod : Π A B : type, term A → term B → term (type.prod A B)
| elem : Π A : type, term A → term (type.pow A) → term type.Omega
| sep : Π A : type, term type.Omega → term (type.pow A)
| and : term type.Omega → term type.Omega → term type.Omega
| or : term type.Omega → term type.Omega → term type.Omega
| imp : term type.Omega → term type.Omega → term type.Omega
| all : Π A : type, term type.Omega → term type.Omega
| ex : Π A : type, term type.Omega → term type.Omega

[Kenny Lau]

like this?

[Mario Carneiro]

It affects FV and subst

[Mario Carneiro]

but yes, in the definition itself that's all

[Mario Carneiro]

you need operations like lift too

[Kenny Lau]

what's the signature of lift?

[Mario Carneiro]

lift' : nat -> nat -> term A -> term A is such that lift' k n changes var i to var i if i < k and var (i+n) otherwise

[Kenny Lau]

def FV : Π {A : type}, term A → finset ℕ
| _ (term.var A n) := {n}
| _ term.star := ∅
| _ term.true := ∅
| _ term.false := ∅
| _ (term.prod A B a b) := FV a ∪ FV b
| _ (term.elem A a α) := FV a ∪ FV α
| _ (term.sep A a) := ((FV a).erase 0).image nat.pred
| _ (term.and p q) := FV p ∪ FV q
| _ (term.or p q) := FV p ∪ FV q
| _ (term.imp p q) := FV p ∪ FV q
| _ (term.all A φ) := ((FV φ).erase 0).image nat.pred
| _ (term.ex A φ) := ((FV φ).erase 0).image nat.pred

[Kenny Lau]

is this right?

[Mario Carneiro]

You should consult the flypitch project, they worked this all out

[Mario Carneiro]

https://github.com/flypitch/flypitch/blob/master/src/fol.lean#L252-L255

[Mario Carneiro]

see also https://github.com/flypitch/flypitch/blob/master/src/fol.lean#L610-L616 for how binders affect things

[Billy Price]

Yeah I've been consulting that as much as possible, but I found it a little difficult to translate to my theory, thank you both for guiding me.

[Mario Carneiro]

I think in flypitch they never bothered to define FV, because in de bruijn world it is just as good to say "all variables are less than n"

[Billy Price]

So if I use de bruijn indices, have I completely avoided the need for alpha equivalence?

[Mario Carneiro]

yes, that's their secret weapon

[Billy Price]

I would imagine this would need to be hardwired into how all, ex and sep are defined, but it seems like you said otherwise above?

[Mario Carneiro]

Well, it's a type theory, so there isn't much of a "definition" of all,ex,sep

[Billy Price]

(deleted)

[Mario Carneiro]

they are just primitive constants, and so far as that goes you just get to remove the x

[Mario Carneiro]

The actual content comes in when you write down the rules of the type theory

[Billy Price]

So if I construct a term with var 7 in it, I have decided at that moment that 7 is bound to the 7th binder "out" from the appearance of 7?

[Billy Price]

And the lifting is to change that number in case I want to bind it to a different "level" binder?

[Mario Carneiro]

yes, although the convention is that if there are fewer than 7 binders then it is a free variable and you haven't decided yet what to bind it to

[Mario Carneiro]

Right, you need lifting when you want to move an expression from an outer context under a binder without accidentally capturing the new variable

[Mario Carneiro]

I find it helpful to think of the expression like x : nat, y : nat |- x + y carrying its context with it, where here x is var 1 and y is var 0, and lift corresponds to moving this expression into a new context x : nat, y : nat, z : nat |- x + y where now x is var 2 and y is var 1

[Billy Price]

Thats makes it seem that you'd only ever need to lift by 1?

[Mario Carneiro]

The general lift comes up when you define lift by recursion

[Billy Price]

Ah okay

[Billy Price]

Do I need to use lift again (with negative n?) when you want to substitute a variable for a term?

[Mario Carneiro]

You use subst : term A -> term A -> term A, which has the effect of substituting variable 0 for t and lowering all other variables by 1

[Billy Price]

So I'm limited to only substituting variable 0?

[Mario Carneiro]

The general version of this also has to include a lift component, where variable k gets substituted, variables above k get reduced by 1, and variables below k stay the same

[Mario Carneiro]

You should only ever have to substitute variable 0

[Mario Carneiro]

because of the way the binders are set up

[Billy Price]

I'm not sure I follow, you just said I could substitute for general variable k

[Mario Carneiro]

Like with lift, where you only actually need to lift by 1 but other lifts come up in the inductive definition, in subst you only need to substitute variable 0 but as you go through the binders it stops being variable 0

[Mario Carneiro]

you should look at subst_realize, subst_term and subst_formula in flypitch to see how it is done

[Billy Price]

Cheers, will do

[Billy Price]

Thanks again for your help :)

[Patrick Massot]

I think we really need to create a new stream here. We have a math string so that people who are not interested in maths can avoid math messages. I don't know how to call that new stream, and maybe we need more than one, but I would really like to avoid seeing all those discussions about embedding other type theories or ZFC into Lean, and all those discussions about proving programs. I'm very happy that other people find this interesting and use Lean for this purpose. But many people around here have zero interest in those things and can't contribute any useful comment. This is a pretty high traffic chat so we need order. We can't put such specialized discussion in the general stream I also guess some people would actually ask more computer science questions if we had a dedicated stream.

[Donald Sebastian Leung]

Perhaps we could create a stream "computer science"?

Or should we name it "type theory" / "PL theory"?

[Patrick Massot]

And I just had my standard half second of utter confusion about why piecewise linear theory enters this discussion. I proves once again we really need to sort things a bit.

[Kenny Lau]

Computer Science, Logic, Program Verification

[Patrick Massot]

I think we need to separate CS/logic from Program verification, but people who understand those things should tell us

[Billy Price]

My apologies, I'm new to Zulip Chat so I wasn't sure where else to put this topic.

[Kevin Buzzard]

It's a fine place to put it :-) But it's certainly true that for people like Patrick and me, we can understand a lot of the chat in general but just don't have the CS background to follow stuff like this because we're mathematicians

[Patrick Massot]

@Billy Price there is no reason to apologize. I'm exactly pointing out that you had no choice, and this is a problem.

[Billy Price]

Okay no worries :)

[Patrick Massot]

Let me emphasize: when I write I'm happy that people work on this topic, use Lean for this, and ask questions about it, I really mean it. And I'm also super happy there are so many messages on this chat. But we simply need ways to filter out stuff. There is no hierarchy involved here, only a lot of people with a lot of different priorities, and only 24 hours a day.

[Billy Price]

I haven't seen any more discussion of this. Who's decision is it regarding making new streams?

[Patrick Massot]

Anyone can create one. But it would be natural for @Mario Carneiro to decide something here

[Mario Carneiro]

I guess we can do a type theory stream, CS is too broad

[Mario Carneiro]

Logic is also a bit unclear

[Billy Price]

Just to clarify, we're talking about making a stream on the same level as "announce", "general", "maths" etc? Do you call the ones inside those substreams?

[Patrick Massot]

Yes, same level

[Mario Carneiro]

Program verification would be cool, although I think there has been vanishingly small amount of discussion on this topic here

[Patrick Massot]

Things inside are called topics or threads

[Patrick Massot]

(Zulip says topic)

[Patrick Massot]

Mario Carneiro said:

Program verification would be cool, although I think there has been vanishingly small amount of discussion on this topic here

I hope that would help raise this amount

[Patrick Massot]

Those things are self-sustaining. Program verification is not visible here, hence people don't ask many questions

[Mario Carneiro]

Should they be default streams? I think last time we found out that it's better to make them default at creation time rather than later

[Johan Commelin]

Yup, just make things default. that will also help new users

[Johan Commelin]

It is easier to disable a stream than to discover it

[Kevin Buzzard]

(deleted)