Modelling a Type Theory in Lean

Stream: Type theory

[Billy Price]

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]

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]

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]

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]

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]

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]

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

[Billy Price]

Sorry what step are you referring to?

[Mario Carneiro]

step in the construction

[Mario Carneiro]

I would separate the grammar from the syntax rules

[Jannis Limperg]

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]

Lean's support for indexed families is fine

[Mario Carneiro]

mutual is not fine

[Mario Carneiro]

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]

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]

@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]

@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]

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

[Billy Price]

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

[Billy Price]

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]

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

[Billy Price]

Ah yes

[Reid Barton]

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]

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

[Anton Lorenzen]

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]

Awesome! thanks I'll take a look

[Billy Price]

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

[Reid Barton]

More specifically?

[Reid Barton]

What is the English translation of what you wrote?

[Billy Price]

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]

Hang on let me paste my term definition

[Billy Price]

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

[Billy Price]

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]

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

[Billy Price]

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]

Inductively defined propositions:

1. TPIL
2. Codewars: Multiples of 3, you say?
3. Codewars: Times Three, Plus Five

[Billy Price]

@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]

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

[Kenny Lau]

yes, but inductive might be better for this case

[Billy Price]

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]

it allows you to "inject" things

[Kenny Lau]

and you don't need to go through every case

[Kenny Lau]

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

[Mario Carneiro]

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]

Beautiful, thank you.

[Billy Price]

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]

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]

Kenny Lau said:

Inductively defined propositions:

1. TPIL
2. Codewars: Multiples of 3, you say?
3. Codewars: Times Three, Plus Five

[Jannis Limperg]

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]

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

[Billy Price]

@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]

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]

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

[Billy Price]

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

[Reid Barton]

Basically, yes

[Reid Barton]

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

[Reid Barton]

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]

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]

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

[Reid Barton]

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

[Billy Price]

Good point

[Billy Price]

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]

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]

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]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Billy Price]

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

[Mario Carneiro]

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

[Mario Carneiro]

that one gives you a de bruijn index

[Billy Price]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Billy Price]

defeq meaning definitional equality?

[Mario Carneiro]

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]

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

[Billy Price]

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

[Mario Carneiro]

You can't because Γ is a variable

[Mario Carneiro]

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

[Billy Price]

that's pretty interesting

[Reid Barton]

Obviously you should use a difference list for your context flees

[Billy Price]

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]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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]

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]

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

[Billy Price]

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]

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]

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]

I really appreciate the help in getting me started.

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

No, a sequent is still just two terms

[Mario Carneiro]

But the inductive defining the proof relation will contain WF hypotheses

[Billy Price]

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]

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

[Mario Carneiro]

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]

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

[Billy Price]

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]

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]

can you make that a #mwe?

[Jalex Stark]

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

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]

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]

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

TL_zulip.lean

[Jalex Stark]

why not paste it into a message?

[Jalex Stark]

that's probably much easier for both of us

[Jalex Stark]

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]

so yes, you can replace the unused variable names with _

[Billy Price]

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]

i think in your tactic state, the autogenerated variable names appear in the order they're generated

[Billy Price]

Actually you're right - I think they just reappear in a different order once I've named them for some reason.

[Billy Price]

Can I avoid re-introducing Γ every time I do a case?

[Jalex Stark]

a mostly-not-serious suggestion is to redefine things so that the arguments that you're introducing come first

[Jalex Stark]

in the proof.comp case you do a lot of work tracking down metavariables

[Jalex Stark]

apply @WF.all _ _ A, seems like a better thing to write for the first line than apply WF.all

[Jalex Stark]

similarly apply @WF.elem _ _ _ A, a few lines later

[Billy Price]

Sorry could you explain what that's achieving?

[Jalex Stark]

well as it's written you get a metavariable and a goal that's just type

[Jalex Stark]

and then later you close that goal by supplying A

[Jalex Stark]

here we're feeding it A right when it's needed, instead of making lean ask us for it

[Jalex Stark]

I think you should abstract out the hard cases like proof.comp as lemmas

[Jalex Stark]

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]

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]

Yeah if in fact you end up always stating A explicitly then probably you want A to be an explicit argument

[Jalex Stark]

the first three implicit arguments get dealt with just fine

[Billy Price]

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]

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]

you could have a lemma whose type signature is this tactic state

[Billy Price]

That's a nice way to go about it. That reminds me, what's up with the multiple Gammas?

[Billy Price]

Shouldn't they be unified or something?

[Jalex Stark]

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]

unified?

[Jalex Stark]

they have different types

[Billy Price]

context is list type

[Jalex Stark]

depends on what you mean by is

[Billy Price]

Definitional is? I'm not even sure why one of them became list type

[Jalex Stark]

context is defeq to list type

[Jalex Stark]

but defeq is weaker than syntactic equality

[Jalex Stark]

and some things (I don't know which ones, really) only work up to syntactic equality

[Jalex Stark]

i do share some of your confusion

[Billy Price]

So when I do some case - I wanna say "use the same context here"

[Jalex Stark]

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]

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]

Whereas I need to unpack all the different cases for the context and terms

[Jalex Stark]

okay, I don't understand but vaguely believe you

[Jalex Stark]

also i'm gonna go sleep now

[Jalex Stark]

uh I guess to go back to one of your first questions

[Jalex Stark]

if you want more automation you could tag things with the simp attribute

[Jalex Stark]

and I think that the tidy tactic knows how to do some of the proofs you're doing

[Billy Price]

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]

tactic#tidy

[Jannis Limperg]

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]

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]

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]

It can also be ignored

[Billy Price]

Not sure what you mean by sticky position. Like multiple cursors?

[Bryan Gin-ge Chen]

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]

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]

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]

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]

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]

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]

list.concat isn't a constructor, and indeed the result of list.concat could even be list.nil.

[Reid Barton]

I would ditch the induction on Γ, and induct on h instead

[Reid Barton]

What is mod supposed to represent?

[Reid Barton]

Oh whoops, list.concat doesn't mean what it means in every other language. Nevertheless, the first point remains.

[Billy Price]

haha yeah, also list.append is what I first thought list.concat would be

[Billy Price]

mod adds a single junk type to the back of the context of a well-formed term

[Billy Price]

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]

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]

What does mod stand for then?

[Reid Barton]

I would have thought WF already has this property, am I missing something?

[Billy Price]

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]

I think the mod constructor should be a theorem (usually called "weakening")

[Billy Price]

I think I need quotients now to find the objects of my category - where can I find good examples of quotient types?

[Johan Commelin]

git grep quotient?

[Billy Price]

That didn't work but I have been searching - just found Zmod37.lean - perfect!

[Kevin Buzzard]

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]

What happens when you form a quotient type using a relation that's not an equivalence relation?

[Billy Price]

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]

There should be quotient.lift\3

[Billy Price]

There isn't :(

[Reid Barton]

Add it!

[Billy Price]

:grimacing: I'll try when I have time :(

[Mario Carneiro]

Look at the proof of lift2 and copy it

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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

[Billy Price]

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]

Most or all of your second set of rules (starting with and_left) shouldn't be used with apply_rules.

[Billy Price]

Ah good point, they would generate infinite possibilities for derivation right?

[Reid Barton]

right, they are possibly suitable for forwards reasoning, but not for backwards reasoning

[Reid Barton]

oh, you just have a namespace problem actually

[Reid Barton]

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]

outside namespace TT?

[Reid Barton]

right. Alternatively, call it TT.WF_rules everywhere

[Billy Price]

Everywhere except the definition?

[Reid Barton]

right, not literally in meta def WF_rules but everywhere else

[Reid Barton]

probably it's optional in `WF_rules , I forget how the backticked names work exactly

[Billy Price]

I can't add TT. to any of the other WF_rules without red-lines "unknown attribute [TT.WF_rules]"

[Mario Carneiro]

Not optional with `WF_rules but you should be using ``WF_rules and there it is optional

[Mario Carneiro]

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]

I'm not sure I understand the relevance. Is the name checking time relevant to whether a TT. is needed?

[Billy Price]

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]

maybe you have no matching rule

[Reid Barton]

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]

name resolution means that it inserts namespaces based on the current context

[Reid Barton]

and once I comment out all the bad rules

[Mario Carneiro]

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]

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]

Could you paste what you got working @Reid Barton ?

[Reid Barton]

/-
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]

Oh you change the name too

[Reid Barton]

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]

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

[Reid Barton]

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

[Billy Price]

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]

That's right, this is why lift is not good enough

[Mario Carneiro]

you have to prove the analogous theorem for lift_d

[Billy Price]

Hmm okay, so prepending some list of types of length d in the lift_d d case?

[Mario Carneiro]

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]

but you definitely have to generalize k

[Mario Carneiro]

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

[Billy Price]

Ah okay, so splitting the original context at the kth position and shoving d variables in there.

[Mario Carneiro]

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]

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]

Yep that makes sense to me

[Billy Price]

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]

How did you start the proof?

[Mario Carneiro]

You need generalizing K at least

[Billy Price]

@[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]

You also need to generalize generalize e : K ++ Γ = Γ' before the induction

[Mario Carneiro]

You should also be able to use constructor instead of apply_rules for an inductive proof like this

[Billy Price]

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

[Mario Carneiro]

K needs to be forall-quantified in the inductive hypothesis

[Mario Carneiro]

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]

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]

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]

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]

right of the colon in the inductive statement

[Mario Carneiro]

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

[Billy Price]

yep, context, type and term?

[Mario Carneiro]

right

[Billy Price]

K appears in the context of wfa - why does that not automatically generalise?

[Billy Price]

Because the context is an append of two contexts?

[Billy Price]

So it can't do it?

[Mario Carneiro]

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]

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]

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]

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

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]

I think I should have length K' appearing in ih, not length K

[Mario Carneiro]

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

[Mario Carneiro]

K' is just Γ'

[Mario Carneiro]

but that inductive hypothesis does look like bad news

[Billy Price]

Oh right I got the renaming wrong.

[Mario Carneiro]

what is the state before induction

[Mario Carneiro]

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]

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

[Mario Carneiro]

the idea here is that immediately before the induction wfa should have variables in all the indices, no composed expressions

[Billy Price]

Yep that makes sense

[Billy Price]

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]

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]

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]

you have to explicitly specify ih (A' :: K), but it looks defeq modulo that

[Mario Carneiro]

(you should get out of the habit of using apply; refine and exact are better because they have the expected type)

[Billy Price]

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]

whaaat refine is the best tactic

[Mario Carneiro]

the argument of refine e or exact e is typechecked using the goal as the target type

[Mario Carneiro]

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]

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

[Mario Carneiro]

anything using structure constructor brackets for example

[Mario Carneiro]

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]

refine is great for compact and powerful combinations of existsi, intro and simple proof terms like refine ⟨x, easy_lemma, λ t, _⟩,

[Billy Price]

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

[Mario Carneiro]

no, I wrote what I meant

[Mario Carneiro]

that is, apply isn't replacing refine in this example

[Mario Carneiro]

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

[Mario Carneiro]

and it would still fail

[Billy Price]

Oh sorry I interpreted it wrong

[Billy Price]

Can I undo the generalizing of K to simplify my other inductive cases?

[Mario Carneiro]

You can use exact ih K

[Mario Carneiro]

or apply ih if it works

[Mario Carneiro]

You could use specialize ih K but it's probably not worth the characters it takes to say

[Billy Price]

Some of them have multiple inductive hypotheses

[Mario Carneiro]

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

[Mario Carneiro]

or try { ... }

[Mario Carneiro]

probably some higher level thing like solve_by_elim works too

[Billy Price]

But how would I name the inductive hypotheses like that?

[Billy Price]

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

[Billy Price]

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]

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

[Kevin Buzzard]

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]

There is one key theorem called something like nth_le_nth

[Mario Carneiro]

^ that

[Mario Carneiro]

also nth_eq_some

[Kevin Buzzard]

My student needed some nth_le_append lemmas

[Kevin Buzzard]

We never managed to formalise what nth_le_bind was but fortunately we were only glueing two lists together at that point

[Mario Carneiro]

I see nth_le_append and nth_le_append_right

[Mario Carneiro]

I wouldn't bother with nth_le_bind, the expression is not any better than what you get by induction

[Kevin Buzzard]

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

[Billy Price]

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]

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]

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]

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

[David Wärn]

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]

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]

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

[Kevin Buzzard]

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]

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

[Billy Price]

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]

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

[Billy Price]

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]

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]

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

[Billy Price]

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

[Mario Carneiro]

If induction used the same motive as cases, the inductive hypothesis would be guaranteed useless

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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]

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]

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]

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

[Mario Carneiro]

that's just a cases proof

[Mario Carneiro]

no need for induction

[Billy Price]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

yes

[Mario Carneiro]

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]

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]

I don't quite see what ties the [] or the Γ in e1 to anything that appears in the inductive state.

[Mario Carneiro]

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]

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

[Billy Price]

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

[Mario Carneiro]

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

[Billy Price]

Oh is it because generalize e1 : [] = Γ looks at the target and looks for instances of []?

[Mario Carneiro]

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]

Yes, generalize automatically replaces instances of [] with Γ

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

Here's another good example

[Mario Carneiro]

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]

Cool that looks like a useful practice.

[Billy Price]

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]

You will need a stronger inductive hypothesis

[Mario Carneiro]

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]

What do the stars do?

[Kenny Lau]

they make the sky more beautiful

[Billy Price]

Hahaha, oh I found the docs explaining what they are too

[Billy Price]

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]

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]

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]

this is pretty common of inductive proofs

[Mario Carneiro]

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]

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]

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

You're referring to the suffices pattern?

[Mario Carneiro]

yes

[Mario Carneiro]

You could use it here too

[Mario Carneiro]

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]

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]

the point isn't "here's the proof", it is "here's a technique for solving problems of this kind"

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

ah whoops sent too soon, I'll edit it (done)

[Billy Price]

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]

yeah that version is false

[Billy Price]

Good to know

[Mario Carneiro]

Do you have a substitution operator? If so you can express that t[a1/x] = t[a2/x] is provable

[Mario Carneiro]

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]

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]

How would one say "a function which is just some composition of the term constructors?"

[Jannis Limperg]

@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]

Oh cool! I will gladly do so :)

[Mario Carneiro]

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]

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]

What do you mean by the equality axioms?

[Kevin Buzzard]

@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]

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]

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]

More succinct

lemma lift_zero_does_nothing {k} {a : term} : lift_d 0 k a = a :=
  by induction a generalizing k;simp *

[Mario Carneiro]

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]

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]

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]

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]

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]

@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]

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]

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]

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]

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]

I mean the context and the type

[Mario Carneiro]

Hard to get definitional equalities are things like Gamma ++ a :: Delta = (Gamma ++ [a]) ++ Delta that come up in proofs

[Mario Carneiro]

it's even worse when Gamma itself has sequential dependencies as in dependent type theory

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

This mostly matches the way we treat types in simple type theory

[Mario Carneiro]

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]

I get what you're saying but I don't see the relevance

[Mario Carneiro]

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]

because it uses inductive functions in rigid positions twice: once in fin (length G) and once in term G (G.nth' i)

[Billy Price]

That's still term : context -> type -> Type though?

[Mario Carneiro]

well you can't write var at all without a context

[Mario Carneiro]

it could be a parameter though

[Mario Carneiro]

as long as you don't also have binders

[Mario Carneiro]

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]

What do you mean by parameter as opposed to a rigid variable?

[Mario Carneiro]

parameters to inductive types meaning left of the colon

[Mario Carneiro]

inductive term (G : context) : type -> Type

[Mario Carneiro]

Then the G in term G A is a rigid variable

[Mario Carneiro]

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]

as long as you only ever do syntactic or defeq matching in rigid positions there are no problems

[Billy Price]

Okay.

[Billy Price]

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]

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]

That works fine

[Mario Carneiro]

you have to parameterize the whole theory over alpha which is kind of annoying but otherwise it works well

[Mario Carneiro]

It's also not very pleasant to actually instantiate and get this nested inductive type of types with more types inside

[Mario Carneiro]

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]

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]

Regarding my 2 ideas, I have a feeling the second one is fundamentally different (perhaps the wrong idea).

[Billy Price]

Perhaps my "give me.." idea is more in the spirit of a type class?

[Mario Carneiro]

the second one should not typecheck

[Mario Carneiro]

because there is a universe issue

[Mario Carneiro]

You want the first one

[Mario Carneiro]

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]

oh wait you mean it's not an inductive type at all

[Mario Carneiro]

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]

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]

Good to know, I think I'll stick with my pure type theory for now.

[Billy Price]

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]

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]

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]

I mean it's fine, but it will never be particularly nice to write terms with de bruijn variables

[Billy Price]

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]

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]

I can't say offhand why that would fail. #mwe

[Billy Price]

I'll come back to this one.

[Billy Price]

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]

Related question - is WF a namespace in WF.star?

[Billy Price]

In the same way that WF is a namespace in WF.foo in the first code block

[Mario Carneiro]

no difference, yes it is a namespace

[Mario Carneiro]

one difference is that the WF namespace is open inside the proof of foo in the first case but not the second

[Billy Price]

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]

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]

meta def tactic.interactive.my_split : tactic unit:= do `[split]

[Billy Price]

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]

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

[Reid Barton]

it's long and hard to tell

[Reid Barton]

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

[Kevin Buzzard]

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

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]

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]

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

[Billy Price]

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]

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]

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

[Reid Barton]

Yes, rcases = "recursive cases"

[Kenny Lau]

rintro = “recursive intro”

[Billy Price]

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

[Billy Price]

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]

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]

It's not true

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

wait, where is your imp intro?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Billy Price]

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]

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

[Billy Price]

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]

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]

@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]

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]

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

[Billy Price]

the latter

[Billy Price]

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]

Do you use elan?

[Johan Commelin]

I suggest using leanproject instead of leanpkg

[Billy Price]

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

[Billy Price]

What do I do instead of leanpkg configure with leanproject?

[Billy Price]

Just straight to leanproject build?

[Billy Price]

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]

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]

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]

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]

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]

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]

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

[Billy Price]

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]

Oh I just saw Reid's first reply

[Billy Price]

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]

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]

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

[Billy Price]

(deleted)

[Billy Price]

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]

what's the theorem?

[Billy Price]

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

[Mario Carneiro]

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]

Yep that's an oversight

[Mario Carneiro]

It should be provable without induction

[Billy Price]

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

[Billy Price]

(those are all entails.*)

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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

[Billy Price]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Billy Price]

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]

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

[Mario Carneiro]

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

[Billy Price]

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]

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

[Billy Price]

(Unrelated to the proof i just posted)

[Mario Carneiro]

Only if h is a structure

[Kenny Lau]

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

[Kenny Lau]

let \<x\> := h in x

[Mario Carneiro]

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]

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]

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

[Billy Price]

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]

What does ⟦A | φ⟧ mean?

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

Very interesting, thanks :)

[Billy Price]

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]

Try the conv mode docs?

[Kevin Buzzard]

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

[Billy Price]

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]

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

[Kenny Lau]

and I wouldn't call that theorem compactness?

[Billy Price]

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]

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

[Kenny Lau]

so from a deduction you can produce a finite set Form

[Kenny Lau]

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

[Kenny Lau]

so you can produce:

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

why not use finset?

[Mario Carneiro]

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]

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

[Billy Price]

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]

You can cast the finset to a set

[Mario Carneiro]

@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]

I see, not sure if I need that but maybe

[Billy Price]

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]

try existsi

[Billy Price]

failed to synthesize type class instance for
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
⊢ has_union (finset Form)
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}

[Billy Price]

Same thing also happens with constructor, swap, exact XA' ∪ XB',

[Billy Price]

Here's a mwe

import data.finset
import tactic
import tactic.induction

namespace nat_deduction

/-- The type of Formulas, defined inductively
-/
inductive Form : Type
-- Atomic Formulas are introduced via natural numbers (atom 0, atom 1, atom 2)
| atom : ℕ → Form
-- conjunction
| and : Form → Form → Form
-- disjunction
| or  : Form → Form → Form
-- implication
| imp : Form → Form → Form

-- ⊥ is atom 0
def Form.bot : Form := Form.atom 0
-- we define `¬A` as `A ⟹ ⊥`
def Form.neg (A : Form) : Form := Form.imp A $ Form.atom 0

/--
We now define notation and coercions for nicer looking formulas
-/

-- Coerce natural numbers to Formulas as atoms
-- Given p : ℕ, just write `p` or `↑p` instead of `atom p`
-- (`↑p` forces the coercion)
instance nat_coe_Form : has_coe ℕ Form := ⟨Form.atom⟩

infix ` ⋀ `:75 := Form.and
infix ` ⋁ `:74 := Form.or
infix ` ⟹ `:75 := Form.imp
notation `⊥` := Form.atom 0
prefix `¬` := λ A, Form.imp A ⊥
notation `⊤` := ¬⊥ -- the simplest tautology

open Form

/-- Inductive definition of a deduction X ≻ A (argument) from a set of Formulas X
to a Formula A. This is equivalent to the usual proof tree presentation, however,
there is no need to "discharge" Formulas - we just choose to keep them as assumptions
or not. This forces us to add a weakening rule to the usual collection of rules.
-/
inductive deduction : set Form → Form → Type
| weakening  {X} {A Y}     : deduction X A → deduction (X ∪ Y) A
| assumption {X} (A)       : (A ∈ X) → deduction X A
| and_intro  {X} {A B}     : deduction X A → deduction X B → deduction X (A ⋀ B)
| and_left   {X} (A B)     : deduction X (A ⋀ B) → deduction X A
| and_right  {X} (A B)     : deduction X (A ⋀ B) → deduction X B
-- note X may or may not contain A, which corresponds to the ability to
-- discharge formulas which are no longer assumptions (or not).
| imp_intro  {X} {A B}     : deduction (X ∪ {A}) B → deduction X (A ⟹ B)
| imp_elim   {X} (A) {B}   : deduction X (A ⟹ B) → deduction X A → deduction X B
| or_left    {X} (A B)     : deduction X A → deduction X (A ⋁ B)
| or_right   {X} (A B)     : deduction X B → deduction X (A ⋁ B)
| or_elim    {X} (A B) {C} : deduction X (A ⋁ B) → deduction (X ∪ {A}) C → deduction (X ∪ {B}) C → deduction X C
| falsum     {X} {A}       : deduction X ⊥ → deduction X A

infix ` ≻ `:60 := deduction

end nat_deduction

/-- A tactic to produce a deduction of something like `X ∪ {A} ≻ A`,
via the assumption rule and an automated proof of `A ∈ X ∪ {A}`
-/
meta def tactic.interactive.assump : tactic unit :=
  do `[apply nat_deduction.deduction.assumption _; obviously]

namespace nat_deduction

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

infix ` ⊢I `:60 := provable

def compactify {X A} : X ≻ A → {X' : finset Form // ↑X' ⊆ X ∧ ↑X' ⊢I A } :=
begin
  intro dXA,
  induction' dXA,
  case weakening :
    { rcases ih with ⟨X', subX, X'pA⟩,
      use X',
      split, apply set.subset_union_of_subset_left,
      tidy },
  case assumption :
    { use {A}, tidy,
      assump },
  case and_intro : X A B dXA dXB ih₁ ih₂
    { rcases ih₁ with ⟨XA', AsubX, XA'pA⟩,
      rcases ih₂ with ⟨XB', BsubX, XB'pB⟩,
      existsi XA' ∪ XB',
      sorry }

end

[Mario Carneiro]

Ah, you forgot to prove decidable_eq Form

[Kenny Lau]

use @[derive decidable_eq]

[Billy Price]

Interesting, how do I know when I need to show decidable equality?

[Billy Price]

Also when defining an inductive type, is it possible to have a constructor whose target type is a product of the inductive type?
For example,

inductive deduction : set Form → Form → Type
| and_elim   {X} (A B)     : deduction X (A ⋀ B) → deduction X A ⨯ deduction X B

[Billy Price]

This gives me unexpected token on the \times

[Mario Carneiro]

No, each constructor must produce a deduction. For this example you need and_left and and_right.

[Billy Price]

Yeah that's what I had, just trying to invest in less cases for the inductive proofs to follow. Could this be added to the functionality of inductive? (where in the background, it just splits it into two constructors). I had the same thought about and \iff kind of constructor for inductive propositions.

[Floris van Doorn]

Even if inductive had this functionality, how would this reduce the number of cases for induction proofs? What induction step do you think you would get from the constructor and_elim?

[Billy Price]

I suppose it wouldn't make sense to collect an \iff induction into single case, since there's different inductive hypotheses for each direction, but for the \times situation like and_elim it would just be like and_left and and_right, and you just produce both within the same case.

[Mario Carneiro]

you can of course write these induction principles if you want to use them

[Billy Price]

I assumed that something inductive would be core and untouchable?

[Billy Price]

This is my attempt at formalising boolean models (this code is self contained). I had to add the reducible tag to Model otherwise it didn't understand n ∈ M, and it wouldn't recognise {p,q} as a Model. I did some reading on reducible semireducible and irreducible but I'm not sure if this is the correct usage - why do I need any tag at all? Isn't it obvious that a model satisfies has_elem and all the other properties of finset Form?

My main question however is that my use of finset.fold does not work properly when I use variable atoms. Specifically the first #reduce command successfully evaluates to tt, but the second is some giant mess with lots of decidable.rec. I do understand somewhat why this relates to decidability, but I have no idea how to fix it.

I am open to suggestions of betters ways of formalising models in Lean, I just did it this way because its very concise to state a model (just declare the set of true atoms). I tried looking through the flypitch project but I didn't find anything I could recognise as a model.

import data.finset

@[derive decidable_eq]
inductive Form : Type
| bot : Form
| atom : ℕ → Form
| and : Form → Form → Form
| or  : Form → Form → Form
| imp : Form → Form → Form

infix ` ⋀ `:75 := Form.and
infix ` ⋁ `:74 := Form.or
infix ` ⟹ `:75 := Form.imp
notation `⊥` := Form.bot

instance nat_coe_Form : has_coe ℕ Form := ⟨Form.atom⟩

@[reducible]
def Model := finset ℕ

def Form.eval_model (M : Model) : Form → bool
| ⊥       := ff
| (n : ℕ) := (n ∈ M)
| (A ⋀ B) := Form.eval_model A && Form.eval_model B
| (A ⋁ B) := Form.eval_model A || Form.eval_model B
| (A ⟹ B) := (bnot $ Form.eval_model A) || Form.eval_model B

instance : is_commutative bool band := ⟨λ a b,   by { cases a; simp }⟩
instance : is_associative bool band := ⟨λ a b c, by { cases a; simp }⟩

def eval_model (M : Model) : finset Form → bool := finset.fold band tt (Form.eval_model M)

variables p q : ℕ

#reduce eval_model {0,1} {↑0 ⋁ ↑1, ↑1}
#reduce eval_model {p,q} {p ⋁ q, q}

[Billy Price]

I've attempted to simplify my question, but this simpler version now gives deterministic timeout on the last line. I know in general it probably isn't possible to "compute" elementhood for any set, but surely it's possible to do so with finite sets and natural numbers, which have decidable equality.

import data.finset

instance : is_commutative bool band := ⟨λ a b,   by { cases a; simp }⟩
instance : is_associative bool band := ⟨λ a b c, by { cases a; simp }⟩

variables {p q r : ℕ}

def A : finset ℕ := {0, 1, 2}
def B : finset ℕ := {p, q, r}

#reduce finset.fold band tt (λ n, n ∈ A) {0, 1}
#reduce finset.fold band tt (λ n, n ∈ B) {p, q}

[Reid Barton]

The last line involves open terms--I'm not sure what you're expecting to happen here?

[Reid Barton]

It will probably generate something pretty big before getting stuck.

[Billy Price]

Well the answer is tt right?

[Reid Barton]

nope!

[Billy Price]

Is that because something like p \in {p} isn't definitionally equal to true or something? Even though it's logically equivalent?

[Reid Barton]

yes, that is a simpler example

[Reid Barton]

p \in {p} is definitionally equal to something like p = p I guess

[Reid Barton]

but this isn't definitionally equal to true, you need an axiom for that

[Reid Barton]

similarly, to know what {p, q} even means (which controls the structure of the computation of finset.fold), you need to know whether p equals q

[Reid Barton]

so you'll get stuck on that front fairly quickly

[Reid Barton]

there is an algorithm for computing {p, q}, which uses the decision procedure for equality on nat, which will try to apply induction to the variable p (or q) and get stuck there

[Billy Price]

How do workaround this, so that I can apply a model to a set of formulas, and have it separate into a bunch of facts about the valuations of each formula. For example take the model v(p)=1, v(q)=0 (and everything other atom gets 0) (represented however), then on this set of formulas {p, p V q, p & q} I want to automatically introduce these facts into the goal state: v(p)=1, v(p V q) = 1, v(p & q) = 0.

[Billy Price]

Whoops instead of 0 and 1 I mean ff and tt

[Billy Price]

Sorry I just realised this is different since I'm not banding the results all together, but both of these are objectives of mine

[Billy Price]

Oh wait I should just do \forall A \in {p,q}, <model assigns tt to A> right?

[Kenny Lau]

definitional equality is overrated

[Kenny Lau]

just use a bunch of simp lemmas

[Kenny Lau]

yes that will work

[Billy Price]

Is there a simp lemma that would convert \forall A \in {p,q,r}, P A to P p \and \forall A \in {q,r} (where repeated application would yield the conjunction P p \and P q \and P r) ? I'm guessing this would come down to how that finset notation is defined, but I couldn't find anything in the finset folder.

[Alex J. Best]

rw mem_insert_iff then something about forall_or?

[Shing Tak Lam]

finset.forall_mem_insert. (not @[simp] btw)

import data.finset

variables (α : Type) (p q r : α) (P : α → Prop) [decidable_eq α]

example : (∀ A ∈ ({p, q, r} : finset α), P A) ↔ (P p ∧ ∀ A ∈ ({q, r} : finset α), P A) :=
by rw finset.forall_mem_insert

[Shing Tak Lam]

and your example yielding a conjunction:

example : (∀ A ∈ ({p, q, r} : finset α), P A) ↔ P p ∧ P q ∧ P r :=
by simp only [finset.forall_mem_insert, forall_eq, finset.mem_singleton]

[Billy Price]

Cool! Thanks for that :)

[Billy Price]

Why isn't this a set theorem?

[Billy Price]

Because it's not true for some subtle reason I'm missing or it just hasn't been written yet?

[Billy Price]

Oh nevermind it's called ball_insert_iff

[Billy Price]

Why does notation not work properly in the goal-view for 𝕏 but it works as expected for 𝕐?

inductive foo : Type
| bar : ℕ → foo
| baz : foo

notation `𝕏` := foo.bar 0
notation `𝕐` := foo.baz

#check 𝕏 -- foo.bar 0 : foo
#check 𝕐 -- 𝕐 : foo

[Billy Price]

Is it because the there's no general notation for foo.bar n?

[Mario Carneiro]

Lean has to have an "unparser" to be able to do printing like this, and apparently it only works on constants, not composite terms

[Billy Price]

:(

[Billy Price]

Ah I see how to fix it,

def zero_bar := foo.bar 0
notation `𝕏` := zero_bar