# Zulip Chat Archive

## 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`

?

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

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 `term`

s 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`

?

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

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

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

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.

#### 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):

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

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

Oh you change the name too

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

By the way, I noticed earlier that the interactive parser for `apply_rules`

is a little weird--it expects an identifier, but it doesn't actually use it as an identifier, it uses it as an attribute name.

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

It gets weird if the attribute name is not the same as the identifier that introduces the attribute itself.

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

Yes, sorry. I literally meant "in the string `meta def WF_rules`

"

#### Billy Price (Jun 10 2020 at 12:30):

I'm now trying to prove you can lift all the variables in a term up by 1 and shove a new type at the start of the context, but it's unclear how to prove it in the quantified cases (WF.all, WF.ex, WF.comp), It looks like I need to do more induction - but doesn't that produce the same problem again?

```
@[TT.WF_rules] lemma WF.lift : WF Γ A a → WF (B::Γ) A (lift a) :=
begin
intro wfa,
induction wfa,
case WF.all : Δ A ψ wfψ ih {simp, apply_rules WF_rules, sorry},
case WF.ex : Δ A ψ wfψ ih {simp, apply_rules WF_rules, sorry},
case WF.comp : Δ A ψ wfψ ih {simp, apply_rules WF_rules, sorry},
all_goals {unfold lift, unfold lift_d, apply_rules WF_rules},
end
```

Here's the state at the first `sorry`

.

```
1 goal
B : type,
Γ : context,
A : type,
a : term,
Δ : list type,
A : type,
ψ : term,
wfψ : WF (A :: Δ) Ω ψ,
ih : WF (B :: A :: Δ) Ω (lift ψ)
⊢ WF (A :: B :: Δ) Ω (lift_d 1 1 ψ)
```

#### Mario Carneiro (Jun 10 2020 at 12:31):

That's right, this is why `lift`

is not good enough

#### Mario Carneiro (Jun 10 2020 at 12:31):

you have to prove the analogous theorem for `lift_d`

#### Billy Price (Jun 10 2020 at 12:34):

Hmm okay, so prepending some list of types of length `d`

in the `lift_d d`

case?

#### Mario Carneiro (Jun 10 2020 at 12:34):

Since you are holding `d`

fixed in the definition of `lift_d`

, you can probably prove it in the special case `d = 1`

#### Mario Carneiro (Jun 10 2020 at 12:35):

but you definitely have to generalize `k`

#### Mario Carneiro (Jun 10 2020 at 12:35):

Then again, the general theorem is not much harder and may come in useful

#### Billy Price (Jun 10 2020 at 12:37):

Ah okay, so splitting the original context at the `k`

th position and shoving `d`

variables in there.

#### Mario Carneiro (Jun 10 2020 at 12:39):

I think it looks something like this:

```
lemma WF.lift_d : ∀ K D Γ A a, length K = k → length D = d → WF (K ++ Γ) (A) a → WF (K ++ D ++ Γ) A (lift_d d k a) :=
sorry
```

#### Mario Carneiro (Jun 10 2020 at 12:40):

since you aren't inducting on `k`

or `d`

you can also simplify this to

```
lemma WF.lift_d : ∀ K D Γ A a, WF (K ++ Γ) (A) a → WF (K ++ D ++ Γ) A (lift_d (length D) (length K) a) :=
sorry
```

#### Billy Price (Jun 10 2020 at 12:45):

Yep that makes sense to me

#### Billy Price (Jun 10 2020 at 12:53):

This state looks equally difficult to solve - am I missing something?

```
1 goal
K Δ Γ : context,
A : type,
a : term,
Δ : list type,
B : type,
ψ : term,
wfψ : WF (B :: Δ) Ω ψ,
ih : WF (K ++ Δ ++ Γ) Ω (lift_d (length Δ) (length K) ψ)
⊢ WF (B :: (K ++ Δ ++ Γ)) Ω (lift_d (length Δ) (length K + 1) ψ)
```

#### Mario Carneiro (Jun 10 2020 at 12:54):

How did you start the proof?

#### Mario Carneiro (Jun 10 2020 at 12:54):

You need `generalizing K`

at least

#### Billy Price (Jun 10 2020 at 12:54):

```
@[TT.WF_rules] lemma WF.lift_d (K Δ Γ : context) : WF (K ++ Γ) A a → WF (K ++ Δ ++ Γ) A (lift_d (length Δ) (length K) a) :=
begin
intro wfa,
induction wfa,
case WF.all : Δ B ψ wfψ ih {apply WF.all,sorry},
case WF.ex : Δ B ψ wfψ ih {apply WF.ex, sorry},
case WF.comp : Δ B ψ wfψ ih {apply WF.comp, sorry},
any_goals {unfold lift_d, apply_rules WF_rules},
end
```

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

You also need to generalize `generalize e : K ++ Γ = Γ'`

before the induction

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

You should also be able to use `constructor`

instead of `apply_rules`

for an inductive proof like this

#### Billy Price (Jun 10 2020 at 12:58):

I don't understand what generalizing K does? What does more general mean here?

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

`K`

needs to be forall-quantified in the inductive hypothesis

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

That was the problem with your stuck goal, if `K`

was generalized in `ih`

then you could have instantiated `K`

to `B :: K`

#### Mario Carneiro (Jun 10 2020 at 13:01):

Another way to put it is, we expect that `K`

will change over the course of the induction, while `Δ`

and `Γ`

for instance don't need to change

#### Mario Carneiro (Jun 10 2020 at 13:01):

`A`

and `a`

also need to change over the induction but since they are indices to the inductive family this is automatic and you don't need to specify `generalizing A a`

#### Billy Price (Jun 10 2020 at 13:03):

That makes so much sense thank you. I've seen "indices" before - what does it mean to be an index to an inductive family?

#### Mario Carneiro (Jun 10 2020 at 13:03):

right of the colon in the `inductive`

statement

#### Mario Carneiro (Jun 10 2020 at 13:04):

In `WF`

there are no parameters (left of the colon) and three indices

#### Billy Price (Jun 10 2020 at 13:05):

yep, context, type and term?

#### Mario Carneiro (Jun 10 2020 at 13:05):

right

#### Billy Price (Jun 10 2020 at 13:06):

K appears in the context of `wfa`

- why does that not automatically generalise?

#### Billy Price (Jun 10 2020 at 13:07):

Because the context is an append of two contexts?

#### Billy Price (Jun 10 2020 at 13:07):

So it can't do it?

#### Mario Carneiro (Jun 10 2020 at 13:08):

If you leave a composed expression in an index when you do `induction`

, it will silently generalize it, losing the connection to the original expression

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

That is, it tries to prove `WF Γ' A a → WF (K ++ Δ ++ Γ) A (lift_d (length Δ) (length K) a)`

, which won't be provable because `K`

is gone from the left side

#### Mario Carneiro (Jun 10 2020 at 13:10):

If you do `generalize e : K ++ Γ = Γ'`

then it is instead proving `WF Γ' A a → \forall K, K ++ Γ = Γ' -> WF (K ++ Δ ++ Γ) A (lift_d (length Δ) (length K) a)`

which is okay

#### Mario Carneiro (Jun 10 2020 at 13:11):

(technically indices aren't generalized in the sense of `generalizing`

, they are handled specially because they participate directly in the statement of the recursor)

#### Billy Price (Jun 10 2020 at 13:16):

Hmm, I'm not sure if this is the right setup. Also what's the reason for the duplicate K's and A's (which I've rename with apostrophe's).

```
@[TT.WF_rules] lemma WF.lift_d (K Δ Γ : context) : WF (K ++ Γ) A a → WF (K ++ Δ ++ Γ) A (lift_d (length Δ) (length K) a) :=
begin
intro wfa,
generalize e : K ++ Γ = Γ',
induction wfa generalizing K,
case WF.all : K' A' ψ wfψ ih {constructor, sorry},
case WF.ex : K' A' ψ wfψ ih {constructor, sorry},
case WF.comp : K' A' ψ wfψ ih {constructor, sorry},
any_goals {unfold lift_d, apply_rules WF_rules},
end
```

this is my state for the first sorry

```
1 goal
Δ Γ : context,
Γ' : list type,
A : type,
a : term,
K : context,
K' : list type,
e : K' = Γ',
A' : type,
ψ : term,
wfψ : WF (A' :: K') Ω ψ,
ih : A' :: K' = Γ' → ∀ (K : context), WF (K ++ Δ ++ Γ) Ω (lift_d (length Δ) (length K) ψ)
⊢ WF (A' :: (K ++ Δ ++ Γ)) Ω (lift_d (length Δ) (length K + 1) ψ)
```

#### Billy Price (Jun 10 2020 at 13:17):

I think I should have `length K'`

appearing in `ih`

, not `length K`

#### Mario Carneiro (Jun 10 2020 at 13:19):

You can simplify this by eliminating the equality immediately using `induction wfa generalizing K; subst e,`

#### Mario Carneiro (Jun 10 2020 at 13:20):

`K'`

is just `Γ'`

#### Mario Carneiro (Jun 10 2020 at 13:21):

but that inductive hypothesis does look like bad news

#### Billy Price (Jun 10 2020 at 13:21):

Oh right I got the renaming wrong.

#### Mario Carneiro (Jun 10 2020 at 13:21):

what is the state before `induction`

#### Mario Carneiro (Jun 10 2020 at 13:23):

Ah, I think I know what happened; `wfa`

is in the context so `generalize`

won't hit it and it is useless (it just adds a useless equality to the context)

#### Mario Carneiro (Jun 10 2020 at 13:23):

Use `generalize_hyp e : K ++ Γ = Γ' at wfa,`

#### Mario Carneiro (Jun 10 2020 at 13:24):

the idea here is that immediately before the induction `wfa`

should have variables in all the indices, no composed expressions

#### Billy Price (Jun 10 2020 at 13:24):

Yep that makes sense

#### Billy Price (Jun 10 2020 at 13:29):

Now we're here

```
@[TT.WF_rules] lemma WF.lift_d (K Δ Γ : context) : WF (K ++ Γ) A a → WF (K ++ Δ ++ Γ) A (lift_d (length Δ) (length K) a) :=
begin
intro wfa,
generalize_hyp e : K ++ Γ = Γ' at wfa,
induction wfa generalizing K,
case WF.all : Γ' A' ψ wfψ ih {subst e, constructor,},
case WF.ex : Γ' A' ψ wfψ ih {constructor, sorry},
case WF.comp : Γ' A' ψ wfψ ih {constructor, sorry},
any_goals {unfold lift_d, apply_rules WF_rules},
end
```

```
1 goal
Δ Γ : context,
Γ' : list type,
A : type,
a : term,
K : context,
A' : type,
ψ : term,
wfψ : WF (A' :: (K ++ Γ)) Ω ψ,
ih : ∀ (K_1 : context), K_1 ++ Γ = A' :: (K ++ Γ) → WF (K_1 ++ Δ ++ Γ) Ω (lift_d (length Δ) (length K_1) ψ)
⊢ WF (A' :: (K ++ Δ ++ Γ)) Ω (lift_d (length Δ) (length K + 1) ψ)
```

#### Billy Price (Jun 10 2020 at 13:30):

That's the state after `constructor,`

. I put the `subst e`

, inside the case because applying it do all the inductive cases via `induction wfa generalizing K; subst e`

anonymised the goals so I couldn't name a case anymore.

#### Billy Price (Jun 10 2020 at 13:33):

The hypothesis seems good to me - is it just failing to see how to unify the lists because of associativity or something? This is what I get when I try to `apply ih`

```
invalid apply tactic, failed to unify
WF (A' :: (K ++ Δ ++ Γ)) Ω (lift_d (length Δ) (length K + 1) ψ)
with
WF (?m_1 ++ Δ ++ Γ) Ω (lift_d (length Δ) (length ?m_1) ψ)
```

#### Mario Carneiro (Jun 10 2020 at 13:39):

you have to explicitly specify `ih (A' :: K)`

, but it looks defeq modulo that

#### Mario Carneiro (Jun 10 2020 at 13:41):

(you should get out of the habit of using `apply`

; `refine`

and `exact`

are better because they have the expected type)

#### Billy Price (Jun 10 2020 at 13:47):

oh okay, I was aware of `exact`

but not `refine`

. Though reading it now I don't quite see the importance - what do you mean by "they have the expected type"?

#### Mario Carneiro (Jun 10 2020 at 13:48):

whaaat `refine`

is the best tactic

#### Mario Carneiro (Jun 10 2020 at 13:48):

the argument of `refine e`

or `exact e`

is typechecked using the goal as the target type

#### Mario Carneiro (Jun 10 2020 at 13:49):

the argument of `apply e`

is typechecked with no expected type, and then the result is unified against the target type after counting the number of pis to eliminate

#### Billy Price (Jun 10 2020 at 13:52):

Is there a minimal situation in which that makes a difference?

#### Mario Carneiro (Jun 10 2020 at 13:52):

anything using structure constructor brackets for example

#### Mario Carneiro (Jun 10 2020 at 13:54):

```
example : true ∧ true ∧ true :=
begin
refine ⟨⟨⟩, _⟩, -- works
exact ⟨⟨⟩, ⟨⟩⟩, -- works
end
example : true ∧ true ∧ true :=
begin
apply ⟨⟨⟩, _⟩, -- invalid constructor ⟨...⟩, expected type must be known
end
```

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

refine is great for compact and powerful combinations of `existsi`

, `intro`

and simple proof terms like `refine ⟨x, easy_lemma, λ t, _⟩,`

#### Billy Price (Jun 10 2020 at 13:56):

Ah I see, I think you mean `exact ⟨⟨⟩, ⟨⟩,⟨⟩⟩`

though

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

no, I wrote what I meant

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

that is, `apply`

isn't replacing `refine`

in this example

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

of course you can also try to give the whole proof term at once as well, making `apply`

act like `exact`

#### Mario Carneiro (Jun 10 2020 at 13:58):

and it would still fail

#### Billy Price (Jun 10 2020 at 13:58):

Oh sorry I interpreted it wrong

#### Billy Price (Jun 10 2020 at 14:01):

Can I undo the generalizing of `K`

to simplify my other inductive cases?

#### Mario Carneiro (Jun 10 2020 at 14:02):

You can use `exact ih K`

#### Mario Carneiro (Jun 10 2020 at 14:02):

or `apply ih`

if it works

#### Mario Carneiro (Jun 10 2020 at 14:03):

You could use `specialize ih K`

but it's probably not worth the characters it takes to say

#### Billy Price (Jun 10 2020 at 14:03):

Some of them have multiple inductive hypotheses

#### Mario Carneiro (Jun 10 2020 at 14:04):

I would do something like `iterate 4 { constructor, exact ih_1 K, exact ih_2 K }`

#### Mario Carneiro (Jun 10 2020 at 14:05):

or `try { ... }`

#### Mario Carneiro (Jun 10 2020 at 14:05):

probably some higher level thing like `solve_by_elim`

works too

#### Billy Price (Jun 10 2020 at 14:07):

But how would I name the inductive hypotheses like that?

#### Billy Price (Jun 10 2020 at 14:07):

They all have gross names and I need to open a single case to name them

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

I'm now proving an equality using `list.nth`

, and I want to use theorems that talk about `list.nth_le`

. I haven't seen any theorems converting between the two.

#### Billy Price (Jun 10 2020 at 14:53):

I'll try write one myself but just wondering if it's already there somewhere (I couldn't find it)

#### Kevin Buzzard (Jun 10 2020 at 15:02):

An MSc student of mine found a lot of missing lemmas about `nth`

and `nth_le`

. Her repo is now public so maybe there is some stuff here https://github.com/ImperialCollegeLondon/dots_and_boxes/tree/master/src/list/lemmas which is of some use. Note that the repo uses Lean 3.4.2.

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

There is one key theorem called something like `nth_le_nth`

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

^ that

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

also `nth_eq_some`

#### Kevin Buzzard (Jun 10 2020 at 15:09):

My student needed some `nth_le_append`

lemmas

#### Kevin Buzzard (Jun 10 2020 at 15:10):

We never managed to formalise what `nth_le_bind`

was but fortunately we were only glueing two lists together at that point

#### Mario Carneiro (Jun 10 2020 at 15:10):

I see `nth_le_append`

and `nth_le_append_right`

#### Mario Carneiro (Jun 10 2020 at 15:11):

I wouldn't bother with `nth_le_bind`

, the expression is not any better than what you get by induction

#### Kevin Buzzard (Jun 10 2020 at 15:12):

They weren't in mathlib when the project started, and the student never bothered keeping up to date with mathlib

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

Thanks for the help, I'm gonna bookmark that proof for now. I have a thing called `tset : type -> Type`

, so if `A : type`

, then `tset A`

is basically a closed term of type `PA`

, and I'd like to form a category of all such tsets of all types. But if I say `instance category : small_category (Π A : type, tset A)`

are the objects in that category elements of Type `tset A`

for some `A`

, or are they indexed families of tsets, which are indexed by the elements of `type`

?

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

I understand that I need to actually define the structure of that category, but I'm just trying to get the Type right for now

#### Billy Price (Jun 11 2020 at 08:05):

To strip away all the unnecessary context here, if I have

```
def foo: Type
def bar : ℕ -> foo
def baz := Π n : ℕ, bar n
```

what *is* an `f : baz`

? Is it an indexed family of `foo`

's (via `bar`

) or is it a `bar n : foo`

for some `n`

? What is the type of all `bar n`

for any `n`

? My best idea is a subtype of `foo`

where any `a`

in the subtype has `∃ n : ℕ, bar n == a`

, but that seems too implicit. I'd like to say maybe pairs of the form `<n,bar n>`

?

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

I think I just figured out that this is what the sigma construction is for lol.

#### David Wärn (Jun 11 2020 at 08:16):

An element of `\Sigma A : type, tset A`

would be a "pointed type" - - are these really the objects you want for your category?

#### David Wärn (Jun 11 2020 at 08:17):

In `category C`

, C is just the type of "abstract objects". An element of C does not need to have any internal structure - - it is just a label. Maybe here you want C to be just `type`

? Then you can define Hom-sets however you like

#### Kevin Buzzard (Jun 11 2020 at 08:35):

@Billy Price what you wrote about bar doesn't typecheck.

#### Kevin Buzzard (Jun 11 2020 at 08:36):

`baz`

doesn't make sense. It looks like it's going to be a function which eats a natural `n`

and returns a term of type `bar n`

, but `bar n`

isn't a type.

#### Kevin Buzzard (Jun 11 2020 at 08:37):

```
def foo: Type := sorry
def bar : ℕ -> foo := sorry
def baz := Π n : ℕ, bar n -- error -- type expected at bar n
```

#### Billy Price (Jun 11 2020 at 08:42):

David Wärn said:

An element of

`\Sigma A : type, tset A`

would be a "pointed type" - - are these really the objects you want for your category?

Yep, I'm not forming the typical category of types. Closer to the category of sets. My objects are terms `α : term`

such that `WF [] (P A) α`

, that is, `α`

is a well-formed term in the empty context (it's closed) "of type (P A)", where `P: type -> type`

is thought of as the powerset of a type. My morphisms are terms which look like the graph of a function between two such "subsets of a type".

@Kevin Buzzard I must have confused myself in translating to that example. I might reattempt, but I think `Σ A : type, tset A`

is what I was looking for, where `tset`

is defined like this

```
def tset (A: type) := {α : term // WF [] (𝒫 A) α}
```

The related definitions to what I'm doing appear here

https://leanprover.zulipchat.com/#narrow/stream/236446-Type-theory/topic/Modelling.20a.20Type.20Theory.20in.20Lean/near/200405009

#### Kevin Buzzard (Jun 11 2020 at 08:44):

Pi's are types of dependent functions and Sigma's are types of dependent pairs

#### Billy Price (Jun 11 2020 at 08:54):

I actually want to form equivalence classes of "provably equal" such terms, but it's becoming difficult to prove the lifting properties, so I'm just ignoring that for now. It definitely doesn't form a category without doing this, since associativity will never hold (composition produces ugly terms which are "provably equal" to simpler terms). Btw, "Provably equal" is its own thing my type theory.

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

How come `cases`

recognises whenever a constructor couldn't possibly produce the target, but `induction`

doesn't? I always end up with absurd cases to prove with induction.

#### Mario Carneiro (Jun 11 2020 at 11:27):

because properties if the input may not hold of the inductive subcases

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

But shouldn't the result of those constructors fail to unify with the target?

#### Mario Carneiro (Jun 11 2020 at 11:31):

If `induction`

used the same motive as `cases`

, the inductive hypothesis would be guaranteed useless

#### Mario Carneiro (Jun 11 2020 at 11:31):

the point is that just because you are inducting on `foo (C1 t)`

, doesn't mean that every subterm of `C1 t`

is also of the form `C1 t`

#### Mario Carneiro (Jun 11 2020 at 11:32):

so although you may be able to eliminate case `C2`

at the top level, when you go around the recursion once you won't be able to skip the `C2`

case anymore

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

Hmm lemme make a simple example that I don't understand

#### Mario Carneiro (Jun 11 2020 at 11:34):

If you want to explicitly say that an index is fixed, for example you are proving something about terms in the empty context and don't mind that the inductive hypothesis of `WF.all`

doesn't apply, then you can explicitly generalize it before and eliminate it after using `generalize_hyp e : Gamma = [] at wf, induction wf; cases e,`

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

Oh okay I do have more questions about what's going on here in this example so I'll paste it anyway

```
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 `𝟘` := 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
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
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 φ)
example {p q} : WF [] Ω (p ⋀ q) → WF [] Ω p :=
begin
intro wf,
induction wf,
end
```

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

The recent `generalizes`

tactic by @Jannis Limperg should help with this in the dependent case. I believe that is part of a larger induction tactic but that hasn't been merged AFAIK

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

Firstly, why does the variable `wf`

become a context in the states?

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

that's just a `cases`

proof

#### Mario Carneiro (Jun 11 2020 at 11:38):

no need for induction

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

Yeah I know I've done this proof before, it's just a simpler example for me to understand

#### Mario Carneiro (Jun 11 2020 at 11:38):

Firstly, why does the variable wf become a context in the states?

The induction variables need names, and these names are derived from the input variable when possible

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

If you at all care, or if you need to refer to the variables, you should use `induction with`

or `case`

to name the variables

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

Does it get the same name because there's only one inductive variable, hence no need for the `wf_`

form variables?

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

yes

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

Here's how you can prove that theorem using `induction`

instead of `cases`

:

```
example {p q} : WF [] Ω (p ⋀ q) → WF [] Ω p :=
begin
generalize e1 : [] = Γ,
generalize e2 : p ⋀ q = a,
intro wf,
induction wf; cases e1; cases e2,
assumption
end
```

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

Note that this process of generalizing and casing on the equality cuts down on the cases to prove, but does so at the cost of making the induction hypotheses useless:

```
...
wf_ih_a : list.nil = list.nil → p ⋀ q = p → WF list.nil Ω p,
wf_ih_a_1 : list.nil = list.nil → p ⋀ q = q → WF list.nil Ω p,
```

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

I don't quite see what ties the `[]`

or the `Γ`

in `e1`

to anything that appears in the inductive state.

#### Mario Carneiro (Jun 11 2020 at 11:45):

this is why `cases`

and `induction`

use different default motives even though they both boil down to an application of the recursor. In `cases`

you are saying explicitly that you don't care about induction hypotheses so we can add as many assumptions as we like to the induction motive to say that we are only inducting on something equal to the input, and so kill all the unnecessary cases. In `induction`

we want to generalize the induction hypothesis so we just suck in all assumptions from the context and generalize arguments as specified by `generalizing`

#### Mario Carneiro (Jun 11 2020 at 11:46):

What we are doing is proving `WF Γ Ω a → ([] = Γ → p ⋀ q = a → WF Γ Ω p)`

by induction

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

How are the Gammas the same Gamma in both appearances there?

#### Mario Carneiro (Jun 11 2020 at 11:47):

that is, the motive is `λ Γ A a, [] = Γ → p ⋀ q = a → WF Γ A p`

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

Oh is it because `generalize e1 : [] = Γ`

looks at the target and looks for instances of `[]`

?

#### Mario Carneiro (Jun 11 2020 at 11:49):

Remember what the recursor says. You are proving that `\forall Γ A a, WF Γ A a -> C Γ A a`

and this is how we are picking `C`

#### Mario Carneiro (Jun 11 2020 at 11:49):

Yes, `generalize`

automatically replaces instances of `[]`

with `Γ`

#### Mario Carneiro (Jun 11 2020 at 11:50):

You can also state this explicitly, which I do sometimes when getting the exact induction hypothesis right is more difficult

#### Mario Carneiro (Jun 11 2020 at 11:52):

```
example {p q} : WF [] Ω (p ⋀ q) → WF [] Ω p :=
begin
suffices : ∀ Γ A a, WF Γ A a → p ⋀ q = a → WF Γ A p,
{ exact λ wf, this _ _ _ wf rfl },
intros Γ A a wf,
induction wf; rintro ⟨⟩,
assumption
end
```

#### Mario Carneiro (Jun 11 2020 at 11:53):

this is the most general and powerful form of induction since you can state the induction hypothesis however you wish

#### Mario Carneiro (Jun 11 2020 at 11:58):

For example in my recent proof tm_to_partrec.lean if you search for `induction`

you will find a significant fraction of them are preceded by a `suffices`

, for example in src#turing.partrec_to_TM2.succ_ok

#### Mario Carneiro (Jun 11 2020 at 11:59):

Here's another good example

#### Mario Carneiro (Jun 11 2020 at 12:02):

the `∀ a b, a + b = n → ...`

is hard for lean to guess automatically. (Without going into details, we are proving a fact about `P n 0`

by induction given `P 0 n`

and `P a b -> P (a+1) (b-1)`

.)

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

Cool that looks like a useful practice.

#### Billy Price (Jun 11 2020 at 12:16):

This bottom lemma is what I'm actually trying to prove - I should be able to prove all cases at once, but there's an "list.nil = list.nil ->" in front of all of my inductive hypotheses - can I eliminate them all in one go?

```
import tactic.interactive
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 `𝟘` := 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
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
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 φ)
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
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 | φ⟧)) ⇔ φ)
```

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

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?

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

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.

#### Billy Price (Jul 09 2020 at 11:58):

(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`