## Stream: Type theory

### Topic: Modelling a Type Theory in Lean

#### Billy Price (Apr 28 2020 at 13:30):

My current inductive definition of a term can produce ill-formed terms, for example if A : type is a type that is not Ω , then all A (var 0 Ω) is trying to bind an Ω variable to a A type binder.

inductive type : Type
| One | Omega | Prod (A B : type)| Pow (A : type)

notation Ω := type.Omega
notation 𝟙 := type.One
infix ×× :100 := type.Prod
prefix 𝒫 :101 := type.Pow

inductive term : type → Type
| var  : ℕ → Π A : type, term A
| star : term 𝟙
| top  : term Ω
| bot  : term Ω
| prod : Π {A B : type}, term A → term B → term (A ×× B)
| elem : Π {A : type}, term A → term (𝒫 A) → term Ω
| comp : Π A : type, term Ω → term (𝒫 A)
| and  : term Ω → term Ω → term Ω
| or   : term Ω → term Ω → term Ω
| imp  : term Ω → term Ω → term Ω
| all  : Π A : type, term Ω → term Ω
| ex   : Π A : type, term Ω → term Ω


I'm guessing in Lean you cannot enforce conditions on the creation of inductive terms (like trying to say you can only make an all A φ expression if φ has only var 0 A and no var 0 B).

My next best idea is introducing the context on terms which is a mapping of free variables to types. Here's my start on that, though I am not that familiar with using fin. Should I use array, vector, list? Or is there a more direct approach to only creating well-defined terms?

#### Billy Price (Apr 28 2020 at 13:31):

I guess what I would like to be able to say is that a variable can be any term, and it's really only defined by its number, and when we bind it to a binder, it then has an associated type.

#### Mario Carneiro (Apr 28 2020 at 13:34):

I'm guessing in Lean you cannot enforce conditions on the creation of inductive terms (like trying to say you can only make an all A φ expression if φ has only var 0 A and no var 0 B).

You can, but it's a pain because you are still in the middle of the definition so you can't easily use recursive functions at the same time

#### Mario Carneiro (Apr 28 2020 at 13:34):

I would recommend keeping the term syntax as context free as possible, and have a well typing condition afterward that can have whatever dependencies it wants

#### Billy Price (Apr 28 2020 at 13:41):

Hmm okay I'll take your advice. I was looking at flypitch documentation and they seem to do without a well-formedness predicate. Is that just because their terms are all the same type?

#### Mario Carneiro (Apr 28 2020 at 13:45):

It's easier for them because it's only one type, yes. You end up having to carry around a lot of "type state" in real type theories, and it becomes hard to get all the definitional equalities you want

#### Mario Carneiro (Apr 28 2020 at 13:46):

But they have a clearly distinct step for proofs, which I think should be the analogue of type checking for you

#### Billy Price (Apr 28 2020 at 13:52):

Sorry what step are you referring to?

#### Mario Carneiro (Apr 28 2020 at 13:54):

step in the construction

#### Mario Carneiro (Apr 28 2020 at 13:54):

I would separate the grammar from the syntax rules

#### Jannis Limperg (Apr 28 2020 at 13:55):

If you want terms that embed typing information, so that only well-typed terms can be constructed, the usual approach is to index it not only by a type, but also by a context containing the types of free variables. Thus, you would have something like this:

inductive type : Type
| One | Omega | Prod (A B : type)| Pow (A : type) | Fun (A B : type)

open type

def context := list type

inductive var : context → type → Type
| var0 (α) : var [α] α
| varsucc {Γ α β} : var Γ α → var (β :: Γ) β

-- This is the simply-typed lambda calculus with a unit type and products.
inductive term : context → type → Type
| var {Γ α} : var Γ α → term Γ α
| lam {Γ α β} : term (α :: Γ) β → term Γ (Fun α β)
| prod {Γ α β} : term Γ α → term Γ β → term Γ (Prod α β)
| unit {Γ} : term Γ One


This approach works fine and makes the development a little easier if (a) you don't have dependencies in your types (but I guess your all and ex are supposed to be quantifiers?) and (b) Lean properly supports indexed families (which I don't know). Mario's suggested approach -- keeping the syntax simple and putting a type predicate on top -- requires some additional boilerplate, but has the distinct advantage that it'll work regardless of what object theory you want to encode.

#### Mario Carneiro (Apr 28 2020 at 13:56):

Lean's support for indexed families is fine

#### Mario Carneiro (Apr 28 2020 at 13:56):

mutual is not fine

#### Mario Carneiro (Apr 28 2020 at 13:57):

While I agree with you up to a point, I find that once you get down to proving theorems about these terms, you might want to e.g. prove something by induction on the context from the other end, and then it enters DTT hell

#### Billy Price (Apr 28 2020 at 14:01):

Yeah I'm a little turned off by the fact that my sequents will also have a context, and I'd have to marry them properly.

#### Jannis Limperg (Apr 28 2020 at 14:03):

@Mario Carneiro I can see how that proof might be tricky. I've also become more skeptical of intrinsically typed syntax lately -- it's nice when it works, but when it breaks, it sure breaks.

#### Mario Carneiro (Apr 28 2020 at 14:06):

@Billy Price I don't know exactly what your sequents look like, but you will probably have two contexts, one for the types and one for the hypotheses (as is customary in HOL)

#### Mario Carneiro (Apr 28 2020 at 14:06):

the hypotheses are nondependent so it's not such a big deal

#### Billy Price (Apr 28 2020 at 14:11):

The hypotheses in my sequents are just a single term Ω.

#### Billy Price (Apr 28 2020 at 14:46):

I'm having a little trouble stating the well-foundedness condition - am I on the right track?

It also seems like there's two level's of well-foundedness - that every bound variable has the correct type, and that any free variables can be bound to a single type.

def FV_have_type (Z : type) : ℕ → Π {A : type}, term A → Prop
| v _ (var n A)  := v=n ∧ Z=A
| v _ (comp A φ) := FV_have_type (v+1) φ
| v _ (∀' A φ)   := FV_have_type (v+1) φ
| v _ (∃' A φ)   := FV_have_type (v+1) φ
| v _ ⁎          := true
| v _ top        := true
| v _ bot        := true
| v _ (prod a b) := FV_have_type v a ∧ FV_have_type v b
| v _ (a ∈ α)    := FV_have_type v a ∧ FV_have_type v α
| v _ (p ∧' q)   := FV_have_type v p ∧ FV_have_type v q
| v _ (p ∨' q)   := FV_have_type v p ∧ FV_have_type v q
| v _ (p ⟹ q)  := FV_have_type v p ∧ FV_have_type v q

def well_formed {A : type} (φ : term A) : Prop := sorry


#### Reid Barton (Apr 28 2020 at 14:48):

Do you mean v = n -> Z = A? in other words saying that all occurrences of variable n are used at type Z?

Ah yes

#### Reid Barton (Apr 28 2020 at 15:02):

I think it isn't the traditional presentation, but I'm pretty sure it is better to only have the notion "φ : term A is well-formed in Γ : context"

#### Reid Barton (Apr 28 2020 at 15:03):

rather than having only terms with no context and trying to guess the free variables and their types by inspecting the term

#### Anton Lorenzen (Apr 29 2020 at 06:24):

I started working on a calculus of constructions in Lean à few weeks ago, maybe you find it helpful: https://github.com/anfelor/coc-lean Feel free to contact me if you have any questions.

#### Billy Price (Apr 29 2020 at 12:14):

Awesome! thanks I'll take a look

#### Billy Price (Apr 29 2020 at 13:34):

@Reid Barton WF means the types of the free variables of term A match the context.

#### Reid Barton (Apr 29 2020 at 13:34):

More specifically?

#### Reid Barton (Apr 29 2020 at 13:34):

What is the English translation of what you wrote?

#### Billy Price (Apr 29 2020 at 13:34):

def WF : Π A : type, term A → context →  Prop
| _ (var n A) Γ  := ∀ a : n < Γ.length, (Γ.nth_le n a = A)
| _ (comp A φ) Γ := WF Ω φ (A :: Γ)
| _ (∀' A φ) Γ  := WF Ω φ (A :: Γ)
| _ (∃' A φ) Γ  := WF Ω φ (A :: Γ)


#### Billy Price (Apr 29 2020 at 13:35):

Hang on let me paste my term definition

#### Billy Price (Apr 29 2020 at 13:35):

Also that WF definition is incomplete, there are more terms but they are less interesting to WF

#### Billy Price (Apr 29 2020 at 13:36):

Billy Price said:

My current inductive definition of a term can produce ill-formed terms, for example if A : type is a type that is not Ω , then all A (var 0 Ω) is trying to bind an Ω variable to a A type binder.

inductive type : Type
| One | Omega | Prod (A B : type)| Pow (A : type)

notation Ω := type.Omega
notation 𝟙 := type.One
infix ×× :100 := type.Prod
prefix 𝒫 :101 := type.Pow

inductive term : type → Type
| var  : ℕ → Π A : type, term A
| star : term 𝟙
| top  : term Ω
| bot  : term Ω
| prod : Π {A B : type}, term A → term B → term (A ×× B)
| elem : Π {A : type}, term A → term (𝒫 A) → term Ω
| comp : Π A : type, term Ω → term (𝒫 A)
| and  : term Ω → term Ω → term Ω
| or   : term Ω → term Ω → term Ω
| imp  : term Ω → term Ω → term Ω
| all  : Π A : type, term Ω → term Ω
| ex   : Π A : type, term Ω → term Ω


I'm guessing in Lean you cannot enforce conditions on the creation of inductive terms (like trying to say you can only make an all A φ expression if φ has only var 0 A and no var 0 B).

My next best idea is introducing the context on terms which is a mapping of free variables to types. Here's my start on that, though I am not that familiar with using fin. Should I use array, vector, list? Or is there a more direct approach to only creating well-defined terms?

#### Reid Barton (Apr 29 2020 at 13:37):

Say the context is empty but you have a variable. Is that well-formed?

#### Billy Price (Apr 29 2020 at 13:37):

Ah sorry I just realised it was you I was discussing this with earlier. I'm not sure specifically what I should clarify more about WF, given the definition there

#### Kenny Lau (Apr 29 2020 at 13:38):

Inductively defined propositions:

#### Billy Price (Apr 29 2020 at 13:39):

@Reid Barton Yeah I thought about that and I'm not sure how to fix that. For my use I think I can just allow those terms to exist?

#### Billy Price (Apr 29 2020 at 13:41):

@Kenny Lau Even though I use the keyword def, I'm still defining it inductively on the inductive type term A right?

#### Kenny Lau (Apr 29 2020 at 13:42):

yes, but inductive might be better for this case

#### Billy Price (Apr 29 2020 at 13:44):

Hmm, is that because it allows me to name the axioms for well-formedness on each of the term A's? I'm not sure I see the difference/benefit.

#### Kenny Lau (Apr 29 2020 at 13:45):

it allows you to "inject" things

#### Kenny Lau (Apr 29 2020 at 13:45):

and you don't need to go through every case

#### Kenny Lau (Apr 29 2020 at 13:46):

(cases you haven't gone through are automatically "false")

#### Mario Carneiro (Apr 29 2020 at 13:50):

I'm pretty sure Reid is hinting at this, but more directly: you don't want ∀ a : n < Γ.length, (Γ.nth_le n a = A), you want ∃ a : n < Γ.length, (Γ.nth_le n a = A). The former says that either the type is correct or it's out of range, while the latter says that it is in range and the type is correct. Better yet, skip the hypothesis and use Γ.nth n = some A

#### Billy Price (Apr 29 2020 at 13:53):

Beautiful, thank you.

#### Billy Price (Apr 29 2020 at 14:01):

Here's what I've got now (it compiles). I'm still not understanding the suggestion to use inductive.

def WF : Π A : type, term A → context → Prop
| _ (var n A) Γ  := Γ.nth n = some A
| _ (comp A φ) Γ := WF Ω φ (A :: Γ)
| _ (∀' A φ) Γ   := WF Ω φ (A :: Γ)
| _ (∃' A φ) Γ   := WF Ω φ (A :: Γ)
| _ ⁎ Γ          := true
| _ top Γ        := true
| _ bot Γ        := true
| _ (prod a b) Γ := WF _ a Γ ∧ WF _ b Γ
| _ (a ∈ α) Γ    := WF _ a Γ ∧ WF _ α Γ
| _ (p ∧' q) Γ   := WF _ p Γ ∧ WF _ q Γ
| _ (p ∨' q) Γ   := WF _ p Γ ∧ WF _ q Γ
| _ (p ⟹ q) Γ  := WF _ p Γ ∧ WF _ q Γ


#### Billy Price (Apr 29 2020 at 14:13):

Surely if I use inductive, I can only talking about creating un-named elements of Prop, and I can't actually define which proposition they are right?

#### Kenny Lau (Apr 29 2020 at 14:15):

Kenny Lau said:

Inductively defined propositions:

#### Jannis Limperg (Apr 29 2020 at 14:15):

Billy Price said:

Hmm, is that because it allows me to name the axioms for well-formedness on each of the term A's? I'm not sure I see the difference/benefit.

Benefits of an inductive type for well-formedness (or any similar predicate):

• You can do "rule induction", i.e. induction on the derivation of a well-formedness proof. If you define the predicate by recursion over terms instead, you can't directly eliminate a hypothesis WF t; you'll have to eliminate t first until the WF reduces. (In your case, there's little difference in this regard because the structure of your well-formedness predicate is very close to the structure of your terms.)
• Recursive definitions must pass the termination checker; inductive definitions are generally more liberal. (Also not a concern in your case because you don't need a complicated recursive structure.)
• Lean may make the recursive definition extra cumbersome to use because it's picky about reducing definitional equalities (though that might not be a problem in practice; I haven't experimented with this). Maybe mark the WF def as @[reducible].

Benefits of a recursive definition of well-formedness:

• It may be a little clearer what's going on I guess?

Billy Price said:

Surely if I use inductive, I can only talking about creating un-named elements of Prop, and I can't actually define which proposition they are right?

Sorry, I don't understand your concern; could you rephrase?

#### Billy Price (Apr 29 2020 at 14:28):

Hmm, I'm feeling pretty confused. I definitely need to go back an practice more basic lean.

#### Billy Price (Apr 29 2020 at 14:32):

@Kenny Lau thanks for the resource, I think I understand it in that context but I'm struggling to translate to my case.

#### Reid Barton (Apr 29 2020 at 14:33):

Think of it in terms of what rules build up well-formed formulas into bigger ones, rather than how do you break down a formula to check whether it is well-formed.

#### Reid Barton (Apr 29 2020 at 14:33):

Actually, it's exactly like an inductive type except it's a proposition.

#### Billy Price (Apr 29 2020 at 14:34):

Hmm - aren't I then just redefining term A?

Basically, yes

#### Reid Barton (Apr 29 2020 at 14:35):

But you still have term also, so you aren't restricted to only ever considering well-formed terms

#### Reid Barton (Apr 29 2020 at 14:35):

Also, in general, you might have a more interesting notion of well-formedness which isn't directly defined by recursion on the term, but I think that doesn't happen here.

#### Billy Price (Apr 29 2020 at 14:36):

Mario Carneiro said:

I would recommend keeping the term syntax as context free as possible, and have a well typing condition afterward that can have whatever dependencies it wants

This is the advice I am trying to follow at the moment

#### Reid Barton (Apr 29 2020 at 14:36):

Both your recursive function and an inductive well-formedness predicate fall into this category, I think.

#### Reid Barton (Apr 29 2020 at 14:37):

I mean, your WF function also basically contains a complete definition of term, in the sense that all the constructors are listed

Good point

#### Billy Price (Apr 29 2020 at 14:40):

So are you suggesting keeping the inductive term, and making an inductive WF with a context, or put the context into the term from the start so every term is well-formed (by forcing the binders and var to follow the context)?

#### Reid Barton (Apr 29 2020 at 14:47):

Those are two options. Another is the recursive WF function you already have.
The recursive WF function and the inductive well-formedness predicate are basically equivalent in terms of what you can express easily. (The main difference is that the inductive predicate gives you the ability to induct on the proof of well-formedness, but here it looks basically equivalent to inducting on the term itself; the recursive function is more like an algorithm for computing whether something is well-formed and it lets you directly prove, for example, that if $\varphi \wedge \psi$ is well-formed then the components $\varphi$ and $\psi$ are well-formed, which needs a case analysis if using the inductive predicate.)
Putting the context into the term from the start is not really equivalent, since it means you only have the vocabulary to ever talk about well-formed terms.

#### Billy Price (May 05 2020 at 03:37):

I'm going with the well-typed-from-the-start approach for now, and I've coming up with a var constructer which sandwiches a given type A between the context of terms of about to be bound \Gamma and those which will be bound after this variable, \Delta. To be clear, in any context, the type of the 0th de-bruijn index variable is at the head of the list-context.

def context := list type

inductive term : context → type → Type
| var (Γ A Δ) : term (list.append Γ (A::Δ)) A
| comp {Γ} : Π A : type, term (A::Γ) Ω → term Γ (𝒫 A)
| all  {Γ} : Π A : type, term (A::Γ) Ω → term Γ Ω
| ex   {Γ} : Π A : type, term (A::Γ) Ω → term Γ Ω
| star {Γ} : term Γ 𝟙
| top  {Γ} : term Γ Ω
| bot  {Γ} : term Γ Ω
| prod {Γ} : Π {A B : type}, term Γ A → term Γ B → term Γ (A ×× B)
| elem {Γ} : Π {A : type}, term Γ A → term Γ (𝒫 A) → term Γ Ω
| and  {Γ} : term Γ Ω → term Γ Ω → term Γ Ω
| or   {Γ} : term Γ Ω → term Γ Ω → term Γ Ω
| imp  {Γ} : term Γ Ω → term Γ Ω → term Γ Ω


As the terms currently exist, to construct a big term inductively from smaller terms, you need to know the whole context of the big term to construct and use the variables of the small terms. Obviously this is unsustainable, so I think I need to create a function for modifying contexts. I don't think there's many restrictions on the kind of context modification you can do, which includes adding more context to the end of the context, lifting the context and inserting other context before it, and also any reordering of types in the existing context. Perhaps there's some general pattern there, but I'm struggling to even define a simple case. If I mention A more than once between then | and the :=, it tells me A already appears in this pattern. I understand why that's an error, but I'm not sure what I'm supposed to do instead. I haven't been able to write the other cases for similar reasons.

def add_junk (β : context) : Π (Γ: context) (A: type), term Γ A → term (list.append Γ β) A
| (list.append Γ (A::Δ)) (A) (var Γ A Δ) := var Γ A (list.append Δ β)


#### Mario Carneiro (May 05 2020 at 11:12):

You should leave the first two arguments blank, they are inferred from the third

#### Mario Carneiro (May 05 2020 at 11:14):

Alternatively you should be able to put a dot before them like

def add_junk (β : context) : Π (Γ: context) (A: type), term Γ A → term (list.append Γ β) A
| .(list.append Γ (A::Δ)) .(A) (var Γ A Δ) := var Γ A (list.append Δ β)


and it will mark those positions as "inacessible" meaning that it won't try to split on the first argument and figure out why list.append Γ (A::Δ) is a constructor (because it's not)

#### Billy Price (May 05 2020 at 11:51):

That results in this error

equation type mismatch, term
var Γ A (list.append Δ β)
has type
term (list.append Γ (A :: list.append Δ β)) A
but is expected to have type
term (list.append . (list.append Γ (A :: Δ)) β) .A


#### Billy Price (May 05 2020 at 11:53):

Also what is the . syntax called so I can find it in the documentation?

#### Mario Carneiro (May 05 2020 at 12:31):

It's called an inaccessible pattern. It is almost never used in lean/mathlib because in basically every case you can use _ instead

#### Mario Carneiro (May 05 2020 at 12:31):

If you want to name the parameters, you should do so in the constructor var Γ A Δ, possibly using @var more names Γ A Δ

#### Mario Carneiro (May 05 2020 at 12:32):

Anyway, you've just hit DTT hell in that error there

#### Mario Carneiro (May 05 2020 at 12:32):

You should definitely not have this constructor

| var (Γ A Δ) : term (list.append Γ (A::Δ)) A


because the term will usually not have this form

#### Mario Carneiro (May 05 2020 at 12:33):

Instead you can use | var (Γ A) : A \in Γ -> term Γ A

#### Billy Price (May 05 2020 at 12:34):

But then how can I possibly tell which type in the context list my var is constructing?

#### Mario Carneiro (May 05 2020 at 12:34):

or | var {Γ i A} : list.nth Γ i = some A -> term Γ A

#### Mario Carneiro (May 05 2020 at 12:34):

that one gives you a de bruijn index

#### Billy Price (May 05 2020 at 12:35):

Am I not achieving the same thing by stacking a context below and a context above A in var \Gamma A \Delta?

#### Mario Carneiro (May 05 2020 at 12:36):

"the same thing" up to equality but not up to defeq

#### Mario Carneiro (May 05 2020 at 12:36):

and the reason defeq is coming up is because you have a dependent type

#### Billy Price (May 05 2020 at 12:37):

defeq meaning definitional equality?

#### Mario Carneiro (May 05 2020 at 12:37):

term (list.append Γ (A :: list.append Δ β)) A and term (list.append (list.append Γ (A :: Δ)) β) A are distinct types, so you have to insert a cast between them and this will make everything harder

#### Mario Carneiro (May 05 2020 at 12:38):

(this is the issue I was predicting when I originally recommended to use a weakly typed term syntax + a well formedness judgment)

#### Billy Price (May 05 2020 at 12:38):

ooh that's odd, I would have expected them to reduce to the same thing by unwrapping the definition of list.append?

#### Mario Carneiro (May 05 2020 at 12:38):

You can't because Γ is a variable

#### Mario Carneiro (May 05 2020 at 12:39):

For every concrete term for Γ these two are defeq, but for variable Γ you have to prove it by induction

#### Billy Price (May 05 2020 at 12:39):

that's pretty interesting

#### Reid Barton (May 05 2020 at 12:40):

Obviously you should use a difference list for your context flees

#### Billy Price (May 05 2020 at 12:42):

You might have seen before I was trying to go with your original suggestion, but was struggling to define the well-formedness predicate and was kinda lead back into well-typing it from the start.

#### Mario Carneiro (May 05 2020 at 12:43):

The well formedness predicate can be done with either inductive or def. https://leanprover.zulipchat.com/#narrow/stream/236446-Type-theory/topic/Modelling.20a.20Type.20Theory.20in.20Lean/near/195713258 <- this looks okay

#### Mario Carneiro (May 05 2020 at 12:43):

inductive gives you a bit more freedom to not be strictly recursive

#### Mario Carneiro (May 05 2020 at 12:45):

it's also more natural when proving theorems by induction on well formed terms, so the sort of thing that the dependent type would give you

#### Mario Carneiro (May 05 2020 at 12:46):

the def is what you would want for implementing a type checker, or a proof that the typing judgment is decidable

#### Mario Carneiro (May 05 2020 at 12:47):

but you can have both versions and prove equivalence so there isn't a loss in picking one method over the other at first

#### Billy Price (May 05 2020 at 12:48):

I see the issues with using my non-defeq context-terms, but given your constructor | var {Γ i A} : list.nth Γ i = some A -> term Γ A, would that suffer from similar issues?

#### Mario Carneiro (May 05 2020 at 12:49):

that will solve the problem you have with unifying the context, because var can have any context, and the content is shifted to the hypothesis, which is a Prop and hence has no issues with defeq

#### Mario Carneiro (May 05 2020 at 12:50):

your original var constructor only supports contexts of the form Γ ++ A :: Δ

#### Billy Price (May 05 2020 at 12:52):

Yep, but given that improvement, am I naive to think that fixes everything and using a WF predicate on weakly-typed terms is overly complicated?

#### Mario Carneiro (May 05 2020 at 12:54):

With the inductive version you can set it up so that it looks almost the same. It's only about twice as long because you have two definitions instead of one (the terms, and the well formedness inductive type)

#### Mario Carneiro (May 05 2020 at 12:54):

but feel free to continue with dependent types, I've hopefully unstuck you on that issue and there are fixes or workarounds for most of the other problems that will arise

#### Billy Price (May 05 2020 at 12:55):

I really appreciate the help in getting me started.

#### Mario Carneiro (May 05 2020 at 13:04):

Here's the inductive-ification of the original dependent type:

inductive term : Type
| var : ℕ → term
| comp : type → term → term
| all  : type → term → term
| ex   : type → term → term
| star : term
| top  : term
| bot  : term
| prod : term → term → term
| elem : term → term → term
| and  : term → term → term
| or   : term → term → term
| imp  : term → term → term

inductive WF : context → term → type → Prop
| var (Γ A Δ) : WF (list.append Γ (A::Δ)) (term.var (list.length Γ)) A
| comp {Γ e} : Π A : type, WF (A::Γ) e Ω → WF Γ (term.comp A e) (𝒫 A)
| all  {Γ e} : Π A : type, WF (A::Γ) e Ω → WF Γ (term.all A e) Ω
| ex   {Γ e} : Π A : type, WF (A::Γ) e Ω → WF Γ (term.all A e) Ω
| star {Γ} : WF Γ term.star 𝟙
| top  {Γ} : WF Γ term.top Ω
| bot  {Γ} : WF Γ term.bot Ω
| prod {Γ e₁ e₂} : Π {A B : type}, WF Γ e₁ A → WF Γ e₂ B → WF Γ (term.prod e₁ e₂) (A ×× B)
| elem {Γ e₁ e₂} : Π {A : type}, WF Γ e₁ A → WF Γ e₂ (𝒫 A) → WF Γ (term.elem e₁ e₂) Ω
| and  {Γ e₁ e₂} : WF Γ e₁ Ω → WF Γ e₁ Ω → WF Γ (term.and e₁ e₂) Ω
| or   {Γ e₁ e₂} : WF Γ e₁ Ω → WF Γ e₁ Ω → WF Γ (term.or e₁ e₂) Ω
| imp  {Γ e₁ e₂} : WF Γ e₁ Ω → WF Γ e₁ Ω → WF Γ (term.imp e₁ e₂) Ω


there is actually an algorithm to perform these sort of translations, although I took the liberty of using a nat for the variable and otherwise removing unnecessary arguments from term, which is not obvious to the straightforward algorithm.

#### Billy Price (May 05 2020 at 13:17):

Wow that was definitely non-obvious to me that you could take the types off term's as well. From then on, as I understand, instead of talking about terms, you'd talk about proofs that terms are well-formed? (as if its the term itself)

#### Billy Price (May 05 2020 at 13:18):

So a sequent is constructed from two WF's proofs, rather than from two terms?

#### Mario Carneiro (May 05 2020 at 13:18):

No, a sequent is still just two terms

#### Mario Carneiro (May 05 2020 at 13:19):

But the inductive defining the proof relation will contain WF hypotheses

#### Billy Price (May 05 2020 at 13:26):

Ah, I just wrote down the type and realised of course you must introduce the term objects themselves to talk about their WF'ness
inductive proof : Π {Γ:context} {φ: term} {ψ : term}, WF Γ φ Ω → WF Γ ψ Ω → Type

#### Billy Price (May 05 2020 at 13:29):

In what sense did you mean a proof/sequent is just two terms?

#### Mario Carneiro (May 05 2020 at 13:29):

You can write the proof : context -> term -> term -> Prop relation such that proof Γ φ ψ -> WF Γ φ Ω /\ WF Γ ψ Ω, although I would actually suggest WF Γ φ Ω -> proof Γ φ ψ -> WF Γ ψ Ω instead

#### Billy Price (May 22 2020 at 02:48):

Been working on this lately and oh boy - I need to understand tactics better.

#### Billy Price (May 22 2020 at 02:53):

What tactics do you you expect to be relevant to me? So far I'm familiar with the basic ones (apply, exact, cases, induction, simp). Since I have my own equality - would I need to write my own version of rewrite?

#### Billy Price (May 22 2020 at 03:01):

Also with those tactics - I'm finding that whenever I apply cases or induction, Lean comes up with really ugly local-context names for each case, and I need to manually name up to 10 things manually so they have sensible names. This is the current state of my tactic proof - any suggestions for controlling the growth here?

lemma proof_WF {Γ : context} {φ ψ: term} : WF Γ φ Ω → proof Γ φ ψ → WF Γ ψ Ω :=
begin
intros wf_φ prf_φ_ψ,
induction prf_φ_ψ,
case proof.axm : {assumption},
case proof.abs : {assumption},
case proof.vac : {exact WF.top},
case proof.cut : Γ P Q R prf_PQ prf_QR h₁ h₂
{exact h₂ (h₁ wf_φ)},
case proof.and_intro : Γ p q r prf_pq prf_pr h₁ h₂ h₃
{apply WF.and, exact h₁ h₃, exact h₂ h₃},
case proof.and_left : Γ p q r h₁ h₂ {apply WF_and_left, exact h₂ wf_φ},
case proof.and_right : Γ p q r h₁ h₂ {apply WF_and_right, exact h₂ wf_φ},
case proof.or_intro : Γ p q r prf_pr prf_qr h₁ h₂ h₃
{apply h₁, apply WF_or_left, exact h₃},
case proof.comp : Γ p A h
{apply WF.all,
apply WF.and,
apply WF.imp,
apply WF.elem,
show type, exact A,
show type, exact A,
apply WF.var,
simp,
apply WF.comp,
assumption,
simp,
induction h,
case WF.top : {simp, exact WF.top},
case WF.bot : {simp, exact WF.bot},
case WF.star : {simp, exact WF.star},
case WF.and : Γ p q wf_p wf_q ih₁ ih₂
{simp, apply WF.and, exact ih₁ wf_φ, exact ih₂ wf_φ},
case WF.or : Γ p q wf_p wf_q ih₁ ih₂
{simp, apply WF.or, exact ih₁ wf_φ, exact ih₂ wf_φ},
case WF.imp : Γ p q wf_p wf_q ih₁ ih₂
{simp, apply WF.imp, exact ih₁ wf_φ, exact ih₂ wf_φ},
case WF.var : Γ n A h₁ {simp, split_ifs with h₂, apply WF.var, simp, sorry, sorry},
repeat {sorry},
},
repeat {sorry},
end


#### Jalex Stark (May 22 2020 at 03:05):

can you make that a #mwe?

#### Jalex Stark (May 22 2020 at 03:05):

(I'm not asking you to remove anything, just add imports and definitions so that if I copy-paste it into my VSCode it compiles)

#### Jannis Limperg (May 22 2020 at 03:14):

Billy Price said:

Also with those tactics - I'm finding that whenever I apply cases or induction, Lean comes up with really ugly local-context names for each case, and I need to manually name up to 10 things manually so they have sensible names.

I'm currently working on an alternative induction tactic that would hopefully give you better names (among other things). It's not quite ready yet though. For now, manual renaming is your best option.

In general, your proof looks okay to me. You could probably automate/prettify some of this stuff, but that's a rabbit hole and a half. I'd recommend you just slog through it; these sorts of proofs are always lengthy.

#### Jalex Stark (May 22 2020 at 03:17):

in this part

  case proof.cut : Γ P Q R prf_PQ prf_QR h₁ h₂
{exact h₂ (h₁ wf_φ)},


does it instead work to write the following? (I could answer this question myself if i had a mwe)

  case proof.cut : _ _ _ _ _ _ h₁ h₂
{exact h₂ (h₁ wf_φ)},


#### Billy Price (May 22 2020 at 03:19):

Only issue is the mwe is pretty large. I'll attach the file for now - basically everything is needed.

TL_zulip.lean

#### Jalex Stark (May 22 2020 at 03:20):

why not paste it into a message?

#### Jalex Stark (May 22 2020 at 03:20):

that's probably much easier for both of us

#### Jalex Stark (May 22 2020 at 03:21):

import data.finset
namespace TT

inductive type : Type
| One | Omega | Prod (A B : type)| Pow (A : type)

notation Ω := type.Omega
notation 𝟙 := type.One
infix ××:max := type.Prod
prefix 𝒫 :max := type.Pow

def context := list type

inductive term : Type
| star : term
| top  : term
| bot  : term
| and  : term → term → term
| or   : term → term → term
| imp  : term → term → term
| var  : ℕ → term
| comp : term → term
| all  : term → term
| ex   : term → term
| elem : term → term → term
| prod : term → term → term

open term

-- * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
-- Notation and derived operators
-- * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *

notation <0> := var 0
notation <1> := var 1
notation <2> := var 2
notation <3> := var 3
notation <4> := var 4
notation <5> := var 5
notation <6> := var 6
notation <7> := var 7
notation <8> := var 8
notation <9> := var 9

notation ⁎ := star    -- input \asterisk
notation ⊤ := top     --       \top
notation ⊥ := bot     -- input \bot
infixr  ⟹ :60 := imp -- input \==>
infixr  ⋀  :70 := and -- input \And or \bigwedge
infixr  ⋁  :59 := or  -- input \Or or \bigvee

def not (p : term) := p ⟹ ⊥
prefix ∼:max := not -- input \~, the ASCII character ~ has too low precedence

def biimp (p q: term) := (p ⟹ q) ⋀ (q ⟹ p)
infix  ⇔ :60 := biimp -- input \<=>

infix ∈ := elem
infix ∉ := λ a, λ α, not (elem a α)
notation ⟦ φ ⟧ := comp φ

prefix ∀':1 := all
prefix ∃':2 := ex

def eq (a : term) (a' : term) : term := ∀' (a ∈ <0>) ⇔ (a' ∈ <0>)
infix ≃ :50 := eq

def singleton (a : term) := ⟦a ≃ (<0>)⟧

def ex_unique (φ : term) : term :=
∃' ⟦φ⟧ ≃ singleton (<3>)
prefix ∃!':2 := ex_unique

def subseteq (α : term) (β : term) : term :=
∀' (<0> ∈ α) ⟹ (<0> ∈ β)
infix ⊆ := subseteq

-- * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *

inductive WF : context → term → type → Prop
| star {Γ}         : WF Γ term.star 𝟙
| top  {Γ}         : WF Γ term.top Ω
| bot  {Γ}         : WF Γ term.bot Ω
| and  {Γ p q}     : WF Γ p Ω → WF Γ q Ω → WF Γ (p ⋀ q) Ω
| or   {Γ p q}     : WF Γ p Ω → WF Γ q Ω → WF Γ (p ⋁ q) Ω
| imp  {Γ p q}     : WF Γ p Ω → WF Γ q Ω → WF Γ (p ⟹ q) Ω
| var  {Γ n A}     : list.nth Γ n = some A → WF Γ (var n) A
| comp {Γ φ A}     : WF (A::Γ) φ Ω → WF Γ ⟦φ⟧ (𝒫 A)
| all  {Γ φ A}     : WF (A::Γ) φ Ω → WF Γ (∀' φ) Ω
| ex   {Γ φ A}     : WF (A::Γ) φ Ω → WF Γ (∃' φ) Ω
| elem {Γ a α A}   : WF Γ a A → WF Γ α (𝒫 A) → WF Γ (a ∈ α) Ω
| prod {Γ a b A B} : WF Γ a A → WF Γ b B → WF Γ (prod a b) (A ×× B)

variable Γ : context
variables p q r φ a b α : term
variables A B : type

lemma WF_and_left   : WF Γ (p ⋀ q) Ω → WF Γ p Ω := by {intro h, cases h, assumption}
lemma WF_and_right  : WF Γ (p ⋀ q) Ω → WF Γ q Ω := by {intro h, cases h, assumption}
lemma WF_or_left    : WF Γ (p ⋁ q) Ω → WF Γ p Ω := by {intro h, cases h, assumption}
lemma WF_or_right   : WF Γ (p ⋁ q) Ω → WF Γ q Ω := by {intro h, cases h, assumption}
lemma WF_imp_left   : WF Γ (p ⟹ q) Ω → WF Γ p Ω := by {intro h, cases h, assumption}
lemma WF_imp_right  : WF Γ (p ⟹ q) Ω → WF Γ q Ω := by {intro h, cases h, assumption}
lemma WF_prod_left  : WF Γ (prod a b) (A ×× B) → WF Γ a A := by {intro h, cases h, assumption}
lemma WF_prod_right : WF Γ (prod a b) (A ×× B) → WF Γ b B := by {intro h, cases h, assumption}
lemma WF_comp_elim  : WF Γ (⟦φ⟧) (𝒫 A) → WF (A::Γ) φ Ω := by {intro h, cases h, assumption}
lemma WF_all_elim   : WF Γ (∀' φ) Ω → ∃ A:type, WF (A::Γ) φ Ω := by {intro h, cases h, constructor, assumption}
lemma WF_ex_elim    : WF Γ (∀' φ) Ω → ∃ A:type, WF (A::Γ) φ Ω := by {intro h, cases h, constructor, assumption}

def lift (d : ℕ): ℕ → term → term
| k star       := star
| k top        := top
| k bot        := bot
| k (p ⋀ q)    := (lift k p) ⋀ (lift k q)
| k (p ⋁ q)    := (lift k p) ⋁ (lift k q)
| k (p ⟹ q)    := (lift k p) ⟹ (lift k q)
| k (var m)    := if m≥k then var (m+d) else var m
| k ⟦φ⟧         :=    ⟦lift (k+1) φ⟧
| k (∀' φ)     := ∀' lift (k+1) φ
| k (∃' φ)     := ∃' lift (k+1) φ
| k (a ∈ α)    := (lift k a) ∈ (lift k α)
| k (prod a b) := prod (lift k a) (lift k b)

@[simp]
def subst_nth : term → ℕ → term → term
| b n star       := star
| b n top        := top
| b n bot        := bot
| b n (p ⋀ q)    := (subst_nth b n p) ⋀ (subst_nth b n q)
| b n (p ⋁ q)    := (subst_nth b n p) ⋁ (subst_nth b n q)
| b n (p ⟹ q)  := (subst_nth b n p) ⟹ (subst_nth b n q)
| b n (var m)    := if n=m then b else var m
| b n ⟦φ⟧        :=     ⟦subst_nth (lift 1 0 b) (n+1) φ⟧
| b n (∀' φ)     := ∀' (subst_nth (lift 1 0 b) (n+1) φ)
| b n (∃' φ)     := ∃' (subst_nth (lift 1 0 b) (n+1) φ)
| b n (a ∈ α)    := (subst_nth b n a) ∈ (subst_nth b n α)
| b n (prod a c) := prod (subst_nth b n a) (subst_nth b n c)

@[simp]
def subst (b:term) := subst_nth b 0

inductive proof : context → term → term → Prop
| axm        {Γ φ}     : WF Γ φ Ω → proof Γ φ φ
| vac        {Γ φ}     : WF Γ φ Ω → proof Γ φ term.top
| abs        {Γ φ}     : WF Γ φ Ω → proof Γ term.bot φ
| cut        {Γ φ ψ γ} : proof Γ φ ψ → proof Γ ψ γ → proof Γ φ γ
| and_intro  {Γ p q r} : proof Γ p q → proof Γ p r → proof Γ p (q ⋀ r)
| and_left   {Γ p q r} : proof Γ p (q ⋀ r) → proof Γ p q
| and_right  {Γ p q r} : proof Γ p (q ⋀ r) → proof Γ p r
| or_intro   {Γ p q r} : proof Γ p r → proof Γ q r → proof Γ (p ⋁ q) r
| or_left    {Γ p q r} : proof Γ (p ⋁ q) r → proof Γ p r
| or_right   {Γ p q r} : proof Γ (p ⋁ q) r → proof Γ q r
| imp_to_and {Γ p q r} : proof Γ p (q ⟹ r) → proof Γ (p ⋀ q) r
| and_to_imp {Γ p q r} : proof Γ (p ⋀ q) r → proof Γ p (q ⟹ r)
| add_var    {Γ φ ψ B} : proof Γ φ ψ → proof (B :: Γ) φ ψ

| apply    {Γ φ ψ b B} :
WF Γ b B
→ proof (B::Γ) φ ψ
→ proof Γ (subst b φ) (subst b ψ)

| all_elim   {Γ p φ B} : proof Γ p (∀' φ) → proof (B::Γ) p φ
| all_intro  {Γ p φ B} : proof (B::Γ) p φ → proof Γ p (∀' φ)
| ex_elim    {Γ p φ B} : proof Γ p (∃' φ) → proof (B::Γ) p φ
| ex_intro   {Γ p φ B} : proof (B::Γ) p φ → proof Γ p (∃' φ)

| comp       {Γ φ A}   :
WF (A::A::Γ) φ Ω
→ proof Γ ⊤
(∀' (<0> ∈ ⟦φ⟧) ⇔ (subst <0> φ))

| ext                  :
proof [] ⊤ $∀' ∀' (∀' (<0> ∈ <2>) ⇔ (<0> ∈ <1>)) ⟹ (<1> ≃ <0>) | prop_ext : proof [] ⊤ ∀' ∀' (<1> ⇔ <0>) ⟹ (<1> ≃ <0>) | star_unique : proof [] ⊤ ∀' (<0> ≃ ⁎) | prod_exists_rep : proof [] ⊤ ∀' ∃' ∃' (<2> ≃ (prod <1> <0>)) | prod_distinct_rep : proof [] ⊤ ∀' ∀' ∀' ∀' (prod <3> <1> ≃ prod <2> <0>) ⟹ (<3> ≃ <2> ⋀ <1> ≃ <0>) example : proof [] ⊤ ⊤ := proof.axm WF.top lemma proof_WF {Γ : context} {φ ψ: term} : WF Γ φ Ω → proof Γ φ ψ → WF Γ ψ Ω := begin intros wf_φ prf_φ_ψ, induction prf_φ_ψ, case proof.axm : {assumption}, case proof.abs : {assumption}, case proof.vac : {exact WF.top}, case proof.cut : Γ P Q R prf_PQ prf_QR h₁ h₂ {exact h₂ (h₁ wf_φ)}, case proof.and_intro : Γ p q r prf_pq prf_pr h₁ h₂ h₃ {apply WF.and, exact h₁ h₃, exact h₂ h₃}, case proof.and_left : Γ p q r h₁ h₂ {apply WF_and_left, exact h₂ wf_φ}, case proof.and_right : Γ p q r h₁ h₂ {apply WF_and_right, exact h₂ wf_φ}, case proof.or_intro : Γ p q r prf_pr prf_qr h₁ h₂ h₃ {apply h₁, apply WF_or_left, exact h₃}, case proof.comp : Γ p A h {apply WF.all, apply WF.and, apply WF.imp, apply WF.elem, show type, exact A, show type, exact A, apply WF.var, simp, apply WF.comp, assumption, simp, induction h, case WF.top : {simp, exact WF.top}, case WF.bot : {simp, exact WF.bot}, case WF.star : {simp, exact WF.star}, case WF.and : Γ p q wf_p wf_q ih₁ ih₂ {simp, apply WF.and, exact ih₁ wf_φ, exact ih₂ wf_φ}, case WF.or : Γ p q wf_p wf_q ih₁ ih₂ {simp, apply WF.or, exact ih₁ wf_φ, exact ih₂ wf_φ}, case WF.imp : Γ p q wf_p wf_q ih₁ ih₂ {simp, apply WF.imp, exact ih₁ wf_φ, exact ih₂ wf_φ}, case WF.var : Γ n A h₁ {simp, split_ifs with h₂, apply WF.var, simp, sorry, sorry}, repeat {sorry}, }, repeat {sorry}, end end TT  #### Jalex Stark (May 22 2020 at 03:22): so yes, you can replace the unused variable names with _ #### Billy Price (May 22 2020 at 03:25): Yep I see. As I am naming them (or not naming them) I don't really know what I've named until I move my cursor inside the {}, and each time I do that - it's not clear which "ugly" name is going to become the next variable name I tack on. Is trial and error the only way there? #### Jalex Stark (May 22 2020 at 03:26): i think in your tactic state, the autogenerated variable names appear in the order they're generated #### Billy Price (May 22 2020 at 03:27): Actually you're right - I think they just reappear in a different order once I've named them for some reason. #### Billy Price (May 22 2020 at 03:28): Can I avoid re-introducing Γ every time I do a case? #### Jalex Stark (May 22 2020 at 03:31): a mostly-not-serious suggestion is to redefine things so that the arguments that you're introducing come first #### Jalex Stark (May 22 2020 at 03:31): in the proof.comp case you do a lot of work tracking down metavariables #### Jalex Stark (May 22 2020 at 03:32): apply @WF.all _ _ A, seems like a better thing to write for the first line than apply WF.all #### Jalex Stark (May 22 2020 at 03:33): similarly apply @WF.elem _ _ _ A, a few lines later #### Billy Price (May 22 2020 at 03:34): Sorry could you explain what that's achieving? #### Jalex Stark (May 22 2020 at 03:35): well as it's written you get a metavariable and a goal that's just type #### Jalex Stark (May 22 2020 at 03:35): and then later you close that goal by supplying A #### Jalex Stark (May 22 2020 at 03:36): here we're feeding it A right when it's needed, instead of making lean ask us for it #### Jalex Stark (May 22 2020 at 03:37): I think you should abstract out the hard cases like proof.comp as lemmas #### Jalex Stark (May 22 2020 at 03:38): that way when you prove the theorem you're "just" listing all 24 cases together with either their short proofs or a call to the external lemma #### Billy Price (May 22 2020 at 03:38): I understand. Is that an indication I should change the WF.all to put the type first? And should I have the other arguments explicit or implicit? I thought making them implicit would save me from having to state them but I seems I have to do it anyway with this proof. #### Jalex Stark (May 22 2020 at 03:39): Yeah if in fact you end up always stating A explicitly then probably you want A to be an explicit argument #### Jalex Stark (May 22 2020 at 03:39): the first three implicit arguments get dealt with just fine #### Billy Price (May 22 2020 at 03:40): Jalex Stark said: that way when you prove the theorem you're "just" listing all 24 cases together with either their short proofs or a call to the external lemma If I'm doing it by induction though - do those lemmas need an appropriate hypothesis related to the induction? #### Jalex Stark (May 22 2020 at 03:40): the tactic state looks like this Γ : context, φ ψ : term, Γ : list type, wf_φ : WF Γ ⊤ Ω, p : term, A : type, h : WF (A :: A :: Γ) p Ω ⊢ WF Γ (∀'(var 0 ∈ ⟦p⟧) ⇔ subst (var 0) p) Ω  #### Jalex Stark (May 22 2020 at 03:41): you could have a lemma whose type signature is this tactic state #### Billy Price (May 22 2020 at 03:42): That's a nice way to go about it. That reminds me, what's up with the multiple Gammas? #### Billy Price (May 22 2020 at 03:42): Shouldn't they be unified or something? #### Jalex Stark (May 22 2020 at 03:42): lemma case_proof_comp (Γ : context) (φ ψ : term) (Γ : list type) (wf_φ : WF Γ ⊤ Ω) (p : term) (A : type) (h : WF (A :: A :: Γ) p Ω) : WF Γ (∀'(var 0 ∈ ⟦p⟧) ⇔ subst (var 0) p) Ω := sorry  #### Jalex Stark (May 22 2020 at 03:43): unified? #### Jalex Stark (May 22 2020 at 03:43): they have different types #### Billy Price (May 22 2020 at 03:44): context is list type #### Jalex Stark (May 22 2020 at 03:44): depends on what you mean by is #### Billy Price (May 22 2020 at 03:45): Definitional is? I'm not even sure why one of them became list type #### Jalex Stark (May 22 2020 at 03:45): context is defeq to list type #### Jalex Stark (May 22 2020 at 03:46): but defeq is weaker than syntactic equality #### Jalex Stark (May 22 2020 at 03:46): and some things (I don't know which ones, really) only work up to syntactic equality #### Jalex Stark (May 22 2020 at 03:48): i do share some of your confusion #### Billy Price (May 22 2020 at 03:49): So when I do some case - I wanna say "use the same context here" #### Jalex Stark (May 22 2020 at 03:50): hmm why do you write inductive proof : context → term → term → Prop  instead of e.g. inductive proof (\G : context) (\phi : term) (\psi : term) : Prop  #### Billy Price (May 22 2020 at 03:53): I was under the impression I need to do the first, since my understanding of the second is that it locks in those variables globally to the rest of the inductive definitions. #### Billy Price (May 22 2020 at 03:53): Whereas I need to unpack all the different cases for the context and terms #### Jalex Stark (May 22 2020 at 03:53): okay, I don't understand but vaguely believe you #### Jalex Stark (May 22 2020 at 03:54): also i'm gonna go sleep now #### Jalex Stark (May 22 2020 at 03:54): uh I guess to go back to one of your first questions #### Jalex Stark (May 22 2020 at 03:54): if you want more automation you could tag things with the simp attribute #### Jalex Stark (May 22 2020 at 03:55): and I think that the tidy tactic knows how to do some of the proofs you're doing #### Billy Price (May 22 2020 at 03:56): Goodnight :) That sounds cool and I need to read up on attributes and how that all works. I just put @[simp] next to subst and subst_nth because I had a guess at what it does. #### Jalex Stark (May 22 2020 at 03:56): tactic#tidy #### Jannis Limperg (May 22 2020 at 04:01): Billy Price said: That reminds me, what's up with the multiple Gammas? These are different hypotheses; they just have the same name. You can use dedup to give them different names. The first one may be unnecessary (if nothing in the goal refers to it); if so, you can clear it after the dedup. #### Mario Carneiro (May 22 2020 at 04:53): Billy Price said: Yep I see. As I am naming them (or not naming them) I don't really know what I've named until I move my cursor inside the {}, and each time I do that - it's not clear which "ugly" name is going to become the next variable name I tack on. Is trial and error the only way there? This is what I used to do, but the new "sticky position" vscode feature helps a lot with this. You put the marker inside the body of the case, then you start writing names in the case statement and push underscores until the name lines up with the variable you want #### Mario Carneiro (May 22 2020 at 04:55): To add to what Jannis said about the multiple gammas, the first one is probably the input to the theorem before the induction line. It can be removed, assuming you have generalized all the relevant hypotheses about it. #### Mario Carneiro (May 22 2020 at 04:56): It can also be ignored #### Billy Price (May 22 2020 at 07:00): Not sure what you mean by sticky position. Like multiple cursors? #### Bryan Gin-ge Chen (May 22 2020 at 07:11): When you have an editor with Lean code focused, you should see a button that looks like a pin near the top right of that editor. If you press that, or hit ctrl+P and search for "toggle sticky position", then the current position of the text cursor will get a blue mark. Now you can move your text cursor elsewhere, and the info view will continue to display the messages coming from the blue spot in the file. To turn it off, you can hit the button or call the command again. #### Billy Price (May 22 2020 at 07:23): How can I be more eco-friendly and solve 10 different lemmas at the same time? (they all compile with the same proof) #### Marc Huisinga (May 22 2020 at 07:30): if they are only cases in one bigger proof and not meaningful as separate lemmas, you could use any_goals {proof}. i've also read something on here about a tactic that allows you to select a specific set of goals, but i don't remember what it's called or whether it exists in mathlib. #### Billy Price (May 22 2020 at 07:35): They just deconstruct well-formedness - so I'm predicting using them in various places All of those lemmas should be solved by the first one's proof inductive WF : context → term → type → Prop | star {Γ} : WF Γ term.star 𝟙 | top {Γ} : WF Γ term.top Ω | bot {Γ} : WF Γ term.bot Ω | and {Γ p q} : WF Γ p Ω → WF Γ q Ω → WF Γ (p ⋀ q) Ω | or {Γ p q} : WF Γ p Ω → WF Γ q Ω → WF Γ (p ⋁ q) Ω | imp {Γ p q} : WF Γ p Ω → WF Γ q Ω → WF Γ (p ⟹ q) Ω | var {Γ n} (A) : list.nth Γ n = some A → WF Γ (var n) A | comp {Γ φ} (A) : WF (A::Γ) φ Ω → WF Γ ⟦φ⟧ (𝒫 A) | all {Γ φ} (A) : WF (A::Γ) φ Ω → WF Γ (∀' φ) Ω | ex {Γ φ} (A) : WF (A::Γ) φ Ω → WF Γ (∃' φ) Ω | elem {Γ a α} (A) : WF Γ a A → WF Γ α (𝒫 A) → WF Γ (a ∈ α) Ω | prod {Γ a b A B} : WF Γ a A → WF Γ b B → WF Γ (prod a b) (A ×× B) | mod {Γ a A} (B) : WF Γ a A → WF (B::Γ) a A variable Γ : context variables p q r φ a b α : term variables A B : type lemma WF_and_left : WF Γ (p ⋀ q) Ω → WF Γ p Ω := begin intro h, induction Γ, case list.nil : {cases h, assumption}, case list.cons : B Δ ih {cases h, assumption, apply WF.mod, apply ih, assumption}, end lemma WF_and_right : WF Γ (p ⋀ q) Ω → WF Γ q Ω := lemma WF_or_left : WF Γ (p ⋁ q) Ω → WF Γ p Ω := lemma WF_or_right : WF Γ (p ⋁ q) Ω → WF Γ q Ω := lemma WF_imp_left : WF Γ (p ⟹ q) Ω → WF Γ p Ω := lemma WF_imp_right : WF Γ (p ⟹ q) Ω → WF Γ q Ω := lemma WF_prod_left : WF Γ (prod a b) (A ×× B) → WF Γ a A := lemma WF_prod_right : WF Γ (prod a b) (A ×× B) → WF Γ b B := lemma WF_comp_elim : WF Γ (⟦φ⟧) (𝒫 A) → WF (A::Γ) φ Ω :=  #### Billy Price (May 22 2020 at 07:56): Whoops, my new "mod" constructor for Well-formedness was not supposed to put the new variable at the start of the list (should go at the end). Regardless - my original question is still relevant. #### Billy Price (May 22 2020 at 08:16): Here's my new definition of mod : | mod {Γ a A} (B) : WF Γ a A → WF (list.concat Γ B) a A. I am having trouble with the following proof lemma WF_and_left : WF Γ (p ⋀ q) Ω → WF Γ p Ω := begin intro h, induction Γ, case list.nil : {cases h, sorry}, case list.cons : {sorry} end  Lean is unhappy with "cases h", I think because it tries to unify the (list.concat Γ B) with list.nil to do the WF.mod case. Shouldn't it recognise this as an irrelevant case? This is the error message cases tactic failed, unsupported equality between type and constructor indices (only equalities between constructors and/or variables are supported, try cases on the indices): list.nil = list.concat h_Γ h_B state: p q : term, h : WF list.nil (and p q) Ω, h_Γ : context, h_a : term, h_A h_B : type, h_a_1 : WF h_Γ h_a h_A ⊢ list.nil = list.concat h_Γ h_B → and p q = h_a → Ω = h_A → h == _ → WF list.nil p Ω  a similar thing happens with case list.cons {cases h, } cases tactic failed, unsupported equality between type and constructor indices (only equalities between constructors and/or variables are supported, try cases on the indices): Γ_hd :: Γ_tl = list.concat h_Γ h_B state: p q : term, Γ_hd : type, Γ_tl : list type, Γ_ih : WF Γ_tl (and p q) Ω → WF Γ_tl p Ω, h : WF (Γ_hd :: Γ_tl) (and p q) Ω, h_Γ : context, h_a : term, h_A h_B : type, h_a_1 : WF h_Γ h_a h_A ⊢ Γ_hd :: Γ_tl = list.concat h_Γ h_B → and p q = h_a → Ω = h_A → h == _ → WF (Γ_hd :: Γ_tl) p Ω  #### Reid Barton (May 22 2020 at 09:50): list.concat isn't a constructor, and indeed the result of list.concat could even be list.nil. #### Reid Barton (May 22 2020 at 09:55): I would ditch the induction on Γ, and induct on h instead #### Reid Barton (May 22 2020 at 09:55): What is mod supposed to represent? #### Reid Barton (May 22 2020 at 10:25): Oh whoops, list.concat doesn't mean what it means in every other language. Nevertheless, the first point remains. #### Billy Price (May 22 2020 at 11:16): haha yeah, also list.append is what I first thought list.concat would be #### Billy Price (May 22 2020 at 11:17): mod adds a single junk type to the back of the context of a well-formed term #### Billy Price (May 22 2020 at 11:20): If I do induction h - I don't know how to deal with all of the irrelevant cases that could not construct the given term. For example the first case want me to show WF Δ p 𝟙 #### Alex J. Best (May 22 2020 at 11:22): Billy Price said: How can I be more eco-friendly and solve 10 different lemmas at the same time? (they all compile with the same proof) You can make a simple tactic like so: meta def billy_tac : tactic unit := do [ intro h, induction Γ, case list.nil : {cases h, assumption}, case list.cons : B Δ ih {cases h, assumption, apply WF.mod, apply ih, assumption},]  #### Reid Barton (May 22 2020 at 11:43): What does mod stand for then? #### Reid Barton (May 22 2020 at 11:44): I would have thought WF already has this property, am I missing something? #### Billy Price (May 22 2020 at 11:56): Oh no, I was proving something else and thought I didn't have that - and then added this mod thing (modify context) and that complicated things #### Mario Carneiro (May 22 2020 at 19:12): I think the mod constructor should be a theorem (usually called "weakening") #### Billy Price (May 28 2020 at 09:18): I think I need quotients now to find the objects of my category - where can I find good examples of quotient types? #### Johan Commelin (May 28 2020 at 09:23): git grep quotient? #### Billy Price (May 28 2020 at 10:11): That didn't work but I have been searching - just found Zmod37.lean - perfect! #### Kevin Buzzard (May 28 2020 at 10:38): Just to comment that that file using quotient, which finds the equivalence relation using type class search, but there is also quotient', which finds it via unification. #### Billy Price (May 28 2020 at 10:44): What happens when you form a quotient type using a relation that's not an equivalence relation? #### Billy Price (Jun 02 2020 at 11:22): How does one lift a function a -> a -> a -> b to a function quotient r a -> quotient r a -> quotient r a -> b in a controlled way? I'm away of quot.lift - does this generalise in a manageable way? #### Reid Barton (Jun 02 2020 at 11:24): There should be quotient.lift\3 #### Billy Price (Jun 02 2020 at 11:46): There isn't :( #### Reid Barton (Jun 02 2020 at 11:49): Add it! #### Billy Price (Jun 02 2020 at 11:57): :grimacing: I'll try when I have time :( #### Mario Carneiro (Jun 02 2020 at 12:12): Look at the proof of lift2 and copy it #### Mario Carneiro (Jun 02 2020 at 12:14): or just use lift three times. It's not even a much worse proof obligation, it just has you vary one argument at a time instead of all three in one go #### Billy Price (Jun 02 2020 at 13:06): I'm working with equivalence classes of provably equal closed terms, and I'm trying to define proofs about terms given some such equivalence classes - hence the need for lifting - but now I'm realising I maybe I should show "if you have provably equal terms, you can interchange them in any proof", then I could just apply that a bunch of times. But then I'm guessing I'd need to work in all of the constructors for terms - do I really need to repeat myself about every little thing for terms, but now about equivalence classes of terms? #### Billy Price (Jun 02 2020 at 13:42): Perhaps that was a bit rambly - here's what I have so far in two files, the second file is where I'm trying to do stuff with the equivalence classes of closed terms - which are called tset A for any A : type (an abbreviation for "type theory set"). I feel like I should be able to coerce my tset's into closed_terms (which coerce into terms), so I can talk about proof's about tsets - without having to quotient.lift everything each time. Is that possible? #### Billy Price (Jun 02 2020 at 13:42): TT.lean /- Definitions of a type theory Author: Billy Price -/ import data.finset namespace TT inductive type : Type | Unit | Omega | Prod (A B : type)| Pow (A : type) notation Ω := type.Omega def Unit := type.Unit infix ××:max := type.Prod prefix 𝒫 :max := type.Pow def context := list type inductive term : Type | star : term | top : term | bot : term | and : term → term → term | or : term → term → term | imp : term → term → term | elem : term → term → term | pair : term → term → term | var : ℕ → term | comp : term → term | all : term → term | ex : term → term -- * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * -- Notation and derived operators -- * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * notation 𝟘 := term.var 0 notation 𝟙 := term.var 1 notation 𝟚 := term.var 2 notation 𝟛 := term.var 3 notation 𝟜 := term.var 4 notation 𝟝 := term.var 5 notation ⁎ := term.star -- input \asterisk notation ⊤ := term.top -- \top notation ⊥ := term.bot -- input \bot infixr  ⟹ :60 := term.imp -- input \==> infixr  ⋀  :70 := term.and -- input \And or \bigwedge infixr  ⋁  :59 := term.or -- input \Or or \bigvee def not (p : term) := p ⟹ ⊥ prefix ∼:max := not -- input \~ def iff (p q: term) := (p ⟹ q) ⋀ (q ⟹ p) infix  ⇔ :60 := iff -- input \<=> infix ∈ := term.elem infix ∉ := λ a α, not (term.elem a α) notation ⟦ φ ⟧ := term.comp φ notation ⟪ a , b ⟫ := term.pair a b prefix ∀':1 := term.all prefix ∃':2 := term.ex def eq (a₁ a₂ : term) : term := ∀' (a₁ ∈ 𝟘) ⇔ (a₂ ∈ 𝟘) infix ≃ :50 := eq def singleton (a : term) := ⟦a ≃ (𝟘)⟧ def ex_unique (φ : term) : term := ∃' ⟦φ⟧ ≃ singleton (𝟛) prefix ∃!':2 := ex_unique def subseteq (α : term) (β : term) : term := ∀' (𝟘 ∈ α) ⟹ (𝟘 ∈ β) infix ⊆ := subseteq def set_prod {A B : type} (α β : term) : term := ⟦∃' ∃' (𝟙 ∈ α) ⋀ (𝟘 ∈ β) ⋀ (𝟛 ≃ ⟪𝟚,𝟙⟫)⟧ -- * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * open term section wellformedness inductive WF : context → type → term → Prop | star {Γ} : WF Γ Unit ⁎ | top {Γ} : WF Γ Ω ⊤ | bot {Γ} : WF Γ Ω ⊥ | and {Γ p q} : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⋀ q) | or {Γ p q} : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⋁ q) | imp {Γ p q} : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⟹ q) | elem {Γ A a α} : WF Γ A a → WF Γ (𝒫 A) α → WF Γ Ω (a ∈ α) | pair {Γ A B a b} : WF Γ A a → WF Γ B b → WF Γ (A ×× B) ⟪a,b⟫ | var {Γ A n} : list.nth Γ n = some A → WF Γ A (var n) | comp {Γ A φ} : WF (A::Γ) Ω φ → WF Γ (𝒫 A) ⟦φ⟧ | all {Γ A φ} : WF (A::Γ) Ω φ → WF Γ Ω (∀' φ) | ex {Γ A φ} : WF (A::Γ) Ω φ → WF Γ Ω (∃' φ) variable {Γ : context} variables p q r φ a b α : term variables {A B Ω' : type} -- Ω' is just a fake/variable version of Ω so we don't need to bother proving -- that it must be Ω itself. local notation ez := by {intro h, cases h, assumption} lemma WF.and_left : WF Γ Ω' (p ⋀ q) → WF Γ Ω' p := ez lemma WF.and_right : WF Γ Ω' (p ⋀ q) → WF Γ Ω' q := ez lemma WF.or_left : WF Γ Ω' (p ⋁ q) → WF Γ Ω' p := ez lemma WF.or_right : WF Γ Ω' (p ⋁ q) → WF Γ Ω' q := ez lemma WF.imp_left : WF Γ Ω' (p ⟹ q) → WF Γ Ω' p := ez lemma WF.imp_right : WF Γ Ω' (p ⟹ q) → WF Γ Ω' q := ez lemma WF.pair_left : WF Γ (A ×× B) ⟪a,b⟫ → WF Γ A a := ez lemma WF.pair_right : WF Γ (A ×× B) ⟪a,b⟫ → WF Γ B b := ez lemma WF.comp_elim : WF Γ (𝒫 A) (⟦φ⟧) → WF (A::Γ) Ω φ := ez lemma WF.all_elim : WF Γ Ω' (∀' φ) → ∃ A:type, WF (A::Γ) Ω' φ := by {intro h, cases h, constructor, assumption} lemma WF.ex_elim : WF Γ Ω' (∀' φ) → ∃ A:type, WF (A::Γ) Ω' φ := by {intro h, cases h, constructor, assumption} lemma WF.iff_intro : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⇔ q) := by {intros h₁ h₂, apply WF.and, all_goals {apply WF.imp, assumption, assumption}} lemma WF.iff_elim : WF Γ Ω' (p ⇔ q) → WF Γ Ω' p ∧ WF Γ Ω' q := by {intro h, apply and.intro, all_goals {cases h, cases h_a, assumption}} lemma WF.eq_intro {Γ} {a₁ a₂} (A : type) : WF ((𝒫 A) :: Γ) A a₁ → WF ((𝒫 A) :: Γ) A a₂ → WF Γ Ω (a₁ ≃ a₂) := by {intros h₁ h₂, apply WF.all, apply WF.iff_intro, all_goals {apply WF.elem, assumption, apply WF.var, simp}} end wellformedness section substitution def lift (d : ℕ) : ℕ → term → term | k ⁎ := ⁎ | k ⊤ := ⊤ | k ⊥ := ⊥ | k (p ⋀ q) := (lift k p) ⋀ (lift k q) | k (p ⋁ q) := (lift k p) ⋁ (lift k q) | k (p ⟹ q) := (lift k p) ⟹ (lift k q) | k (a ∈ α) := (lift k a) ∈ (lift k α) | k ⟪a,b⟫ := ⟪lift k a, lift k b⟫ | k (var m) := if m≥k then var (m+d) else var m | k ⟦φ⟧ := ⟦lift (k+1) φ⟧ | k (∀' φ) := ∀' lift (k+1) φ | k (∃' φ) := ∃' lift (k+1) φ def subst_nth : ℕ → term → term → term | n x ⁎ := ⁎ | n x ⊤ := ⊤ | n x ⊥ := ⊥ | n x (p ⋀ q) := (subst_nth n x p) ⋀ (subst_nth n x q) | n x (p ⋁ q) := (subst_nth n x p) ⋁ (subst_nth n x q) | n x (p ⟹ q) := (subst_nth n x p) ⟹ (subst_nth n x q) | n x (a ∈ α) := (subst_nth n x a) ∈ (subst_nth n x α) | n x ⟪a,c⟫ := ⟪subst_nth n x a, subst_nth n x c⟫ | n x (var m) := if n=m then x else var m | n x ⟦φ⟧ := ⟦subst_nth (n+1) (lift 1 0 x) φ⟧ | n x (∀' φ) := ∀' (subst_nth (n+1) (lift 1 0 x) φ) | n x (∃' φ) := ∃' (subst_nth (n+1) (lift 1 0 x) φ) def subst := subst_nth 0 notation φ ⁅ b ⁆ := subst b φ #reduce 𝟘⁅⊤ ⋀ ⊥⁆ #reduce 𝟙⁅⊤ ⋀ ⊥⁆ end substitution section proofs inductive proof : context → term → term → Prop | axm {Γ φ} : WF Γ Ω φ → proof Γ φ φ | vac {Γ φ} : WF Γ Ω φ → proof Γ φ ⊤ | abs {Γ φ} : WF Γ Ω φ → proof Γ ⊥ φ | and_intro {Γ p q r} : proof Γ p q → proof Γ p r → proof Γ p (q ⋀ r) | and_left {Γ} (p q r) : proof Γ p (q ⋀ r) → proof Γ p q | and_right {Γ} (p q r) : proof Γ p (q ⋀ r) → proof Γ p r | or_intro {Γ p q r} : proof Γ p r → proof Γ q r → proof Γ (p ⋁ q) r | or_left {Γ} (p q r) : proof Γ (p ⋁ q) r → proof Γ p r | or_right {Γ} (p q r) : proof Γ (p ⋁ q) r → proof Γ q r | imp_to_and {Γ p q r} : proof Γ p (q ⟹ r) → proof Γ (p ⋀ q) r | and_to_imp {Γ p q r} : proof Γ (p ⋀ q) r → proof Γ p (q ⟹ r) | weakening {Γ φ ψ B} : proof Γ φ ψ → proof (list.concat Γ B) φ ψ | cut {Γ} (φ c ψ) : proof Γ φ c → proof Γ c ψ → proof Γ φ ψ | all_elim {Γ p φ B} : proof Γ p (∀' φ) → proof (B::Γ) p φ | all_intro {Γ p φ} (B) : proof (B::Γ) p φ → proof Γ p (∀' φ) | ex_elim {Γ p φ B} : proof Γ p (∃' φ) → proof (B::Γ) p φ | ex_intro {Γ p φ B} : proof (B::Γ) p φ → proof Γ p (∃' φ) | ext : proof [] ⊤$ ∀' ∀' (∀' (𝟘 ∈ 𝟚) ⇔ (𝟘 ∈ 𝟙)) ⟹ (𝟙 ≃ 𝟘)
| prop_ext                 : proof [] ⊤ ∀' ∀' (𝟙 ⇔ 𝟘) ⟹ (𝟚 ≃ 𝟙)
| star_unique              : proof [] ⊤ ∀' (𝟙 ≃ ⁎)
| pair_exists_rep          : proof [] ⊤ ∀' ∃' ∃' 𝟚 ≃ ⟪𝟙,𝟘⟫
| pair_distinct_rep        : proof [] ⊤ ∀' ∀' ∀' ∀' (⟪𝟜,𝟚⟫ ≃ ⟪𝟛,𝟙⟫) ⟹ (𝟜 ≃ 𝟛 ⋀ 𝟚 ≃ 𝟙)
| apply      {Γ B} (φ ψ b) : WF Γ B b → proof (B::Γ) φ ψ → proof Γ (φ⁅b⁆) (ψ⁅b⁆)
| comp       {Γ φ A}       : WF (A::A::Γ) Ω φ → proof Γ ⊤ (∀' (𝟘 ∈ ⟦φ⟧) ⇔ (φ⁅𝟙⁆))

prefix ⊢ := proof [] ⊤
infix  ⊢ :50 := proof []
notation φ  ⊢[ Γ:(foldr , (h t, list.cons h t) list.nil) ]  ψ := proof Γ φ ψ
notation ⊢[ Γ:(foldr , (h t, list.cons h t) list.nil) ]  ψ := proof Γ ⊤ ψ

variables p q : term

#reduce   ⊢ (p ⋁ ∼p)  -- proof [] ⊤ (or p (imp p ⊥))
#reduce q ⊢ (p ⋁ ∼p)  -- proof [] q (or p (imp p ⊥))
#reduce   ⊢[Ω,Unit] p -- proof [Ω,Unit] ⊤ p
#reduce q ⊢[Ω,Unit] p -- proof [Ω,Unit] q p

variable {Γ : context}
variables φ ψ : term

lemma WF.proof_left  : proof Γ φ ψ → WF Γ Ω φ := sorry
lemma WF.proof_right : proof Γ φ ψ → WF Γ Ω ψ := sorry

end proofs

end TT


#### Billy Price (Jun 02 2020 at 13:43):

category.lean

/-
The associated category of a type theory

Author: Billy Price
-/
import category_theory.category
import TT

namespace TT

section
variable A : type

def closed : type → term → Prop := WF []

def closed_term := {a : term // closed A a}

def closed_term.mk (a : term) : closed A a → closed_term A:= subtype.mk a

instance closed_term_has_coe : has_coe (closed_term A) term := coe_subtype

def proof_eq (a₁ a₂ : closed_term A) := ⊢ (a₁ ≃ a₂)

section equivalence_relation

lemma proof_to_imp {Γ : context} (q r) : proof Γ q r → proof Γ ⊤ (q ⟹ r) :=
begin
intro h₁,
apply proof.and_to_imp,
apply proof.cut _ q _,
apply proof.and_right _ ⊤ _,
apply proof.axm,
apply WF.and,
exact WF.top,
apply WF.proof_left q r,
tidy
end

theorem proof_eq_refl : reflexive (proof_eq A) :=
begin
intro a,
unfold proof_eq,
apply proof.all_intro 𝒫 A,
apply proof.and_intro,
all_goals
{
apply proof_to_imp,
apply proof.axm,
apply @WF.elem _ A,
sorry,
apply WF.var,
simp
}
end

theorem proof_eq_symm : symmetric (proof_eq A) :=
begin
intros a₁ a₂ H,
apply proof.all_intro 𝒫 A,
apply proof.and_intro,
apply proof.and_right _ ((↑a₁ ∈ 𝟘) ⟹ (↑a₂ ∈ 𝟘)) _,
apply proof.all_elim,
exact H,
apply proof.and_left _ _ ((↑a₂ ∈ 𝟘) ⟹ (↑a₁ ∈ 𝟘)),
apply proof.all_elim,
exact H,
end

theorem proof_eq_trans : transitive (proof_eq A) := sorry

theorem proof_eq_equiv : equivalence (proof_eq A) :=
⟨proof_eq_refl A, proof_eq_symm A, proof_eq_trans A⟩

end equivalence_relation

definition TT.setoid : setoid (closed_term A) :=
{r := proof_eq A, iseqv := proof_eq_equiv A}

#check TT.setoid

local attribute [instance] TT.setoid

def tset := quotient (TT.setoid A)

def to_tset := quot.mk (proof_eq A)

def coe_term_tset : has_coe (closed_term A) (tset A) := ⟨to_tset A⟩

local attribute [instance] coe_term_tset

def tset.star : tset Unit :=
by {apply to_tset, apply closed_term.mk _ ⁎, exact WF.star}

end

section

variables {A B : type}

def term_is_subset {A B : type} (α : closed_term A) (β : closed_term B) (F : closed_term 𝒫 (A××B)) : Prop :=
⊢ F ⊆ (@set_prod A B α β)

def is_subset {A B : type} : tset A → tset B → tset 𝒫 (A ×× B) → Prop := sorry

def term_is_graph {A B: type} (F : closed_term 𝒫 (A ×× B)) (α : closed_term A) (β : closed_term B) : Prop :=
⊢ ∀' ((𝟘 ∈ α) ⟹ (∃!' ⟪𝟙,𝟘⟫ ∈ F))

def is_graph {A B: type} : tset A → tset B → tset 𝒫 (A ×× B) → Prop := sorry

end

end TT

namespace category_theory

namespace TT

open TT

instance category : small_category (tset) := sorry -- lean unhappy with tset : type → Type : Type 1

end TT

end category_theory


#### Billy Price (Jun 09 2020 at 10:49):

Now that I've explicitly type-parametrised term.all, I can't define my notation for equality. Any tips for that? I've done it with a placeholder but I don't think it will ever get inferred.

def leibniz_equal (A:type) (a₁ a₂ : term) : term := ∀' A ((lift 1 0 a₁) ∈ 𝟘) ⇔ ((lift 1 0 a₂) ∈ 𝟘)
infix ≃ :50 := leibniz_equal _


#### Mario Carneiro (Jun 09 2020 at 10:56):

To be fair this is exactly what equality in lean looks like

#### Mario Carneiro (Jun 09 2020 at 10:57):

If you want to omit it you will probably have to make it a builtin

#### Mario Carneiro (Jun 09 2020 at 10:59):

Your embedded language isn't going to get type inference so you should get used to ugly terms unless you start writing a deeply embedded proof assistant

#### Mario Carneiro (Jun 09 2020 at 10:59):

However there are ways to make use of tactics to allow reflecting lean exprs into your target language to make things a bit easier

#### Mario Carneiro (Jun 09 2020 at 11:03):

If the struggle is only with the use of infix, a reasonable workaround is to use something like

notation a  ≃[:max A ] :0 b := leibniz_equal A a b


#### Billy Price (Jun 09 2020 at 11:17):

Cool thanks, I was just trying to design something like that.

#### Billy Price (Jun 10 2020 at 11:11):

I can't get my predefined WF_rules to work with apply_rules in the bottom lemma here. Note I have commented out apply_rules [WF.and, WF.imp], which solves it, and those rules are part of WF_rules, so what's the issue? I get no matching rule on the line apply_rules WF_rules.

/-
Definitions of a type theory

Author: Billy Price
-/

import data.finset
namespace TT

inductive type : Type
| Unit | Omega | Prod (A B : type)| Pow (A : type)

notation Ω := type.Omega
def Unit := type.Unit
infix ××:max := type.Prod
notation 𝒫A :max := type.Pow A

def context := list type

inductive term : Type
| star : term
| top  : term
| bot  : term
| and  : term → term → term
| or   : term → term → term
| imp  : term → term → term
| elem : term → term → term
| pair : term → term → term
| var  : ℕ → term
| comp : type → term → term
| all  : type → term → term
| ex   : type → term → term

open term

-- * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
-- Notation and derived operators
-- * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *

notation 𝟘 := term.var 0
notation 𝟙 := term.var 1
notation 𝟚 := term.var 2
notation 𝟛 := term.var 3
notation 𝟜 := term.var 4
notation 𝟝 := term.var 5

notation ⁎ := term.star    -- input \asterisk
notation ⊤ := term.top     --       \top
notation ⊥ := term.bot     -- input \bot
infixr  ⟹ :60 := term.imp -- input \==>
infixr  ⋀  :70 := term.and -- input \And or \bigwedge
infixr  ⋁  :59 := term.or  -- input \Or or \bigvee

def not (p : term) := p ⟹ ⊥
prefix ∼:max := not -- input \~

def iff (p q: term) := (p ⟹ q) ⋀ (q ⟹ p)
infix  ⇔ :60 := iff -- input \<=>

infix ∈ := term.elem
infix ∉ := λ a α, not (term.elem a α)
notation ⟦  A  |  φ  ⟧ := term.comp A φ

notation ⟪ a , b ⟫ := term.pair a b

notation ∀' := term.all
notation ∃' := term.ex

section substitution

@[simp]
def lift_d (d : ℕ) : ℕ → term → term
| k ⁎          := ⁎
| k ⊤          := ⊤
| k ⊥          := ⊥
| k (p ⋀ q)    := (lift_d k p) ⋀ (lift_d k q)
| k (p ⋁ q)    := (lift_d k p) ⋁ (lift_d k q)
| k (p ⟹ q)   := (lift_d k p) ⟹ (lift_d k q)
| k (a ∈ α)    := (lift_d k a) ∈ (lift_d k α)
| k ⟪a,b⟫      := ⟪lift_d k a, lift_d k b⟫
| k (var m)    := if m≥k then var (m+d) else var m
| k ⟦A | φ⟧     :=    ⟦A | lift_d (k+1) φ⟧
| k (∀' A φ)   := ∀' A $lift_d (k+1) φ | k (∃' A φ) := ∃' A$ lift_d (k+1) φ

@[simp]
def lift := lift_d 1 0

@[simp]
def subst : ℕ → term → term → term
| n x ⁎          := ⁎
| n x ⊤          := ⊤
| n x ⊥          := ⊥
| n x (p ⋀ q)    := (subst n x p) ⋀ (subst n x q)
| n x (p ⋁ q)    := (subst n x p) ⋁ (subst n x q)
| n x (p ⟹ q)  := (subst n x p) ⟹ (subst n x q)
| n x (a ∈ α)    := (subst n x a) ∈ (subst n x α)
| n x ⟪a,c⟫      := ⟪subst n x a, subst n x c⟫
| n x (var m)    := if n=m then x else var m
| n x ⟦ A | φ ⟧   :=    ⟦A | subst (n+1) (lift x) φ⟧
| n x (∀' A φ)     := ∀' A (subst (n+1) (lift x) φ)
| n x (∃' A φ)     := ∃' A (subst (n+1) (lift x) φ)

notation  ⁅ φ  //   b ⁆ := subst 0 b φ

#reduce ⁅𝟘 // ⊤ ⋀ ⊥⁆
#reduce ⁅ 𝟙 // ⊤ ⋀ ⊥⁆

end substitution

def eq (A:type) (a₁ a₂ : term) : term := ∀' (𝒫 A) $((lift a₁) ∈ 𝟘) ⇔ ((lift a₂) ∈ 𝟘) notation a  ≃[:max A ] :0 b := eq A a b #check eq Unit 𝟘 𝟘 def singleton (A : type) (a : term) := ⟦A | (lift a) ≃[A] 𝟘⟧ def ex_unique (A : type) (φ : term) : term := ∃' A (⟦A | φ⟧ ≃[𝒫 A] (singleton A 𝟘)) prefix ∃!':2 := ex_unique def subseteq (A : type) (α : term) (β : term) : term := ∀' A (𝟘 ∈ α) ⟹ (𝟘 ∈ β) notation a  ⊆[:max A ] :0 b := subseteq A a b def term_prod {A B : type} (α β : term) : term := ⟦ A ×× B | ∃' A (∃' B ((𝟙 ∈ α) ⋀ (𝟘 ∈ β) ⋀ (eq (A ×× B) 𝟚 ⟪𝟙,𝟘⟫)))⟧ notation α  ×x[:max A ] :0 β := term_prod A α β -- * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * open term @[user_attribute] meta def WF_rules : user_attribute := { name := WF_rules, descr := "lemmas usable to prove Well Formedness" } inductive WF : context → type → term → Prop | star {Γ} : WF Γ Unit ⁎ | top {Γ} : WF Γ Ω ⊤ | bot {Γ} : WF Γ Ω ⊥ | and {Γ p q} : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⋀ q) | or {Γ p q} : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⋁ q) | imp {Γ p q} : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⟹ q) | elem {Γ A a α} : WF Γ A a → WF Γ (𝒫 A) α → WF Γ Ω (a ∈ α) | pair {Γ A B a b} : WF Γ A a → WF Γ B b → WF Γ (A ×× B) ⟪a,b⟫ | var {Γ A n} : list.nth Γ n = some A → WF Γ A (var n) | comp {Γ A φ} : WF (A::Γ) Ω φ → WF Γ (𝒫 A) ⟦A | φ⟧ | all {Γ A φ} : WF (A::Γ) Ω φ → WF Γ Ω (∀' A φ) | ex {Γ A φ} : WF (A::Γ) Ω φ → WF Γ Ω (∃' A φ) attribute [WF_rules] WF.star WF.top WF.bot WF.and WF.or WF.imp WF.elem WF.pair WF.var WF.comp WF.all WF.ex section variable Γ : context variables p q r φ a b α : term variables {A B Ω' : type} -- Ω' is just a fake/variable version of Ω so we don't need to bother proving -- that it must be Ω itself.' meta def WF_prover : tactic unit := do [intro h, cases h, assumption] @[WF_rules] lemma and_left : WF Γ Ω' (p ⋀ q) → WF Γ Ω' p := by WF_prover @[WF_rules] lemma and_right : WF Γ Ω' (p ⋀ q) → WF Γ Ω' q := by WF_prover @[WF_rules] lemma or_left : WF Γ Ω' (p ⋁ q) → WF Γ Ω' p := by WF_prover @[WF_rules] lemma or_right : WF Γ Ω' (p ⋁ q) → WF Γ Ω' q := by WF_prover @[WF_rules] lemma imp_left : WF Γ Ω' (p ⟹ q) → WF Γ Ω' p := by WF_prover @[WF_rules] lemma imp_right : WF Γ Ω' (p ⟹ q) → WF Γ Ω' q := by WF_prover @[WF_rules] lemma pair_left : WF Γ (A ×× B) ⟪a,b⟫ → WF Γ A a := by WF_prover @[WF_rules] lemma pair_right : WF Γ (A ×× B) ⟪a,b⟫ → WF Γ B b := by WF_prover @[WF_rules] lemma comp_elim : WF Γ (𝒫 A) ⟦A | φ⟧ → WF (A::Γ) Ω φ := by WF_prover @[WF_rules] lemma all_elim : WF Γ Ω' (∀' A φ) → WF (A::Γ) Ω' φ := by WF_prover @[WF_rules] lemma ex_elim : WF Γ Ω' (∀' A φ) → WF (A::Γ) Ω' φ := by WF_prover @[WF_rules] lemma iff_intro : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⇔ q) := begin intros, apply_rules WF_rules, -- apply_rules [WF.and, WF.imp], end end end TT  #### Reid Barton (Jun 10 2020 at 11:14): Most or all of your second set of rules (starting with and_left) shouldn't be used with apply_rules. #### Billy Price (Jun 10 2020 at 11:15): Ah good point, they would generate infinite possibilities for derivation right? #### Reid Barton (Jun 10 2020 at 11:16): right, they are possibly suitable for forwards reasoning, but not for backwards reasoning #### Reid Barton (Jun 10 2020 at 11:17): oh, you just have a namespace problem actually #### Reid Barton (Jun 10 2020 at 11:18): I'm not sure what the right way to fix it is, but I would just move the attribute to the root namespace #### Billy Price (Jun 10 2020 at 11:18): outside namespace TT? #### Reid Barton (Jun 10 2020 at 11:18): right. Alternatively, call it TT.WF_rules everywhere #### Billy Price (Jun 10 2020 at 11:19): Everywhere except the definition? #### Reid Barton (Jun 10 2020 at 11:21): right, not literally in meta def WF_rules but everywhere else #### Reid Barton (Jun 10 2020 at 11:21): probably it's optional in  WF_rules , I forget how the backticked names work exactly #### Billy Price (Jun 10 2020 at 11:26): I can't add TT. to any of the other WF_rules without red-lines "unknown attribute [TT.WF_rules]" #### Mario Carneiro (Jun 10 2020 at 11:26): Not optional with WF_rules but you should be using WF_rules and there it is optional #### Mario Carneiro (Jun 10 2020 at 11:28): For reference:  name  goes through name resolution and is checked at tactic compile time, while name is used as is (and so is generally checked at run time) #### Billy Price (Jun 10 2020 at 11:31): I'm not sure I understand the relevance. Is the name checking time relevant to whether a TT. is needed? #### Billy Price (Jun 10 2020 at 11:33): By the way apply_rules WF_rules and apply_rules TT.WF_rules both give "no matching rule", and apply_rules hsdfsfj gives unknown identifier hsdfsfj , so it seems to be recognising the object #### Mario Carneiro (Jun 10 2020 at 11:34): maybe you have no matching rule #### Reid Barton (Jun 10 2020 at 11:34): Weird. It works for me when I change all occurrences of WF_rules to TT.WF_rules except the one in meta def WF_rules #### Mario Carneiro (Jun 10 2020 at 11:34): name resolution means that it inserts namespaces based on the current context #### Reid Barton (Jun 10 2020 at 11:34): and once I comment out all the bad rules #### Mario Carneiro (Jun 10 2020 at 11:35): so  WF_rules  is equivalent to  TT.WF_rules except that it will give an error if WF_rules can't be found #### Billy Price (Jun 10 2020 at 11:41): I can't get anything working here's the most updated version of what I've got, as soon as I change any instances of WF_rules to TT.WF_rules it doesn't recognise it, and the usage in the actual proof is ambilavent to TT.. However apply_rules [WF.and, WF.imp] works fine. /- Definitions of a type theory Author: Billy Price -/ import data.finset namespace TT inductive type : Type | Unit | Omega | Prod (A B : type)| Pow (A : type) notation Ω := type.Omega def Unit := type.Unit infix ××:max := type.Prod notation 𝒫A :max := type.Pow A def context := list type inductive term : Type | star : term | top : term | bot : term | and : term → term → term | or : term → term → term | imp : term → term → term | elem : term → term → term | pair : term → term → term | var : ℕ → term | comp : type → term → term | all : type → term → term | ex : type → term → term open term -- * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * -- Notation and derived operators -- * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * notation 𝟘 := term.var 0 notation 𝟙 := term.var 1 notation 𝟚 := term.var 2 notation 𝟛 := term.var 3 notation 𝟜 := term.var 4 notation 𝟝 := term.var 5 notation ⁎ := term.star -- input \asterisk notation ⊤ := term.top -- \top notation ⊥ := term.bot -- input \bot infixr  ⟹ :60 := term.imp -- input \==> infixr  ⋀  :70 := term.and -- input \And or \bigwedge infixr  ⋁  :59 := term.or -- input \Or or \bigvee def not (p : term) := p ⟹ ⊥ prefix ∼:max := not -- input \~ def iff (p q: term) := (p ⟹ q) ⋀ (q ⟹ p) infix  ⇔ :60 := iff -- input \<=> infix ∈ := term.elem infix ∉ := λ a α, not (term.elem a α) notation ⟦  A  |  φ  ⟧ := term.comp A φ notation ⟪ a , b ⟫ := term.pair a b notation ∀' := term.all notation ∃' := term.ex section substitution @[simp] def lift_d (d : ℕ) : ℕ → term → term | k ⁎ := ⁎ | k ⊤ := ⊤ | k ⊥ := ⊥ | k (p ⋀ q) := (lift_d k p) ⋀ (lift_d k q) | k (p ⋁ q) := (lift_d k p) ⋁ (lift_d k q) | k (p ⟹ q) := (lift_d k p) ⟹ (lift_d k q) | k (a ∈ α) := (lift_d k a) ∈ (lift_d k α) | k ⟪a,b⟫ := ⟪lift_d k a, lift_d k b⟫ | k (var m) := if m≥k then var (m+d) else var m | k ⟦A | φ⟧ := ⟦A | lift_d (k+1) φ⟧ | k (∀' A φ) := ∀' A$ lift_d (k+1) φ
| k (∃' A φ)   := ∃' A $lift_d (k+1) φ @[simp] def lift := lift_d 1 0 @[simp] def subst : ℕ → term → term → term | n x ⁎ := ⁎ | n x ⊤ := ⊤ | n x ⊥ := ⊥ | n x (p ⋀ q) := (subst n x p) ⋀ (subst n x q) | n x (p ⋁ q) := (subst n x p) ⋁ (subst n x q) | n x (p ⟹ q) := (subst n x p) ⟹ (subst n x q) | n x (a ∈ α) := (subst n x a) ∈ (subst n x α) | n x ⟪a,c⟫ := ⟪subst n x a, subst n x c⟫ | n x (var m) := if n=m then x else var m | n x ⟦ A | φ ⟧ := ⟦A | subst (n+1) (lift x) φ⟧ | n x (∀' A φ) := ∀' A (subst (n+1) (lift x) φ) | n x (∃' A φ) := ∃' A (subst (n+1) (lift x) φ) notation ⁅ φ  //  b ⁆ := subst 0 b φ #reduce ⁅𝟘 // ⊤ ⋀ ⊥⁆ #reduce ⁅ 𝟙 // ⊤ ⋀ ⊥⁆ end substitution def eq (A:type) (a₁ a₂ : term) : term := ∀' (𝒫 A)$ ((lift a₁) ∈ 𝟘) ⇔ ((lift a₂) ∈ 𝟘)
notation a  ≃[:max A ] :0 b := eq A a b

#check eq Unit 𝟘 𝟘

def singleton (A : type) (a : term) := ⟦A | (lift a) ≃[A] 𝟘⟧

def ex_unique (A : type) (φ : term) : term :=
∃' A (⟦A | φ⟧ ≃[𝒫 A] (singleton A 𝟘))
prefix ∃!':2 := ex_unique

def subseteq (A : type) (α : term) (β : term) : term :=
∀' A (𝟘 ∈ α) ⟹ (𝟘 ∈ β)
notation a  ⊆[:max A ] :0 b := subseteq A a b

def term_prod {A B : type} (α β : term) : term :=
⟦ A ×× B | ∃' A (∃' B ((𝟙 ∈ α) ⋀ (𝟘 ∈ β) ⋀ (eq (A ×× B) 𝟚 ⟪𝟙,𝟘⟫)))⟧
notation α  ×x[:max A ] :0 β := term_prod A α β

-- * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
open term

inductive WF : context → type → term → Prop
| star {Γ}         : WF Γ Unit ⁎
| top  {Γ}         : WF Γ Ω ⊤
| bot  {Γ}         : WF Γ Ω ⊥
| and  {Γ p q}     : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⋀ q)
| or   {Γ p q}     : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⋁ q)
| imp  {Γ p q}     : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⟹ q)
| elem {Γ A a α}   : WF Γ A a → WF Γ (𝒫 A) α → WF Γ Ω (a ∈ α)
| pair {Γ A B a b} : WF Γ A a → WF Γ B b → WF Γ (A ×× B) ⟪a,b⟫
| var  {Γ A n}     : list.nth Γ n = some A → WF Γ A (var n)
| comp {Γ A φ}     : WF (A::Γ) Ω φ → WF Γ (𝒫 A) ⟦A | φ⟧
| all  {Γ A φ}     : WF (A::Γ) Ω φ → WF Γ Ω (∀' A φ)
| ex   {Γ A φ}     : WF (A::Γ) Ω φ → WF Γ Ω (∃' A φ)

@[user_attribute]
meta def WF_rules : user_attribute :=
{ name := WF_rules,
descr := "lemmas usable to prove Well Formedness" }

attribute [WF_rules] WF.star WF.top WF.bot WF.and WF.or WF.imp WF.elem WF.pair WF.var WF.comp WF.all WF.ex

section

variable Γ : context
variables p q r φ a b α : term
variables {A B Ω' : type}
-- Ω' is just a fake/variable version of Ω so we don't need to bother proving
-- that it must be Ω itself.'

meta def WF_prover : tactic unit := do [intro h, cases h, assumption]

lemma WF.and_left   : WF Γ Ω' (p ⋀ q) → WF Γ Ω' p := by WF_prover
lemma WF.and_right  : WF Γ Ω' (p ⋀ q) → WF Γ Ω' q := by WF_prover
lemma WF.or_left    : WF Γ Ω' (p ⋁ q) → WF Γ Ω' p := by WF_prover
lemma WF.or_right   : WF Γ Ω' (p ⋁ q) → WF Γ Ω' q := by WF_prover
lemma WF.imp_left   : WF Γ Ω' (p ⟹ q) → WF Γ Ω' p := by WF_prover
lemma WF.imp_right  : WF Γ Ω' (p ⟹ q) → WF Γ Ω' q := by WF_prover
lemma WF.pair_left  : WF Γ (A ×× B) ⟪a,b⟫ → WF Γ A a := by WF_prover
lemma WF.pair_right : WF Γ (A ×× B) ⟪a,b⟫ → WF Γ B b := by WF_prover
lemma WF.comp_elim  : WF Γ (𝒫 A) ⟦A | φ⟧ → WF (A::Γ) Ω φ := by WF_prover
lemma WF.all_elim   : WF Γ Ω' (∀' A φ) → WF (A::Γ) Ω' φ := by WF_prover
lemma WF.ex_elim    : WF Γ Ω' (∀' A φ) → WF (A::Γ) Ω' φ := by WF_prover
@[WF_rules] lemma WF.iff_intro : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⇔ q) :=
begin
intros,
apply_rules WF_rules,
-- apply_rules [WF.and, WF.imp],
end

end

end TT


#### Billy Price (Jun 10 2020 at 11:41):

Could you paste what you got working @Reid Barton ?

#### Reid Barton (Jun 10 2020 at 11:44):

/-
Definitions of a type theory

Author: Billy Price
-/

import data.finset
namespace TT

inductive type : Type
| Unit | Omega | Prod (A B : type)| Pow (A : type)

notation Ω := type.Omega
def Unit := type.Unit
infix ××:max := type.Prod
notation 𝒫A :max := type.Pow A

def context := list type

inductive term : Type
| star : term
| top  : term
| bot  : term
| and  : term → term → term
| or   : term → term → term
| imp  : term → term → term
| elem : term → term → term
| pair : term → term → term
| var  : ℕ → term
| comp : type → term → term
| all  : type → term → term
| ex   : type → term → term

open term

-- * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
-- Notation and derived operators
-- * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *

notation 𝟘 := term.var 0
notation 𝟙 := term.var 1
notation 𝟚 := term.var 2
notation 𝟛 := term.var 3
notation 𝟜 := term.var 4
notation 𝟝 := term.var 5

notation ⁎ := term.star    -- input \asterisk
notation ⊤ := term.top     --       \top
notation ⊥ := term.bot     -- input \bot
infixr  ⟹ :60 := term.imp -- input \==>
infixr  ⋀  :70 := term.and -- input \And or \bigwedge
infixr  ⋁  :59 := term.or  -- input \Or or \bigvee

def not (p : term) := p ⟹ ⊥
prefix ∼:max := not -- input \~

def iff (p q: term) := (p ⟹ q) ⋀ (q ⟹ p)
infix  ⇔ :60 := iff -- input \<=>

infix ∈ := term.elem
infix ∉ := λ a α, not (term.elem a α)
notation ⟦  A  |  φ  ⟧ := term.comp A φ

notation ⟪ a , b ⟫ := term.pair a b

notation ∀' := term.all
notation ∃' := term.ex

section substitution

@[simp]
def lift_d (d : ℕ) : ℕ → term → term
| k ⁎          := ⁎
| k ⊤          := ⊤
| k ⊥          := ⊥
| k (p ⋀ q)    := (lift_d k p) ⋀ (lift_d k q)
| k (p ⋁ q)    := (lift_d k p) ⋁ (lift_d k q)
| k (p ⟹ q)   := (lift_d k p) ⟹ (lift_d k q)
| k (a ∈ α)    := (lift_d k a) ∈ (lift_d k α)
| k ⟪a,b⟫      := ⟪lift_d k a, lift_d k b⟫
| k (var m)    := if m≥k then var (m+d) else var m
| k ⟦A | φ⟧     :=    ⟦A | lift_d (k+1) φ⟧
| k (∀' A φ)   := ∀' A $lift_d (k+1) φ | k (∃' A φ) := ∃' A$ lift_d (k+1) φ

@[simp]
def lift := lift_d 1 0

@[simp]
def subst : ℕ → term → term → term
| n x ⁎          := ⁎
| n x ⊤          := ⊤
| n x ⊥          := ⊥
| n x (p ⋀ q)    := (subst n x p) ⋀ (subst n x q)
| n x (p ⋁ q)    := (subst n x p) ⋁ (subst n x q)
| n x (p ⟹ q)  := (subst n x p) ⟹ (subst n x q)
| n x (a ∈ α)    := (subst n x a) ∈ (subst n x α)
| n x ⟪a,c⟫      := ⟪subst n x a, subst n x c⟫
| n x (var m)    := if n=m then x else var m
| n x ⟦ A | φ ⟧   :=    ⟦A | subst (n+1) (lift x) φ⟧
| n x (∀' A φ)     := ∀' A (subst (n+1) (lift x) φ)
| n x (∃' A φ)     := ∃' A (subst (n+1) (lift x) φ)

notation  ⁅ φ  //   b ⁆ := subst 0 b φ

#reduce ⁅𝟘 // ⊤ ⋀ ⊥⁆
#reduce ⁅ 𝟙 // ⊤ ⋀ ⊥⁆

end substitution

| k (∃' A φ)   := ∃' A $lift_d (k+1) φ @[simp] def lift := lift_d 1 0 @[simp] def subst : ℕ → term → term → term | n x ⁎ := ⁎ | n x ⊤ := ⊤ | n x ⊥ := ⊥ | n x (p ⋀ q) := (subst n x p) ⋀ (subst n x q) | n x (p ⋁ q) := (subst n x p) ⋁ (subst n x q) | n x (p ⟹ q) := (subst n x p) ⟹ (subst n x q) | n x (a ∈ α) := (subst n x a) ∈ (subst n x α) | n x ⟪a,c⟫ := ⟪subst n x a, subst n x c⟫ | n x (var m) := if n=m then x else var m | n x ⟦ A | φ ⟧ := ⟦A | subst (n+1) (lift x) φ⟧ | n x (∀' A φ) := ∀' A (subst (n+1) (lift x) φ) | n x (∃' A φ) := ∃' A (subst (n+1) (lift x) φ) notation ⁅ φ  //  b ⁆ := subst 0 b φ #reduce ⁅𝟘 // ⊤ ⋀ ⊥⁆ #reduce ⁅ 𝟙 // ⊤ ⋀ ⊥⁆ end substitution lemma WF.lift_closed {a A} : WF [] A a → a = lift a := begin generalize_hyp e : [] = Γ, intro wf, induction wf;cases e;simp, end end TT  #### Mario Carneiro (Jun 11 2020 at 12:21): You will need a stronger inductive hypothesis #### Mario Carneiro (Jun 11 2020 at 12:24): simp will do a lot of the work here, although it doesn't like that you wrote the equality the wrong way around lemma WF.lift_closed {a A} : WF [] A a → lift a = a := begin generalize_hyp e : [] = Γ, intro wf, induction wf;cases e;simp * at *, end  #### Billy Price (Jun 11 2020 at 12:25): What do the stars do? #### Kenny Lau (Jun 11 2020 at 12:26): they make the sky more beautiful #### Billy Price (Jun 11 2020 at 12:26): Hahaha, oh I found the docs explaining what they are too #### Billy Price (Jun 11 2020 at 12:29): Lemme guess, I need to be proving the strong lemma which says "if the highest free variable is below the lift-cutoff, then lift a = a" #### Mario Carneiro (Jun 11 2020 at 12:30): Indeed. I believe the most similar statement to what you have here that will do the job is WF G A a → length G <= k -> lift_d 1 k a = a #### Billy Price (Jun 11 2020 at 12:36): This is an interesting pattern - the most "appropriately general" statement of a theorem is typically easier to prove than specialisations of that theorem. Is this specific to inductive proofs or formal proofs in general? #### Mario Carneiro (Jun 11 2020 at 12:39): this is pretty common of inductive proofs #### Mario Carneiro (Jun 11 2020 at 12:40): the examples I showed earlier were also of that form - I said that I wanted to prove something about P n 0 but the obvious inductive proof would try to show P 0 0 and P a 0 -> P (a+1) 0 which doesn't work #### Mario Carneiro (Jun 11 2020 at 12:41): induction proofs can vary a lot in their dependency structure, so the easiest reliable way to make lean do what you want is to say what you want #### Mario Carneiro (Jun 11 2020 at 12:41): (unfortunately this is also quite verbose so I usually use it as a last resort when basic induction doesn't do the right thing) #### Billy Price (Jun 11 2020 at 12:41): You're referring to the suffices pattern? #### Mario Carneiro (Jun 11 2020 at 12:42): yes #### Mario Carneiro (Jun 11 2020 at 12:42): You could use it here too #### Mario Carneiro (Jun 11 2020 at 12:45): lemma WF.lift_closed {a A} : WF [] A a → lift a = a := begin suffices : ∀ G A a, WF G A a → lift_d 1 (list.length G) a = a, { exact this _ _ _ }, introv wf, induction wf; simp * at *, exact if_neg (not_le_of_gt (list.nth_eq_some.1 wf_a).fst) end  #### Billy Price (Jun 11 2020 at 13:00): So I've been doing all of this stuff for a 1 semester project (I convinced a mathematician at my uni to supervise me for a project in Lean), and I'm going to be ending it on "here's a statement in Lean that says this type theory forms a category". Once the semester is over (very soon) I want to go back to the basics of Lean so I'm better equipped to actual prove all the theorems From what you've seen from me, is there any particular ways you'd recommend learning the relevant intricacies of Lean I need to understand how to do my proofs? Do the mathematics tutorials (NNG, Real Number Game etc) cover the same stuff but on different topics? Should I keep posting "how do I do this proof" whenever I get to a new roadblock? Usually the easiest answer (like this time) is just "here's the proof" and I feel bad that I'm just constantly getting other people to do my work for me. Thoughts? #### Mario Carneiro (Jun 11 2020 at 13:11): the point isn't "here's the proof", it is "here's a technique for solving problems of this kind" #### Mario Carneiro (Jun 11 2020 at 13:11): don't worry about my having "stolen" a proof from you, trust me there are more than enough proof obligations to go around #### Mario Carneiro (Jun 11 2020 at 13:14): For a type theory category, I suggest jumping into the formalization and asking questions when you don't know how to express something #### Mario Carneiro (Jun 11 2020 at 13:15): My sense is that it should not be too difficult to write something down that vaguely resembles your goal statement. There will then be some rearranging and fixing of the definition to make it amenable to proof stuff #### Mario Carneiro (Jun 11 2020 at 13:17): For the first pass, figure out what a category is: if you intend to use mathlib categories, then study the mathlib definition of a category, or if you plan to write your own then figure out how to make that definition. You said something about quotienting by equivalence, so figure out how to write down a quotient and specify functions on quotients. Don't concern yourself with proofs too much, but try not to write something that you know is false #### Mario Carneiro (Jun 11 2020 at 13:18): I think the best way to learn about intricacies of lean is to trip over them on your way to getting something done #### Billy Price (Jun 11 2020 at 13:26): Thanks, that's good to hear. My concern is less about intellectual property (though that's important), and more about using up your time! At a basic level, I do understand how to define a math lib category and I feel somewhat comfortable with quotient stuff (I've followed the Zmod37 example and created my own quotient type), but one of my roadblocks there is how to say the following theorem (which I hope is true), "If I have a proof Γ p q and either of p or q contains some a : term which is well-formed of type A (WF Γ A a), and a is provably equal to a' (I can show proof Γ ⊤ a ≃[A] a'), then I can swap out occurrences of a with a'. I think that would help me a lot with lifting things to the quotients. #### Billy Price (Jun 11 2020 at 13:26): ah whoops sent too soon, I'll edit it (done) #### Billy Price (Jun 11 2020 at 13:37): Here's an attempt which I'm worried is too general and false. theorem eq_sound {Γ} (A : type) (a₁ a₂ : term) (eq : proof Γ ⊤ (a₁ ≃[A] a₂)) (f g : term → term) : proof Γ (f a₁) (g a₁) → proof Γ (f a₂) (g a₂)  (made it a theorem because wew, it looks powerful.) #### Mario Carneiro (Jun 11 2020 at 13:38): yeah that version is false #### Billy Price (Jun 11 2020 at 13:39): Good to know #### Mario Carneiro (Jun 11 2020 at 13:39): Do you have a substitution operator? If so you can express that t[a1/x] = t[a2/x] is provable #### Mario Carneiro (Jun 11 2020 at 13:43): You can also define a subset of functions term -> term according to whether they respect equality. The theorem holds for such functions more or less by definition, but the interesting observation is that all the term constructors are examples of such functions #### Billy Price (Jun 11 2020 at 13:53): I actually tried that substitution method but I found it difficult to apply it. Thinking about the second option - that sounds like you could inductively define all such functions based on the term constructors? #### Billy Price (Jun 11 2020 at 13:55): How would one say "a function which is just some composition of the term constructors?" #### Jannis Limperg (Jun 11 2020 at 13:56): @Billy Price I'd be very happy if you could try the current version of my induction tactic. It should take care of all the generalising for you and give less scary names as a bonus. The current draft is at the induction branch. When you have that, you should be able to import tactic.induction and use induction' instead of the generalize ..., induction dance. I'll gladly fix any bugs you find. #### Billy Price (Jun 11 2020 at 13:59): Oh cool! I will gladly do so :) #### Mario Carneiro (Jun 11 2020 at 14:03): How would one say "a function which is just some composition of the term constructors?" Of course the import of the substitution operator is that it is a way to represent such functions using terms #### Mario Carneiro (Jun 11 2020 at 14:05): The simpler alternative is just to prove in each individual case that a concretely given function satisfies the equality property by applying equality axioms using e.g. apply_rules #### Billy Price (Jun 11 2020 at 14:13): What do you mean by the equality axioms? #### Kevin Buzzard (Jun 11 2020 at 22:00): @Billy Price the way to learn the intricacies of Lean is to have a healthy source of projects in your area of interest and then just keep formalising and ask whenever you get stuck. After a few months (maybe it took me a year but I am old and have no CS background) you find that you're asking fewer questions and are in fact now answering them. #### Billy Price (Jun 12 2020 at 02:25): Tada I did a proof, I think I better understand the idea of generalising hypotheses in induction now. @Jannis Limperg I haven't yet switched to the induction branch to try your tactic - how do I do that? lemma lift_zero_does_nothing {k} {a : term} : lift_d 0 k a = a := begin suffices : ∀ k, lift_d 0 k a = a, { exact this _ }, induction a;simp * at *, end  Let me phrase some subtlety I was overlooking before (lemme know if this is the wrong way of thinking about it): Although k is an arbitrary hypothesis to the lemma, within the goal state, it's thought of as fixed. It's a 'given' number. So without the suffices line, the inductive cases must be proved for that fixed k. This seems to highlight the subtle difference between example (k : nat) : P k and example : ∀ k : nat, P k. #### Billy Price (Jun 12 2020 at 02:27): I could make my original lemma lemma lift_zero_does_nothing {a : term} : ∀ k, lift_d 0 k a = a, but that would make it less usable right? #### Billy Price (Jun 12 2020 at 02:29): More succinct lemma lift_zero_does_nothing {k} {a : term} : lift_d 0 k a = a := by induction a generalizing k;simp *  #### Mario Carneiro (Jun 12 2020 at 02:35): Although k is an arbitrary hypothesis to the lemma, within the goal state, it's thought of as fixed. It's a 'given' number. So without the suffices line, the inductive cases must be proved for that fixed k. Yes and no. The induction tactic will generalize the variable k, ignoring the initial value that it had. It's just that when the input was a variable to start with this is no loss (but you will see k hanging around uselessly in the inductive subcases) #### Mario Carneiro (Jun 12 2020 at 02:36): I could make my original lemma lemma lift_zero_does_nothing {a : term} : ∀ k, lift_d 0 k a = a, but that would make it less usable right? Externally these are indistinguishable, except that you reordered the two variables and made k explicit in this version #### Mario Carneiro (Jun 12 2020 at 02:38): In tactic mode you will always end up intro'ing all variables before the induction, so it makes no difference what is "right of the colon". This does affect inductive proofs performed using the equation compiler though (you will not be able to use the equation compiler with the first version) #### Mario Carneiro (Jun 12 2020 at 02:40): Oh, correction: since you are doing induction on term in this case, there are no indices and so k will be held fixed unless you explicitly use generalizing to indicate that you want it to change #### Jannis Limperg (Jun 12 2020 at 13:00): Billy Price said: Jannis Limperg I haven't yet switched to the induction branch to try your tactic - how do I do that? Could you post your leanpkg.toml? Alternatively put your project on Github or something, then I'll see what needs to be changed. #### Kevin Buzzard (Jun 12 2020 at 17:25): @Billy Price the answer depends on whether you're working in mathlib or working on your own project and have mathlib as a dependency. If you have mathlib as a dependency then you probably have to edit your project's leanpkg.toml. @Jannis Limperg 's branch is here https://github.com/leanprover-community/mathlib/commits/induction and the most recent commit is 52c995b6ee3ed40c6c962043e8bdd37176a942e3 so you want to change your mathlib rev to that commit hash and then do leanproject get-mathlib-cache in the root directory of your project, and it should then all work by magic. #### Kevin Buzzard (Jun 12 2020 at 17:27): If you're working in mathlib directory then you might be able to just checkout the induction branch and then do leanproject up. #### Billy Price (Jun 18 2020 at 05:54): Mario Carneiro said: I would recommend keeping the term syntax as context free as possible, and have a well typing condition afterward that can have whatever dependencies it wants I'm currently reflecting on the decisions I made for the definitions in my type theory, and I'm trying to justify why terms and Well-formedness are defined separately - it seemed that I had to do a lot of work later regarding lemmas to prove well-formedness. Would this have not gone away if I defined only well-formed terms? Are there more obvious reasons why keeping terms context free is valuable? #### Mario Carneiro (Jun 18 2020 at 08:04): If you find yourself manually constructing terms with a proof of well formedness a lot (for example if you are acting like a typechecker and have some concrete terms of interest), then one thing you can do is construct a sigma type of a term and a proof of its well foundedness, and then the construction of the term will be carried out in parallel with the proof of well foundedness. Here a separate WF proof is not particularly helpful. (This is done in the flypitch formalization, for example.) The advantage comes when you are doing metatheory, which is usually what people want to do with defined type theories such as this inside lean. (If you just want a typechecker, it is often simpler to just write one directly in a standard programming language, as the many proof assistants for HoTT-based type theories can attest.) Here you really want to be able to do things like reassociate contexts or do other non-defeq manipulations inside the indices to the WF inductive, and then if WF is not a Prop but is rather a dependent type of well formed terms, this will cause no end of headaches due to the induced cast. #### Billy Price (Jun 19 2020 at 02:10): I think you've interpreted my question as "I'm sick of the separation of terms and Well-formedness, so how can I remedy that in the current setup (thanks for the suggestions), but I'm interested in what are the downsides of doing it all in one with term : context -> type -> Type. I think you were answering that in this reply - but could you explain what you mean here about carrying around type state, and what definitional equalities are hard to get? Mario Carneiro said: It's easier for them because it's only one type, yes. You end up having to carry around a lot of "type state" in real type theories, and it becomes hard to get all the definitional equalities you want #### Mario Carneiro (Jun 19 2020 at 02:47): I mean the context and the type #### Mario Carneiro (Jun 19 2020 at 02:48): Hard to get definitional equalities are things like Gamma ++ a :: Delta = (Gamma ++ [a]) ++ Delta that come up in proofs #### Mario Carneiro (Jun 19 2020 at 02:48): it's even worse when Gamma itself has sequential dependencies as in dependent type theory #### Mario Carneiro (Jun 19 2020 at 02:51): If you have a term Gamma ++ a :: Delta |- e : A and want the same term (Gamma ++ [a]) ++ Delta |- e : A you can't do the obvious thing. Instead you have to cast e to the new context, and now it's not a constructor so you can't pattern match on it, and things sort of go downhill from there #### Mario Carneiro (Jun 19 2020 at 02:52): It's certainly possible to construct things so that everything beautifully meshes together. But this is like a sudoku puzzle, a quite mind bending exercise that has little relation to the original problem you set out to solve #### Mario Carneiro (Jun 19 2020 at 02:54): If you like that sort of thing it's possible to build a career on it but you might find that you've left your original problem behind. (I would argue this is what happened to Voevodsky with HoTT) #### Mario Carneiro (Jun 19 2020 at 02:56): If you have extrinsic typing, then you can transport terms to new contexts without apology. All the ugliness is encapsulated in proofs that don't interfere with later statements because of proof irrelevance #### Billy Price (Jun 19 2020 at 03:05): Ah okay I think I follow. If we dump the context from the constructor, is the remaining problem just that it's hard to define the var constructor with no context? Or are there still downsides without the var problem? #### Mario Carneiro (Jun 19 2020 at 03:09): I like to think about indices to dependent types as "rigid variables". Variables in these positions can only be manipulated in very restrictive ways, essentially by applying constructors and pattern matching. Using functions defined by induction is a no-no #### Mario Carneiro (Jun 19 2020 at 03:09): This mostly matches the way we treat types in simple type theory #### Mario Carneiro (Jun 19 2020 at 03:10): for example a list A is not the same as a list A' even if A and A' are extensionally equivalent (have the same elements or some other synthetic notion of equality) #### Billy Price (Jun 19 2020 at 03:13): I get what you're saying but I don't see the relevance #### Mario Carneiro (Jun 19 2020 at 03:14): If you take the context out of a term, it just has a type, and presumably the inductive type type is a simple inductive. So this is plausible. But variables have a weird type in this context: you didn't do this but a classically reasonable alternative type for the var constructor would have been var (i : fin (length G)) : term G (G.nth' i) but this is a bad idea in DTT #### Mario Carneiro (Jun 19 2020 at 03:15): because it uses inductive functions in rigid positions twice: once in fin (length G) and once in term G (G.nth' i) #### Billy Price (Jun 19 2020 at 03:21): That's still term : context -> type -> Type though? #### Mario Carneiro (Jun 19 2020 at 03:22): well you can't write var at all without a context #### Mario Carneiro (Jun 19 2020 at 03:23): it could be a parameter though #### Mario Carneiro (Jun 19 2020 at 03:23): as long as you don't also have binders #### Mario Carneiro (Jun 19 2020 at 03:24): parameters to inductive types are also rigid variables, but you usually don't have as pressing a need to change them in the middle of a proof #### Billy Price (Jun 19 2020 at 03:26): What do you mean by parameter as opposed to a rigid variable? #### Mario Carneiro (Jun 19 2020 at 03:27): parameters to inductive types meaning left of the colon #### Mario Carneiro (Jun 19 2020 at 03:27): inductive term (G : context) : type -> Type #### Mario Carneiro (Jun 19 2020 at 03:27): Then the G in term G A is a rigid variable #### Mario Carneiro (Jun 19 2020 at 03:29): One way to conceptualize rigid variables are as terms about which it is common to have equalities, like list.append_assoc, but for which simp refuses to touch and rw gives motive is not type correct when you try to use those equalities #### Mario Carneiro (Jun 19 2020 at 03:32): as long as you only ever do syntactic or defeq matching in rigid positions there are no problems #### Billy Price (Jun 19 2020 at 05:18): Okay. #### Billy Price (Jun 19 2020 at 05:25): By the way, my type theory as it is, is the "pure" version, which is supposed to be extensible. How would I go about defining a type theory which has at least everything I've defined, but maybe more types, more terms, more deduction rules etc? For example, if I wanted to throw in a mynat : type and corresponding terms which are WF [] mynat? I imagine doing so would ruin all the lemmas I've proved. All my lemmas just talk about stuff in the pure type theory, so they should hold in any extension (I imagine there are pathological counterexamples depending on the generality of the lemma). #### Billy Price (Jun 19 2020 at 05:35): Just an idea that probably doesn't work because of cardinality. variable \alpha : Type inductive type : Type | special (\alpha : Type) | Unit | Omega | Pow (A : type) | Prod (A B : type)  #### Mario Carneiro (Jun 19 2020 at 05:58): That works fine #### Mario Carneiro (Jun 19 2020 at 05:59): you have to parameterize the whole theory over alpha which is kind of annoying but otherwise it works well #### Mario Carneiro (Jun 19 2020 at 06:00): It's also not very pleasant to actually instantiate and get this nested inductive type of types with more types inside #### Mario Carneiro (Jun 19 2020 at 06:04): Since you are wondering about universe issues: note that alpha will usually be a small type, for example inductive base_types | nat | bool | real | extra_special (beta : Type) where perhaps beta is yet another parameter #### Billy Price (Jun 19 2020 at 06:46): Ah whoops I made \alpha a variable and a parameter at the same time. I have two possible ideas below, both of which I think are ugly - is there not a more natural way to do this? Instead of taking some other variable Type and incorporating it into my definition, I just say to the user "give me a Type of things which I will think of as types in my theory, as long Unit, Omega are of that type and the Pow, Prod constructors make new types out of old ones". I am somewhat ambivalent to whether Unit and Omega are naturally a part of the type of types that the user creates or if they are just tacked on. variable \alpha : Type inductive type : Type | special (X : \alpha) | Unit | Omega | Pow (A : type) | Prod (A B : type)  inductive type : Type | special (X : Type) | Unit | Omega | Pow (A : type) | Prod (A B : type)  #### Billy Price (Jun 19 2020 at 06:47): Regarding my 2 ideas, I have a feeling the second one is fundamentally different (perhaps the wrong idea). #### Billy Price (Jun 19 2020 at 06:48): Perhaps my "give me.." idea is more in the spirit of a type class? #### Mario Carneiro (Jun 19 2020 at 07:11): the second one should not typecheck #### Mario Carneiro (Jun 19 2020 at 07:11): because there is a universe issue #### Mario Carneiro (Jun 19 2020 at 07:12): You want the first one #### Mario Carneiro (Jun 19 2020 at 07:12): I just say to the user "give me a Type of things which I will think of as types in my theory, as long Unit, Omega are of that type and the Pow, Prod constructors make new types out of old ones". :point_up: this #### Mario Carneiro (Jun 19 2020 at 07:13): oh wait you mean it's not an inductive type at all #### Mario Carneiro (Jun 19 2020 at 07:13): you can do that, and the interface will be nicer, but you will not be able to prove theorems about the PTS by induction anymore #### Mario Carneiro (Jun 19 2020 at 07:15): You could prove theorems relative to a partial recursor that the user also provides, but then every theorem is going to come with side conditions saying that the theorem already holds in some way for all the types the PTS doesn't know about #### Billy Price (Jun 19 2020 at 09:56): Good to know, I think I'll stick with my pure type theory for now. #### Billy Price (Jun 19 2020 at 10:04): I just realised I could do this instance nat_coe_var : has_coe ℕ term := ⟨term.var⟩  instead of this notation 𝟘 := term.var 0 notation 𝟙 := term.var 1 notation 𝟚 := term.var 2 notation 𝟛 := term.var 3 notation 𝟜 := term.var 4 notation 𝟝 := term.var 5  is the coercion one a bad idea? #### Billy Price (Jun 19 2020 at 10:06): Or is there any way I can do a unique term construction like ⟨0⟩ since there's only one term constructor that takes a single (nat) argument? #### Billy Price (Jun 19 2020 at 10:07): It doesn't work out of the box, because it expects term to only have one term constructor. inductive term : Type | star : term | top : term | bot : term | and : term → term → term | or : term → term → term | imp : term → term → term | elem : term → term → term | pair : term → term → term | var : ℕ → term | comp : type → term → term | all : type → term → term | ex : type → term → term  #### Mario Carneiro (Jun 19 2020 at 17:14): I mean it's fine, but it will never be particularly nice to write terms with de bruijn variables #### Billy Price (Jun 20 2020 at 05:26): Why does this happen? I write rw append_nil Γ in this state and it tells me rewrite tactic failed, did not find instance of the pattern in the target expression Γ ++ nil ¿que? 2 goals case list.nil Γ : context, A : type, n : ℕ, h : WF Γ A (var n), eq : nth Γ n = some A ⊢ WF (Γ ++ nil) A (var n)  #### Billy Price (Jun 20 2020 at 06:01): Also how would I do apply_rules on all of the hypotheses? (to extract more hypotheses) Or on one hypothesis? Something like simp at * (Not for this goal state) #### Mario Carneiro (Jun 20 2020 at 07:06): I can't say offhand why that would fail. #mwe #### Billy Price (Jun 21 2020 at 04:41): I'll come back to this one. #### Billy Price (Jun 21 2020 at 04:46): Is there any practical difference between these two code blocks? I'd like to treat WF.foo : Prop just like the inductively defined lemmas. inductive WF : context → type → term → Prop | star {Γ} : WF Γ 𝟙 ⁎ | top {Γ} : WF Γ Ω ⊤ | bot {Γ} : WF Γ Ω ⊥ | and {Γ p q} : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⋀ q) | or {Γ p q} : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⋁ q) | imp {Γ p q} : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⟹ q) | elem {Γ A a α} : WF Γ A a → WF Γ (𝒫 A) α → WF Γ Ω (a ∈ α) | pair {Γ A B a b} : WF Γ A a → WF Γ B b → WF Γ (A 𝕏 B) ⟪a,b⟫ | var {Γ A n} : list.nth Γ n = some A → WF Γ A (var n) | comp {Γ A φ} : WF (A::Γ) Ω φ → WF Γ (𝒫 A) ⟦A | φ⟧ | all {Γ A φ} : WF (A::Γ) Ω φ → WF Γ Ω (∀' A φ) | ex {Γ A φ} : WF (A::Γ) Ω φ → WF Γ Ω (∃' A φ) namespace WF lemma foo : Prop end  inductive WF : context → type → term → Prop | star {Γ} : WF Γ 𝟙 ⁎ | top {Γ} : WF Γ Ω ⊤ | bot {Γ} : WF Γ Ω ⊥ | and {Γ p q} : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⋀ q) | or {Γ p q} : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⋁ q) | imp {Γ p q} : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⟹ q) | elem {Γ A a α} : WF Γ A a → WF Γ (𝒫 A) α → WF Γ Ω (a ∈ α) | pair {Γ A B a b} : WF Γ A a → WF Γ B b → WF Γ (A 𝕏 B) ⟪a,b⟫ | var {Γ A n} : list.nth Γ n = some A → WF Γ A (var n) | comp {Γ A φ} : WF (A::Γ) Ω φ → WF Γ (𝒫 A) ⟦A | φ⟧ | all {Γ A φ} : WF (A::Γ) Ω φ → WF Γ Ω (∀' A φ) | ex {Γ A φ} : WF (A::Γ) Ω φ → WF Γ Ω (∃' A φ) lemma WF.foo : Prop  #### Billy Price (Jun 21 2020 at 04:47): Related question - is WF a namespace in WF.star? #### Billy Price (Jun 21 2020 at 04:47): In the same way that WF is a namespace in WF.foo in the first code block #### Mario Carneiro (Jun 21 2020 at 04:49): no difference, yes it is a namespace #### Mario Carneiro (Jun 21 2020 at 04:49): one difference is that the WF namespace is open inside the proof of foo in the first case but not the second #### Billy Price (Jun 22 2020 at 13:39): Is there a proper way to write this meta definition? I'll do my best to render the backticks properly. meta def WF_prover : tactic unit:= do [apply_rules WF_rules]. It works for the most part but where I could previously do apply_rules WF_rules; refl, I cannot now do WF_prover; refl, with this error resulting. type mismatch at application WF_prover; refl term refl has type ∀ (a : ?m_1), ?m_2 a a : Prop but is expected to have type ?m_1 : Type ?  I have to do WF_prover, all_goals {refl} (which works). I'm guessing it's because I derived that meta definition from another one which sequenced several tactics, and I'm now just trying to rename one tactic. #### Billy Price (Jun 22 2020 at 13:45): Here's a related #mwe (more like #mnwe) meta def my_split : tactic unit:= do [split] example {p q} : p → q → (p ∧ q) := begin intros, split;assumption, end example {p q} : p → q → (p ∧ q) := begin intros, my_split;assumption -- doesn't work end  #### Reid Barton (Jun 22 2020 at 13:48): meta def tactic.interactive.my_split : tactic unit:= do [split]  #### Billy Price (Jun 22 2020 at 13:57): I don't have a more minimal #mwe for this, but the very last line here, it doesn't recognise WF_prover /- Definitions of a type theory Author: Billy Price -/ import data.finset import tactic.tidy namespace TT inductive type : Type | Unit | Omega | Prod (A B : type)| Pow (A : type) notation Ω := type.Omega notation 𝟙 := type.Unit infix 𝕏:max := type.Prod notation 𝒫A :max := type.Pow A inductive term : Type | star : term | top : term | bot : term | and : term → term → term | or : term → term → term | imp : term → term → term | elem : term → term → term | pair : term → term → term | var : ℕ → term | comp : type → term → term | all : type → term → term | ex : type → term → term open term -- * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * -- Notation and derived operators -- * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * def nat_coe_var : has_coe ℕ term := ⟨term.var⟩ local attribute [instance] nat_coe_var notation ⁎ := term.star -- input \asterisk notation ⊤ := term.top -- \top notation ⊥ := term.bot -- input \bot infixr  ⟹ :60 := term.imp -- input \==> infixr  ⋀  :70 := term.and -- input \And or \bigwedge infixr  ⋁  :59 := term.or -- input \Or or \bigvee def not (p : term) := p ⟹ ⊥ prefix ∼:max := not -- input \~ def iff (p q: term) := (p ⟹ q) ⋀ (q ⟹ p) infix  ⇔ :60 := iff -- input \<=> infix ∈ := term.elem infix ∉ := λ a α, not (term.elem a α) notation {{  A  |  φ  }} := term.comp A φ notation ⟪ a , b ⟫ := term.pair a b notation ∀' := term.all notation ∃' := term.ex def term.all_chain (Γ : list type) : term → term := flip (list.foldr (λ A ψ, term.all A ψ)) Γ def term.ex_chain (Γ : list type) : term → term := flip (list.foldr (λ A ψ, term.ex A ψ)) Γ @[simp] lemma term.unfold_all_chain {A Γ φ} : term.all_chain (A :: Γ) φ = ∀' A (term.all_chain Γ φ) := rfl @[simp] lemma term.unfold_ex_chain {A Γ φ} : term.ex_chain (A :: Γ) φ = ∃' A (term.ex_chain Γ φ) := rfl notation ∀[ Γ:(foldr , (h t, list.cons h t) list.nil) ] := term.all_chain Γ notation ∃[ Γ:(foldr , (h t, list.cons h t) list.nil) ] := term.ex_chain Γ section substitution @[simp] def lift_d (d : ℕ) : ℕ → term → term | k ⁎ := ⁎ | k ⊤ := ⊤ | k ⊥ := ⊥ | k (p ⋀ q) := (lift_d k p) ⋀ (lift_d k q) | k (p ⋁ q) := (lift_d k p) ⋁ (lift_d k q) | k (p ⟹ q) := (lift_d k p) ⟹ (lift_d k q) | k (a ∈ α) := (lift_d k a) ∈ (lift_d k α) | k ⟪a,b⟫ := ⟪lift_d k a, lift_d k b⟫ | k (var m) := if m≥k then var (m+d) else var m | k {{A | φ}} := {{A | lift_d (k+1) φ}} | k (∀' A φ) := ∀' A$ lift_d (k+1) φ
| k (∃' A φ)   := ∃' A $lift_d (k+1) φ notation ^ := lift_d 1 0 @[simp] def subst : ℕ → term → term → term | n x ⁎ := ⁎ | n x ⊤ := ⊤ | n x ⊥ := ⊥ | n x (p ⋀ q) := (subst n x p) ⋀ (subst n x q) | n x (p ⋁ q) := (subst n x p) ⋁ (subst n x q) | n x (p ⟹ q) := (subst n x p) ⟹ (subst n x q) | n x (a ∈ α) := (subst n x a) ∈ (subst n x α) | n x ⟪a,c⟫ := ⟪subst n x a, subst n x c⟫ | n x (var m) := if n=m then x else var m | n x {{ A | φ }} := {{A | subst (n+1) (^ x) φ}} | n x (∀' A φ) := ∀' A (subst (n+1) (^ x) φ) | n x (∃' A φ) := ∃' A (subst (n+1) (^ x) φ) notation ⁅ φ  //  b ⁆ := subst 0 b φ #reduce ⁅ ↑0 // ⊤ ⋀ ⊥⁆ #reduce ⁅ ↑1 // ⊤ ⋀ ⊥⁆ def FV : term → finset ℕ | ⁎ := ∅ | ⊤ := ∅ | ⊥ := ∅ | (p ⋀ q) := FV p ∪ FV q | (p ⋁ q) := FV p ∪ FV q | (p ⟹ q) := FV p ∪ FV q | (a ∈ α) := FV a ∪ FV α | ⟪a,b⟫ := FV a ∪ FV b | (var m) := finset.singleton m | {{ A | φ }} := ((FV φ).erase 0).image nat.pred | (∀' A φ) := ((FV φ).erase 0).image nat.pred | (∃' A φ) := ((FV φ).erase 0).image nat.pred end substitution def eq (A:type) (a₁ a₂ : term) : term := ∀' (𝒫 A)$ ((^ a₁) ∈ ↑0) ⇔ ((^ a₂) ∈ ↑0)
notation a  ≃[:max A ] :0 b := eq A a b

#check eq 𝟙 ↑0 ↑0

def singleton (A : type) (a : term) := {{A | (^ a) ≃[A] ↑0}}

def ex_unique (A : type) (φ : term) : term :=
∃' A ({{ A | φ }} ≃[𝒫 A] (singleton A ↑0))
prefix ∃!':2 := ex_unique

def subseteq (A : type) (α : term) (β : term) : term :=
∀' A (↑0 ∈ (^ α)) ⟹ (↑0 ∈ (^ β))
notation a  ⊆[:max A ] :0 b := subseteq A a b

def term_prod (A B : type) (α β : term) : term :=
{{ A 𝕏 B | ∃' A (∃' B ((↑1 ∈ α) ⋀ (↑0 ∈ β) ⋀ (↑2 ≃[A 𝕏 B] ⟪↑1,↑0⟫)))}}
-- notation α  𝕏[:max A,B ] :0 β := term_prod A B α β

section
variables p q r : term

#check p ⋀ (q ⋁ r)
#check ∃' 𝟙 (∀' 𝟙 (∀' (𝒫 𝟙) ((var 2) ∈ (var 0) ⇔ (var 1) ∈ (var 0))))
end

@[simp]
lemma subst.subseteq {x n α β A}: subst n x (α ⊆[A] β) = (subst n x α) ⊆[A] (subst n x β) :=
sorry

-- * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
section WellFormedness

open term
open list
local notation l₁ ++ l₂ := list.append l₁ l₂

def context := list type

variables {Γ Δ : context}
variables {p q r φ a b α : term}
variables {A B Ω' : type}

@[user_attribute]
meta def WF_rules : user_attribute :=
{ name := TT.WF_rules,
descr := "lemmas usable to prove Well Formedness" }

meta def tactic.interactive.WF_prover : tactic unit:= do [apply_rules WF_rules, any_goals {refl}]

inductive WF : context → type → term → Prop
| star {Γ}         : WF Γ 𝟙 ⁎
| top  {Γ}         : WF Γ Ω ⊤
| bot  {Γ}         : WF Γ Ω ⊥
| and  {Γ p q}     : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⋀ q)
| or   {Γ p q}     : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⋁ q)
| imp  {Γ p q}     : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⟹ q)
| elem {Γ A a α}   : WF Γ A a → WF Γ (𝒫 A) α → WF Γ Ω (a ∈ α)
| pair {Γ A B a b} : WF Γ A a → WF Γ B b → WF Γ (A 𝕏 B) ⟪a,b⟫
| var  {Γ A n}     : list.nth Γ n = some A → WF Γ A (var n)
| comp {Γ A φ}     : WF (A::Γ) Ω φ → WF Γ (𝒫 A) {{A | φ}}
| all  {Γ A φ}     : WF (A::Γ) Ω φ → WF Γ Ω (∀' A φ)
| ex   {Γ A φ}     : WF (A::Γ) Ω φ → WF Γ Ω (∃' A φ)

attribute [TT.WF_rules] WF.star WF.top WF.bot WF.and WF.or WF.imp WF.elem WF.pair WF.var WF.comp WF.all WF.ex

-- Ω' is just a fake/variable version of Ω so we don't need to bother proving
-- that it must be Ω itself.'

meta def WF_cases : tactic unit := do [intro h, cases h, assumption]

lemma WF.and_left   : WF Γ Ω' (p ⋀ q) → WF Γ Ω' p := by WF_cases
lemma WF.and_right  : WF Γ Ω' (p ⋀ q) → WF Γ Ω' q := by WF_cases
lemma WF.or_left    : WF Γ Ω' (p ⋁ q) → WF Γ Ω' p := by WF_cases
lemma WF.or_right   : WF Γ Ω' (p ⋁ q) → WF Γ Ω' q := by WF_cases
lemma WF.imp_left   : WF Γ Ω' (p ⟹ q) → WF Γ Ω' p := by WF_cases
lemma WF.imp_right  : WF Γ Ω' (p ⟹ q) → WF Γ Ω' q := by WF_cases
lemma WF.pair_left  : WF Γ (A 𝕏 B) ⟪a,b⟫ → WF Γ A a := by WF_cases
lemma WF.pair_right : WF Γ (A 𝕏 B) ⟪a,b⟫ → WF Γ B b := by WF_cases
lemma WF.comp_elim  : WF Γ (𝒫 A) {{A | φ}} → WF (A::Γ) Ω φ := by WF_cases
lemma WF.all_elim   : WF Γ Ω' (∀' A φ) → WF (A::Γ) Ω' φ := by WF_cases
lemma WF.ex_elim    : WF Γ Ω' (∃' A φ) → WF (A::Γ) Ω' φ := by WF_cases
@[TT.WF_rules] lemma WF.iff : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⇔ q) := by {intros, WF_prover}


#### Reid Barton (Jun 22 2020 at 14:10):

probably because you're in another namespace when you defined WF_prover?

#### Reid Barton (Jun 22 2020 at 14:10):

it's long and hard to tell

#### Reid Barton (Jun 22 2020 at 14:15):

that is, if you're inside namespace TT then def foo.bar defined TT.foo.bar

#### Kevin Buzzard (Jun 22 2020 at 14:18):

#where will tell you which namespace you're in at a given point in a file (and also what variables you have defined, what you have open...)

#### Billy Price (Jun 23 2020 at 12:08):

I'm failing to deconstruct the arguments to comp in this category definition - I think it's because the first 3 arguments are implicit in comp unlike in hom. The constants are there in place of actual things I've defined.

import category_theory.category

namespace category_theory

constant type : Type
constant tset : type → Type

constant graph {A B} (α : tset A) (β : tset B) : Type

constant id_graph {A} (α : tset A) : graph α α

constant composition {A B C} {α : tset A} {β : tset B} {η : tset C} (F : graph α β) (G : graph β η) : graph α η

instance category : small_category (Σ A : type, tset A) :=
{ hom := λ ⟨A,α⟩ ⟨B,β⟩, graph α β,
id := λ ⟨A,α⟩, id_graph α,
comp := λ ⟨A,α⟩ ⟨B,β⟩ ⟨C,η⟩ F G, composition F G,
id_comp' := sorry,
comp_id' := sorry,
assoc' := sorry
}

end category_theory


I thought it compile, even if I had underscores for the first three arguments - but I get this error.

type mismatch at application
composition F
term
F
has type
_x ⟶ _x_1
but is expected to have type
graph ?m_3 ?m_4


Evidently composition doesn't know that the hom-type is exactly the graph type it wants.

#### Reid Barton (Jun 23 2020 at 12:28):

You should write the instance this way:

instance category : small_category (Σ A : type, tset A) :=
{ hom := λ A B, graph A.2 B.2,
id := λ A, id_graph A.2,
comp := λ _ _ _ F G, composition F G,
id_comp' := sorry,
comp_id' := sorry,
assoc' := sorry
}


#### Reid Barton (Jun 23 2020 at 12:31):

In general, avoid λ ⟨A,α⟩ except for proofs

#### Billy Price (Jun 23 2020 at 12:33):

Cool thanks!

I would also like to know how to do deconstruction of terms in this way for hypotheses in a goal state. Something like this but for tactic mode?

variables (α : Type) (p q : α → Prop)

example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
match h with ⟨w, hw⟩ :=
⟨w, hw.right, hw.left⟩
end


#### Reid Barton (Jun 23 2020 at 12:36):

example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
begin
obtain ⟨w, hw₁, hw₂⟩ := h, -- or rcases h with ⟨w, hw₁, hw₂⟩,
exact ⟨w, hw₂, hw₁⟩
end


#### Billy Price (Jun 23 2020 at 12:40):

Ah awesome, does the r in rcases and rintros refer to the deconstruction of the hypothesis being vaguely recursive?

#### Reid Barton (Jun 23 2020 at 12:43):

Yes, rcases = "recursive cases"

#### Kenny Lau (Jun 23 2020 at 12:44):

rintro = “recursive intro”

#### Billy Price (Jun 23 2020 at 12:48):

Is it possible to print all definitions/lemmas using sorry?

#### Billy Price (Jun 26 2020 at 11:07):

Here's something interesting, the first of these is very easy to prove, but I don't know where to start on the second (I hope I'm not missing something obvious). I feel like perhaps I need to invoke classical reasoning, since I don't actually have anything to work with. I have a suspicion that it's just not true.

lemma ent_to_meta : entails Γ φ ψ  → entails Γ ⊤ φ → entails Γ ⊤ ψ :=
λ _ _, (by {apply entails.cut _ φ _, tidy})

lemma meta_to_ent (wfφ : WF Γ Ω φ) (wfψ : WF Γ Ω ψ) : (entails Γ ⊤ φ → entails Γ ⊤ ψ) → entails Γ φ ψ :=
begin
intro h,
sorry
end


#### Billy Price (Jun 26 2020 at 11:09):

Here's what entails is.

inductive entails : context → term → term → Prop
| axm        {Γ} {p}       : WF Γ Ω p → entails Γ p p
| vac        {Γ} {p}       : WF Γ Ω p → entails Γ p ⊤
| abs        {Γ} {p}       : WF Γ Ω p → entails Γ ⊥ p
| and_intro  {Γ} {p q r}   : entails Γ p q → entails Γ p r → entails Γ p (q ⋀ r)
| and_left   {Γ} (p q r)   : entails Γ p (q ⋀ r) → entails Γ p q
| and_right  {Γ} (p q r)   : entails Γ p (q ⋀ r) → entails Γ p r
| or_intro   {Γ} {p q r}   : entails Γ p r → entails Γ q r → entails Γ (p ⋁ q) r
| or_left    {Γ} (p q r)   : entails Γ (p ⋁ q) r → entails Γ p r
| or_right   {Γ} (p q r)   : entails Γ (p ⋁ q) r → entails Γ q r
| imp_to_and {Γ} {p q r}   : entails Γ p (q ⟹ r) → entails Γ (p ⋀ q) r
| and_to_imp {Γ} {p q r}   : entails Γ (p ⋀ q) r → entails Γ p (q ⟹ r)
| weakening  {Γ} {p q} (Δ) : entails Γ p q → entails (list.append Γ Δ) p q
| cut        {Γ} (p c q)   : entails Γ p c → entails Γ c q → entails Γ p q
| all_elim   {Γ} {p φ A}   : entails Γ p (∀[A] φ) → entails (A::Γ) (^ p) φ
| all_intro  {Γ} {p φ} (A) : entails (A::Γ) (^ p) φ → entails Γ p (∀[A] φ)
| ex_elim    {Γ} {p φ A}   : entails Γ p (∃[A] φ) → entails (A::Γ) (^ p) φ
| ex_intro   {Γ} {p φ} (A) : entails (A::Γ) (^ p) φ → entails Γ p (∃[A] φ)
| extensionality {A}       : entails [] ⊤ $∀[𝒫 A, 𝒫 A]$ (∀' A $(↑0 ∈ ↑2) ⇔ (↑0 ∈ ↑1)) ⟹ (↑1 ≃[𝒫 A] ↑0) | prop_ext : entails [] ⊤$ ∀[Ω,Ω] $(↑1 ⇔ ↑0) ⟹ (↑1 ≃[Ω] ↑0) | star_unique : entails [] ⊤$ ∀[𝟙] (↑0 ≃[𝟙] ⁎)
| pair_rep      {A B}      : entails [] ⊤ $∀[A 𝕏 B]$ ∃[A,B] $↑2 ≃[A 𝕏 B] ⟪↑1,↑0⟫ | pair_distinct {A B} : entails [] ⊤$ ∀[A,B,A,B] $(⟪↑3,↑2⟫ ≃[A 𝕏 B] ⟪↑1,↑0⟫) ⟹ ((↑3 ≃[A] ↑1) ⋀ (↑2 ≃[B] ↑0)) | sub {Γ} (B) (b p q) : WF Γ B b → entails (B::Γ) p q → entails Γ (⁅p // b⁆) (⁅q // b⁆) | comp {Γ} (A) (φ) : WF (A::Γ) Ω φ → entails Γ ⊤ (∀' A$ (↑0 ∈ (^ ⟦A | φ⟧)) ⇔ φ)


It's not true

#### Mario Carneiro (Jun 26 2020 at 11:37):

for example with phi = p, a variable of type Omega, and psi = ⊥, then the antecedent is true because entails [p:Ω] ⊤ p is false, but entails [p:Ω] ⊤ (p -> ⊥) is also false

#### Mario Carneiro (Jun 26 2020 at 11:39):

If you generalize the meta assumption to contexts extending Gamma then it is true

#### Mario Carneiro (Jun 26 2020 at 11:40):

because then you can just instantiate it with context (φ::Γ) to derive entails (φ::Γ) ⊤ ψ, after which you can use imp intro to derive entails Γ ⊤ (φ -> ψ)

#### Mario Carneiro (Jun 26 2020 at 11:41):

wait, where is your imp intro?

#### Mario Carneiro (Jun 26 2020 at 11:42):

I suppose you could generalize the ⊤ in the antecedent instead, but it's kind of trivial at that point using axm

#### Mario Carneiro (Jun 26 2020 at 11:43):

Oh I see, hypotheses don't go in the context like in DTT because this is a HOL like system

#### Billy Price (Jun 26 2020 at 11:43):

I think whatever you mean by imp intro is derivable. One of these?

lemma from_imp {Γ : context} : entails Γ ⊤ (q ⟹ r) → entails Γ q r :=
begin
intro h₁,
apply entails.cut _ (⊤ ⋀ q) _,
apply_rules [entails.and_intro, entails.vac, entails.axm];
{ apply @WF.imp_left _ q r,
exact WF.proof_right h₁
},
exact entails.imp_to_and h₁,
end

lemma to_imp {Γ : context} : entails Γ q r → entails Γ ⊤ (q ⟹ r) :=
begin
intro h₁,
apply_rules [entails.and_to_imp, entails.cut _ q _, entails.and_right _ ⊤ _, entails.axm],
WF_prover,
apply WF.proof_left h₁,
end


#### Mario Carneiro (Jun 26 2020 at 11:44):

So yeah you have to have the assumption \all p, entails Γ p φ → entails Γ p ψ at which point the theorem is trivial

#### Billy Price (Jun 26 2020 at 11:44):

Yeah this is from Lambek and Scott, Introduction to Higher Order Logic, (but really via these notes http://therisingsea.org/notes/ch2018-lecture9.pdf)

#### Billy Price (Jun 26 2020 at 11:47):

Ah that makes sense, it's strengthening the hypotheses to ensure that the function entails Γ p φ → entails Γ p ψ doesn't just just rely on entails Γ p φ being false.

#### Billy Price (Jul 01 2020 at 03:41):

@Jannis Limperg I switched to your induction branch by changing my mathlib rev and then I did leanproject get-mathlib-cache. Then when I tried to import tactic.induction, I get this message. invalid import: control.basic invalid object declaration, environment already has an object named 'simp_attr.functor_norm'

I then tried running leanpkg configure, after which I get this output. Any ideas? output.txt

#### Kevin Buzzard (Jul 01 2020 at 06:46):

I just delete _target and start again when I get into situations like this, but I'm afraid I am a luddite (a busy one).

#### Kevin Buzzard (Jul 01 2020 at 06:47):

Wait -- are you working on mathlib or in a repo with mathlib as a dependency?

the latter

#### Billy Price (Jul 01 2020 at 11:14):

Hmm - now when I redo leanpkg configure, I have a massive stream of warnings saying basically every file coming from mathlib uses sorry. My mathlib rev is this commit is https://github.com/leanprover-community/mathlib/commit/d05800077970a187c948f6e3e316aea2beac4e92

#### Johan Commelin (Jul 01 2020 at 11:14):

Do you use elan?

#### Johan Commelin (Jul 01 2020 at 11:15):

I suggest using leanproject instead of leanpkg

#### Billy Price (Jul 01 2020 at 11:18):

Ah okay - I thought they were different tools because leanproject configure isn't a command

#### Billy Price (Jul 01 2020 at 11:18):

What do I do instead of leanpkg configure with leanproject?

#### Billy Price (Jul 01 2020 at 11:24):

Just straight to leanproject build?

#### Billy Price (Jul 01 2020 at 11:27):

If I do so - I get the same errors. Namely lines like this

/Users/billy/gits/TL/_target/deps/mathlib/src/algebra/field.lean:173:6: error: invalid definition, a declaration named 'div_eq_one_iff_eq' has already been declared

and this

/Users/billy/gits/TL/_target/deps/mathlib/src/data/nat/pairing.lean:8:0: warning: imported file '/Users/billy/gits/TL/_target/deps/mathlib/src/tactic/doc_commands.lean' uses sorry

and this

/Users/billy/gits/TL/_target/deps/mathlib/src/data/list/intervals.lean:146:45: error: type mismatch at application lt_of_lt_of_le (mem.mp hk).right term (mem.mp hk).right has type k < m but is expected to have type ?m_3 < ?m_4

Is this a problem with the commit?

#### Billy Price (Jul 01 2020 at 11:30):

Okay I figured out how to retrieve the pre-compiled oleans with get-mathlib-cache, and now I'm back at my original problem. When I import tactic.induction, I get

invalid import: control.basic invalid object declaration, environment already has an object named 'simp_attr.functor_norm'Lean

#### Billy Price (Jul 01 2020 at 12:03):

Also src/tactic/induction.lean seems to be mostly commented out? Is this an unstable commit @Jannis Limperg ? Is there another commit I should be using?

#### Reid Barton (Jul 01 2020 at 13:40):

Make sure your project's leanpkg.toml file specifies the same version of Lean as the mathlib version you're using ("leanprover-community/lean:3.16.3")

#### Jannis Limperg (Jul 01 2020 at 14:00):

What Reid said. This recipe should work:

• Delete _target.
• Put in your leanpkg.toml:
• Mathlib commit: f5d662fd391b7aa737506a490da11fd7467c0934
• Lean version: leanprover-community/lean:3.16.5
• leanpkg configure
• leanproject get-mathlib-cache

The Lean update may require minor changes to your code.

#### Reid Barton (Jul 01 2020 at 14:02):

I didn't look through the history carefully enough to be confident that this is the issue, it's just something easy to mess up and easy to check.

#### Reid Barton (Jul 01 2020 at 14:03):

Aren't olean files versioned to a specific Lean release though? Or do we not always bump that?

#### Billy Price (Jul 02 2020 at 00:19):

Hmm I'm guessing I just had the wrong version of lean or something? Here's my current leanpkg.toml before making any changes

[package]
name = "TL"
version = "0.1"
lean_version = "leanprover-community/lean:3.9.0"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "d05800077970a187c948f6e3e316aea2beac4e92"}


#### Billy Price (Jul 02 2020 at 00:20):

Oh I just saw Reid's first reply

#### Billy Price (Jul 07 2020 at 03:26):

I have a lot of questions to ask, and a lot of them might be easiest to answer with a mwe. However many questions genuinely need my whole project (or at least 80% of it) to either compile or give context. What's the best way to go about this? It feels wrong to paste all my code in every post (especially since I now have multiple files). I have a git repo - though I'm not sure about committing half-cooked code every time I need to ask a question - (also the need for others to clone/copy/pull changes). Is there a better option than that or would using git be feasible? How do you guys work around this?

#### Alex J. Best (Jul 07 2020 at 03:39):

You could commit half cooked code to a different branch, then give people a oneliner to run with leanproject to get that branch on their computer like leanproject get githubname/repo:branch (or whatever the syntax is).

#### Billy Price (Jul 07 2020 at 03:48):

Thanks for the suggestion - I'll look into that.

(deleted)

#### Billy Price (Jul 09 2020 at 12:13):

The work-in-progress branch of my project can be grabbed here leanproject get https://github.com/billy-price/TL.git:WIP. Definitions and syntax are in src/definitions.lean - but most of it should be readable or just ask me. Stuff mentioned in this question are in src/entails.lean

The second half of the deduction rules and axioms of entailment in my type theory are quite unusable in their current state, so I'm trying to develop some more usable rules, for example I'm guessing I'd need something like this

lemma all_sub {A φ a} : WF (A :: Γ) Ω φ → entails (A::Γ) (^ (∀' A φ)) (φ⁅a⁆)

(the ^ means lift 1 0).

My guess is that would be much more usable than the current axioms relating to universal quantification, which are

| all_elim   {Γ} {p φ A}   : entails Γ p (∀' A φ) → entails (A::Γ) (^ p) φ
| all_intro  {Γ} {p φ} (A) : entails (A::Γ) (^ p) φ → entails Γ p (∀' A φ)
| sub      {Γ} {p q} (B b) : WF Γ B b → entails (B::Γ) p q → entails Γ (p⁅b⁆) (q⁅b⁆)


This is the proof so far,

begin
intro wf,
apply cut φ,
{ apply_rules [all_elim, axm], WF_prover },
{
sorry
}
end


I've managed to reduce it to this goal state, which seems closer to applying sub somewhere, but doesn't quite match

1 goal
Γ: context
A: type
φa: term
wf: WF (A :: Γ) Ω φ
⊢ entails (A :: Γ) φ φ⁅a//0⁆


It was possible to prove a slight variation of this here

lemma meta_all_sub {A φ a} : WF Γ A a → entails Γ ⊤ (∀' A φ) → entails Γ ⊤ (φ⁅a⁆) :=
begin
intros wfa ent_all,
have : (⊤ : term) =  ⊤⁅a⁆, by refl, rw this,
apply sub _ _ wfa,
have : (⊤ : term) = ^ ⊤, by refl, rw this,
exact all_elim ent_all
end


but I don't believe this is equivalent, I'd have to prove it for all hypotheses on both entailments, not just ⊤, which is just as difficult

#### Mario Carneiro (Jul 09 2020 at 12:18):

what's the theorem?

#### Billy Price (Jul 09 2020 at 12:18):

lemma all_sub {A φ a} : WF (A :: Γ) Ω φ → entails (A::Γ) (^ (∀' A φ)) (φ⁅a⁆)

#### Mario Carneiro (Jul 09 2020 at 12:20):

You need a to be well typed, right? Why not

lemma all_sub {A φ a} : WF Γ a A → WF (A :: Γ) Ω φ → entails Γ (∀' A φ) (φ⁅a⁆)


#### Billy Price (Jul 09 2020 at 12:20):

Yep that's an oversight

#### Mario Carneiro (Jul 09 2020 at 12:21):

It should be provable without induction

#### Billy Price (Jul 09 2020 at 12:24):

Do you agree that all_elim, all_intro, sub are the main relevant deduction rules or am I missing one?

#### Billy Price (Jul 09 2020 at 12:25):

(those are all entails.*)

#### Mario Carneiro (Jul 09 2020 at 12:25):

From all_elim and identity, you have (^ (all A ph)) -> ph, and from sub you get (^ (all A ph))[a] -> ph[a], which simplifies to (all A ph) -> ph[a]

#### Billy Price (Jul 09 2020 at 12:47):

Thank you, that seems like a general pattern to think about for other proofs. Here's my implementation - I kinda think the have line sucks. I'm finding myself going through a lot of effort to dress up my entailments to something that I can apply an entailment rule too. How do I make this easier?

lemma all_sub {A φ a} : WF Γ A a → WF (A :: Γ) Ω φ → entails (A::Γ) (^ (∀' A φ)) (φ⁅a⁆) :=
begin
intros wfa wfφ,
have : (^ (∀' A φ)) = (^ (∀' A φ))⁅a⁆, by sorry,
rw this,
refine sub _ _ wfa _,
refine all_elim _,
refine axm _,
WF_prover
end


#### Mario Carneiro (Jul 09 2020 at 22:51):

the have line should be (^ (∀' A φ))⁅a⁆ = (∀' A φ)

#### Mario Carneiro (Jul 09 2020 at 22:52):

which is a special case of the theorem (^ e)⁅a⁆ = e

#### Billy Price (Jul 10 2020 at 02:28):

I got the contexts wrong and that led me to the wrong equality, though isn't the theorem (^ e)⁅a⁆ = ^ e?

#### Mario Carneiro (Jul 10 2020 at 02:32):

No, p⁅a⁆ lives in context Γ if p is in context A :: Γ and a : A

#### Mario Carneiro (Jul 10 2020 at 02:33):

At least the way it's usually defined, substitution on de bruijn terms substitutes variable 0 and reduces all other variables by 1

#### Billy Price (Jul 10 2020 at 02:55):

Oh lol, I didn't define it like that and that might need some refactoring

#### Billy Price (Jul 10 2020 at 02:58):

In non-de bruijn world I would expect something like phi[x:=x] = phi, and that's clearly ruled out in de-bruijn world according to what you just said

#### Mario Carneiro (Jul 10 2020 at 04:02):

no, that's not a thing with de bruijn because the x:=x part is not well scoped

#### Mario Carneiro (Jul 10 2020 at 04:03):

the nearest equivalent is something like (lift phi 1 1)[0] = phi

#### Billy Price (Jul 10 2020 at 05:46):

Tada here's my proof (of an appropriate generalization), was scratching my head for a while wondering why I couldn't use add_sub (a b c) : a + (b-c) = a+b-c, it's not true for naturals!

@[simp]
lemma sub_lift {d k} {a b : term} {hd : d ≥ 1} : (lift d k a)⁅b // k⁆ = lift (d-1) k a :=
begin
induction' a; simp,
any_goals {tidy},
case var :
{ split_ifs; simp,
{ rw [if_neg, if_pos]; {linarith <|> {cases hd;refl}} },
{ rw if_neg, rw if_neg, linarith, linarith} }
end


#### Billy Price (Jul 10 2020 at 05:55):

is there a direct term or tactic equivalent to cases h with x, exact x? Assuming h has one possible case?

#### Billy Price (Jul 10 2020 at 05:55):

(Unrelated to the proof i just posted)

#### Mario Carneiro (Jul 10 2020 at 06:05):

Only if h is a structure

#### Kenny Lau (Jul 10 2020 at 06:06):

match h with | (foo x) := x end

#### Kenny Lau (Jul 10 2020 at 06:07):

let \<x\> := h in x

#### Mario Carneiro (Jul 10 2020 at 06:08):

Usually, if that proof works, it should be a structure field, in which case you can write foo.out h or the like

#### Mario Carneiro (Jul 10 2020 at 06:09):

However it's also possible that your h has a type with many constructors, and the others are being excluded for being impossible. In that case the match proof of Kenny's will work but the let will not and the field also will not

#### Billy Price (Jul 10 2020 at 06:39):

Thanks, it's the inductive WF type so I don't think this applies.

#### Billy Price (Jul 10 2020 at 06:55):

In light of the new substitution rule, does my axiom of comprehension still make sense?
| comp {Γ} (A) (φ) : WF (A::Γ) Ω φ → entails Γ ⊤ (∀' A $(↑0 ∈ (^ ⟦A | φ⟧)) ⇔ φ) I'm lifting the set in order to prevent Russell's paradox and the like, but then when I try and prove this lemma I run into trouble lemma elem_comp {H} {A φ a} : entails Γ H (a ∈ (^ (⟦A | φ⟧))) → entails Γ H (φ⁅a⁆) := begin intro ent_elem, apply cut _ ent_elem, apply from_imp, have : ((a ∈ ^ (⟦ A | φ ⟧)) ⟹ φ⁅a//0⁆) = ((↑0 ∈ ^ (⟦ A | φ ⟧)) ⟹ φ)⁅a⁆, simp, sorry, sorry end  the state before the first sorry is, in which the right conjunct isn't true. Γ: context H: term A: type φa: term ent_elem: entails Γ H (a ∈ lift 1 0 ⟦ A | φ ⟧) ⊢ a = ↑0⁅a//0⁆ ∧ lift 1 1 φ = φ  Do I just need to change comp to this? (lifting the last phi) | comp {Γ} (A) (φ) : WF (A::Γ) Ω φ → entails Γ ⊤ (∀' A$ (↑0 ∈ (^ ⟦A | φ⟧)) ⇔ (lift 1 1 φ))

or is there a better alternative?

#### Mario Carneiro (Jul 10 2020 at 18:49):

What does ⟦A | φ⟧ mean?

#### Mario Carneiro (Jul 10 2020 at 18:51):

oh I see it's your comprehension operator, i.e {x : A | φ}

#### Mario Carneiro (Jul 10 2020 at 18:53):

your elem_comp is missing WF assumptions again. I suggest you put them in because it makes it clearer where to put the lifts

#### Mario Carneiro (Jul 10 2020 at 18:55):

In this case a, A and live in context Γ and φ is in context A::Γ so a and ⟦A | φ⟧ live in the same context and no lifting is necessary

#### Billy Price (Jul 11 2020 at 04:29):

I did end up figuring that out! I was thinking I'd need to lift in order to match with the comprehension axiom, but that is taken care of by reducing all the higher indices during substitution!

I can actually pull the well-formedness of a and phi out of the hypothesis entails Γ H (a ∈ (^ ⟦A | φ⟧)), however I did put them in because I changed it to an if and only if lemma and you can't pull well-formedness out of the other entailment.

#### Billy Price (Jul 11 2020 at 04:52):

I've been doing a bunch of lemmas relating to compositions of lift and substitution operations, and it reminds me of order preserving maps. Specifically I've come across the simplex category of finite ordinals and order preserving maps, and I remember a theorem stating any order preserving map can be decomposed into a composition of these two classes of maps.
image.png

These are just like how lift 1 i and subst i (var i) act on de-bruijn indices/vars. lift and subst are defined like this

def lift (d : ℕ) : ℕ → term → term
| k ⁎          := ⁎
| k ⊤          := ⊤
| k ⊥          := ⊥
| k (p ⋀ q)    := (lift k p) ⋀ (lift k q)
| k (p ⋁ q)    := (lift k p) ⋁ (lift k q)
| k (p ⟹ q)   := (lift k p) ⟹ (lift k q)
| k (a ∈ α)    := (lift k a) ∈ (lift k α)
| k ⟪a,b⟫      := ⟪lift k a, lift k b⟫
| k (var m)    := if m≥k then var (m+d) else var m
| k ⟦A | φ⟧  :=   ⟦A | lift (k+1) φ⟧
| k (∀' A φ)   := ∀' A $lift (k+1) φ | k (∃' A φ) := ∃' A$ lift (k+1) φ

def subst : ℕ → term → term → term
| n x ⁎          := ⁎
| n x ⊤          := ⊤
| n x ⊥          := ⊥
| n x (p ⋀ q)    := (subst n x p) ⋀ (subst n x q)
| n x (p ⋁ q)    := (subst n x p) ⋁ (subst n x q)
| n x (p ⟹ q)  := (subst n x p) ⟹ (subst n x q)
| n x (a ∈ α)    := (subst n x a) ∈ (subst n x α)
| n x ⟪a,b⟫      := ⟪subst n x a, subst n x b⟫
| n x (var m)    := if n=m then x else (if m > n then var (m-1) else var m)
| n x ⟦ A | φ ⟧   := ⟦A | subst (n+1) (^ x) φ⟧
| n x (∀' A φ)   := ∀' A (subst (n+1) (^ x) φ)
| n x (∃' A φ)   := ∃' A (subst (n+1) (^ x) φ)


So far I've found it difficult to visualise compositions of lift and subst and come up with the right lemmas to prove, so maybe some practice in the theory of finite order-preserving maps will help. Is this a known connection?

#### Mario Carneiro (Jul 11 2020 at 05:27):

I believe that the semantics of type theories leads to the structure of contextual categories. If you simplify away the types, so that contexts are basically list unit (which is just nat), as in untyped (but well scoped) lambda calculus, then I think you can use the simplex category to represent the contexts.

#### Billy Price (Jul 11 2020 at 13:11):

Very interesting, thanks :)

#### Billy Price (Jul 12 2020 at 08:47):

I've proved @[simp] lemma sub_lift {d n k} {a b : term} {hd : d ≥ 1} {hn : n < d} : (lift d k a)⁅b // n+k⁆ = lift (d-1) k a and I'd like to show the following as a simple corollary, since simp won't recognise the first case when n is 0, @[simp] lemma sub_lift' {d k} {a b : term} {hd : d ≥ 1} : (lift d k a)⁅b // k⁆ = lift (d-1) k a

However I can't use rw <-zero_add k, since it will rewrite both k to 0+k, and I just want the second one to be 0+k.

#### Kevin Buzzard (Jul 12 2020 at 09:08):

Try the conv mode docs?

#### Kevin Buzzard (Jul 12 2020 at 09:09):

https://leanprover-community.github.io/extras/conv.html

#### Billy Price (Jul 29 2020 at 04:04):

I have a compactness theorem (for a different theory) that looks like this theorem compactness {X : set Form} {A : Form} : (X ⊢I A) → ∃ X' ⊆ X, X'.finite ∧ (X' ⊢I A), but the proof is entirely constructive. Am I correct in understanding that I won't be able to recover the finite set X' from the exists? I tried to change it to sigma in the hopes of making it recoverable, but it looks like the sigma type doesn't want the second thing to be a proposition?

#### Kenny Lau (Jul 29 2020 at 07:37):

constructive exists is called subtype ({ x // p x })

#### Kenny Lau (Jul 29 2020 at 07:38):

and I wouldn't call that theorem compactness?

#### Billy Price (Jul 30 2020 at 07:37):

I'm not quite sure how to utilise subtype in my situation I have the following types/props

inductive deduction : set Form → Form → Type

inductive provable (X : set Form) (A : Form) : Prop
| mk : deduction X A → provable


There's are the three potential subtypes I thought of, but it's not clear how to state the theorem using them, since there's no subset constraint.

def fin_deduction (X : set Form) (A : Form) : Type := { d : deduction X A // X.finite }

inductive fin_provable (X : set Form) (A : Form) : Prop
| mk : fin_deduction X A → fin_provable

inductive fin_provable' (X : set Form) (A : Form) : Prop
| mk : provable X A → X.finite → fin_provable'


Also the comment about the name compactness, is that just because compactness is about models, not provability? I'm just formalising the natural deduction section of the class I'm taking, and this theorem appeared in the textbook.

#### Kenny Lau (Jul 30 2020 at 07:39):

the thing is, you can't go from Prop to data

#### Kenny Lau (Jul 30 2020 at 07:39):

so from a deduction you can produce a finite set Form

#### Kenny Lau (Jul 30 2020 at 07:39):

but once you go to provable, you can't go back to data

#### Kenny Lau (Jul 30 2020 at 07:41):

so you can produce:

def axioms_used : deduction X A → { X' : set Form // X'.finite }


#### Kenny Lau (Jul 30 2020 at 07:42):

of course, the actual signature depends on your implementation and usage etc

#### Kenny Lau (Jul 30 2020 at 07:42):

for example you might want to generalize A, i.e. put A after the colon

#### Kenny Lau (Jul 30 2020 at 07:43):

def extract_axioms : Π {A : Form}, deduction X A → { X' : set Form // X'.finite ∧ X' ⊆ X ∧ deduction X' A }


#### Kenny Lau (Jul 30 2020 at 07:44):

why not use finset?

#### Mario Carneiro (Jul 30 2020 at 09:27):

You can probably define a function from deduction X A to { X' : finset Form // X' \sub X }, based on my guess of how deduction is defined

#### Mario Carneiro (Jul 30 2020 at 09:28):

And therefore you can also go from provable X A to \ex X' : finset Form, X' \sub X

#### Billy Price (Jul 30 2020 at 12:43):

I didn't use finset because subset doesn't seem to work between finset and set. Also could you explain what putting the A after the colon does? Why does that generalise it?

#### Mario Carneiro (Jul 30 2020 at 13:09):

You can cast the finset to a set

#### Mario Carneiro (Jul 30 2020 at 13:11):

@Billy Price I think Kenny means that if you put the A after the colon then in the recursive definition you can change A

#### Billy Price (Jul 30 2020 at 13:25):

I see, not sure if I need that but maybe

#### Billy Price (Jul 30 2020 at 13:25):

What does this error mean? The line that triggered it is use XA' ∪ XB'

failed to instantiate goal with (frozen_name has_union.union) XA' XB'
state:
X : set Form,
A B : Form,
dXA : X ≻ A,
dXB : X ≻ B,
XA' : finset Form,
AsubX : ↑XA' ⊆ X,
XA'A : ↑XA' ⊢I A,
XB' : finset Form,
BsubX : ↑XB' ⊆ X,
XB'B : ↑XB' ⊢I B
⊢ {X' // ↑X' ⊆ X ∧ ↑X' ⊢I A ⋀ B}


#### Mario Carneiro (Jul 30 2020 at 13:31):

try existsi`