Zulip Chat Archive

Stream: Type theory

Topic: Modelling a Type Theory in Lean


view this post on Zulip Billy Price (Apr 28 2020 at 13:30):

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

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

notation `Ξ©` := type.Omega
notation `πŸ™` := type.One
infix `Γ—Γ—` :100 := type.Prod
prefix 𝒫 :101 := type.Pow

inductive term : type β†’ Type
| var  : β„• β†’ Ξ  A : type, term A
| star : term πŸ™
| top  : term Ξ©
| bot  : term Ξ©
| prod : Ξ  {A B : type}, term A β†’ term B β†’ term (A Γ—Γ— B)
| elem : Ξ  {A : type}, term A β†’ term (𝒫 A) β†’ term Ξ©
| comp : Ξ  A : type, term Ξ© β†’ term (𝒫 A)
| and  : term Ξ© β†’ term Ξ© β†’ term Ξ©
| or   : term Ξ© β†’ term Ξ© β†’ term Ξ©
| imp  : term Ξ© β†’ term Ξ© β†’ term Ξ©
| all  : Ξ  A : type, term Ξ© β†’ term Ξ©
| ex   : Ξ  A : type, term Ξ© β†’ term Ξ©

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

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

view this post on Zulip Billy Price (Apr 28 2020 at 13:31):

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

view this post on Zulip Mario Carneiro (Apr 28 2020 at 13:34):

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

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

view this post on Zulip Mario Carneiro (Apr 28 2020 at 13:34):

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

view this post on Zulip Billy Price (Apr 28 2020 at 13:41):

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

view this post on Zulip Mario Carneiro (Apr 28 2020 at 13:45):

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

view this post on Zulip Mario Carneiro (Apr 28 2020 at 13:46):

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

view this post on Zulip Billy Price (Apr 28 2020 at 13:52):

Sorry what step are you referring to?

view this post on Zulip Mario Carneiro (Apr 28 2020 at 13:54):

step in the construction

view this post on Zulip Mario Carneiro (Apr 28 2020 at 13:54):

I would separate the grammar from the syntax rules

view this post on Zulip Jannis Limperg (Apr 28 2020 at 13:55):

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

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

open type

def context := list type

inductive var : context β†’ type β†’ Type
| var0 (Ξ±) : var [Ξ±] Ξ±
| varsucc {Ξ“ Ξ± Ξ²} : var Ξ“ Ξ± β†’ var (Ξ² :: Ξ“) Ξ²

-- This is the simply-typed lambda calculus with a unit type and products.
inductive term : context β†’ type β†’ Type
| var {Ξ“ Ξ±} : var Ξ“ Ξ± β†’ term Ξ“ Ξ±
| lam {Ξ“ Ξ± Ξ²} : term (Ξ± :: Ξ“) Ξ² β†’ term Ξ“ (Fun Ξ± Ξ²)
| prod {Ξ“ Ξ± Ξ²} : term Ξ“ Ξ± β†’ term Ξ“ Ξ² β†’ term Ξ“ (Prod Ξ± Ξ²)
| unit {Ξ“} : term Ξ“ One

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

view this post on Zulip Mario Carneiro (Apr 28 2020 at 13:56):

Lean's support for indexed families is fine

view this post on Zulip Mario Carneiro (Apr 28 2020 at 13:56):

mutual is not fine

view this post on Zulip Mario Carneiro (Apr 28 2020 at 13:57):

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

view this post on Zulip Billy Price (Apr 28 2020 at 14:01):

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

view this post on Zulip Jannis Limperg (Apr 28 2020 at 14:03):

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

view this post on Zulip Mario Carneiro (Apr 28 2020 at 14:06):

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

view this post on Zulip Mario Carneiro (Apr 28 2020 at 14:06):

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

view this post on Zulip Billy Price (Apr 28 2020 at 14:11):

The hypotheses in my sequents are just a single term Ξ©.

view this post on Zulip Billy Price (Apr 28 2020 at 14:46):

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

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

def FV_have_type (Z : type) : β„• β†’ Ξ  {A : type}, term A β†’ Prop
| v _ (var n A)  := v=n ∧ Z=A
| v _ (comp A Ο†) := FV_have_type (v+1) Ο†
| v _ (βˆ€' A Ο†)   := FV_have_type (v+1) Ο†
| v _ (βˆƒ' A Ο†)   := FV_have_type (v+1) Ο†
| v _ ⁎          := true
| v _ top        := true
| v _ bot        := true
| v _ (prod a b) := FV_have_type v a ∧ FV_have_type v b
| v _ (a ∈ α)    := FV_have_type v a ∧ FV_have_type v α
| v _ (p ∧' q)   := FV_have_type v p ∧ FV_have_type v q
| v _ (p ∨' q)   := FV_have_type v p ∧ FV_have_type v q
| v _ (p ⟹ q)  := FV_have_type v p ∧ FV_have_type v q

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

view this post on Zulip Reid Barton (Apr 28 2020 at 14:48):

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

view this post on Zulip Billy Price (Apr 28 2020 at 14:50):

Ah yes

view this post on Zulip Reid Barton (Apr 28 2020 at 15:02):

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

view this post on Zulip Reid Barton (Apr 28 2020 at 15:03):

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

view this post on Zulip Anton Lorenzen (Apr 29 2020 at 06:24):

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

view this post on Zulip Billy Price (Apr 29 2020 at 12:14):

Awesome! thanks I'll take a look

view this post on Zulip Billy Price (Apr 29 2020 at 13:34):

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

view this post on Zulip Reid Barton (Apr 29 2020 at 13:34):

More specifically?

view this post on Zulip Reid Barton (Apr 29 2020 at 13:34):

What is the English translation of what you wrote?

view this post on Zulip Billy Price (Apr 29 2020 at 13:34):

def WF : Ξ  A : type, term A β†’ context β†’  Prop
| _ (var n A) Ξ“  := βˆ€ a : n < Ξ“.length, (Ξ“.nth_le n a = A)
| _ (comp A Ο†) Ξ“ := WF Ξ© Ο† (A :: Ξ“)
| _ (βˆ€' A Ο†) Ξ“  := WF Ξ© Ο† (A :: Ξ“)
| _ (βˆƒ' A Ο†) Ξ“  := WF Ξ© Ο† (A :: Ξ“)

view this post on Zulip Billy Price (Apr 29 2020 at 13:35):

Hang on let me paste my term definition

view this post on Zulip Billy Price (Apr 29 2020 at 13:35):

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

view this post on Zulip Billy Price (Apr 29 2020 at 13:36):

Billy Price said:

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

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

notation `Ξ©` := type.Omega
notation `πŸ™` := type.One
infix `Γ—Γ—` :100 := type.Prod
prefix 𝒫 :101 := type.Pow

inductive term : type β†’ Type
| var  : β„• β†’ Ξ  A : type, term A
| star : term πŸ™
| top  : term Ξ©
| bot  : term Ξ©
| prod : Ξ  {A B : type}, term A β†’ term B β†’ term (A Γ—Γ— B)
| elem : Ξ  {A : type}, term A β†’ term (𝒫 A) β†’ term Ξ©
| comp : Ξ  A : type, term Ξ© β†’ term (𝒫 A)
| and  : term Ξ© β†’ term Ξ© β†’ term Ξ©
| or   : term Ξ© β†’ term Ξ© β†’ term Ξ©
| imp  : term Ξ© β†’ term Ξ© β†’ term Ξ©
| all  : Ξ  A : type, term Ξ© β†’ term Ξ©
| ex   : Ξ  A : type, term Ξ© β†’ term Ξ©

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

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

view this post on Zulip Reid Barton (Apr 29 2020 at 13:37):

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

view this post on Zulip Billy Price (Apr 29 2020 at 13:37):

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

view this post on Zulip Kenny Lau (Apr 29 2020 at 13:38):

Inductively defined propositions:

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

view this post on Zulip Billy Price (Apr 29 2020 at 13:39):

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

view this post on Zulip Billy Price (Apr 29 2020 at 13:41):

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

view this post on Zulip Kenny Lau (Apr 29 2020 at 13:42):

yes, but inductive might be better for this case

view this post on Zulip Billy Price (Apr 29 2020 at 13:44):

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

view this post on Zulip Kenny Lau (Apr 29 2020 at 13:45):

it allows you to "inject" things

view this post on Zulip Kenny Lau (Apr 29 2020 at 13:45):

and you don't need to go through every case

view this post on Zulip Kenny Lau (Apr 29 2020 at 13:46):

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

view this post on Zulip Mario Carneiro (Apr 29 2020 at 13:50):

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

view this post on Zulip Billy Price (Apr 29 2020 at 13:53):

Beautiful, thank you.

view this post on Zulip Billy Price (Apr 29 2020 at 14:01):

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

def WF : Ξ  A : type, term A β†’ context β†’ Prop
| _ (var n A) Ξ“  := Ξ“.nth n = some A
| _ (comp A Ο†) Ξ“ := WF Ξ© Ο† (A :: Ξ“)
| _ (βˆ€' A Ο†) Ξ“   := WF Ξ© Ο† (A :: Ξ“)
| _ (βˆƒ' A Ο†) Ξ“   := WF Ξ© Ο† (A :: Ξ“)
| _ ⁎ Ξ“          := true
| _ top Ξ“        := true
| _ bot Ξ“        := true
| _ (prod a b) Ξ“ := WF _ a Ξ“ ∧ WF _ b Ξ“
| _ (a ∈ Ξ±) Ξ“    := WF _ a Ξ“ ∧ WF _ Ξ± Ξ“
| _ (p ∧' q) Ξ“   := WF _ p Ξ“ ∧ WF _ q Ξ“
| _ (p ∨' q) Ξ“   := WF _ p Ξ“ ∧ WF _ q Ξ“
| _ (p ⟹ q) Ξ“  := WF _ p Ξ“ ∧ WF _ q Ξ“

view this post on Zulip Billy Price (Apr 29 2020 at 14:13):

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

view this post on Zulip Kenny Lau (Apr 29 2020 at 14:15):

Kenny Lau said:

Inductively defined propositions:

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

view this post on Zulip Jannis Limperg (Apr 29 2020 at 14:15):

Billy Price said:

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

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

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

Benefits of a recursive definition of well-formedness:

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

Billy Price said:

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

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

view this post on Zulip Billy Price (Apr 29 2020 at 14:28):

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

view this post on Zulip Billy Price (Apr 29 2020 at 14:32):

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

view this post on Zulip Reid Barton (Apr 29 2020 at 14:33):

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

view this post on Zulip Reid Barton (Apr 29 2020 at 14:33):

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

view this post on Zulip Billy Price (Apr 29 2020 at 14:34):

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

view this post on Zulip Reid Barton (Apr 29 2020 at 14:34):

Basically, yes

view this post on Zulip Reid Barton (Apr 29 2020 at 14:35):

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

view this post on Zulip Reid Barton (Apr 29 2020 at 14:35):

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

view this post on Zulip Billy Price (Apr 29 2020 at 14:36):

Mario Carneiro said:

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

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

view this post on Zulip Reid Barton (Apr 29 2020 at 14:36):

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

view this post on Zulip Reid Barton (Apr 29 2020 at 14:37):

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

view this post on Zulip Billy Price (Apr 29 2020 at 14:38):

Good point

view this post on Zulip Billy Price (Apr 29 2020 at 14:40):

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

view this post on Zulip Reid Barton (Apr 29 2020 at 14:47):

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

view this post on Zulip Billy Price (May 05 2020 at 03:37):

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

def context := list type

inductive term : context β†’ type β†’ Type
| var (Ξ“ A Ξ”) : term (list.append Ξ“ (A::Ξ”)) A
| comp {Ξ“} : Ξ  A : type, term (A::Ξ“) Ξ© β†’ term Ξ“ (𝒫 A)
| all  {Ξ“} : Ξ  A : type, term (A::Ξ“) Ξ© β†’ term Ξ“ Ξ©
| ex   {Ξ“} : Ξ  A : type, term (A::Ξ“) Ξ© β†’ term Ξ“ Ξ©
| star {Ξ“} : term Ξ“ πŸ™
| top  {Ξ“} : term Ξ“ Ξ©
| bot  {Ξ“} : term Ξ“ Ξ©
| prod {Ξ“} : Ξ  {A B : type}, term Ξ“ A β†’ term Ξ“ B β†’ term Ξ“ (A Γ—Γ— B)
| elem {Ξ“} : Ξ  {A : type}, term Ξ“ A β†’ term Ξ“ (𝒫 A) β†’ term Ξ“ Ξ©
| and  {Ξ“} : term Ξ“ Ξ© β†’ term Ξ“ Ξ© β†’ term Ξ“ Ξ©
| or   {Ξ“} : term Ξ“ Ξ© β†’ term Ξ“ Ξ© β†’ term Ξ“ Ξ©
| imp  {Ξ“} : term Ξ“ Ξ© β†’ term Ξ“ Ξ© β†’ term Ξ“ Ξ©

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

def add_junk (Ξ² : context) : Ξ  (Ξ“: context) (A: type), term Ξ“ A β†’ term (list.append Ξ“ Ξ²) A
| (list.append Ξ“ (A::Ξ”)) (A) (var Ξ“ A Ξ”) := var Ξ“ A (list.append Ξ” Ξ²)

view this post on Zulip Mario Carneiro (May 05 2020 at 11:12):

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

view this post on Zulip Mario Carneiro (May 05 2020 at 11:14):

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

def add_junk (Ξ² : context) : Ξ  (Ξ“: context) (A: type), term Ξ“ A β†’ term (list.append Ξ“ Ξ²) A
| .(list.append Ξ“ (A::Ξ”)) .(A) (var Ξ“ A Ξ”) := var Ξ“ A (list.append Ξ” Ξ²)

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

view this post on Zulip Billy Price (May 05 2020 at 11:51):

That results in this error

equation type mismatch, term
  var Ξ“ A (list.append Ξ” Ξ²)
has type
  term (list.append Ξ“ (A :: list.append Ξ” Ξ²)) A
but is expected to have type
  term (list.append . (list.append Ξ“ (A :: Ξ”)) Ξ²) .A

view this post on Zulip Billy Price (May 05 2020 at 11:53):

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

view this post on Zulip Mario Carneiro (May 05 2020 at 12:31):

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

view this post on Zulip Mario Carneiro (May 05 2020 at 12:31):

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

view this post on Zulip Mario Carneiro (May 05 2020 at 12:32):

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

view this post on Zulip Mario Carneiro (May 05 2020 at 12:32):

You should definitely not have this constructor

| var (Ξ“ A Ξ”) : term (list.append Ξ“ (A::Ξ”)) A

because the term will usually not have this form

view this post on Zulip Mario Carneiro (May 05 2020 at 12:33):

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

view this post on Zulip Billy Price (May 05 2020 at 12:34):

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

view this post on Zulip Mario Carneiro (May 05 2020 at 12:34):

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

view this post on Zulip Mario Carneiro (May 05 2020 at 12:34):

that one gives you a de bruijn index

view this post on Zulip Billy Price (May 05 2020 at 12:35):

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

view this post on Zulip Mario Carneiro (May 05 2020 at 12:36):

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

view this post on Zulip Mario Carneiro (May 05 2020 at 12:36):

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

view this post on Zulip Billy Price (May 05 2020 at 12:37):

defeq meaning definitional equality?

view this post on Zulip Mario Carneiro (May 05 2020 at 12:37):

term (list.append Ξ“ (A :: list.append Ξ” Ξ²)) A and term (list.append (list.append Ξ“ (A :: Ξ”)) Ξ²) A are distinct types, so you have to insert a cast between them and this will make everything harder

view this post on Zulip Mario Carneiro (May 05 2020 at 12:38):

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

view this post on Zulip Billy Price (May 05 2020 at 12:38):

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

view this post on Zulip Mario Carneiro (May 05 2020 at 12:38):

You can't because Ξ“ is a variable

view this post on Zulip Mario Carneiro (May 05 2020 at 12:39):

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

view this post on Zulip Billy Price (May 05 2020 at 12:39):

that's pretty interesting

view this post on Zulip Reid Barton (May 05 2020 at 12:40):

Obviously you should use a difference list for your context flees

view this post on Zulip Billy Price (May 05 2020 at 12:42):

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

view this post on Zulip Mario Carneiro (May 05 2020 at 12:43):

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

view this post on Zulip Mario Carneiro (May 05 2020 at 12:43):

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

view this post on Zulip Mario Carneiro (May 05 2020 at 12:45):

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

view this post on Zulip Mario Carneiro (May 05 2020 at 12:46):

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

view this post on Zulip Mario Carneiro (May 05 2020 at 12:47):

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

view this post on Zulip Billy Price (May 05 2020 at 12:48):

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

view this post on Zulip Mario Carneiro (May 05 2020 at 12:49):

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

view this post on Zulip Mario Carneiro (May 05 2020 at 12:50):

your original var constructor only supports contexts of the form Ξ“ ++ A :: Ξ”

view this post on Zulip Billy Price (May 05 2020 at 12:52):

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

view this post on Zulip Mario Carneiro (May 05 2020 at 12:54):

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

view this post on Zulip Mario Carneiro (May 05 2020 at 12:54):

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

view this post on Zulip Billy Price (May 05 2020 at 12:55):

I really appreciate the help in getting me started.

view this post on Zulip Mario Carneiro (May 05 2020 at 13:04):

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

inductive term : Type
| var : β„• β†’ term
| comp : type β†’ term β†’ term
| all  : type β†’ term β†’ term
| ex   : type β†’ term β†’ term
| star : term
| top  : term
| bot  : term
| prod : term β†’ term β†’ term
| elem : term β†’ term β†’ term
| and  : term β†’ term β†’ term
| or   : term β†’ term β†’ term
| imp  : term β†’ term β†’ term


inductive WF : context β†’ term β†’ type β†’ Prop
| var (Ξ“ A Ξ”) : WF (list.append Ξ“ (A::Ξ”)) (term.var (list.length Ξ“)) A
| comp {Ξ“ e} : Ξ  A : type, WF (A::Ξ“) e Ξ© β†’ WF Ξ“ (term.comp A e) (𝒫 A)
| all  {Ξ“ e} : Ξ  A : type, WF (A::Ξ“) e Ξ© β†’ WF Ξ“ (term.all A e) Ξ©
| ex   {Ξ“ e} : Ξ  A : type, WF (A::Ξ“) e Ξ© β†’ WF Ξ“ (term.all A e) Ξ©
| star {Ξ“} : WF Ξ“ term.star πŸ™
| top  {Ξ“} : WF Ξ“ term.top Ξ©
| bot  {Ξ“} : WF Ξ“ term.bot Ξ©
| prod {Ξ“ e₁ eβ‚‚} : Ξ  {A B : type}, WF Ξ“ e₁ A β†’ WF Ξ“ eβ‚‚ B β†’ WF Ξ“ (term.prod e₁ eβ‚‚) (A Γ—Γ— B)
| elem {Ξ“ e₁ eβ‚‚} : Ξ  {A : type}, WF Ξ“ e₁ A β†’ WF Ξ“ eβ‚‚ (𝒫 A) β†’ WF Ξ“ (term.elem e₁ eβ‚‚) Ξ©
| and  {Ξ“ e₁ eβ‚‚} : WF Ξ“ e₁ Ξ© β†’ WF Ξ“ e₁ Ξ© β†’ WF Ξ“ (term.and e₁ eβ‚‚) Ξ©
| or   {Ξ“ e₁ eβ‚‚} : WF Ξ“ e₁ Ξ© β†’ WF Ξ“ e₁ Ξ© β†’ WF Ξ“ (term.or e₁ eβ‚‚) Ξ©
| imp  {Ξ“ e₁ eβ‚‚} : WF Ξ“ e₁ Ξ© β†’ WF Ξ“ e₁ Ξ© β†’ WF Ξ“ (term.imp e₁ eβ‚‚) Ξ©

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

view this post on Zulip Billy Price (May 05 2020 at 13:17):

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

view this post on Zulip Billy Price (May 05 2020 at 13:18):

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

view this post on Zulip Mario Carneiro (May 05 2020 at 13:18):

No, a sequent is still just two terms

view this post on Zulip Mario Carneiro (May 05 2020 at 13:19):

But the inductive defining the proof relation will contain WF hypotheses

view this post on Zulip Billy Price (May 05 2020 at 13:26):

Ah, I just wrote down the type and realised of course you must introduce the term objects themselves to talk about their WF'ness
inductive proof : Ξ  {Ξ“:context} {Ο†: term} {ψ : term}, WF Ξ“ Ο† Ξ© β†’ WF Ξ“ ψ Ξ© β†’ Type

view this post on Zulip Billy Price (May 05 2020 at 13:29):

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

view this post on Zulip Mario Carneiro (May 05 2020 at 13:29):

You can write the proof : context -> term -> term -> Prop relation such that proof Ξ“ Ο† ψ -> WF Ξ“ Ο† Ξ© /\ WF Ξ“ ψ Ξ©, although I would actually suggest WF Ξ“ Ο† Ξ© -> proof Ξ“ Ο† ψ -> WF Ξ“ ψ Ξ© instead

view this post on Zulip Billy Price (May 22 2020 at 02:48):

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

view this post on Zulip Billy Price (May 22 2020 at 02:53):

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

view this post on Zulip Billy Price (May 22 2020 at 03:01):

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

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

view this post on Zulip Jalex Stark (May 22 2020 at 03:05):

can you make that a #mwe?

view this post on Zulip Jalex Stark (May 22 2020 at 03:05):

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

view this post on Zulip Jannis Limperg (May 22 2020 at 03:14):

Billy Price said:

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

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

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

view this post on Zulip Jalex Stark (May 22 2020 at 03:17):

in this part

  case proof.cut : Ξ“ P Q R prf_PQ prf_QR h₁ hβ‚‚
    {exact hβ‚‚ (h₁ wf_Ο†)},

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

  case proof.cut : _ _ _ _ _ _ h₁ hβ‚‚
    {exact hβ‚‚ (h₁ wf_Ο†)},

view this post on Zulip Billy Price (May 22 2020 at 03:19):

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

TL_zulip.lean

view this post on Zulip Jalex Stark (May 22 2020 at 03:20):

why not paste it into a message?

view this post on Zulip Jalex Stark (May 22 2020 at 03:20):

that's probably much easier for both of us

view this post on Zulip Jalex Stark (May 22 2020 at 03:21):

import data.finset
namespace TT

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

notation `Ξ©` := type.Omega
notation `πŸ™` := type.One
infix `Γ—Γ—`:max := type.Prod
prefix 𝒫 :max := type.Pow

def context := list type

inductive term : Type
| star : term
| top  : term
| bot  : term
| and  : term β†’ term β†’ term
| or   : term β†’ term β†’ term
| imp  : term β†’ term β†’ term
| var  : β„• β†’ term
| comp : term β†’ term
| all  : term β†’ term
| ex   : term β†’ term
| elem : term β†’ term β†’ term
| prod : term β†’ term β†’ term

open term



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

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

notation `⁎` := star    -- input \asterisk
notation `⊀` := top     --       \top
notation `βŠ₯` := bot     -- input \bot
infixr ` ⟹ `:60 := imp -- input \==>
infixr ` β‹€ ` :70 := and -- input \And or \bigwedge
infixr ` ⋁ ` :59 := or  -- input \Or or \bigvee

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

def biimp (p q: term) := (p ⟹ q) β‹€ (q ⟹ p)
infix ` ⇔ `:60 := biimp -- input \<=>

infix ∈ := elem
infix βˆ‰ := Ξ» a, Ξ» Ξ±, not (elem a Ξ±)
notation `⟦` Ο† `⟧` := comp Ο†

prefix `βˆ€'`:1 := all
prefix `βˆƒ'`:2 := ex

def eq (a : term) (a' : term) : term := βˆ€' (a ∈ <0>) ⇔ (a' ∈ <0>)
infix `≃` :50 := eq

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

def ex_unique (Ο† : term) : term :=
  βˆƒ' βŸ¦Ο†βŸ§ ≃ singleton (<3>)
prefix `βˆƒ!'`:2 := ex_unique

def subseteq (Ξ± : term) (Ξ² : term) : term :=
  βˆ€' (<0> ∈ Ξ±) ⟹ (<0> ∈ Ξ²)
infix βŠ† := subseteq

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

inductive WF : context β†’ term β†’ type β†’ Prop
| star {Ξ“}         : WF Ξ“ term.star πŸ™
| top  {Ξ“}         : WF Ξ“ term.top Ξ©
| bot  {Ξ“}         : WF Ξ“ term.bot Ξ©
| and  {Ξ“ p q}     : WF Ξ“ p Ξ© β†’ WF Ξ“ q Ξ© β†’ WF Ξ“ (p β‹€ q) Ξ©
| or   {Ξ“ p q}     : WF Ξ“ p Ξ© β†’ WF Ξ“ q Ξ© β†’ WF Ξ“ (p ⋁ q) Ξ©
| imp  {Ξ“ p q}     : WF Ξ“ p Ξ© β†’ WF Ξ“ q Ξ© β†’ WF Ξ“ (p ⟹ q) Ξ©
| var  {Ξ“ n A}     : list.nth Ξ“ n = some A β†’ WF Ξ“ (var n) A
| comp {Ξ“ Ο† A}     : WF (A::Ξ“) Ο† Ξ© β†’ WF Ξ“ βŸ¦Ο†βŸ§ (𝒫 A)
| all  {Ξ“ Ο† A}     : WF (A::Ξ“) Ο† Ξ© β†’ WF Ξ“ (βˆ€' Ο†) Ξ©
| ex   {Ξ“ Ο† A}     : WF (A::Ξ“) Ο† Ξ© β†’ WF Ξ“ (βˆƒ' Ο†) Ξ©
| elem {Ξ“ a Ξ± A}   : WF Ξ“ a A β†’ WF Ξ“ Ξ± (𝒫 A) β†’ WF Ξ“ (a ∈ Ξ±) Ξ©
| prod {Ξ“ a b A B} : WF Ξ“ a A β†’ WF Ξ“ b B β†’ WF Ξ“ (prod a b) (A Γ—Γ— B)

variable Ξ“ : context
variables p q r Ο† a b Ξ± : term
variables A B : type

lemma WF_and_left   : WF Ξ“ (p β‹€ q) Ξ© β†’ WF Ξ“ p Ξ© := by {intro h, cases h, assumption}
lemma WF_and_right  : WF Ξ“ (p β‹€ q) Ξ© β†’ WF Ξ“ q Ξ© := by {intro h, cases h, assumption}
lemma WF_or_left    : WF Ξ“ (p ⋁ q) Ξ© β†’ WF Ξ“ p Ξ© := by {intro h, cases h, assumption}
lemma WF_or_right   : WF Ξ“ (p ⋁ q) Ξ© β†’ WF Ξ“ q Ξ© := by {intro h, cases h, assumption}
lemma WF_imp_left   : WF Ξ“ (p ⟹ q) Ξ© β†’ WF Ξ“ p Ξ© := by {intro h, cases h, assumption}
lemma WF_imp_right  : WF Ξ“ (p ⟹ q) Ξ© β†’ WF Ξ“ q Ξ© := by {intro h, cases h, assumption}
lemma WF_prod_left  : WF Ξ“ (prod a b) (A Γ—Γ— B) β†’ WF Ξ“ a A := by {intro h, cases h, assumption}
lemma WF_prod_right : WF Ξ“ (prod a b) (A Γ—Γ— B) β†’ WF Ξ“ b B := by {intro h, cases h, assumption}
lemma WF_comp_elim  : WF Ξ“ (βŸ¦Ο†βŸ§) (𝒫 A) β†’ WF (A::Ξ“) Ο† Ξ© := by {intro h, cases h, assumption}
lemma WF_all_elim   : WF Ξ“ (βˆ€' Ο†) Ξ© β†’ βˆƒ A:type, WF (A::Ξ“) Ο† Ξ© := by {intro h, cases h, constructor, assumption}
lemma WF_ex_elim    : WF Ξ“ (βˆ€' Ο†) Ξ© β†’ βˆƒ A:type, WF (A::Ξ“) Ο† Ξ© := by {intro h, cases h, constructor, assumption}

def lift (d : β„•): β„• β†’ term β†’ term
| k star       := star
| k top        := top
| k bot        := bot
| k (p β‹€ q)    := (lift k p) β‹€ (lift k q)
| k (p ⋁ q)    := (lift k p) ⋁ (lift k q)
| k (p ⟹ q)    := (lift k p) ⟹ (lift k q)
| k (var m)    := if mβ‰₯k then var (m+d) else var m
| k βŸ¦Ο†βŸ§         :=    ⟦lift (k+1) Ο†βŸ§
| k (βˆ€' Ο†)     := βˆ€' lift (k+1) Ο†
| k (βˆƒ' Ο†)     := βˆƒ' lift (k+1) Ο†
| k (a ∈ α)    := (lift k a) ∈ (lift k α)
| k (prod a b) := prod (lift k a) (lift k b)

@[simp]
def subst_nth : term β†’ β„• β†’ term β†’ term
| b n star       := star
| b n top        := top
| b n bot        := bot
| b n (p β‹€ q)    := (subst_nth b n p) β‹€ (subst_nth b n q)
| b n (p ⋁ q)    := (subst_nth b n p) ⋁ (subst_nth b n q)
| b n (p ⟹ q)  := (subst_nth b n p) ⟹ (subst_nth b n q)
| b n (var m)    := if n=m then b else var m
| b n βŸ¦Ο†βŸ§        :=     ⟦subst_nth (lift 1 0 b) (n+1) Ο†βŸ§
| b n (βˆ€' Ο†)     := βˆ€' (subst_nth (lift 1 0 b) (n+1) Ο†)
| b n (βˆƒ' Ο†)     := βˆƒ' (subst_nth (lift 1 0 b) (n+1) Ο†)
| b n (a ∈ α)    := (subst_nth b n a) ∈ (subst_nth b n α)
| b n (prod a c) := prod (subst_nth b n a) (subst_nth b n c)

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


inductive proof : context β†’ term β†’ term β†’ Prop
| axm        {Ξ“ Ο†}     : WF Ξ“ Ο† Ξ© β†’ proof Ξ“ Ο† Ο†
| vac        {Ξ“ Ο†}     : WF Ξ“ Ο† Ξ© β†’ proof Ξ“ Ο† term.top
| abs        {Ξ“ Ο†}     : WF Ξ“ Ο† Ξ© β†’ proof Ξ“ term.bot Ο†
| cut        {Ξ“ Ο† ψ Ξ³} : proof Ξ“ Ο† ψ β†’ proof Ξ“ ψ Ξ³ β†’ proof Ξ“ Ο† Ξ³
| and_intro  {Ξ“ p q r} : proof Ξ“ p q β†’ proof Ξ“ p r β†’ proof Ξ“ p (q β‹€ r)
| and_left   {Ξ“ p q r} : proof Ξ“ p (q β‹€ r) β†’ proof Ξ“ p q
| and_right  {Ξ“ p q r} : proof Ξ“ p (q β‹€ r) β†’ proof Ξ“ p r
| or_intro   {Ξ“ p q r} : proof Ξ“ p r β†’ proof Ξ“ q r β†’ proof Ξ“ (p ⋁ q) r
| or_left    {Ξ“ p q r} : proof Ξ“ (p ⋁ q) r β†’ proof Ξ“ p r
| or_right   {Ξ“ p q r} : proof Ξ“ (p ⋁ q) r β†’ proof Ξ“ q r
| imp_to_and {Ξ“ p q r} : proof Ξ“ p (q ⟹ r) β†’ proof Ξ“ (p β‹€ q) r
| and_to_imp {Ξ“ p q r} : proof Ξ“ (p β‹€ q) r β†’ proof Ξ“ p (q ⟹ r)
| add_var    {Ξ“ Ο† ψ B} : proof Ξ“ Ο† ψ β†’ proof (B :: Ξ“) Ο† ψ

| apply    {Ξ“ Ο† ψ b B} :
    WF Ξ“ b B
    β†’ proof (B::Ξ“) Ο† ψ
    β†’ proof Ξ“ (subst b Ο†) (subst b ψ)

| all_elim   {Ξ“ p Ο† B} : proof Ξ“ p (βˆ€' Ο†) β†’ proof (B::Ξ“) p Ο†
| all_intro  {Ξ“ p Ο† B} : proof (B::Ξ“) p Ο† β†’ proof Ξ“ p (βˆ€' Ο†)
| ex_elim    {Ξ“ p Ο† B} : proof Ξ“ p (βˆƒ' Ο†) β†’ proof (B::Ξ“) p Ο†
| ex_intro   {Ξ“ p Ο† B} : proof (B::Ξ“) p Ο† β†’ proof Ξ“ p (βˆƒ' Ο†)

| comp       {Ξ“ Ο† A}   :
    WF (A::A::Ξ“) Ο† Ξ©
    β†’ proof Ξ“ ⊀
      (βˆ€' (<0> ∈ βŸ¦Ο†βŸ§) ⇔ (subst <0> Ο†))

| ext                  :
    proof [] ⊀ $
      βˆ€' βˆ€' (βˆ€' (<0> ∈ <2>) ⇔ (<0> ∈ <1>)) ⟹ (<1> ≃ <0>)

| prop_ext             : proof [] ⊀ βˆ€' βˆ€' (<1> ⇔ <0>) ⟹ (<1> ≃ <0>)
| star_unique          : proof [] ⊀ βˆ€' (<0> ≃ ⁎)
| prod_exists_rep      : proof [] ⊀ βˆ€' βˆƒ' βˆƒ' (<2> ≃ (prod <1> <0>))

| prod_distinct_rep    :
    proof [] ⊀
      βˆ€' βˆ€' βˆ€' βˆ€' (prod <3> <1> ≃ prod <2> <0>) ⟹ (<3> ≃ <2> β‹€ <1> ≃ <0>)

example : proof [] ⊀ ⊀ := proof.axm WF.top


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

end TT

view this post on Zulip Jalex Stark (May 22 2020 at 03:22):

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

view this post on Zulip Billy Price (May 22 2020 at 03:25):

Yep I see. As I am naming them (or not naming them) I don't really know what I've named until I move my cursor inside the {}, and each time I do that - it's not clear which "ugly" name is going to become the next variable name I tack on. Is trial and error the only way there?

view this post on Zulip Jalex Stark (May 22 2020 at 03:26):

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

view this post on Zulip Billy Price (May 22 2020 at 03:27):

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

view this post on Zulip Billy Price (May 22 2020 at 03:28):

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

view this post on Zulip Jalex Stark (May 22 2020 at 03:31):

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

view this post on Zulip Jalex Stark (May 22 2020 at 03:31):

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

view this post on Zulip Jalex Stark (May 22 2020 at 03:32):

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

view this post on Zulip Jalex Stark (May 22 2020 at 03:33):

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

view this post on Zulip Billy Price (May 22 2020 at 03:34):

Sorry could you explain what that's achieving?

view this post on Zulip Jalex Stark (May 22 2020 at 03:35):

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

view this post on Zulip Jalex Stark (May 22 2020 at 03:35):

and then later you close that goal by supplying A

view this post on Zulip Jalex Stark (May 22 2020 at 03:36):

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

view this post on Zulip Jalex Stark (May 22 2020 at 03:37):

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

view this post on Zulip Jalex Stark (May 22 2020 at 03:38):

that way when you prove the theorem you're "just" listing all 24 cases together with either their short proofs or a call to the external lemma

view this post on Zulip Billy Price (May 22 2020 at 03:38):

I understand. Is that an indication I should change the WF.all to put the type first? And should I have the other arguments explicit or implicit? I thought making them implicit would save me from having to state them but I seems I have to do it anyway with this proof.

view this post on Zulip Jalex Stark (May 22 2020 at 03:39):

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

view this post on Zulip Jalex Stark (May 22 2020 at 03:39):

the first three implicit arguments get dealt with just fine

view this post on Zulip Billy Price (May 22 2020 at 03:40):

Jalex Stark said:

that way when you prove the theorem you're "just" listing all 24 cases together with either their short proofs or a call to the external lemma

If I'm doing it by induction though - do those lemmas need an appropriate hypothesis related to the induction?

view this post on Zulip Jalex Stark (May 22 2020 at 03:40):

the tactic state looks like this

Ξ“ : context,
Ο† ψ : term,
Ξ“ : list type,
wf_Ο† : WF Ξ“ ⊀ Ξ©,
p : term,
A : type,
h : WF (A :: A :: Ξ“) p Ξ©
⊒ WF Ξ“ (βˆ€'(var 0 ∈ ⟦p⟧) ⇔ subst (var 0) p) Ξ©

view this post on Zulip Jalex Stark (May 22 2020 at 03:41):

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

view this post on Zulip Billy Price (May 22 2020 at 03:42):

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

view this post on Zulip Billy Price (May 22 2020 at 03:42):

Shouldn't they be unified or something?

view this post on Zulip Jalex Stark (May 22 2020 at 03:42):

lemma case_proof_comp
(Ξ“ : context)
(Ο† ψ : term)
(Ξ“ : list type)
(wf_Ο† : WF Ξ“ ⊀ Ξ©)
(p : term)
(A : type)
(h : WF (A :: A :: Ξ“) p Ξ©) :
 WF Ξ“ (βˆ€'(var 0 ∈ ⟦p⟧) ⇔ subst (var 0) p) Ξ© := sorry

view this post on Zulip Jalex Stark (May 22 2020 at 03:43):

unified?

view this post on Zulip Jalex Stark (May 22 2020 at 03:43):

they have different types

view this post on Zulip Billy Price (May 22 2020 at 03:44):

context is list type

view this post on Zulip Jalex Stark (May 22 2020 at 03:44):

depends on what you mean by is

view this post on Zulip Billy Price (May 22 2020 at 03:45):

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

view this post on Zulip Jalex Stark (May 22 2020 at 03:45):

context is defeq to list type

view this post on Zulip Jalex Stark (May 22 2020 at 03:46):

but defeq is weaker than syntactic equality

view this post on Zulip Jalex Stark (May 22 2020 at 03:46):

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

view this post on Zulip Jalex Stark (May 22 2020 at 03:48):

i do share some of your confusion

view this post on Zulip Billy Price (May 22 2020 at 03:49):

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

view this post on Zulip Jalex Stark (May 22 2020 at 03:50):

hmm why do you write

inductive proof : context β†’ term β†’ term β†’ Prop

instead of e.g.

inductive proof  (\G : context)  (\phi : term) (\psi : term) : Prop

view this post on Zulip Billy Price (May 22 2020 at 03:53):

I was under the impression I need to do the first, since my understanding of the second is that it locks in those variables globally to the rest of the inductive definitions.

view this post on Zulip Billy Price (May 22 2020 at 03:53):

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

view this post on Zulip Jalex Stark (May 22 2020 at 03:53):

okay, I don't understand but vaguely believe you

view this post on Zulip Jalex Stark (May 22 2020 at 03:54):

also i'm gonna go sleep now

view this post on Zulip Jalex Stark (May 22 2020 at 03:54):

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

view this post on Zulip Jalex Stark (May 22 2020 at 03:54):

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

view this post on Zulip Jalex Stark (May 22 2020 at 03:55):

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

view this post on Zulip Billy Price (May 22 2020 at 03:56):

Goodnight :) That sounds cool and I need to read up on attributes and how that all works. I just put @[simp] next to subst and subst_nth because I had a guess at what it does.

view this post on Zulip Jalex Stark (May 22 2020 at 03:56):

tactic#tidy

view this post on Zulip Jannis Limperg (May 22 2020 at 04:01):

Billy Price said:

That reminds me, what's up with the multiple Gammas?

These are different hypotheses; they just have the same name. You can use dedup to give them different names. The first one may be unnecessary (if nothing in the goal refers to it); if so, you can clear it after the dedup.

view this post on Zulip Mario Carneiro (May 22 2020 at 04:53):

Billy Price said:

Yep I see. As I am naming them (or not naming them) I don't really know what I've named until I move my cursor inside the {}, and each time I do that - it's not clear which "ugly" name is going to become the next variable name I tack on. Is trial and error the only way there?

This is what I used to do, but the new "sticky position" vscode feature helps a lot with this. You put the marker inside the body of the case, then you start writing names in the case statement and push underscores until the name lines up with the variable you want

view this post on Zulip Mario Carneiro (May 22 2020 at 04:55):

To add to what Jannis said about the multiple gammas, the first one is probably the input to the theorem before the induction line. It can be removed, assuming you have generalized all the relevant hypotheses about it.

view this post on Zulip Mario Carneiro (May 22 2020 at 04:56):

It can also be ignored

view this post on Zulip Billy Price (May 22 2020 at 07:00):

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

view this post on Zulip Bryan Gin-ge Chen (May 22 2020 at 07:11):

When you have an editor with Lean code focused, you should see a button that looks like a pin near the top right of that editor. If you press that, or hit ctrl+P and search for "toggle sticky position", then the current position of the text cursor will get a blue mark. Now you can move your text cursor elsewhere, and the info view will continue to display the messages coming from the blue spot in the file. To turn it off, you can hit the button or call the command again.

view this post on Zulip Billy Price (May 22 2020 at 07:23):

How can I be more eco-friendly and solve 10 different lemmas at the same time? (they all compile with the same proof)

view this post on Zulip Marc Huisinga (May 22 2020 at 07:30):

if they are only cases in one bigger proof and not meaningful as separate lemmas, you could use any_goals {proof}. i've also read something on here about a tactic that allows you to select a specific set of goals, but i don't remember what it's called or whether it exists in mathlib.

view this post on Zulip Billy Price (May 22 2020 at 07:35):

They just deconstruct well-formedness - so I'm predicting using them in various places

All of those lemmas should be solved by the first one's proof

inductive WF : context β†’ term β†’ type β†’ Prop
| star {Ξ“}         : WF Ξ“ term.star πŸ™
| top  {Ξ“}         : WF Ξ“ term.top Ξ©
| bot  {Ξ“}         : WF Ξ“ term.bot Ξ©
| and  {Ξ“ p q}     : WF Ξ“ p Ξ© β†’ WF Ξ“ q Ξ© β†’ WF Ξ“ (p β‹€ q) Ξ©
| or   {Ξ“ p q}     : WF Ξ“ p Ξ© β†’ WF Ξ“ q Ξ© β†’ WF Ξ“ (p ⋁ q) Ξ©
| imp  {Ξ“ p q}     : WF Ξ“ p Ξ© β†’ WF Ξ“ q Ξ© β†’ WF Ξ“ (p ⟹ q) Ξ©
| var  {Ξ“ n} (A)   : list.nth Ξ“ n = some A β†’ WF Ξ“ (var n) A
| comp {Ξ“ Ο†} (A)   : WF (A::Ξ“) Ο† Ξ© β†’ WF Ξ“ βŸ¦Ο†βŸ§ (𝒫 A)
| all  {Ξ“ Ο†} (A)   : WF (A::Ξ“) Ο† Ξ© β†’ WF Ξ“ (βˆ€' Ο†) Ξ©
| ex   {Ξ“ Ο†} (A)   : WF (A::Ξ“) Ο† Ξ© β†’ WF Ξ“ (βˆƒ' Ο†) Ξ©
| elem {Ξ“ a Ξ±} (A) : WF Ξ“ a A β†’ WF Ξ“ Ξ± (𝒫 A) β†’ WF Ξ“ (a ∈ Ξ±) Ξ©
| prod {Ξ“ a b A B} : WF Ξ“ a A β†’ WF Ξ“ b B β†’ WF Ξ“ (prod a b) (A Γ—Γ— B)
| mod  {Ξ“ a A} (B) : WF Ξ“ a A β†’ WF (B::Ξ“) a A

variable Ξ“ : context
variables p q r Ο† a b Ξ± : term
variables A B : type

lemma WF_and_left   : WF Ξ“ (p β‹€ q) Ξ© β†’ WF Ξ“ p Ξ© :=
begin
intro h,
induction Ξ“,
  case list.nil : {cases h, assumption},
  case list.cons : B Ξ” ih {cases h, assumption, apply WF.mod, apply ih, assumption},
end
lemma WF_and_right  : WF Ξ“ (p β‹€ q) Ξ© β†’ WF Ξ“ q Ξ© :=
lemma WF_or_left    : WF Ξ“ (p ⋁ q) Ξ© β†’ WF Ξ“ p Ξ© :=
lemma WF_or_right   : WF Ξ“ (p ⋁ q) Ξ© β†’ WF Ξ“ q Ξ© :=
lemma WF_imp_left   : WF Ξ“ (p ⟹ q) Ξ© β†’ WF Ξ“ p Ξ© :=
lemma WF_imp_right  : WF Ξ“ (p ⟹ q) Ξ© β†’ WF Ξ“ q Ξ© :=
lemma WF_prod_left  : WF Ξ“ (prod a b) (A Γ—Γ— B) β†’ WF Ξ“ a A :=
lemma WF_prod_right : WF Ξ“ (prod a b) (A Γ—Γ— B) β†’ WF Ξ“ b B :=
lemma WF_comp_elim  : WF Ξ“ (βŸ¦Ο†βŸ§) (𝒫 A) β†’ WF (A::Ξ“) Ο† Ξ© :=

view this post on Zulip Billy Price (May 22 2020 at 07:56):

Whoops, my new "mod" constructor for Well-formedness was not supposed to put the new variable at the start of the list (should go at the end). Regardless - my original question is still relevant.

view this post on Zulip Billy Price (May 22 2020 at 08:16):

Here's my new definition of mod : | mod {Ξ“ a A} (B) : WF Ξ“ a A β†’ WF (list.concat Ξ“ B) a A. I am having trouble with the following proof

lemma WF_and_left   : WF Ξ“ (p β‹€ q) Ξ© β†’ WF Ξ“ p Ξ© :=
begin
intro h,
induction Ξ“,
  case list.nil : {cases h, sorry},
  case list.cons : {sorry}
end

Lean is unhappy with "cases h", I think because it tries to unify the (list.concat Ξ“ B) with list.nil to do the WF.mod case. Shouldn't it recognise this as an irrelevant case?

This is the error message

cases tactic failed, unsupported equality between type and constructor indices
(only equalities between constructors and/or variables are supported, try cases on the indices):
list.nil = list.concat h_Ξ“ h_B

state:
p q : term,
h : WF list.nil (and p q) Ξ©,
h_Ξ“ : context,
h_a : term,
h_A h_B : type,
h_a_1 : WF h_Ξ“ h_a h_A
⊒ list.nil = list.concat h_Ξ“ h_B β†’ and p q = h_a β†’ Ξ© = h_A β†’ h == _ β†’ WF list.nil p Ξ©

a similar thing happens with case list.cons {cases h, }

cases tactic failed, unsupported equality between type and constructor indices
(only equalities between constructors and/or variables are supported, try cases on the indices):
Ξ“_hd :: Ξ“_tl = list.concat h_Ξ“ h_B

state:
p q : term,
Ξ“_hd : type,
Ξ“_tl : list type,
Ξ“_ih : WF Ξ“_tl (and p q) Ξ© β†’ WF Ξ“_tl p Ξ©,
h : WF (Ξ“_hd :: Ξ“_tl) (and p q) Ξ©,
h_Ξ“ : context,
h_a : term,
h_A h_B : type,
h_a_1 : WF h_Ξ“ h_a h_A
⊒ Ξ“_hd :: Ξ“_tl = list.concat h_Ξ“ h_B β†’ and p q = h_a β†’ Ξ© = h_A β†’ h == _ β†’ WF (Ξ“_hd :: Ξ“_tl) p Ξ©

view this post on Zulip Reid Barton (May 22 2020 at 09:50):

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

view this post on Zulip Reid Barton (May 22 2020 at 09:55):

I would ditch the induction on Ξ“, and induct on h instead

view this post on Zulip Reid Barton (May 22 2020 at 09:55):

What is mod supposed to represent?

view this post on Zulip Reid Barton (May 22 2020 at 10:25):

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

view this post on Zulip Billy Price (May 22 2020 at 11:16):

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

view this post on Zulip Billy Price (May 22 2020 at 11:17):

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

view this post on Zulip Billy Price (May 22 2020 at 11:20):

If I do induction h - I don't know how to deal with all of the irrelevant cases that could not construct the given term. For example the first case want me to show WF Ξ” p πŸ™

view this post on Zulip Alex J. Best (May 22 2020 at 11:22):

Billy Price said:

How can I be more eco-friendly and solve 10 different lemmas at the same time? (they all compile with the same proof)

You can make a simple tactic like so:

meta def billy_tac : tactic unit := do
`[
intro h,
induction Ξ“,
  case list.nil : {cases h, assumption},
  case list.cons : B Ξ” ih {cases h, assumption, apply WF.mod, apply ih, assumption},]

view this post on Zulip Reid Barton (May 22 2020 at 11:43):

What does mod stand for then?

view this post on Zulip Reid Barton (May 22 2020 at 11:44):

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

view this post on Zulip Billy Price (May 22 2020 at 11:56):

Oh no, I was proving something else and thought I didn't have that - and then added this mod thing (modify context) and that complicated things

view this post on Zulip Mario Carneiro (May 22 2020 at 19:12):

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

view this post on Zulip Billy Price (May 28 2020 at 09:18):

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

view this post on Zulip Johan Commelin (May 28 2020 at 09:23):

git grep quotient?

view this post on Zulip Billy Price (May 28 2020 at 10:11):

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

view this post on Zulip Kevin Buzzard (May 28 2020 at 10:38):

Just to comment that that file using quotient, which finds the equivalence relation using type class search, but there is also quotient', which finds it via unification.

view this post on Zulip Billy Price (May 28 2020 at 10:44):

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

view this post on Zulip Billy Price (Jun 02 2020 at 11:22):

How does one lift a function a -> a -> a -> b to a function quotient r a -> quotient r a -> quotient r a -> b in a controlled way? I'm away of quot.lift - does this generalise in a manageable way?

view this post on Zulip Reid Barton (Jun 02 2020 at 11:24):

There should be quotient.lift\3

view this post on Zulip Billy Price (Jun 02 2020 at 11:46):

There isn't :(

view this post on Zulip Reid Barton (Jun 02 2020 at 11:49):

Add it!

view this post on Zulip Billy Price (Jun 02 2020 at 11:57):

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

view this post on Zulip Mario Carneiro (Jun 02 2020 at 12:12):

Look at the proof of lift2 and copy it

view this post on Zulip Mario Carneiro (Jun 02 2020 at 12:14):

or just use lift three times. It's not even a much worse proof obligation, it just has you vary one argument at a time instead of all three in one go

view this post on Zulip Billy Price (Jun 02 2020 at 13:06):

I'm working with equivalence classes of provably equal closed terms, and I'm trying to define proofs about terms given some such equivalence classes - hence the need for lifting - but now I'm realising I maybe I should show "if you have provably equal terms, you can interchange them in any proof", then I could just apply that a bunch of times. But then I'm guessing I'd need to work in all of the constructors for terms - do I really need to repeat myself about every little thing for terms, but now about equivalence classes of terms?

view this post on Zulip Billy Price (Jun 02 2020 at 13:42):

Perhaps that was a bit rambly - here's what I have so far in two files, the second file is where I'm trying to do stuff with the equivalence classes of closed terms - which are called tset A for any A : type (an abbreviation for "type theory set"). I feel like I should be able to coerce my tset's into closed_terms (which coerce into terms), so I can talk about proof's about tsets - without having to quotient.lift everything each time. Is that possible?

view this post on Zulip Billy Price (Jun 02 2020 at 13:42):

TT.lean

/-
Definitions of a type theory

Author: Billy Price
-/

import data.finset
namespace TT

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

notation `Ξ©` := type.Omega
def Unit := type.Unit
infix `Γ—Γ—`:max := type.Prod
prefix 𝒫 :max := type.Pow

def context := list type

inductive term : Type
| star : term
| top  : term
| bot  : term
| and  : term β†’ term β†’ term
| or   : term β†’ term β†’ term
| imp  : term β†’ term β†’ term
| elem : term β†’ term β†’ term
| pair : term β†’ term β†’ term
| var  : β„• β†’ term
| comp : term β†’ term
| all  : term β†’ term
| ex   : term β†’ term

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

notation `𝟘` := term.var 0
notation `πŸ™` := term.var 1
notation `𝟚` := term.var 2
notation `πŸ›` := term.var 3
notation `𝟜` := term.var 4
notation `𝟝` := term.var 5

notation `⁎` := term.star    -- input \asterisk
notation `⊀` := term.top     --       \top
notation `βŠ₯` := term.bot     -- input \bot
infixr ` ⟹ `:60 := term.imp -- input \==>
infixr ` β‹€ ` :70 := term.and -- input \And or \bigwedge
infixr ` ⋁ ` :59 := term.or  -- input \Or or \bigvee

def not (p : term) := p ⟹ βŠ₯
prefix `∼`:max := not -- input \~

def iff (p q: term) := (p ⟹ q) β‹€ (q ⟹ p)
infix ` ⇔ `:60 := iff -- input \<=>

infix ∈ := term.elem
infix βˆ‰ := Ξ» a Ξ±, not (term.elem a Ξ±)
notation `⟦` Ο† `⟧` := term.comp Ο†

notation `βŸͺ` a `,` b `⟫` := term.pair a b

prefix `βˆ€'`:1 := term.all
prefix `βˆƒ'`:2 := term.ex

def eq (a₁ aβ‚‚ : term) : term := βˆ€' (a₁ ∈ 𝟘) ⇔ (aβ‚‚ ∈ 𝟘)
infix `≃` :50 := eq

def singleton (a : term) := ⟦a ≃ (𝟘)⟧

def ex_unique (Ο† : term) : term :=
  βˆƒ' βŸ¦Ο†βŸ§ ≃ singleton (πŸ›)
prefix `βˆƒ!'`:2 := ex_unique

def subseteq (Ξ± : term) (Ξ² : term) : term :=
  βˆ€' (𝟘 ∈ Ξ±) ⟹ (𝟘 ∈ Ξ²)
infix βŠ† := subseteq

def set_prod {A B : type} (Ξ± Ξ² : term) : term :=
  βŸ¦βˆƒ' βˆƒ' (πŸ™ ∈ Ξ±) β‹€ (𝟘 ∈ Ξ²) β‹€ (πŸ› ≃ βŸͺ𝟚,πŸ™βŸ«)⟧

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


section wellformedness

  inductive WF : context β†’ type β†’ term β†’ Prop
  | star {Ξ“}         : WF Ξ“ Unit ⁎
  | top  {Ξ“}         : WF Ξ“ Ξ© ⊀
  | bot  {Ξ“}         : WF Ξ“ Ξ© βŠ₯
  | and  {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p β‹€ q)
  | or   {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p ⋁ q)
  | imp  {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p ⟹ q)
  | elem {Ξ“ A a Ξ±}   : WF Ξ“ A a β†’ WF Ξ“ (𝒫 A) Ξ± β†’ WF Ξ“ Ξ© (a ∈ Ξ±)
  | pair {Ξ“ A B a b} : WF Ξ“ A a β†’ WF Ξ“ B b β†’ WF Ξ“ (A Γ—Γ— B) βŸͺa,b⟫
  | var  {Ξ“ A n}     : list.nth Ξ“ n = some A β†’ WF Ξ“ A (var n)
  | comp {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ (𝒫 A) βŸ¦Ο†βŸ§
  | all  {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ Ξ© (βˆ€' Ο†)
  | ex   {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ Ξ© (βˆƒ' Ο†)


  variable {Ξ“ : context}
  variables p q r Ο† a b Ξ± : term
  variables {A B Ξ©' : type}
  -- Ξ©' is just a fake/variable version of Ξ© so we don't need to bother proving
  -- that it must be Ξ© itself.

  local notation `ez` := by {intro h, cases h, assumption}
  lemma WF.and_left   : WF Ξ“ Ξ©' (p β‹€ q) β†’ WF Ξ“ Ξ©' p               := ez
  lemma WF.and_right  : WF Ξ“ Ξ©' (p β‹€ q) β†’ WF Ξ“ Ξ©' q               := ez
  lemma WF.or_left    : WF Ξ“ Ξ©' (p ⋁ q) β†’ WF Ξ“ Ξ©' p               := ez
  lemma WF.or_right   : WF Ξ“ Ξ©' (p ⋁ q) β†’ WF Ξ“ Ξ©' q               := ez
  lemma WF.imp_left   : WF Ξ“ Ξ©' (p ⟹ q) β†’ WF Ξ“ Ξ©' p             := ez
  lemma WF.imp_right  : WF Ξ“ Ξ©' (p ⟹ q) β†’ WF Ξ“ Ξ©' q             := ez
  lemma WF.pair_left  : WF Ξ“ (A Γ—Γ— B) βŸͺa,b⟫ β†’ WF Ξ“ A a            := ez
  lemma WF.pair_right : WF Ξ“ (A Γ—Γ— B) βŸͺa,b⟫ β†’ WF Ξ“ B b            := ez
  lemma WF.comp_elim  : WF Ξ“ (𝒫 A) (βŸ¦Ο†βŸ§) β†’ WF (A::Ξ“) Ξ© Ο†          := ez
  lemma WF.all_elim   : WF Ξ“ Ξ©' (βˆ€' Ο†) β†’ βˆƒ A:type, WF (A::Ξ“) Ξ©' Ο† :=
    by {intro h, cases h, constructor, assumption}
  lemma WF.ex_elim    : WF Ξ“ Ξ©' (βˆ€' Ο†) β†’ βˆƒ A:type, WF (A::Ξ“) Ξ©' Ο† :=
    by {intro h, cases h, constructor, assumption}
  lemma WF.iff_intro : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p ⇔ q) :=
    by {intros h₁ hβ‚‚, apply WF.and, all_goals {apply WF.imp, assumption, assumption}}
  lemma WF.iff_elim : WF Ξ“ Ξ©' (p ⇔ q) β†’ WF Ξ“ Ξ©' p ∧ WF Ξ“ Ξ©' q :=
    by {intro h, apply and.intro, all_goals {cases h, cases h_a, assumption}}
  lemma WF.eq_intro {Ξ“} {a₁ aβ‚‚} (A : type) : WF ((𝒫 A) :: Ξ“) A a₁ β†’ WF ((𝒫 A) :: Ξ“) A aβ‚‚ β†’ WF Ξ“ Ξ© (a₁ ≃ aβ‚‚) :=
    by {intros h₁ hβ‚‚, apply WF.all, apply WF.iff_intro, all_goals {apply WF.elem, assumption, apply WF.var, simp}}

end wellformedness

section substitution

  def lift (d : β„•) : β„• β†’ term β†’ term
  | k ⁎          := ⁎
  | k ⊀          := ⊀
  | k βŠ₯          := βŠ₯
  | k (p β‹€ q)    := (lift k p) β‹€ (lift k q)
  | k (p ⋁ q)    := (lift k p) ⋁ (lift k q)
  | k (p ⟹ q)   := (lift k p) ⟹ (lift k q)
  | k (a ∈ α)    := (lift k a) ∈ (lift k α)
  | k βŸͺa,b⟫      := βŸͺlift k a, lift k b⟫
  | k (var m)    := if mβ‰₯k then var (m+d) else var m
  | k βŸ¦Ο†βŸ§         :=    ⟦lift (k+1) Ο†βŸ§
  | k (βˆ€' Ο†)     := βˆ€' lift (k+1) Ο†
  | k (βˆƒ' Ο†)     := βˆƒ' lift (k+1) Ο†

  def subst_nth : β„• β†’ term β†’ term β†’ term
  | n x ⁎          := ⁎
  | n x ⊀          := ⊀
  | n x βŠ₯          := βŠ₯
  | n x (p β‹€ q)    := (subst_nth n x p) β‹€ (subst_nth n x q)
  | n x (p ⋁ q)    := (subst_nth n x p) ⋁ (subst_nth n x q)
  | n x (p ⟹ q)  := (subst_nth n x p) ⟹ (subst_nth n x q)
  | n x (a ∈ α)    := (subst_nth n x a) ∈ (subst_nth n x α)
  | n x βŸͺa,c⟫      := βŸͺsubst_nth n x a, subst_nth n x c⟫
  | n x (var m)    := if n=m then x else var m
  | n x βŸ¦Ο†βŸ§         :=    ⟦subst_nth (n+1) (lift 1 0 x) Ο†βŸ§
  | n x (βˆ€' Ο†)     := βˆ€' (subst_nth (n+1) (lift 1 0 x) Ο†)
  | n x (βˆƒ' Ο†)     := βˆƒ' (subst_nth (n+1) (lift 1 0 x) Ο†)

  def subst := subst_nth 0

  notation  Ο† `⁅` b `⁆` := subst b Ο†

  #reduce πŸ˜β…βŠ€ β‹€ βŠ₯⁆
  #reduce πŸ™β…βŠ€ β‹€ βŠ₯⁆

end substitution

section proofs

  inductive proof : context β†’ term β†’ term β†’ Prop
  | axm        {Ξ“ Ο†}         : WF Ξ“ Ξ© Ο† β†’ proof Ξ“ Ο† Ο†
  | vac        {Ξ“ Ο†}         : WF Ξ“ Ξ© Ο† β†’ proof Ξ“ Ο† ⊀
  | abs        {Ξ“ Ο†}         : WF Ξ“ Ξ© Ο† β†’ proof Ξ“ βŠ₯ Ο†
  | and_intro  {Ξ“ p q r}     : proof Ξ“ p q β†’ proof Ξ“ p r β†’ proof Ξ“ p (q β‹€ r)
  | and_left   {Ξ“} (p q r)   : proof Ξ“ p (q β‹€ r) β†’ proof Ξ“ p q
  | and_right  {Ξ“} (p q r)   : proof Ξ“ p (q β‹€ r) β†’ proof Ξ“ p r
  | or_intro   {Ξ“ p q r}     : proof Ξ“ p r β†’ proof Ξ“ q r β†’ proof Ξ“ (p ⋁ q) r
  | or_left    {Ξ“} (p q r)   : proof Ξ“ (p ⋁ q) r β†’ proof Ξ“ p r
  | or_right   {Ξ“} (p q r)   : proof Ξ“ (p ⋁ q) r β†’ proof Ξ“ q r
  | imp_to_and {Ξ“ p q r}     : proof Ξ“ p (q ⟹ r) β†’ proof Ξ“ (p β‹€ q) r
  | and_to_imp {Ξ“ p q r}     : proof Ξ“ (p β‹€ q) r β†’ proof Ξ“ p (q ⟹ r)
  | weakening  {Ξ“ Ο† ψ B}     : proof Ξ“ Ο† ψ β†’ proof (list.concat Ξ“ B) Ο† ψ
  | cut        {Ξ“} (Ο† c ψ)   : proof Ξ“ Ο† c β†’ proof Ξ“ c ψ β†’ proof Ξ“ Ο† ψ
  | all_elim   {Ξ“ p Ο† B}     : proof Ξ“ p (βˆ€' Ο†) β†’ proof (B::Ξ“) p Ο†
  | all_intro  {Ξ“ p Ο†} (B)   : proof (B::Ξ“) p Ο† β†’ proof Ξ“ p (βˆ€' Ο†)
  | ex_elim    {Ξ“ p Ο† B}     : proof Ξ“ p (βˆƒ' Ο†) β†’ proof (B::Ξ“) p Ο†
  | ex_intro   {Ξ“ p Ο† B}     : proof (B::Ξ“) p Ο† β†’ proof Ξ“ p (βˆƒ' Ο†)
  | ext                      : proof [] ⊀ $ βˆ€' βˆ€' (βˆ€' (𝟘 ∈ 𝟚) ⇔ (𝟘 ∈ πŸ™)) ⟹ (πŸ™ ≃ 𝟘)
  | prop_ext                 : proof [] ⊀ βˆ€' βˆ€' (πŸ™ ⇔ 𝟘) ⟹ (𝟚 ≃ πŸ™)
  | star_unique              : proof [] ⊀ βˆ€' (πŸ™ ≃ ⁎)
  | pair_exists_rep          : proof [] ⊀ βˆ€' βˆƒ' βˆƒ' 𝟚 ≃ βŸͺπŸ™,𝟘⟫
  | pair_distinct_rep        : proof [] ⊀ βˆ€' βˆ€' βˆ€' βˆ€' (βŸͺ𝟜,𝟚⟫ ≃ βŸͺπŸ›,πŸ™βŸ«) ⟹ (𝟜 ≃ πŸ› β‹€ 𝟚 ≃ πŸ™)
  | apply      {Ξ“ B} (Ο† ψ b) : WF Ξ“ B b β†’ proof (B::Ξ“) Ο† ψ β†’ proof Ξ“ (φ⁅b⁆) (Οˆβ…b⁆)
  | comp       {Ξ“ Ο† A}       : WF (A::A::Ξ“) Ξ© Ο† β†’ proof Ξ“ ⊀ (βˆ€' (𝟘 ∈ βŸ¦Ο†βŸ§) ⇔ (Ο†β…πŸ™β†))

  prefix ⊒ := proof [] ⊀
  infix ` ⊒ `:50 := proof []
  notation Ο† ` ⊒[` Ξ“:(foldr `,` (h t, list.cons h t) list.nil) `] ` ψ := proof Ξ“ Ο† ψ
  notation `⊒[` Ξ“:(foldr `,` (h t, list.cons h t) list.nil) `] ` ψ := proof Ξ“ ⊀ ψ

  variables p q : term

  #reduce   ⊒ (p ⋁ ∼p)  -- proof [] ⊀ (or p (imp p βŠ₯))
  #reduce q ⊒ (p ⋁ ∼p)  -- proof [] q (or p (imp p βŠ₯))
  #reduce   ⊒[Ω,Unit] p -- proof [Ω,Unit] ⊀ p
  #reduce q ⊒[Ω,Unit] p -- proof [Ω,Unit] q p

  variable {Ξ“ : context}
  variables Ο† ψ : term

  lemma WF.proof_left  : proof Ξ“ Ο† ψ β†’ WF Ξ“ Ξ© Ο† := sorry
  lemma WF.proof_right : proof Ξ“ Ο† ψ β†’ WF Ξ“ Ξ© ψ := sorry

end proofs

end TT

view this post on Zulip Billy Price (Jun 02 2020 at 13:43):

category.lean

/-
The associated category of a type theory

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

namespace TT

section
  variable A : type

  def closed : type β†’ term β†’ Prop := WF []

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

  def closed_term.mk (a : term) : closed A a β†’ closed_term A:= subtype.mk a

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

  def proof_eq (a₁ aβ‚‚ : closed_term A) := ⊒ (a₁ ≃ aβ‚‚)

  section equivalence_relation

  lemma proof_to_imp {Ξ“ : context} (q r) : proof Ξ“ q r β†’ proof Ξ“ ⊀ (q ⟹ r) :=
  begin
    intro h₁,
    apply proof.and_to_imp,
    apply proof.cut _ q _,
    apply proof.and_right _ ⊀ _,
    apply proof.axm,
    apply WF.and,
    exact WF.top,
    apply WF.proof_left q r,
    tidy
  end

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

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

  theorem proof_eq_trans : transitive (proof_eq A) := sorry

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

  end equivalence_relation

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

  #check TT.setoid

  local attribute [instance] TT.setoid


  def tset := quotient (TT.setoid A)

  def to_tset := quot.mk (proof_eq A)

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

  local attribute [instance] coe_term_tset

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

end

section

  variables {A B : type}

  def term_is_subset {A B : type} (Ξ± : closed_term A) (Ξ² : closed_term B) (F : closed_term 𝒫 (AΓ—Γ—B)) : Prop :=
    ⊒ F βŠ† (@set_prod A B Ξ± Ξ²)

  def is_subset {A B : type} : tset A β†’ tset B β†’ tset 𝒫 (A Γ—Γ— B) β†’ Prop := sorry

  def term_is_graph {A B: type} (F : closed_term 𝒫 (A Γ—Γ— B)) (Ξ± : closed_term A) (Ξ² : closed_term B) : Prop :=
    ⊒ βˆ€' ((𝟘 ∈ Ξ±) ⟹ (βˆƒ!' βŸͺπŸ™,𝟘⟫ ∈ F))

  def is_graph {A B: type} : tset A β†’ tset B β†’ tset 𝒫 (A Γ—Γ— B) β†’ Prop := sorry

end

end TT

namespace category_theory

  namespace TT

  open TT

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

  end TT

end category_theory

view this post on Zulip Billy Price (Jun 09 2020 at 10:49):

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

def leibniz_equal (A:type) (a₁ aβ‚‚ : term) : term := βˆ€' A ((lift 1 0 a₁) ∈ 𝟘) ⇔ ((lift 1 0 aβ‚‚) ∈ 𝟘)
infix ≃ :50 := leibniz_equal _

view this post on Zulip Mario Carneiro (Jun 09 2020 at 10:56):

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

view this post on Zulip Mario Carneiro (Jun 09 2020 at 10:57):

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

view this post on Zulip Mario Carneiro (Jun 09 2020 at 10:59):

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

view this post on Zulip Mario Carneiro (Jun 09 2020 at 10:59):

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

view this post on Zulip Mario Carneiro (Jun 09 2020 at 11:03):

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

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

view this post on Zulip Billy Price (Jun 09 2020 at 11:17):

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

view this post on Zulip Billy Price (Jun 10 2020 at 11:11):

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

/-
Definitions of a type theory

Author: Billy Price
-/

import data.finset
namespace TT

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

notation `Ξ©` := type.Omega
def Unit := type.Unit
infix `Γ—Γ—`:max := type.Prod
notation `𝒫`A :max := type.Pow A

def context := list type

inductive term : Type
| star : term
| top  : term
| bot  : term
| and  : term β†’ term β†’ term
| or   : term β†’ term β†’ term
| imp  : term β†’ term β†’ term
| elem : term β†’ term β†’ term
| pair : term β†’ term β†’ term
| var  : β„• β†’ term
| comp : type β†’ term β†’ term
| all  : type β†’ term β†’ term
| ex   : type β†’ term β†’ term

open term

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

notation `𝟘` := term.var 0
notation `πŸ™` := term.var 1
notation `𝟚` := term.var 2
notation `πŸ›` := term.var 3
notation `𝟜` := term.var 4
notation `𝟝` := term.var 5

notation `⁎` := term.star    -- input \asterisk
notation `⊀` := term.top     --       \top
notation `βŠ₯` := term.bot     -- input \bot
infixr ` ⟹ `:60 := term.imp -- input \==>
infixr ` β‹€ ` :70 := term.and -- input \And or \bigwedge
infixr ` ⋁ ` :59 := term.or  -- input \Or or \bigvee

def not (p : term) := p ⟹ βŠ₯
prefix `∼`:max := not -- input \~

def iff (p q: term) := (p ⟹ q) β‹€ (q ⟹ p)
infix ` ⇔ `:60 := iff -- input \<=>

infix ∈ := term.elem
infix βˆ‰ := Ξ» a Ξ±, not (term.elem a Ξ±)
notation `⟦ ` A ` | ` Ο† ` ⟧` := term.comp A Ο†

notation `βŸͺ` a `,` b `⟫` := term.pair a b

notation `βˆ€'` := term.all
notation `βˆƒ'` := term.ex


section substitution

  @[simp]
  def lift_d (d : β„•) : β„• β†’ term β†’ term
  | k ⁎          := ⁎
  | k ⊀          := ⊀
  | k βŠ₯          := βŠ₯
  | k (p β‹€ q)    := (lift_d k p) β‹€ (lift_d k q)
  | k (p ⋁ q)    := (lift_d k p) ⋁ (lift_d k q)
  | k (p ⟹ q)   := (lift_d k p) ⟹ (lift_d k q)
  | k (a ∈ α)    := (lift_d k a) ∈ (lift_d k α)
  | k βŸͺa,b⟫      := βŸͺlift_d k a, lift_d k b⟫
  | k (var m)    := if mβ‰₯k then var (m+d) else var m
  | k ⟦A | Ο†βŸ§     :=    ⟦A | lift_d (k+1) Ο†βŸ§
  | k (βˆ€' A Ο†)   := βˆ€' A $ lift_d (k+1) Ο†
  | k (βˆƒ' A Ο†)   := βˆƒ' A $ lift_d (k+1) Ο†

  @[simp]
  def lift := lift_d 1 0

  @[simp]
  def subst : β„• β†’ term β†’ term β†’ term
  | n x ⁎          := ⁎
  | n x ⊀          := ⊀
  | n x βŠ₯          := βŠ₯
  | n x (p β‹€ q)    := (subst n x p) β‹€ (subst n x q)
  | n x (p ⋁ q)    := (subst n x p) ⋁ (subst n x q)
  | n x (p ⟹ q)  := (subst n x p) ⟹ (subst n x q)
  | n x (a ∈ α)    := (subst n x a) ∈ (subst n x α)
  | n x βŸͺa,c⟫      := βŸͺsubst n x a, subst n x c⟫
  | n x (var m)    := if n=m then x else var m
  | n x ⟦ A | Ο† ⟧   :=    ⟦A | subst (n+1) (lift x) Ο†βŸ§
  | n x (βˆ€' A Ο†)     := βˆ€' A (subst (n+1) (lift x) Ο†)
  | n x (βˆƒ' A Ο†)     := βˆƒ' A (subst (n+1) (lift x) Ο†)

  notation  `⁅` Ο† ` // `  b `⁆` := subst 0 b Ο†

  #reduce β…πŸ˜ // ⊀ β‹€ βŠ₯⁆
  #reduce ⁅ πŸ™ // ⊀ β‹€ βŠ₯⁆

end substitution

def eq (A:type) (a₁ aβ‚‚ : term) : term := βˆ€' (𝒫 A) $ ((lift a₁) ∈ 𝟘) ⇔ ((lift aβ‚‚) ∈ 𝟘)
notation a ` ≃[`:max A `] `:0 b := eq A a b

#check eq Unit 𝟘 𝟘

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

def ex_unique (A : type) (Ο† : term) : term :=
  βˆƒ' A (⟦A | Ο†βŸ§ ≃[𝒫 A] (singleton A 𝟘))
prefix `βˆƒ!'`:2 := ex_unique

def subseteq (A : type) (Ξ± : term) (Ξ² : term) : term :=
  βˆ€' A (𝟘 ∈ Ξ±) ⟹ (𝟘 ∈ Ξ²)
notation a ` βŠ†[`:max A `] `:0 b := subseteq A a b

def term_prod {A B : type} (Ξ± Ξ² : term) : term :=
  ⟦ A Γ—Γ— B | βˆƒ' A (βˆƒ' B ((πŸ™ ∈ Ξ±) β‹€ (𝟘 ∈ Ξ²) β‹€ (eq (A Γ—Γ— B) 𝟚 βŸͺπŸ™,𝟘⟫)))⟧
notation Ξ± ` Γ—x[`:max A `] `:0 Ξ² := term_prod A Ξ± Ξ²

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

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

inductive WF : context β†’ type β†’ term β†’ Prop
| star {Ξ“}         : WF Ξ“ Unit ⁎
| top  {Ξ“}         : WF Ξ“ Ξ© ⊀
| bot  {Ξ“}         : WF Ξ“ Ξ© βŠ₯
| and  {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p β‹€ q)
| or   {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p ⋁ q)
| imp  {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p ⟹ q)
| elem {Ξ“ A a Ξ±}   : WF Ξ“ A a β†’ WF Ξ“ (𝒫 A) Ξ± β†’ WF Ξ“ Ξ© (a ∈ Ξ±)
| pair {Ξ“ A B a b} : WF Ξ“ A a β†’ WF Ξ“ B b β†’ WF Ξ“ (A Γ—Γ— B) βŸͺa,b⟫
| var  {Ξ“ A n}     : list.nth Ξ“ n = some A β†’ WF Ξ“ A (var n)
| comp {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ (𝒫 A) ⟦A | Ο†βŸ§
| all  {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ Ξ© (βˆ€' A Ο†)
| ex   {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ Ξ© (βˆƒ' A Ο†)

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

section

variable Ξ“ : context
variables p q r Ο† a b Ξ± : term
variables {A B Ξ©' : type}
-- Ξ©' is just a fake/variable version of Ξ© so we don't need to bother proving
-- that it must be Ξ© itself.'

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

@[WF_rules] lemma and_left   : WF Ξ“ Ξ©' (p β‹€ q) β†’ WF Ξ“ Ξ©' p := by WF_prover
@[WF_rules] lemma and_right  : WF Ξ“ Ξ©' (p β‹€ q) β†’ WF Ξ“ Ξ©' q := by WF_prover
@[WF_rules] lemma or_left    : WF Ξ“ Ξ©' (p ⋁ q) β†’ WF Ξ“ Ξ©' p := by WF_prover
@[WF_rules] lemma or_right   : WF Ξ“ Ξ©' (p ⋁ q) β†’ WF Ξ“ Ξ©' q := by WF_prover
@[WF_rules] lemma imp_left   : WF Ξ“ Ξ©' (p ⟹ q) β†’ WF Ξ“ Ξ©' p := by WF_prover
@[WF_rules] lemma imp_right  : WF Ξ“ Ξ©' (p ⟹ q) β†’ WF Ξ“ Ξ©' q := by WF_prover
@[WF_rules] lemma pair_left  : WF Ξ“ (A Γ—Γ— B) βŸͺa,b⟫ β†’ WF Ξ“ A a := by WF_prover
@[WF_rules] lemma pair_right : WF Ξ“ (A Γ—Γ— B) βŸͺa,b⟫ β†’ WF Ξ“ B b := by WF_prover
@[WF_rules] lemma comp_elim  : WF Ξ“ (𝒫 A) ⟦A | Ο†βŸ§ β†’ WF (A::Ξ“) Ξ© Ο† := by WF_prover
@[WF_rules] lemma all_elim   : WF Ξ“ Ξ©' (βˆ€' A Ο†) β†’ WF (A::Ξ“) Ξ©' Ο† := by WF_prover
@[WF_rules] lemma ex_elim    : WF Ξ“ Ξ©' (βˆ€' A Ο†) β†’ WF (A::Ξ“) Ξ©' Ο† := by WF_prover
@[WF_rules] lemma iff_intro : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p ⇔ q) :=
begin
  intros,
  apply_rules WF_rules,
  -- apply_rules [WF.and, WF.imp],
end

end

end TT

view this post on Zulip Reid Barton (Jun 10 2020 at 11:14):

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

view this post on Zulip Billy Price (Jun 10 2020 at 11:15):

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

view this post on Zulip Reid Barton (Jun 10 2020 at 11:16):

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

view this post on Zulip Reid Barton (Jun 10 2020 at 11:17):

oh, you just have a namespace problem actually

view this post on Zulip Reid Barton (Jun 10 2020 at 11:18):

I'm not sure what the right way to fix it is, but I would just move the attribute to the root namespace

view this post on Zulip Billy Price (Jun 10 2020 at 11:18):

outside namespace TT?

view this post on Zulip Reid Barton (Jun 10 2020 at 11:18):

right. Alternatively, call it TT.WF_rules everywhere

view this post on Zulip Billy Price (Jun 10 2020 at 11:19):

Everywhere except the definition?

view this post on Zulip Reid Barton (Jun 10 2020 at 11:21):

right, not literally in meta def WF_rules but everywhere else

view this post on Zulip Reid Barton (Jun 10 2020 at 11:21):

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

view this post on Zulip Billy Price (Jun 10 2020 at 11:26):

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

view this post on Zulip Mario Carneiro (Jun 10 2020 at 11:26):

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

view this post on Zulip Mario Carneiro (Jun 10 2020 at 11:28):

For reference: ``name goes through name resolution and is checked at tactic compile time, while `name is used as is (and so is generally checked at run time)

view this post on Zulip Billy Price (Jun 10 2020 at 11:31):

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

view this post on Zulip Billy Price (Jun 10 2020 at 11:33):

By the way apply_rules WF_rules and apply_rules TT.WF_rules both give "no matching rule", and apply_rules hsdfsfj gives unknown identifier hsdfsfj , so it seems to be recognising the object

view this post on Zulip Mario Carneiro (Jun 10 2020 at 11:34):

maybe you have no matching rule

view this post on Zulip Reid Barton (Jun 10 2020 at 11:34):

Weird. It works for me when I change all occurrences of WF_rules to TT.WF_rules except the one in meta def WF_rules

view this post on Zulip Mario Carneiro (Jun 10 2020 at 11:34):

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

view this post on Zulip Reid Barton (Jun 10 2020 at 11:34):

and once I comment out all the bad rules

view this post on Zulip Mario Carneiro (Jun 10 2020 at 11:35):

so ``WF_rules is equivalent to `TT.WF_rules except that it will give an error if WF_rules can't be found

view this post on Zulip Billy Price (Jun 10 2020 at 11:41):

I can't get anything working here's the most updated version of what I've got, as soon as I change any instances of WF_rules to TT.WF_rules it doesn't recognise it, and the usage in the actual proof is ambilavent to TT.. However apply_rules [WF.and, WF.imp] works fine.

/-
Definitions of a type theory

Author: Billy Price
-/

import data.finset
namespace TT

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

notation `Ξ©` := type.Omega
def Unit := type.Unit
infix `Γ—Γ—`:max := type.Prod
notation `𝒫`A :max := type.Pow A

def context := list type

inductive term : Type
| star : term
| top  : term
| bot  : term
| and  : term β†’ term β†’ term
| or   : term β†’ term β†’ term
| imp  : term β†’ term β†’ term
| elem : term β†’ term β†’ term
| pair : term β†’ term β†’ term
| var  : β„• β†’ term
| comp : type β†’ term β†’ term
| all  : type β†’ term β†’ term
| ex   : type β†’ term β†’ term

open term

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

notation `𝟘` := term.var 0
notation `πŸ™` := term.var 1
notation `𝟚` := term.var 2
notation `πŸ›` := term.var 3
notation `𝟜` := term.var 4
notation `𝟝` := term.var 5

notation `⁎` := term.star    -- input \asterisk
notation `⊀` := term.top     --       \top
notation `βŠ₯` := term.bot     -- input \bot
infixr ` ⟹ `:60 := term.imp -- input \==>
infixr ` β‹€ ` :70 := term.and -- input \And or \bigwedge
infixr ` ⋁ ` :59 := term.or  -- input \Or or \bigvee

def not (p : term) := p ⟹ βŠ₯
prefix `∼`:max := not -- input \~

def iff (p q: term) := (p ⟹ q) β‹€ (q ⟹ p)
infix ` ⇔ `:60 := iff -- input \<=>

infix ∈ := term.elem
infix βˆ‰ := Ξ» a Ξ±, not (term.elem a Ξ±)
notation `⟦ ` A ` | ` Ο† ` ⟧` := term.comp A Ο†

notation `βŸͺ` a `,` b `⟫` := term.pair a b

notation `βˆ€'` := term.all
notation `βˆƒ'` := term.ex


section substitution

  @[simp]
  def lift_d (d : β„•) : β„• β†’ term β†’ term
  | k ⁎          := ⁎
  | k ⊀          := ⊀
  | k βŠ₯          := βŠ₯
  | k (p β‹€ q)    := (lift_d k p) β‹€ (lift_d k q)
  | k (p ⋁ q)    := (lift_d k p) ⋁ (lift_d k q)
  | k (p ⟹ q)   := (lift_d k p) ⟹ (lift_d k q)
  | k (a ∈ α)    := (lift_d k a) ∈ (lift_d k α)
  | k βŸͺa,b⟫      := βŸͺlift_d k a, lift_d k b⟫
  | k (var m)    := if mβ‰₯k then var (m+d) else var m
  | k ⟦A | Ο†βŸ§     :=    ⟦A | lift_d (k+1) Ο†βŸ§
  | k (βˆ€' A Ο†)   := βˆ€' A $ lift_d (k+1) Ο†
  | k (βˆƒ' A Ο†)   := βˆƒ' A $ lift_d (k+1) Ο†

  @[simp]
  def lift := lift_d 1 0

  @[simp]
  def subst : β„• β†’ term β†’ term β†’ term
  | n x ⁎          := ⁎
  | n x ⊀          := ⊀
  | n x βŠ₯          := βŠ₯
  | n x (p β‹€ q)    := (subst n x p) β‹€ (subst n x q)
  | n x (p ⋁ q)    := (subst n x p) ⋁ (subst n x q)
  | n x (p ⟹ q)  := (subst n x p) ⟹ (subst n x q)
  | n x (a ∈ α)    := (subst n x a) ∈ (subst n x α)
  | n x βŸͺa,c⟫      := βŸͺsubst n x a, subst n x c⟫
  | n x (var m)    := if n=m then x else var m
  | n x ⟦ A | Ο† ⟧   :=    ⟦A | subst (n+1) (lift x) Ο†βŸ§
  | n x (βˆ€' A Ο†)     := βˆ€' A (subst (n+1) (lift x) Ο†)
  | n x (βˆƒ' A Ο†)     := βˆƒ' A (subst (n+1) (lift x) Ο†)

  notation  `⁅` Ο† ` // `  b `⁆` := subst 0 b Ο†

  #reduce β…πŸ˜ // ⊀ β‹€ βŠ₯⁆
  #reduce ⁅ πŸ™ // ⊀ β‹€ βŠ₯⁆

end substitution

def eq (A:type) (a₁ aβ‚‚ : term) : term := βˆ€' (𝒫 A) $ ((lift a₁) ∈ 𝟘) ⇔ ((lift aβ‚‚) ∈ 𝟘)
notation a ` ≃[`:max A `] `:0 b := eq A a b

#check eq Unit 𝟘 𝟘

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

def ex_unique (A : type) (Ο† : term) : term :=
  βˆƒ' A (⟦A | Ο†βŸ§ ≃[𝒫 A] (singleton A 𝟘))
prefix `βˆƒ!'`:2 := ex_unique

def subseteq (A : type) (Ξ± : term) (Ξ² : term) : term :=
  βˆ€' A (𝟘 ∈ Ξ±) ⟹ (𝟘 ∈ Ξ²)
notation a ` βŠ†[`:max A `] `:0 b := subseteq A a b

def term_prod {A B : type} (Ξ± Ξ² : term) : term :=
  ⟦ A Γ—Γ— B | βˆƒ' A (βˆƒ' B ((πŸ™ ∈ Ξ±) β‹€ (𝟘 ∈ Ξ²) β‹€ (eq (A Γ—Γ— B) 𝟚 βŸͺπŸ™,𝟘⟫)))⟧
notation Ξ± ` Γ—x[`:max A `] `:0 Ξ² := term_prod A Ξ± Ξ²

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

inductive WF : context β†’ type β†’ term β†’ Prop
| star {Ξ“}         : WF Ξ“ Unit ⁎
| top  {Ξ“}         : WF Ξ“ Ξ© ⊀
| bot  {Ξ“}         : WF Ξ“ Ξ© βŠ₯
| and  {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p β‹€ q)
| or   {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p ⋁ q)
| imp  {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p ⟹ q)
| elem {Ξ“ A a Ξ±}   : WF Ξ“ A a β†’ WF Ξ“ (𝒫 A) Ξ± β†’ WF Ξ“ Ξ© (a ∈ Ξ±)
| pair {Ξ“ A B a b} : WF Ξ“ A a β†’ WF Ξ“ B b β†’ WF Ξ“ (A Γ—Γ— B) βŸͺa,b⟫
| var  {Ξ“ A n}     : list.nth Ξ“ n = some A β†’ WF Ξ“ A (var n)
| comp {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ (𝒫 A) ⟦A | Ο†βŸ§
| all  {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ Ξ© (βˆ€' A Ο†)
| ex   {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ Ξ© (βˆƒ' A Ο†)



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

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


section

variable Ξ“ : context
variables p q r Ο† a b Ξ± : term
variables {A B Ξ©' : type}
-- Ξ©' is just a fake/variable version of Ξ© so we don't need to bother proving
-- that it must be Ξ© itself.'

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

lemma WF.and_left   : WF Ξ“ Ξ©' (p β‹€ q) β†’ WF Ξ“ Ξ©' p := by WF_prover
lemma WF.and_right  : WF Ξ“ Ξ©' (p β‹€ q) β†’ WF Ξ“ Ξ©' q := by WF_prover
lemma WF.or_left    : WF Ξ“ Ξ©' (p ⋁ q) β†’ WF Ξ“ Ξ©' p := by WF_prover
lemma WF.or_right   : WF Ξ“ Ξ©' (p ⋁ q) β†’ WF Ξ“ Ξ©' q := by WF_prover
lemma WF.imp_left   : WF Ξ“ Ξ©' (p ⟹ q) β†’ WF Ξ“ Ξ©' p := by WF_prover
lemma WF.imp_right  : WF Ξ“ Ξ©' (p ⟹ q) β†’ WF Ξ“ Ξ©' q := by WF_prover
lemma WF.pair_left  : WF Ξ“ (A Γ—Γ— B) βŸͺa,b⟫ β†’ WF Ξ“ A a := by WF_prover
lemma WF.pair_right : WF Ξ“ (A Γ—Γ— B) βŸͺa,b⟫ β†’ WF Ξ“ B b := by WF_prover
lemma WF.comp_elim  : WF Ξ“ (𝒫 A) ⟦A | Ο†βŸ§ β†’ WF (A::Ξ“) Ξ© Ο† := by WF_prover
lemma WF.all_elim   : WF Ξ“ Ξ©' (βˆ€' A Ο†) β†’ WF (A::Ξ“) Ξ©' Ο† := by WF_prover
lemma WF.ex_elim    : WF Ξ“ Ξ©' (βˆ€' A Ο†) β†’ WF (A::Ξ“) Ξ©' Ο† := by WF_prover
@[WF_rules] lemma WF.iff_intro : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p ⇔ q) :=
begin
  intros,
  apply_rules WF_rules,
  -- apply_rules [WF.and, WF.imp],
end

end

end TT

view this post on Zulip Billy Price (Jun 10 2020 at 11:41):

Could you paste what you got working @Reid Barton ?

view this post on Zulip Reid Barton (Jun 10 2020 at 11:44):

/-
Definitions of a type theory

Author: Billy Price
-/

import data.finset
namespace TT

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

notation `Ξ©` := type.Omega
def Unit := type.Unit
infix `Γ—Γ—`:max := type.Prod
notation `𝒫`A :max := type.Pow A

def context := list type

inductive term : Type
| star : term
| top  : term
| bot  : term
| and  : term β†’ term β†’ term
| or   : term β†’ term β†’ term
| imp  : term β†’ term β†’ term
| elem : term β†’ term β†’ term
| pair : term β†’ term β†’ term
| var  : β„• β†’ term
| comp : type β†’ term β†’ term
| all  : type β†’ term β†’ term
| ex   : type β†’ term β†’ term

open term

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

notation `𝟘` := term.var 0
notation `πŸ™` := term.var 1
notation `𝟚` := term.var 2
notation `πŸ›` := term.var 3
notation `𝟜` := term.var 4
notation `𝟝` := term.var 5

notation `⁎` := term.star    -- input \asterisk
notation `⊀` := term.top     --       \top
notation `βŠ₯` := term.bot     -- input \bot
infixr ` ⟹ `:60 := term.imp -- input \==>
infixr ` β‹€ ` :70 := term.and -- input \And or \bigwedge
infixr ` ⋁ ` :59 := term.or  -- input \Or or \bigvee

def not (p : term) := p ⟹ βŠ₯
prefix `∼`:max := not -- input \~

def iff (p q: term) := (p ⟹ q) β‹€ (q ⟹ p)
infix ` ⇔ `:60 := iff -- input \<=>

infix ∈ := term.elem
infix βˆ‰ := Ξ» a Ξ±, not (term.elem a Ξ±)
notation `⟦ ` A ` | ` Ο† ` ⟧` := term.comp A Ο†

notation `βŸͺ` a `,` b `⟫` := term.pair a b

notation `βˆ€'` := term.all
notation `βˆƒ'` := term.ex


section substitution

  @[simp]
  def lift_d (d : β„•) : β„• β†’ term β†’ term
  | k ⁎          := ⁎
  | k ⊀          := ⊀
  | k βŠ₯          := βŠ₯
  | k (p β‹€ q)    := (lift_d k p) β‹€ (lift_d k q)
  | k (p ⋁ q)    := (lift_d k p) ⋁ (lift_d k q)
  | k (p ⟹ q)   := (lift_d k p) ⟹ (lift_d k q)
  | k (a ∈ α)    := (lift_d k a) ∈ (lift_d k α)
  | k βŸͺa,b⟫      := βŸͺlift_d k a, lift_d k b⟫
  | k (var m)    := if mβ‰₯k then var (m+d) else var m
  | k ⟦A | Ο†βŸ§     :=    ⟦A | lift_d (k+1) Ο†βŸ§
  | k (βˆ€' A Ο†)   := βˆ€' A $ lift_d (k+1) Ο†
  | k (βˆƒ' A Ο†)   := βˆƒ' A $ lift_d (k+1) Ο†

  @[simp]
  def lift := lift_d 1 0

  @[simp]
  def subst : β„• β†’ term β†’ term β†’ term
  | n x ⁎          := ⁎
  | n x ⊀          := ⊀
  | n x βŠ₯          := βŠ₯
  | n x (p β‹€ q)    := (subst n x p) β‹€ (subst n x q)
  | n x (p ⋁ q)    := (subst n x p) ⋁ (subst n x q)
  | n x (p ⟹ q)  := (subst n x p) ⟹ (subst n x q)
  | n x (a ∈ α)    := (subst n x a) ∈ (subst n x α)
  | n x βŸͺa,c⟫      := βŸͺsubst n x a, subst n x c⟫
  | n x (var m)    := if n=m then x else var m
  | n x ⟦ A | Ο† ⟧   :=    ⟦A | subst (n+1) (lift x) Ο†βŸ§
  | n x (βˆ€' A Ο†)     := βˆ€' A (subst (n+1) (lift x) Ο†)
  | n x (βˆƒ' A Ο†)     := βˆƒ' A (subst (n+1) (lift x) Ο†)

  notation  `⁅` Ο† ` // `  b `⁆` := subst 0 b Ο†

  #reduce β…πŸ˜ // ⊀ β‹€ βŠ₯⁆
  #reduce ⁅ πŸ™ // ⊀ β‹€ βŠ₯⁆

end substitution

def eq (A:type) (a₁ aβ‚‚ : term) : term := βˆ€' (𝒫 A) $ ((lift a₁) ∈ 𝟘) ⇔ ((lift aβ‚‚) ∈ 𝟘)
notation a ` ≃[`:max A `] `:0 b := eq A a b

#check eq Unit 𝟘 𝟘

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

def ex_unique (A : type) (Ο† : term) : term :=
  βˆƒ' A (⟦A | Ο†βŸ§ ≃[𝒫 A] (singleton A 𝟘))
prefix `βˆƒ!'`:2 := ex_unique

def subseteq (A : type) (Ξ± : term) (Ξ² : term) : term :=
  βˆ€' A (𝟘 ∈ Ξ±) ⟹ (𝟘 ∈ Ξ²)
notation a ` βŠ†[`:max A `] `:0 b := subseteq A a b

def term_prod {A B : type} (Ξ± Ξ² : term) : term :=
  ⟦ A Γ—Γ— B | βˆƒ' A (βˆƒ' B ((πŸ™ ∈ Ξ±) β‹€ (𝟘 ∈ Ξ²) β‹€ (eq (A Γ—Γ— B) 𝟚 βŸͺπŸ™,𝟘⟫)))⟧
notation Ξ± ` Γ—x[`:max A `] `:0 Ξ² := term_prod A Ξ± Ξ²

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

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

inductive WF : context β†’ type β†’ term β†’ Prop
| star {Ξ“}         : WF Ξ“ Unit ⁎
| top  {Ξ“}         : WF Ξ“ Ξ© ⊀
| bot  {Ξ“}         : WF Ξ“ Ξ© βŠ₯
| and  {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p β‹€ q)
| or   {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p ⋁ q)
| imp  {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p ⟹ q)
| elem {Ξ“ A a Ξ±}   : WF Ξ“ A a β†’ WF Ξ“ (𝒫 A) Ξ± β†’ WF Ξ“ Ξ© (a ∈ Ξ±)
| pair {Ξ“ A B a b} : WF Ξ“ A a β†’ WF Ξ“ B b β†’ WF Ξ“ (A Γ—Γ— B) βŸͺa,b⟫
| var  {Ξ“ A n}     : list.nth Ξ“ n = some A β†’ WF Ξ“ A (var n)
| comp {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ (𝒫 A) ⟦A | Ο†βŸ§
| all  {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ Ξ© (βˆ€' A Ο†)
| ex   {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ Ξ© (βˆƒ' A Ο†)

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

section

variable Ξ“ : context
variables p q r Ο† a b Ξ± : term
variables {A B Ξ©' : type}
-- Ξ©' is just a fake/variable version of Ξ© so we don't need to bother proving
-- that it must be Ξ© itself.'

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

/-
@[TT.WF_rules] lemma and_left   : WF Ξ“ Ξ©' (p β‹€ q) β†’ WF Ξ“ Ξ©' p := by WF_prover
@[TT.WF_rules] lemma and_right  : WF Ξ“ Ξ©' (p β‹€ q) β†’ WF Ξ“ Ξ©' q := by WF_prover
@[TT.WF_rules] lemma or_left    : WF Ξ“ Ξ©' (p ⋁ q) β†’ WF Ξ“ Ξ©' p := by WF_prover
@[TT.WF_rules] lemma or_right   : WF Ξ“ Ξ©' (p ⋁ q) β†’ WF Ξ“ Ξ©' q := by WF_prover
@[TT.WF_rules] lemma imp_left   : WF Ξ“ Ξ©' (p ⟹ q) β†’ WF Ξ“ Ξ©' p := by WF_prover
@[TT.WF_rules] lemma imp_right  : WF Ξ“ Ξ©' (p ⟹ q) β†’ WF Ξ“ Ξ©' q := by WF_prover
@[TT.WF_rules] lemma pair_left  : WF Ξ“ (A Γ—Γ— B) βŸͺa,b⟫ β†’ WF Ξ“ A a := by WF_prover
@[TT.WF_rules] lemma pair_right : WF Ξ“ (A Γ—Γ— B) βŸͺa,b⟫ β†’ WF Ξ“ B b := by WF_prover
@[TT.WF_rules] lemma comp_elim  : WF Ξ“ (𝒫 A) ⟦A | Ο†βŸ§ β†’ WF (A::Ξ“) Ξ© Ο† := by WF_prover
@[TT.WF_rules] lemma all_elim   : WF Ξ“ Ξ©' (βˆ€' A Ο†) β†’ WF (A::Ξ“) Ξ©' Ο† := by WF_prover
@[TT.WF_rules] lemma ex_elim    : WF Ξ“ Ξ©' (βˆ€' A Ο†) β†’ WF (A::Ξ“) Ξ©' Ο† := by WF_prover
-/
@[TT.WF_rules] lemma iff_intro : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p ⇔ q) :=
begin
  intros,
  apply_rules TT.WF_rules,
  -- apply_rules [WF.and, WF.imp],
end

end

end TT

view this post on Zulip Billy Price (Jun 10 2020 at 11:45):

Oh you change the name too

view this post on Zulip Reid Barton (Jun 10 2020 at 11:46):

By the way, I noticed earlier that the interactive parser for apply_rules is a little weird--it expects an identifier, but it doesn't actually use it as an identifier, it uses it as an attribute name.

view this post on Zulip Reid Barton (Jun 10 2020 at 11:46):

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

view this post on Zulip Reid Barton (Jun 10 2020 at 11:47):

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

view this post on Zulip Billy Price (Jun 10 2020 at 12:30):

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

@[TT.WF_rules] lemma WF.lift : WF Ξ“ A a β†’ WF (B::Ξ“) A (lift a) :=
begin
  intro wfa,
  induction wfa,
  case WF.all : Ξ” A ψ wfψ ih {simp, apply_rules WF_rules, sorry},
  case WF.ex : Ξ” A ψ wfψ ih {simp, apply_rules WF_rules, sorry},
  case WF.comp : Ξ” A ψ wfψ ih {simp, apply_rules WF_rules, sorry},
  all_goals {unfold lift, unfold lift_d, apply_rules WF_rules},
end

Here's the state at the first sorry.

1 goal
B : type,
Ξ“ : context,
A : type,
a : term,
Ξ” : list type,
A : type,
ψ : term,
wfψ : WF (A :: Ξ”) Ξ© ψ,
ih : WF (B :: A :: Ξ”) Ξ© (lift ψ)
⊒ WF (A :: B :: Ξ”) Ξ© (lift_d 1 1 ψ)

view this post on Zulip Mario Carneiro (Jun 10 2020 at 12:31):

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

view this post on Zulip Mario Carneiro (Jun 10 2020 at 12:31):

you have to prove the analogous theorem for lift_d

view this post on Zulip Billy Price (Jun 10 2020 at 12:34):

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

view this post on Zulip Mario Carneiro (Jun 10 2020 at 12:34):

Since you are holding d fixed in the definition of lift_d, you can probably prove it in the special case d = 1

view this post on Zulip Mario Carneiro (Jun 10 2020 at 12:35):

but you definitely have to generalize k

view this post on Zulip Mario Carneiro (Jun 10 2020 at 12:35):

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

view this post on Zulip Billy Price (Jun 10 2020 at 12:37):

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

view this post on Zulip Mario Carneiro (Jun 10 2020 at 12:39):

I think it looks something like this:

lemma WF.lift_d : βˆ€ K D Ξ“ A a, length K = k β†’ length D = d β†’ WF (K ++ Ξ“) (A) a β†’ WF (K ++ D ++ Ξ“) A (lift_d d k a) :=
sorry

view this post on Zulip Mario Carneiro (Jun 10 2020 at 12:40):

since you aren't inducting on k or d you can also simplify this to

lemma WF.lift_d : βˆ€ K D Ξ“ A a, WF (K ++ Ξ“) (A) a β†’ WF (K ++ D ++ Ξ“) A (lift_d (length D) (length K) a) :=
sorry

view this post on Zulip Billy Price (Jun 10 2020 at 12:45):

Yep that makes sense to me

view this post on Zulip Billy Price (Jun 10 2020 at 12:53):

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

1 goal
K Ξ” Ξ“ : context,
A : type,
a : term,
Ξ” : list type,
B : type,
ψ : term,
wfψ : WF (B :: Ξ”) Ξ© ψ,
ih : WF (K ++ Ξ” ++ Ξ“) Ξ© (lift_d (length Ξ”) (length K) ψ)
⊒ WF (B :: (K ++ Ξ” ++ Ξ“)) Ξ© (lift_d (length Ξ”) (length K + 1) ψ)

view this post on Zulip Mario Carneiro (Jun 10 2020 at 12:54):

How did you start the proof?

view this post on Zulip Mario Carneiro (Jun 10 2020 at 12:54):

You need generalizing K at least

view this post on Zulip Billy Price (Jun 10 2020 at 12:54):

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

view this post on Zulip Mario Carneiro (Jun 10 2020 at 12:56):

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

view this post on Zulip Mario Carneiro (Jun 10 2020 at 12:57):

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

view this post on Zulip Billy Price (Jun 10 2020 at 12:58):

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

view this post on Zulip Mario Carneiro (Jun 10 2020 at 12:59):

K needs to be forall-quantified in the inductive hypothesis

view this post on Zulip Mario Carneiro (Jun 10 2020 at 12:59):

That was the problem with your stuck goal, if K was generalized in ih then you could have instantiated K to B :: K

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:01):

Another way to put it is, we expect that K will change over the course of the induction, while Ξ” and Ξ“ for instance don't need to change

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:01):

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

view this post on Zulip Billy Price (Jun 10 2020 at 13:03):

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

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:03):

right of the colon in the inductive statement

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:04):

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

view this post on Zulip Billy Price (Jun 10 2020 at 13:05):

yep, context, type and term?

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:05):

right

view this post on Zulip Billy Price (Jun 10 2020 at 13:06):

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

view this post on Zulip Billy Price (Jun 10 2020 at 13:07):

Because the context is an append of two contexts?

view this post on Zulip Billy Price (Jun 10 2020 at 13:07):

So it can't do it?

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:08):

If you leave a composed expression in an index when you do induction, it will silently generalize it, losing the connection to the original expression

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:09):

That is, it tries to prove WF Ξ“' A a β†’ WF (K ++ Ξ” ++ Ξ“) A (lift_d (length Ξ”) (length K) a), which won't be provable because K is gone from the left side

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:10):

If you do generalize e : K ++ Ξ“ = Ξ“' then it is instead proving WF Ξ“' A a β†’ \forall K, K ++ Ξ“ = Ξ“' -> WF (K ++ Ξ” ++ Ξ“) A (lift_d (length Ξ”) (length K) a) which is okay

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:11):

(technically indices aren't generalized in the sense of generalizing, they are handled specially because they participate directly in the statement of the recursor)

view this post on Zulip Billy Price (Jun 10 2020 at 13:16):

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

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

this is my state for the first sorry

1 goal
Ξ” Ξ“ : context,
Ξ“' : list type,
A : type,
a : term,
K : context,
K' : list type,
e : K' = Ξ“',
A' : type,
ψ : term,
wfψ : WF (A' :: K') Ω ψ,
ih : A' :: K' = Ξ“' β†’ βˆ€ (K : context), WF (K ++ Ξ” ++ Ξ“) Ξ© (lift_d (length Ξ”) (length K) ψ)
⊒ WF (A' :: (K ++ Ξ” ++ Ξ“)) Ξ© (lift_d (length Ξ”) (length K + 1) ψ)

view this post on Zulip Billy Price (Jun 10 2020 at 13:17):

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

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:19):

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

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:20):

K' is just Ξ“'

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:21):

but that inductive hypothesis does look like bad news

view this post on Zulip Billy Price (Jun 10 2020 at 13:21):

Oh right I got the renaming wrong.

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:21):

what is the state before induction

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:23):

Ah, I think I know what happened; wfa is in the context so generalize won't hit it and it is useless (it just adds a useless equality to the context)

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:23):

Use generalize_hyp e : K ++ Ξ“ = Ξ“' at wfa,

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:24):

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

view this post on Zulip Billy Price (Jun 10 2020 at 13:24):

Yep that makes sense

view this post on Zulip Billy Price (Jun 10 2020 at 13:29):

Now we're here

@[TT.WF_rules] lemma WF.lift_d (K Ξ” Ξ“ : context) : WF (K ++ Ξ“) A a β†’ WF (K ++ Ξ” ++ Ξ“) A (lift_d (length Ξ”) (length K) a) :=
begin
  intro wfa,
  generalize_hyp e : K ++ Ξ“ = Ξ“' at wfa,
  induction wfa generalizing K,
  case WF.all : Ξ“' A' ψ wfψ ih {subst e, constructor,},
  case WF.ex : Ξ“' A' ψ wfψ ih {constructor, sorry},
  case WF.comp : Ξ“' A' ψ wfψ ih {constructor, sorry},
  any_goals {unfold lift_d, apply_rules WF_rules},
end
1 goal
Ξ” Ξ“ : context,
Ξ“' : list type,
A : type,
a : term,
K : context,
A' : type,
ψ : term,
wfψ : WF (A' :: (K ++ Ξ“)) Ξ© ψ,
ih : βˆ€ (K_1 : context), K_1 ++ Ξ“ = A' :: (K ++ Ξ“) β†’ WF (K_1 ++ Ξ” ++ Ξ“) Ξ© (lift_d (length Ξ”) (length K_1) ψ)
⊒ WF (A' :: (K ++ Ξ” ++ Ξ“)) Ξ© (lift_d (length Ξ”) (length K + 1) ψ)

view this post on Zulip Billy Price (Jun 10 2020 at 13:30):

That's the state after constructor,. I put the subst e, inside the case because applying it do all the inductive cases via induction wfa generalizing K; subst e anonymised the goals so I couldn't name a case anymore.

view this post on Zulip Billy Price (Jun 10 2020 at 13:33):

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

invalid apply tactic, failed to unify
  WF (A' :: (K ++ Ξ” ++ Ξ“)) Ξ© (lift_d (length Ξ”) (length K + 1) ψ)
with
  WF (?m_1 ++ Ξ” ++ Ξ“) Ξ© (lift_d (length Ξ”) (length ?m_1) ψ)

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:39):

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

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:41):

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

view this post on Zulip Billy Price (Jun 10 2020 at 13:47):

oh okay, I was aware of exact but not refine. Though reading it now I don't quite see the importance - what do you mean by "they have the expected type"?

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:48):

whaaat refine is the best tactic

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:48):

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

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:49):

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

view this post on Zulip Billy Price (Jun 10 2020 at 13:52):

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

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:52):

anything using structure constructor brackets for example

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:54):

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

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:56):

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

view this post on Zulip Billy Price (Jun 10 2020 at 13:56):

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

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:57):

no, I wrote what I meant

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:57):

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

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:57):

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

view this post on Zulip Mario Carneiro (Jun 10 2020 at 13:58):

and it would still fail

view this post on Zulip Billy Price (Jun 10 2020 at 13:58):

Oh sorry I interpreted it wrong

view this post on Zulip Billy Price (Jun 10 2020 at 14:01):

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

view this post on Zulip Mario Carneiro (Jun 10 2020 at 14:02):

You can use exact ih K

view this post on Zulip Mario Carneiro (Jun 10 2020 at 14:02):

or apply ih if it works

view this post on Zulip Mario Carneiro (Jun 10 2020 at 14:03):

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

view this post on Zulip Billy Price (Jun 10 2020 at 14:03):

Some of them have multiple inductive hypotheses

view this post on Zulip Mario Carneiro (Jun 10 2020 at 14:04):

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

view this post on Zulip Mario Carneiro (Jun 10 2020 at 14:05):

or try { ... }

view this post on Zulip Mario Carneiro (Jun 10 2020 at 14:05):

probably some higher level thing like solve_by_elim works too

view this post on Zulip Billy Price (Jun 10 2020 at 14:07):

But how would I name the inductive hypotheses like that?

view this post on Zulip Billy Price (Jun 10 2020 at 14:07):

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

view this post on Zulip Billy Price (Jun 10 2020 at 14:49):

I'm now proving an equality using list.nth, and I want to use theorems that talk about list.nth_le. I haven't seen any theorems converting between the two.

view this post on Zulip Billy Price (Jun 10 2020 at 14:53):

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

view this post on Zulip Kevin Buzzard (Jun 10 2020 at 15:02):

An MSc student of mine found a lot of missing lemmas about nth and nth_le. Her repo is now public so maybe there is some stuff here https://github.com/ImperialCollegeLondon/dots_and_boxes/tree/master/src/list/lemmas which is of some use. Note that the repo uses Lean 3.4.2.

view this post on Zulip Mario Carneiro (Jun 10 2020 at 15:09):

There is one key theorem called something like nth_le_nth

view this post on Zulip Mario Carneiro (Jun 10 2020 at 15:09):

^ that

view this post on Zulip Mario Carneiro (Jun 10 2020 at 15:09):

also nth_eq_some

view this post on Zulip Kevin Buzzard (Jun 10 2020 at 15:09):

My student needed some nth_le_append lemmas

view this post on Zulip Kevin Buzzard (Jun 10 2020 at 15:10):

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

view this post on Zulip Mario Carneiro (Jun 10 2020 at 15:10):

I see nth_le_append and nth_le_append_right

view this post on Zulip Mario Carneiro (Jun 10 2020 at 15:11):

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

view this post on Zulip Kevin Buzzard (Jun 10 2020 at 15:12):

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

view this post on Zulip Billy Price (Jun 11 2020 at 07:50):

Thanks for the help, I'm gonna bookmark that proof for now. I have a thing called tset : type -> Type, so if A : type, then tset A is basically a closed term of type PA, and I'd like to form a category of all such tsets of all types. But if I say instance category : small_category (Ξ  A : type, tset A) are the objects in that category elements of Type tset A for some A, or are they indexed families of tsets, which are indexed by the elements of type?

view this post on Zulip Billy Price (Jun 11 2020 at 07:51):

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

view this post on Zulip Billy Price (Jun 11 2020 at 08:05):

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

def foo: Type
def bar : β„• -> foo
def baz := Ξ  n : β„•, bar n

what is an f : baz? Is it an indexed family of foo's (via bar) or is it a bar n : foo for some n? What is the type of all bar n for any n? My best idea is a subtype of foo where any a in the subtype has βˆƒ n : β„•, bar n == a, but that seems too implicit. I'd like to say maybe pairs of the form <n,bar n>?

view this post on Zulip Billy Price (Jun 11 2020 at 08:12):

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

view this post on Zulip David WΓ€rn (Jun 11 2020 at 08:16):

An element of \Sigma A : type, tset A would be a "pointed type" - - are these really the objects you want for your category?

view this post on Zulip David WΓ€rn (Jun 11 2020 at 08:17):

In category C, C is just the type of "abstract objects". An element of C does not need to have any internal structure - - it is just a label. Maybe here you want C to be just type? Then you can define Hom-sets however you like

view this post on Zulip Kevin Buzzard (Jun 11 2020 at 08:35):

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

view this post on Zulip Kevin Buzzard (Jun 11 2020 at 08:36):

baz doesn't make sense. It looks like it's going to be a function which eats a natural n and returns a term of type bar n, but bar n isn't a type.

view this post on Zulip Kevin Buzzard (Jun 11 2020 at 08:37):

def foo: Type := sorry
def bar : β„• -> foo := sorry
def baz := Ξ  n : β„•, bar n -- error -- type expected at bar n

view this post on Zulip Billy Price (Jun 11 2020 at 08:42):

David WΓ€rn said:

An element of \Sigma A : type, tset A would be a "pointed type" - - are these really the objects you want for your category?

Yep, I'm not forming the typical category of types. Closer to the category of sets. My objects are terms Ξ± : term such that WF [] (P A) Ξ±, that is, Ξ± is a well-formed term in the empty context (it's closed) "of type (P A)", where P: type -> type is thought of as the powerset of a type. My morphisms are terms which look like the graph of a function between two such "subsets of a type".

@Kevin Buzzard I must have confused myself in translating to that example. I might reattempt, but I think Ξ£ A : type, tset A is what I was looking for, where tset is defined like this

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

The related definitions to what I'm doing appear here
https://leanprover.zulipchat.com/#narrow/stream/236446-Type-theory/topic/Modelling.20a.20Type.20Theory.20in.20Lean/near/200405009

view this post on Zulip Kevin Buzzard (Jun 11 2020 at 08:44):

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

view this post on Zulip Billy Price (Jun 11 2020 at 08:54):

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

view this post on Zulip Billy Price (Jun 11 2020 at 11:26):

How come cases recognises whenever a constructor couldn't possibly produce the target, but induction doesn't? I always end up with absurd cases to prove with induction.

view this post on Zulip Mario Carneiro (Jun 11 2020 at 11:27):

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

view this post on Zulip Billy Price (Jun 11 2020 at 11:31):

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

view this post on Zulip Mario Carneiro (Jun 11 2020 at 11:31):

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

view this post on Zulip Mario Carneiro (Jun 11 2020 at 11:31):

the point is that just because you are inducting on foo (C1 t), doesn't mean that every subterm of C1 t is also of the form C1 t

view this post on Zulip Mario Carneiro (Jun 11 2020 at 11:32):

so although you may be able to eliminate case C2 at the top level, when you go around the recursion once you won't be able to skip the C2 case anymore

view this post on Zulip Billy Price (Jun 11 2020 at 11:33):

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

view this post on Zulip Mario Carneiro (Jun 11 2020 at 11:34):

If you want to explicitly say that an index is fixed, for example you are proving something about terms in the empty context and don't mind that the inductive hypothesis of WF.all doesn't apply, then you can explicitly generalize it before and eliminate it after using generalize_hyp e : Gamma = [] at wf, induction wf; cases e,

view this post on Zulip Billy Price (Jun 11 2020 at 11:37):

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

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

notation `Ξ©` := type.Omega
def Unit := type.Unit
infix `Γ—Γ—`:max := type.Prod
notation `𝒫`A :max := type.Pow A

def context := list type

inductive term : Type
| star : term
| top  : term
| bot  : term
| and  : term β†’ term β†’ term
| or   : term β†’ term β†’ term
| imp  : term β†’ term β†’ term
| elem : term β†’ term β†’ term
| pair : term β†’ term β†’ term
| var  : β„• β†’ term
| comp : type β†’ term β†’ term
| all  : type β†’ term β†’ term
| ex   : type β†’ term β†’ term

open term

notation `𝟘` := term.var 0
notation `πŸ™` := term.var 1
notation `𝟚` := term.var 2
notation `πŸ›` := term.var 3
notation `𝟜` := term.var 4
notation `𝟝` := term.var 5

notation `⁎` := term.star    -- input \asterisk
notation `⊀` := term.top     --       \top
notation `βŠ₯` := term.bot     -- input \bot
infixr ` ⟹ `:60 := term.imp -- input \==>
infixr ` β‹€ ` :70 := term.and -- input \And or \bigwedge
infixr ` ⋁ ` :59 := term.or  -- input \Or or \bigvee

infix ∈ := term.elem
infix βˆ‰ := Ξ» a Ξ±, not (term.elem a Ξ±)
notation `⟦ ` A ` | ` Ο† ` ⟧` := term.comp A Ο†

notation `βŸͺ` a `,` b `⟫` := term.pair a b

notation `βˆ€'` := term.all
notation `βˆƒ'` := term.ex

inductive WF : context β†’ type β†’ term β†’ Prop
| star {Ξ“}         : WF Ξ“ Unit ⁎
| top  {Ξ“}         : WF Ξ“ Ξ© ⊀
| bot  {Ξ“}         : WF Ξ“ Ξ© βŠ₯
| and  {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p β‹€ q)
| or   {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p ⋁ q)
| imp  {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p ⟹ q)
| elem {Ξ“ A a Ξ±}   : WF Ξ“ A a β†’ WF Ξ“ (𝒫 A) Ξ± β†’ WF Ξ“ Ξ© (a ∈ Ξ±)
| pair {Ξ“ A B a b} : WF Ξ“ A a β†’ WF Ξ“ B b β†’ WF Ξ“ (A Γ—Γ— B) βŸͺa,b⟫
| var  {Ξ“ A n}     : list.nth Ξ“ n = some A β†’ WF Ξ“ A (var n)
| comp {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ (𝒫 A) ⟦A | Ο†βŸ§
| all  {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ Ξ© (βˆ€' A Ο†)
| ex   {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ Ξ© (βˆƒ' A Ο†)

example {p q} : WF [] Ξ© (p β‹€ q) β†’ WF [] Ξ© p :=
begin
  intro wf,
  induction wf,

end

view this post on Zulip Mario Carneiro (Jun 11 2020 at 11:37):

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

view this post on Zulip Billy Price (Jun 11 2020 at 11:37):

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

view this post on Zulip Mario Carneiro (Jun 11 2020 at 11:37):

that's just a cases proof

view this post on Zulip Mario Carneiro (Jun 11 2020 at 11:38):

no need for induction

view this post on Zulip Billy Price (Jun 11 2020 at 11:38):

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

view this post on Zulip Mario Carneiro (Jun 11 2020 at 11:38):

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

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

view this post on Zulip Mario Carneiro (Jun 11 2020 at 11:39):

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

view this post on Zulip Billy Price (Jun 11 2020 at 11:39):

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

view this post on Zulip Mario Carneiro (Jun 11 2020 at 11:39):

yes

view this post on Zulip Mario Carneiro (Jun 11 2020 at 11:41):

Here's how you can prove that theorem using induction instead of cases:

example {p q} : WF [] Ξ© (p β‹€ q) β†’ WF [] Ξ© p :=
begin
  generalize e1 : [] = Ξ“,
  generalize e2 : p β‹€ q = a,
  intro wf,
  induction wf; cases e1; cases e2,
  assumption
end

view this post on Zulip Mario Carneiro (Jun 11 2020 at 11:43):

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

...
wf_ih_a : list.nil = list.nil β†’ p β‹€ q = p β†’ WF list.nil Ξ© p,
wf_ih_a_1 : list.nil = list.nil β†’ p β‹€ q = q β†’ WF list.nil Ξ© p,

view this post on Zulip Billy Price (Jun 11 2020 at 11:45):

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

view this post on Zulip Mario Carneiro (Jun 11 2020 at 11:45):

this is why cases and induction use different default motives even though they both boil down to an application of the recursor. In cases you are saying explicitly that you don't care about induction hypotheses so we can add as many assumptions as we like to the induction motive to say that we are only inducting on something equal to the input, and so kill all the unnecessary cases. In induction we want to generalize the induction hypothesis so we just suck in all assumptions from the context and generalize arguments as specified by generalizing

view this post on Zulip Mario Carneiro (Jun 11 2020 at 11:46):

What we are doing is proving WF Ξ“ Ξ© a β†’ ([] = Ξ“ β†’ p β‹€ q = a β†’ WF Ξ“ Ξ© p) by induction

view this post on Zulip Billy Price (Jun 11 2020 at 11:46):

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

view this post on Zulip Mario Carneiro (Jun 11 2020 at 11:47):

that is, the motive is Ξ» Ξ“ A a, [] = Ξ“ β†’ p β‹€ q = a β†’ WF Ξ“ A p

view this post on Zulip Billy Price (Jun 11 2020 at 11:49):

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

view this post on Zulip Mario Carneiro (Jun 11 2020 at 11:49):

Remember what the recursor says. You are proving that \forall Ξ“ A a, WF Ξ“ A a -> C Ξ“ A a and this is how we are picking C

view this post on Zulip Mario Carneiro (Jun 11 2020 at 11:49):

Yes, generalize automatically replaces instances of [] with Ξ“

view this post on Zulip Mario Carneiro (Jun 11 2020 at 11:50):

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

view this post on Zulip Mario Carneiro (Jun 11 2020 at 11:52):

example {p q} : WF [] Ξ© (p β‹€ q) β†’ WF [] Ξ© p :=
begin
  suffices : βˆ€ Ξ“ A a, WF Ξ“ A a β†’ p β‹€ q = a β†’ WF Ξ“ A p,
  { exact Ξ» wf, this _ _ _ wf rfl },
  intros Ξ“ A a wf,
  induction wf; rintro ⟨⟩,
  assumption
end

view this post on Zulip Mario Carneiro (Jun 11 2020 at 11:53):

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

view this post on Zulip Mario Carneiro (Jun 11 2020 at 11:58):

For example in my recent proof tm_to_partrec.lean if you search for induction you will find a significant fraction of them are preceded by a suffices, for example in src#turing.partrec_to_TM2.succ_ok

view this post on Zulip Mario Carneiro (Jun 11 2020 at 11:59):

Here's another good example

view this post on Zulip Mario Carneiro (Jun 11 2020 at 12:02):

the βˆ€ a b, a + b = n β†’ ... is hard for lean to guess automatically. (Without going into details, we are proving a fact about P n 0 by induction given P 0 n and P a b -> P (a+1) (b-1).)

view this post on Zulip Billy Price (Jun 11 2020 at 12:10):

Cool that looks like a useful practice.

view this post on Zulip Billy Price (Jun 11 2020 at 12:16):

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

import tactic.interactive

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

notation `Ξ©` := type.Omega
def Unit := type.Unit
infix `Γ—Γ—`:max := type.Prod
notation `𝒫`A :max := type.Pow A

def context := list type

inductive term : Type
| star : term
| top  : term
| bot  : term
| and  : term β†’ term β†’ term
| or   : term β†’ term β†’ term
| imp  : term β†’ term β†’ term
| elem : term β†’ term β†’ term
| pair : term β†’ term β†’ term
| var  : β„• β†’ term
| comp : type β†’ term β†’ term
| all  : type β†’ term β†’ term
| ex   : type β†’ term β†’ term

open term

notation `𝟘` := term.var 0
notation `πŸ™` := term.var 1
notation `𝟚` := term.var 2
notation `πŸ›` := term.var 3
notation `𝟜` := term.var 4
notation `𝟝` := term.var 5

notation `⁎` := term.star    -- input \asterisk
notation `⊀` := term.top     --       \top
notation `βŠ₯` := term.bot     -- input \bot
infixr ` ⟹ `:60 := term.imp -- input \==>
infixr ` β‹€ ` :70 := term.and -- input \And or \bigwedge
infixr ` ⋁ ` :59 := term.or  -- input \Or or \bigvee

infix ∈ := term.elem
infix βˆ‰ := Ξ» a Ξ±, not (term.elem a Ξ±)
notation `⟦ ` A ` | ` Ο† ` ⟧` := term.comp A Ο†

notation `βŸͺ` a `,` b `⟫` := term.pair a b

notation `βˆ€'` := term.all
notation `βˆƒ'` := term.ex

inductive WF : context β†’ type β†’ term β†’ Prop
| star {Ξ“}         : WF Ξ“ Unit ⁎
| top  {Ξ“}         : WF Ξ“ Ξ© ⊀
| bot  {Ξ“}         : WF Ξ“ Ξ© βŠ₯
| and  {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p β‹€ q)
| or   {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p ⋁ q)
| imp  {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p ⟹ q)
| elem {Ξ“ A a Ξ±}   : WF Ξ“ A a β†’ WF Ξ“ (𝒫 A) Ξ± β†’ WF Ξ“ Ξ© (a ∈ Ξ±)
| pair {Ξ“ A B a b} : WF Ξ“ A a β†’ WF Ξ“ B b β†’ WF Ξ“ (A Γ—Γ— B) βŸͺa,b⟫
| var  {Ξ“ A n}     : list.nth Ξ“ n = some A β†’ WF Ξ“ A (var n)
| comp {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ (𝒫 A) ⟦A | Ο†βŸ§
| all  {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ Ξ© (βˆ€' A Ο†)
| ex   {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ Ξ© (βˆƒ' A Ο†)

section substitution

  @[simp]
  def lift_d (d : β„•) : β„• β†’ term β†’ term
  | k ⁎          := ⁎
  | k ⊀          := ⊀
  | k βŠ₯          := βŠ₯
  | k (p β‹€ q)    := (lift_d k p) β‹€ (lift_d k q)
  | k (p ⋁ q)    := (lift_d k p) ⋁ (lift_d k q)
  | k (p ⟹ q)   := (lift_d k p) ⟹ (lift_d k q)
  | k (a ∈ α)    := (lift_d k a) ∈ (lift_d k α)
  | k βŸͺa,b⟫      := βŸͺlift_d k a, lift_d k b⟫
  | k (var m)    := if mβ‰₯k then var (m+d) else var m
  | k ⟦A | Ο†βŸ§     :=   ⟦A | lift_d (k+1) Ο†βŸ§
  | k (βˆ€' A Ο†)   := βˆ€' A $ lift_d (k+1) Ο†
  | k (βˆƒ' A Ο†)   := βˆƒ' A $ lift_d (k+1) Ο†

  @[simp]
  def lift := lift_d 1 0

  @[simp]
  def subst : β„• β†’ term β†’ term β†’ term
  | n x ⁎          := ⁎
  | n x ⊀          := ⊀
  | n x βŠ₯          := βŠ₯
  | n x (p β‹€ q)    := (subst n x p) β‹€ (subst n x q)
  | n x (p ⋁ q)    := (subst n x p) ⋁ (subst n x q)
  | n x (p ⟹ q)  := (subst n x p) ⟹ (subst n x q)
  | n x (a ∈ α)    := (subst n x a) ∈ (subst n x α)
  | n x βŸͺa,c⟫      := βŸͺsubst n x a, subst n x c⟫
  | n x (var m)    := if n=m then x else var m
  | n x ⟦ A | Ο† ⟧   :=    ⟦A | subst (n+1) (lift x) Ο†βŸ§
  | n x (βˆ€' A Ο†)     := βˆ€' A (subst (n+1) (lift x) Ο†)
  | n x (βˆƒ' A Ο†)     := βˆƒ' A (subst (n+1) (lift x) Ο†)

  notation  `⁅` Ο† ` // `  b `⁆` := subst 0 b Ο†

  #reduce β…πŸ˜ // ⊀ β‹€ βŠ₯⁆
  #reduce ⁅ πŸ™ // ⊀ β‹€ βŠ₯⁆

end substitution

lemma WF.lift_closed {a A} : WF [] A a β†’ a = lift a :=
begin
  generalize_hyp e : [] = Ξ“,
  intro wf,
  induction wf;cases e;simp,
end

end TT

view this post on Zulip Mario Carneiro (Jun 11 2020 at 12:21):

You will need a stronger inductive hypothesis

view this post on Zulip Mario Carneiro (Jun 11 2020 at 12:24):

simp will do a lot of the work here, although it doesn't like that you wrote the equality the wrong way around

lemma WF.lift_closed {a A} : WF [] A a β†’ lift a = a :=
begin
  generalize_hyp e : [] = Ξ“,
  intro wf,
  induction wf;cases e;simp * at *,

end

view this post on Zulip Billy Price (Jun 11 2020 at 12:25):

What do the stars do?

view this post on Zulip Kenny Lau (Jun 11 2020 at 12:26):

they make the sky more beautiful

view this post on Zulip Billy Price (Jun 11 2020 at 12:26):

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

view this post on Zulip Billy Price (Jun 11 2020 at 12:29):

Lemme guess, I need to be proving the strong lemma which says "if the highest free variable is below the lift-cutoff, then lift a = a"

view this post on Zulip Mario Carneiro (Jun 11 2020 at 12:30):

Indeed. I believe the most similar statement to what you have here that will do the job is WF G A a β†’ length G <= k -> lift_d 1 k a = a

view this post on Zulip Billy Price (Jun 11 2020 at 12:36):

This is an interesting pattern - the most "appropriately general" statement of a theorem is typically easier to prove than specialisations of that theorem. Is this specific to inductive proofs or formal proofs in general?

view this post on Zulip Mario Carneiro (Jun 11 2020 at 12:39):

this is pretty common of inductive proofs

view this post on Zulip Mario Carneiro (Jun 11 2020 at 12:40):

the examples I showed earlier were also of that form - I said that I wanted to prove something about P n 0 but the obvious inductive proof would try to show P 0 0 and P a 0 -> P (a+1) 0 which doesn't work

view this post on Zulip Mario Carneiro (Jun 11 2020 at 12:41):

induction proofs can vary a lot in their dependency structure, so the easiest reliable way to make lean do what you want is to say what you want

view this post on Zulip Mario Carneiro (Jun 11 2020 at 12:41):

(unfortunately this is also quite verbose so I usually use it as a last resort when basic induction doesn't do the right thing)

view this post on Zulip Billy Price (Jun 11 2020 at 12:41):

You're referring to the suffices pattern?

view this post on Zulip Mario Carneiro (Jun 11 2020 at 12:42):

yes

view this post on Zulip Mario Carneiro (Jun 11 2020 at 12:42):

You could use it here too

view this post on Zulip Mario Carneiro (Jun 11 2020 at 12:45):

lemma WF.lift_closed {a A} : WF [] A a β†’ lift a = a :=
begin
  suffices : βˆ€ G A a, WF G A a β†’ lift_d 1 (list.length G) a = a,
  { exact this _ _ _ },
  introv wf,
  induction wf; simp * at *,
  exact if_neg (not_le_of_gt (list.nth_eq_some.1 wf_a).fst)
end

view this post on Zulip Billy Price (Jun 11 2020 at 13:00):

So I've been doing all of this stuff for a 1 semester project (I convinced a mathematician at my uni to supervise me for a project in Lean), and I'm going to be ending it on "here's a statement in Lean that says this type theory forms a category". Once the semester is over (very soon) I want to go back to the basics of Lean so I'm better equipped to actual prove all the theorems

From what you've seen from me, is there any particular ways you'd recommend learning the relevant intricacies of Lean I need to understand how to do my proofs? Do the mathematics tutorials (NNG, Real Number Game etc) cover the same stuff but on different topics? Should I keep posting "how do I do this proof" whenever I get to a new roadblock? Usually the easiest answer (like this time) is just "here's the proof" and I feel bad that I'm just constantly getting other people to do my work for me. Thoughts?

view this post on Zulip Mario Carneiro (Jun 11 2020 at 13:11):

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

view this post on Zulip Mario Carneiro (Jun 11 2020 at 13:11):

don't worry about my having "stolen" a proof from you, trust me there are more than enough proof obligations to go around

view this post on Zulip Mario Carneiro (Jun 11 2020 at 13:14):

For a type theory category, I suggest jumping into the formalization and asking questions when you don't know how to express something

view this post on Zulip Mario Carneiro (Jun 11 2020 at 13:15):

My sense is that it should not be too difficult to write something down that vaguely resembles your goal statement. There will then be some rearranging and fixing of the definition to make it amenable to proof stuff

view this post on Zulip Mario Carneiro (Jun 11 2020 at 13:17):

For the first pass, figure out what a category is: if you intend to use mathlib categories, then study the mathlib definition of a category, or if you plan to write your own then figure out how to make that definition. You said something about quotienting by equivalence, so figure out how to write down a quotient and specify functions on quotients. Don't concern yourself with proofs too much, but try not to write something that you know is false

view this post on Zulip Mario Carneiro (Jun 11 2020 at 13:18):

I think the best way to learn about intricacies of lean is to trip over them on your way to getting something done

view this post on Zulip Billy Price (Jun 11 2020 at 13:26):

Thanks, that's good to hear. My concern is less about intellectual property (though that's important), and more about using up your time!

At a basic level, I do understand how to define a math lib category and I feel somewhat comfortable with quotient stuff (I've followed the Zmod37 example and created my own quotient type), but one of my roadblocks there is how to say the following theorem (which I hope is true), "If I have a proof Ξ“ p q and either of p or q contains some a : term which is well-formed of type A (WF Ξ“ A a), and a is provably equal to a' (I can show proof Ξ“ ⊀ a ≃[A] a'), then I can swap out occurrences of a with a'. I think that would help me a lot with lifting things to the quotients.

view this post on Zulip Billy Price (Jun 11 2020 at 13:26):

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

view this post on Zulip Billy Price (Jun 11 2020 at 13:37):

Here's an attempt which I'm worried is too general and false.

theorem eq_sound {Ξ“} (A : type) (a₁ aβ‚‚ : term) (eq : proof Ξ“ ⊀ (a₁ ≃[A] aβ‚‚)) (f g : term β†’ term) : proof Ξ“ (f a₁) (g a₁) β†’ proof Ξ“ (f aβ‚‚) (g aβ‚‚)

(made it a theorem because wew, it looks powerful.)

view this post on Zulip Mario Carneiro (Jun 11 2020 at 13:38):

yeah that version is false

view this post on Zulip Billy Price (Jun 11 2020 at 13:39):

Good to know

view this post on Zulip Mario Carneiro (Jun 11 2020 at 13:39):

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

view this post on Zulip Mario Carneiro (Jun 11 2020 at 13:43):

You can also define a subset of functions term -> term according to whether they respect equality. The theorem holds for such functions more or less by definition, but the interesting observation is that all the term constructors are examples of such functions

view this post on Zulip Billy Price (Jun 11 2020 at 13:53):

I actually tried that substitution method but I found it difficult to apply it. Thinking about the second option - that sounds like you could inductively define all such functions based on the term constructors?

view this post on Zulip Billy Price (Jun 11 2020 at 13:55):

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

view this post on Zulip Jannis Limperg (Jun 11 2020 at 13:56):

@Billy Price I'd be very happy if you could try the current version of my induction tactic. It should take care of all the generalising for you and give less scary names as a bonus. The current draft is at the induction branch. When you have that, you should be able to import tactic.induction and use induction' instead of the generalize ..., induction dance. I'll gladly fix any bugs you find.

view this post on Zulip Billy Price (Jun 11 2020 at 13:59):

Oh cool! I will gladly do so :)

view this post on Zulip Mario Carneiro (Jun 11 2020 at 14:03):

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

Of course the import of the substitution operator is that it is a way to represent such functions using terms

view this post on Zulip Mario Carneiro (Jun 11 2020 at 14:05):

The simpler alternative is just to prove in each individual case that a concretely given function satisfies the equality property by applying equality axioms using e.g. apply_rules

view this post on Zulip Billy Price (Jun 11 2020 at 14:13):

What do you mean by the equality axioms?

view this post on Zulip Kevin Buzzard (Jun 11 2020 at 22:00):

@Billy Price the way to learn the intricacies of Lean is to have a healthy source of projects in your area of interest and then just keep formalising and ask whenever you get stuck. After a few months (maybe it took me a year but I am old and have no CS background) you find that you're asking fewer questions and are in fact now answering them.

view this post on Zulip Billy Price (Jun 12 2020 at 02:25):

Tada I did a proof, I think I better understand the idea of generalising hypotheses in induction now. @Jannis Limperg I haven't yet switched to the induction branch to try your tactic - how do I do that?

lemma lift_zero_does_nothing {k} {a : term} : lift_d 0 k a = a :=
begin
  suffices : βˆ€ k, lift_d 0 k a = a, { exact this _ },
  induction a;simp * at *,
end

Let me phrase some subtlety I was overlooking before (lemme know if this is the wrong way of thinking about it): Although k is an arbitrary hypothesis to the lemma, within the goal state, it's thought of as fixed. It's a 'given' number. So without the suffices line, the inductive cases must be proved for that fixed k. This seems to highlight the subtle difference between example (k : nat) : P k and example : βˆ€ k : nat, P k.

view this post on Zulip Billy Price (Jun 12 2020 at 02:27):

I could make my original lemma lemma lift_zero_does_nothing {a : term} : βˆ€ k, lift_d 0 k a = a, but that would make it less usable right?

view this post on Zulip Billy Price (Jun 12 2020 at 02:29):

More succinct

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

view this post on Zulip Mario Carneiro (Jun 12 2020 at 02:35):

Although k is an arbitrary hypothesis to the lemma, within the goal state, it's thought of as fixed. It's a 'given' number. So without the suffices line, the inductive cases must be proved for that fixed k.

Yes and no. The induction tactic will generalize the variable k, ignoring the initial value that it had. It's just that when the input was a variable to start with this is no loss (but you will see k hanging around uselessly in the inductive subcases)

view this post on Zulip Mario Carneiro (Jun 12 2020 at 02:36):

I could make my original lemma lemma lift_zero_does_nothing {a : term} : βˆ€ k, lift_d 0 k a = a, but that would make it less usable right?

Externally these are indistinguishable, except that you reordered the two variables and made k explicit in this version

view this post on Zulip Mario Carneiro (Jun 12 2020 at 02:38):

In tactic mode you will always end up intro'ing all variables before the induction, so it makes no difference what is "right of the colon". This does affect inductive proofs performed using the equation compiler though (you will not be able to use the equation compiler with the first version)

view this post on Zulip Mario Carneiro (Jun 12 2020 at 02:40):

Oh, correction: since you are doing induction on term in this case, there are no indices and so k will be held fixed unless you explicitly use generalizing to indicate that you want it to change

view this post on Zulip Jannis Limperg (Jun 12 2020 at 13:00):

Billy Price said:

Jannis Limperg I haven't yet switched to the induction branch to try your tactic - how do I do that?

Could you post your leanpkg.toml? Alternatively put your project on Github or something, then I'll see what needs to be changed.

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 17:25):

@Billy Price the answer depends on whether you're working in mathlib or working on your own project and have mathlib as a dependency. If you have mathlib as a dependency then you probably have to edit your project's leanpkg.toml. @Jannis Limperg 's branch is here https://github.com/leanprover-community/mathlib/commits/induction and the most recent commit is 52c995b6ee3ed40c6c962043e8bdd37176a942e3 so you want to change your mathlib rev to that commit hash and then do leanproject get-mathlib-cache in the root directory of your project, and it should then all work by magic.

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 17:27):

If you're working in mathlib directory then you might be able to just checkout the induction branch and then do leanproject up.

view this post on Zulip Billy Price (Jun 18 2020 at 05:54):

Mario Carneiro said:

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

I'm currently reflecting on the decisions I made for the definitions in my type theory, and I'm trying to justify why terms and Well-formedness are defined separately - it seemed that I had to do a lot of work later regarding lemmas to prove well-formedness. Would this have not gone away if I defined only well-formed terms? Are there more obvious reasons why keeping terms context free is valuable?

view this post on Zulip Mario Carneiro (Jun 18 2020 at 08:04):

If you find yourself manually constructing terms with a proof of well formedness a lot (for example if you are acting like a typechecker and have some concrete terms of interest), then one thing you can do is construct a sigma type of a term and a proof of its well foundedness, and then the construction of the term will be carried out in parallel with the proof of well foundedness. Here a separate WF proof is not particularly helpful. (This is done in the flypitch formalization, for example.)

The advantage comes when you are doing metatheory, which is usually what people want to do with defined type theories such as this inside lean. (If you just want a typechecker, it is often simpler to just write one directly in a standard programming language, as the many proof assistants for HoTT-based type theories can attest.) Here you really want to be able to do things like reassociate contexts or do other non-defeq manipulations inside the indices to the WF inductive, and then if WF is not a Prop but is rather a dependent type of well formed terms, this will cause no end of headaches due to the induced cast.

view this post on Zulip Billy Price (Jun 19 2020 at 02:10):

I think you've interpreted my question as "I'm sick of the separation of terms and Well-formedness, so how can I remedy that in the current setup (thanks for the suggestions), but I'm interested in what are the downsides of doing it all in one with term : context -> type -> Type. I think you were answering that in this reply - but could you explain what you mean here about carrying around type state, and what definitional equalities are hard to get?

Mario Carneiro said:

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

view this post on Zulip Mario Carneiro (Jun 19 2020 at 02:47):

I mean the context and the type

view this post on Zulip Mario Carneiro (Jun 19 2020 at 02:48):

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

view this post on Zulip Mario Carneiro (Jun 19 2020 at 02:48):

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

view this post on Zulip Mario Carneiro (Jun 19 2020 at 02:51):

If you have a term Gamma ++ a :: Delta |- e : A and want the same term (Gamma ++ [a]) ++ Delta |- e : A you can't do the obvious thing. Instead you have to cast e to the new context, and now it's not a constructor so you can't pattern match on it, and things sort of go downhill from there

view this post on Zulip Mario Carneiro (Jun 19 2020 at 02:52):

It's certainly possible to construct things so that everything beautifully meshes together. But this is like a sudoku puzzle, a quite mind bending exercise that has little relation to the original problem you set out to solve

view this post on Zulip Mario Carneiro (Jun 19 2020 at 02:54):

If you like that sort of thing it's possible to build a career on it but you might find that you've left your original problem behind. (I would argue this is what happened to Voevodsky with HoTT)

view this post on Zulip Mario Carneiro (Jun 19 2020 at 02:56):

If you have extrinsic typing, then you can transport terms to new contexts without apology. All the ugliness is encapsulated in proofs that don't interfere with later statements because of proof irrelevance

view this post on Zulip Billy Price (Jun 19 2020 at 03:05):

Ah okay I think I follow. If we dump the context from the constructor, is the remaining problem just that it's hard to define the var constructor with no context? Or are there still downsides without the var problem?

view this post on Zulip Mario Carneiro (Jun 19 2020 at 03:09):

I like to think about indices to dependent types as "rigid variables". Variables in these positions can only be manipulated in very restrictive ways, essentially by applying constructors and pattern matching. Using functions defined by induction is a no-no

view this post on Zulip Mario Carneiro (Jun 19 2020 at 03:09):

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

view this post on Zulip Mario Carneiro (Jun 19 2020 at 03:10):

for example a list A is not the same as a list A' even if A and A' are extensionally equivalent (have the same elements or some other synthetic notion of equality)

view this post on Zulip Billy Price (Jun 19 2020 at 03:13):

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

view this post on Zulip Mario Carneiro (Jun 19 2020 at 03:14):

If you take the context out of a term, it just has a type, and presumably the inductive type type is a simple inductive. So this is plausible. But variables have a weird type in this context: you didn't do this but a classically reasonable alternative type for the var constructor would have been var (i : fin (length G)) : term G (G.nth' i) but this is a bad idea in DTT

view this post on Zulip Mario Carneiro (Jun 19 2020 at 03:15):

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

view this post on Zulip Billy Price (Jun 19 2020 at 03:21):

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

view this post on Zulip Mario Carneiro (Jun 19 2020 at 03:22):

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

view this post on Zulip Mario Carneiro (Jun 19 2020 at 03:23):

it could be a parameter though

view this post on Zulip Mario Carneiro (Jun 19 2020 at 03:23):

as long as you don't also have binders

view this post on Zulip Mario Carneiro (Jun 19 2020 at 03:24):

parameters to inductive types are also rigid variables, but you usually don't have as pressing a need to change them in the middle of a proof

view this post on Zulip Billy Price (Jun 19 2020 at 03:26):

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

view this post on Zulip Mario Carneiro (Jun 19 2020 at 03:27):

parameters to inductive types meaning left of the colon

view this post on Zulip Mario Carneiro (Jun 19 2020 at 03:27):

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

view this post on Zulip Mario Carneiro (Jun 19 2020 at 03:27):

Then the G in term G A is a rigid variable

view this post on Zulip Mario Carneiro (Jun 19 2020 at 03:29):

One way to conceptualize rigid variables are as terms about which it is common to have equalities, like list.append_assoc, but for which simp refuses to touch and rw gives motive is not type correct when you try to use those equalities

view this post on Zulip Mario Carneiro (Jun 19 2020 at 03:32):

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

view this post on Zulip Billy Price (Jun 19 2020 at 05:18):

Okay.

view this post on Zulip Billy Price (Jun 19 2020 at 05:25):

By the way, my type theory as it is, is the "pure" version, which is supposed to be extensible. How would I go about defining a type theory which has at least everything I've defined, but maybe more types, more terms, more deduction rules etc? For example, if I wanted to throw in a mynat : type and corresponding terms which are WF [] mynat? I imagine doing so would ruin all the lemmas I've proved. All my lemmas just talk about stuff in the pure type theory, so they should hold in any extension (I imagine there are pathological counterexamples depending on the generality of the lemma).

view this post on Zulip Billy Price (Jun 19 2020 at 05:35):

Just an idea that probably doesn't work because of cardinality.

variable \alpha : Type

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

view this post on Zulip Mario Carneiro (Jun 19 2020 at 05:58):

That works fine

view this post on Zulip Mario Carneiro (Jun 19 2020 at 05:59):

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

view this post on Zulip Mario Carneiro (Jun 19 2020 at 06:00):

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

view this post on Zulip Mario Carneiro (Jun 19 2020 at 06:04):

Since you are wondering about universe issues: note that alpha will usually be a small type, for example inductive base_types | nat | bool | real | extra_special (beta : Type) where perhaps beta is yet another parameter

view this post on Zulip Billy Price (Jun 19 2020 at 06:46):

Ah whoops I made \alpha a variable and a parameter at the same time. I have two possible ideas below, both of which I think are ugly - is there not a more natural way to do this? Instead of taking some other variable Type and incorporating it into my definition, I just say to the user "give me a Type of things which I will think of as types in my theory, as long Unit, Omega are of that type and the Pow, Prod constructors make new types out of old ones". I am somewhat ambivalent to whether Unit and Omega are naturally a part of the type of types that the user creates or if they are just tacked on.

variable \alpha : Type

inductive type : Type
| special (X : \alpha) | Unit | Omega | Pow (A : type) | Prod (A B : type)
inductive type : Type
| special (X : Type) | Unit | Omega | Pow (A : type) | Prod (A B : type)

view this post on Zulip Billy Price (Jun 19 2020 at 06:47):

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

view this post on Zulip Billy Price (Jun 19 2020 at 06:48):

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

view this post on Zulip Mario Carneiro (Jun 19 2020 at 07:11):

the second one should not typecheck

view this post on Zulip Mario Carneiro (Jun 19 2020 at 07:11):

because there is a universe issue

view this post on Zulip Mario Carneiro (Jun 19 2020 at 07:12):

You want the first one

view this post on Zulip Mario Carneiro (Jun 19 2020 at 07:12):

I just say to the user "give me a Type of things which I will think of as types in my theory, as long Unit, Omega are of that type and the Pow, Prod constructors make new types out of old ones".

:point_up: this

view this post on Zulip Mario Carneiro (Jun 19 2020 at 07:13):

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

view this post on Zulip Mario Carneiro (Jun 19 2020 at 07:13):

you can do that, and the interface will be nicer, but you will not be able to prove theorems about the PTS by induction anymore

view this post on Zulip Mario Carneiro (Jun 19 2020 at 07:15):

You could prove theorems relative to a partial recursor that the user also provides, but then every theorem is going to come with side conditions saying that the theorem already holds in some way for all the types the PTS doesn't know about

view this post on Zulip Billy Price (Jun 19 2020 at 09:56):

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

view this post on Zulip Billy Price (Jun 19 2020 at 10:04):

I just realised I could do this

instance nat_coe_var : has_coe β„• term := ⟨term.var⟩

instead of this

notation `𝟘` := term.var 0
notation `πŸ™` := term.var 1
notation `𝟚` := term.var 2
notation `πŸ›` := term.var 3
notation `𝟜` := term.var 4
notation `𝟝` := term.var 5

is the coercion one a bad idea?

view this post on Zulip Billy Price (Jun 19 2020 at 10:06):

Or is there any way I can do a unique term construction like ⟨0⟩ since there's only one term constructor that takes a single (nat) argument?

view this post on Zulip Billy Price (Jun 19 2020 at 10:07):

It doesn't work out of the box, because it expects term to only have one term constructor.

inductive term : Type
| star : term
| top  : term
| bot  : term
| and  : term β†’ term β†’ term
| or   : term β†’ term β†’ term
| imp  : term β†’ term β†’ term
| elem : term β†’ term β†’ term
| pair : term β†’ term β†’ term
| var  : β„• β†’ term
| comp : type β†’ term β†’ term
| all  : type β†’ term β†’ term
| ex   : type β†’ term β†’ term

view this post on Zulip Mario Carneiro (Jun 19 2020 at 17:14):

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

view this post on Zulip Billy Price (Jun 20 2020 at 05:26):

Why does this happen? I write rw append_nil Ξ“ in this state and it tells me

rewrite tactic failed, did not find instance of the pattern in the target expression Ξ“ ++ nil

ΒΏque?

2 goals
case list.nil
Ξ“ : context,
A : type,
n : β„•,
h : WF Ξ“ A (var n),
eq : nth Ξ“ n = some A
⊒ WF (Ξ“ ++ nil) A (var n)

view this post on Zulip Billy Price (Jun 20 2020 at 06:01):

Also how would I do apply_rules on all of the hypotheses? (to extract more hypotheses) Or on one hypothesis? Something like simp at *

(Not for this goal state)

view this post on Zulip Mario Carneiro (Jun 20 2020 at 07:06):

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

view this post on Zulip Billy Price (Jun 21 2020 at 04:41):

I'll come back to this one.

view this post on Zulip Billy Price (Jun 21 2020 at 04:46):

Is there any practical difference between these two code blocks? I'd like to treat WF.foo : Prop just like the inductively defined lemmas.

inductive WF : context β†’ type β†’ term β†’ Prop
| star {Ξ“}         : WF Ξ“ πŸ™ ⁎
| top  {Ξ“}         : WF Ξ“ Ξ© ⊀
| bot  {Ξ“}         : WF Ξ“ Ξ© βŠ₯
| and  {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p β‹€ q)
| or   {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p ⋁ q)
| imp  {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p ⟹ q)
| elem {Ξ“ A a Ξ±}   : WF Ξ“ A a β†’ WF Ξ“ (𝒫 A) Ξ± β†’ WF Ξ“ Ξ© (a ∈ Ξ±)
| pair {Ξ“ A B a b} : WF Ξ“ A a β†’ WF Ξ“ B b β†’ WF Ξ“ (A 𝕏 B) βŸͺa,b⟫
| var  {Ξ“ A n}     : list.nth Ξ“ n = some A β†’ WF Ξ“ A (var n)
| comp {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ (𝒫 A) ⟦A | Ο†βŸ§
| all  {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ Ξ© (βˆ€' A Ο†)
| ex   {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ Ξ© (βˆƒ' A Ο†)

namespace WF

lemma foo : Prop

end
inductive WF : context β†’ type β†’ term β†’ Prop
| star {Ξ“}         : WF Ξ“ πŸ™ ⁎
| top  {Ξ“}         : WF Ξ“ Ξ© ⊀
| bot  {Ξ“}         : WF Ξ“ Ξ© βŠ₯
| and  {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p β‹€ q)
| or   {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p ⋁ q)
| imp  {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p ⟹ q)
| elem {Ξ“ A a Ξ±}   : WF Ξ“ A a β†’ WF Ξ“ (𝒫 A) Ξ± β†’ WF Ξ“ Ξ© (a ∈ Ξ±)
| pair {Ξ“ A B a b} : WF Ξ“ A a β†’ WF Ξ“ B b β†’ WF Ξ“ (A 𝕏 B) βŸͺa,b⟫
| var  {Ξ“ A n}     : list.nth Ξ“ n = some A β†’ WF Ξ“ A (var n)
| comp {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ (𝒫 A) ⟦A | Ο†βŸ§
| all  {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ Ξ© (βˆ€' A Ο†)
| ex   {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ Ξ© (βˆƒ' A Ο†)

lemma WF.foo : Prop

view this post on Zulip Billy Price (Jun 21 2020 at 04:47):

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

view this post on Zulip Billy Price (Jun 21 2020 at 04:47):

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

view this post on Zulip Mario Carneiro (Jun 21 2020 at 04:49):

no difference, yes it is a namespace

view this post on Zulip Mario Carneiro (Jun 21 2020 at 04:49):

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

view this post on Zulip Billy Price (Jun 22 2020 at 13:39):

Is there a proper way to write this meta definition? I'll do my best to render the backticks properly. meta def WF_prover : tactic unit:= do `[apply_rules WF_rules].

It works for the most part but where I could previously do apply_rules WF_rules; refl, I cannot now do WF_prover; refl, with this error resulting.

type mismatch at application
  WF_prover; refl
term
  refl
has type
  βˆ€ (a : ?m_1), ?m_2 a a : Prop
but is expected to have type
  ?m_1 : Type ?

I have to do WF_prover, all_goals {refl} (which works).

I'm guessing it's because I derived that meta definition from another one which sequenced several tactics, and I'm now just trying to rename one tactic.

view this post on Zulip Billy Price (Jun 22 2020 at 13:45):

Here's a related #mwe (more like #mnwe)

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

example {p q} : p β†’ q β†’ (p ∧ q) :=
begin
  intros,
  split;assumption,
end

example {p q} : p β†’ q β†’ (p ∧ q) :=
begin
  intros,
  my_split;assumption -- doesn't work
end

view this post on Zulip Reid Barton (Jun 22 2020 at 13:48):

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

view this post on Zulip Billy Price (Jun 22 2020 at 13:57):

I don't have a more minimal #mwe for this, but the very last line here, it doesn't recognise WF_prover

/-
Definitions of a type theory

Author: Billy Price
-/

import data.finset
import tactic.tidy
namespace TT

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

notation `Ξ©` := type.Omega
notation `πŸ™` := type.Unit
infix `𝕏`:max := type.Prod
notation `𝒫`A :max := type.Pow A


inductive term : Type
| star : term
| top  : term
| bot  : term
| and  : term β†’ term β†’ term
| or   : term β†’ term β†’ term
| imp  : term β†’ term β†’ term
| elem : term β†’ term β†’ term
| pair : term β†’ term β†’ term
| var  : β„• β†’ term
| comp : type β†’ term β†’ term
| all  : type β†’ term β†’ term
| ex   : type β†’ term β†’ term

open term

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

def nat_coe_var : has_coe β„• term := ⟨term.var⟩

local attribute [instance] nat_coe_var

notation `⁎` := term.star    -- input \asterisk
notation `⊀` := term.top     --       \top
notation `βŠ₯` := term.bot     -- input \bot
infixr ` ⟹ `:60 := term.imp -- input \==>
infixr ` β‹€ ` :70 := term.and -- input \And or \bigwedge
infixr ` ⋁ ` :59 := term.or  -- input \Or or \bigvee

def not (p : term) := p ⟹ βŠ₯
prefix `∼`:max := not -- input \~

def iff (p q: term) := (p ⟹ q) β‹€ (q ⟹ p)
infix ` ⇔ `:60 := iff -- input \<=>

infix ∈ := term.elem
infix βˆ‰ := Ξ» a Ξ±, not (term.elem a Ξ±)
notation `{{ ` A ` | ` Ο† ` }}` := term.comp A Ο†

notation `βŸͺ` a `,` b `⟫` := term.pair a b

notation `βˆ€'` := term.all
notation `βˆƒ'` := term.ex

def term.all_chain (Ξ“ : list type) : term β†’ term := flip (list.foldr (Ξ» A ψ, term.all A ψ)) Ξ“
def term.ex_chain  (Ξ“ : list type) : term β†’ term := flip (list.foldr (Ξ» A ψ, term.ex A ψ)) Ξ“

@[simp] lemma term.unfold_all_chain {A Ξ“ Ο†} : term.all_chain (A :: Ξ“) Ο† = βˆ€' A (term.all_chain Ξ“ Ο†) := rfl
@[simp] lemma term.unfold_ex_chain {A Ξ“ Ο†} : term.ex_chain (A :: Ξ“) Ο† = βˆƒ' A (term.ex_chain Ξ“ Ο†) := rfl

notation `βˆ€[` Ξ“:(foldr `,` (h t, list.cons h t) list.nil) `]` := term.all_chain Ξ“
notation `βˆƒ[` Ξ“:(foldr `,` (h t, list.cons h t) list.nil) `]` := term.ex_chain Ξ“

section substitution

  @[simp]
  def lift_d (d : β„•) : β„• β†’ term β†’ term
  | k ⁎          := ⁎
  | k ⊀          := ⊀
  | k βŠ₯          := βŠ₯
  | k (p β‹€ q)    := (lift_d k p) β‹€ (lift_d k q)
  | k (p ⋁ q)    := (lift_d k p) ⋁ (lift_d k q)
  | k (p ⟹ q)   := (lift_d k p) ⟹ (lift_d k q)
  | k (a ∈ α)    := (lift_d k a) ∈ (lift_d k α)
  | k βŸͺa,b⟫      := βŸͺlift_d k a, lift_d k b⟫
  | k (var m)    := if mβ‰₯k then var (m+d) else var m
  | k {{A | Ο†}}     :=   {{A | lift_d (k+1) Ο†}}
  | k (βˆ€' A Ο†)   := βˆ€' A $ lift_d (k+1) Ο†
  | k (βˆƒ' A Ο†)   := βˆƒ' A $ lift_d (k+1) Ο†

  notation `^` := lift_d 1 0

  @[simp]
  def subst : β„• β†’ term β†’ term β†’ term
  | n x ⁎          := ⁎
  | n x ⊀          := ⊀
  | n x βŠ₯          := βŠ₯
  | n x (p β‹€ q)    := (subst n x p) β‹€ (subst n x q)
  | n x (p ⋁ q)    := (subst n x p) ⋁ (subst n x q)
  | n x (p ⟹ q)  := (subst n x p) ⟹ (subst n x q)
  | n x (a ∈ α)    := (subst n x a) ∈ (subst n x α)
  | n x βŸͺa,c⟫      := βŸͺsubst n x a, subst n x c⟫
  | n x (var m)    := if n=m then x else var m
  | n x {{ A | Ο† }}   :=    {{A | subst (n+1) (^ x) Ο†}}
  | n x (βˆ€' A Ο†)   := βˆ€' A (subst (n+1) (^ x) Ο†)
  | n x (βˆƒ' A Ο†)   := βˆƒ' A (subst (n+1) (^ x) Ο†)

  notation  `⁅` Ο† ` // `  b `⁆` := subst 0 b Ο†

  #reduce ⁅ ↑0 // ⊀ β‹€ βŠ₯⁆
  #reduce ⁅ ↑1 // ⊀ β‹€ βŠ₯⁆

  def FV : term β†’ finset β„•
  | ⁎          := βˆ…
  | ⊀          := βˆ…
  | βŠ₯          := βˆ…
  | (p β‹€ q)    := FV p βˆͺ FV q
  | (p ⋁ q)    := FV p βˆͺ FV q
  | (p ⟹ q)  := FV p βˆͺ FV q
  | (a ∈ Ξ±)    := FV a βˆͺ FV Ξ±
  | βŸͺa,b⟫      := FV a βˆͺ FV b
  | (var m)    := finset.singleton m
  | {{ A | Ο† }}   := ((FV Ο†).erase 0).image nat.pred
  | (βˆ€' A Ο†)   := ((FV Ο†).erase 0).image nat.pred
  | (βˆƒ' A Ο†)   := ((FV Ο†).erase 0).image nat.pred


end substitution



def eq (A:type) (a₁ aβ‚‚ : term) : term := βˆ€' (𝒫 A) $ ((^ a₁) ∈ ↑0) ⇔ ((^ aβ‚‚) ∈ ↑0)
notation a ` ≃[`:max A `] `:0 b := eq A a b

#check eq πŸ™ ↑0 ↑0

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

def ex_unique (A : type) (Ο† : term) : term :=
  βˆƒ' A ({{ A | Ο† }} ≃[𝒫 A] (singleton A ↑0))
prefix `βˆƒ!'`:2 := ex_unique

def subseteq (A : type) (Ξ± : term) (Ξ² : term) : term :=
  βˆ€' A (↑0 ∈ (^ Ξ±)) ⟹ (↑0 ∈ (^ Ξ²))
notation a ` βŠ†[`:max A `] `:0 b := subseteq A a b

def term_prod (A B : type) (Ξ± Ξ² : term) : term :=
  {{ A 𝕏 B | βˆƒ' A (βˆƒ' B ((↑1 ∈ Ξ±) β‹€ (↑0 ∈ Ξ²) β‹€ (↑2 ≃[A 𝕏 B] βŸͺ↑1,↑0⟫)))}}
-- notation Ξ± ` 𝕏[`:max A,B `] `:0 Ξ² := term_prod A B Ξ± Ξ²

section
  variables p q r : term

  #check p β‹€ (q ⋁ r)
  #check βˆƒ' πŸ™ (βˆ€' πŸ™ (βˆ€' (𝒫 πŸ™) ((var 2) ∈ (var 0) ⇔ (var 1) ∈ (var 0))))
end


@[simp]
lemma subst.subseteq {x n Ξ± Ξ² A}: subst n x (Ξ± βŠ†[A] Ξ²) = (subst n x Ξ±) βŠ†[A] (subst n x Ξ²) :=
  sorry

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

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

def context := list type

variables {Ξ“ Ξ” : context}
variables {p q r Ο† a b Ξ± : term}
variables {A B Ξ©' : type}

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

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

inductive WF : context β†’ type β†’ term β†’ Prop
| star {Ξ“}         : WF Ξ“ πŸ™ ⁎
| top  {Ξ“}         : WF Ξ“ Ξ© ⊀
| bot  {Ξ“}         : WF Ξ“ Ξ© βŠ₯
| and  {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p β‹€ q)
| or   {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p ⋁ q)
| imp  {Ξ“ p q}     : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p ⟹ q)
| elem {Ξ“ A a Ξ±}   : WF Ξ“ A a β†’ WF Ξ“ (𝒫 A) Ξ± β†’ WF Ξ“ Ξ© (a ∈ Ξ±)
| pair {Ξ“ A B a b} : WF Ξ“ A a β†’ WF Ξ“ B b β†’ WF Ξ“ (A 𝕏 B) βŸͺa,b⟫
| var  {Ξ“ A n}     : list.nth Ξ“ n = some A β†’ WF Ξ“ A (var n)
| comp {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ (𝒫 A) {{A | Ο†}}
| all  {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ Ξ© (βˆ€' A Ο†)
| ex   {Ξ“ A Ο†}     : WF (A::Ξ“) Ξ© Ο† β†’ WF Ξ“ Ξ© (βˆƒ' A Ο†)

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


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

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

lemma WF.and_left   : WF Ξ“ Ξ©' (p β‹€ q) β†’ WF Ξ“ Ξ©' p := by WF_cases
lemma WF.and_right  : WF Ξ“ Ξ©' (p β‹€ q) β†’ WF Ξ“ Ξ©' q := by WF_cases
lemma WF.or_left    : WF Ξ“ Ξ©' (p ⋁ q) β†’ WF Ξ“ Ξ©' p := by WF_cases
lemma WF.or_right   : WF Ξ“ Ξ©' (p ⋁ q) β†’ WF Ξ“ Ξ©' q := by WF_cases
lemma WF.imp_left   : WF Ξ“ Ξ©' (p ⟹ q) β†’ WF Ξ“ Ξ©' p := by WF_cases
lemma WF.imp_right  : WF Ξ“ Ξ©' (p ⟹ q) β†’ WF Ξ“ Ξ©' q := by WF_cases
lemma WF.pair_left  : WF Ξ“ (A 𝕏 B) βŸͺa,b⟫ β†’ WF Ξ“ A a := by WF_cases
lemma WF.pair_right : WF Ξ“ (A 𝕏 B) βŸͺa,b⟫ β†’ WF Ξ“ B b := by WF_cases
lemma WF.comp_elim  : WF Ξ“ (𝒫 A) {{A | Ο†}} β†’ WF (A::Ξ“) Ξ© Ο† := by WF_cases
lemma WF.all_elim   : WF Ξ“ Ξ©' (βˆ€' A Ο†) β†’ WF (A::Ξ“) Ξ©' Ο† := by WF_cases
lemma WF.ex_elim    : WF Ξ“ Ξ©' (βˆƒ' A Ο†) β†’ WF (A::Ξ“) Ξ©' Ο† := by WF_cases
@[TT.WF_rules] lemma WF.iff : WF Ξ“ Ξ© p β†’ WF Ξ“ Ξ© q β†’ WF Ξ“ Ξ© (p ⇔ q) := by {intros, WF_prover}

view this post on Zulip Reid Barton (Jun 22 2020 at 14:10):

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

view this post on Zulip Reid Barton (Jun 22 2020 at 14:10):

it's long and hard to tell

view this post on Zulip Reid Barton (Jun 22 2020 at 14:15):

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

view this post on Zulip Kevin Buzzard (Jun 22 2020 at 14:18):

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

view this post on Zulip Billy Price (Jun 23 2020 at 12:08):

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

import category_theory.category

namespace category_theory

constant type : Type
constant tset : type β†’ Type

constant graph {A B} (Ξ± : tset A) (Ξ² : tset B) : Type

constant id_graph {A} (Ξ± : tset A) : graph Ξ± Ξ±

constant composition {A B C} {Ξ± : tset A} {Ξ² : tset B} {Ξ· : tset C} (F : graph Ξ± Ξ²) (G : graph Ξ² Ξ·) : graph Ξ± Ξ·

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

end category_theory

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

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

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

view this post on Zulip Reid Barton (Jun 23 2020 at 12:28):

You should write the instance this way:

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

view this post on Zulip Reid Barton (Jun 23 2020 at 12:31):

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

view this post on Zulip Billy Price (Jun 23 2020 at 12:33):

Cool thanks!

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

variables (Ξ± : Type) (p q : Ξ± β†’ Prop)

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

view this post on Zulip Reid Barton (Jun 23 2020 at 12:36):

example (h : βˆƒ x, p x ∧ q x) : βˆƒ x, q x ∧ p x :=
begin
  obtain ⟨w, hw₁, hwβ‚‚βŸ© := h, -- or rcases h with ⟨w, hw₁, hwβ‚‚βŸ©,
  exact ⟨w, hwβ‚‚, hwβ‚βŸ©
end

view this post on Zulip Billy Price (Jun 23 2020 at 12:40):

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

view this post on Zulip Reid Barton (Jun 23 2020 at 12:43):

Yes, rcases = "recursive cases"

view this post on Zulip Kenny Lau (Jun 23 2020 at 12:44):

rintro = β€œrecursive intro”

view this post on Zulip Billy Price (Jun 23 2020 at 12:48):

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

view this post on Zulip Billy Price (Jun 26 2020 at 11:07):

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

lemma ent_to_meta : entails Ξ“ Ο† ψ  β†’ entails Ξ“ ⊀ Ο† β†’ entails Ξ“ ⊀ ψ :=
  Ξ» _ _, (by {apply entails.cut _ Ο† _, tidy})

lemma meta_to_ent (wfΟ† : WF Ξ“ Ξ© Ο†) (wfψ : WF Ξ“ Ξ© ψ) : (entails Ξ“ ⊀ Ο† β†’ entails Ξ“ ⊀ ψ) β†’ entails Ξ“ Ο† ψ :=
begin
  intro h,
  sorry
end

view this post on Zulip Billy Price (Jun 26 2020 at 11:09):

Here's what entails is.

inductive entails : context β†’ term β†’ term β†’ Prop
| axm        {Ξ“} {p}       : WF Ξ“ Ξ© p β†’ entails Ξ“ p p
| vac        {Ξ“} {p}       : WF Ξ“ Ξ© p β†’ entails Ξ“ p ⊀
| abs        {Ξ“} {p}       : WF Ξ“ Ξ© p β†’ entails Ξ“ βŠ₯ p
| and_intro  {Ξ“} {p q r}   : entails Ξ“ p q β†’ entails Ξ“ p r β†’ entails Ξ“ p (q β‹€ r)
| and_left   {Ξ“} (p q r)   : entails Ξ“ p (q β‹€ r) β†’ entails Ξ“ p q
| and_right  {Ξ“} (p q r)   : entails Ξ“ p (q β‹€ r) β†’ entails Ξ“ p r
| or_intro   {Ξ“} {p q r}   : entails Ξ“ p r β†’ entails Ξ“ q r β†’ entails Ξ“ (p ⋁ q) r
| or_left    {Ξ“} (p q r)   : entails Ξ“ (p ⋁ q) r β†’ entails Ξ“ p r
| or_right   {Ξ“} (p q r)   : entails Ξ“ (p ⋁ q) r β†’ entails Ξ“ q r
| imp_to_and {Ξ“} {p q r}   : entails Ξ“ p (q ⟹ r) β†’ entails Ξ“ (p β‹€ q) r
| and_to_imp {Ξ“} {p q r}   : entails Ξ“ (p β‹€ q) r β†’ entails Ξ“ p (q ⟹ r)
| weakening  {Ξ“} {p q} (Ξ”) : entails Ξ“ p q β†’ entails (list.append Ξ“ Ξ”) p q
| cut        {Ξ“} (p c q)   : entails Ξ“ p c β†’ entails Ξ“ c q β†’ entails Ξ“ p q
| all_elim   {Ξ“} {p Ο† A}   : entails Ξ“ p (βˆ€[A] Ο†) β†’ entails (A::Ξ“) (^ p) Ο†
| all_intro  {Ξ“} {p Ο†} (A) : entails (A::Ξ“) (^ p) Ο† β†’ entails Ξ“ p (βˆ€[A] Ο†)
| ex_elim    {Ξ“} {p Ο† A}   : entails Ξ“ p (βˆƒ[A] Ο†) β†’ entails (A::Ξ“) (^ p) Ο†
| ex_intro   {Ξ“} {p Ο†} (A) : entails (A::Ξ“) (^ p) Ο† β†’ entails Ξ“ p (βˆƒ[A] Ο†)
| extensionality {A}       : entails [] ⊀ $ βˆ€[𝒫 A, 𝒫 A] $ (βˆ€' A $ (↑0 ∈ ↑2) ⇔ (↑0 ∈ ↑1)) ⟹ (↑1 ≃[𝒫 A] ↑0)
| prop_ext                 : entails [] ⊀ $ βˆ€[Ξ©,Ξ©] $ (↑1 ⇔ ↑0) ⟹ (↑1 ≃[Ξ©] ↑0)
| star_unique              : entails [] ⊀ $ βˆ€[πŸ™] (↑0 ≃[πŸ™] ⁎)
| pair_rep      {A B}      : entails [] ⊀ $ βˆ€[A 𝕏 B] $ βˆƒ[A,B] $ ↑2 ≃[A 𝕏 B] βŸͺ↑1,↑0⟫
| pair_distinct {A B}      : entails [] ⊀ $ βˆ€[A,B,A,B] $ (βŸͺ↑3,↑2⟫ ≃[A 𝕏 B] βŸͺ↑1,↑0⟫) ⟹ ((↑3 ≃[A] ↑1) β‹€ (↑2 ≃[B] ↑0))
| sub      {Ξ“} (B) (b p q) : WF Ξ“ B b β†’ entails (B::Ξ“) p q β†’ entails Ξ“ (⁅p // b⁆) (⁅q // b⁆)
| comp     {Ξ“} (A) (Ο†)     : WF (A::Ξ“) Ξ© Ο† β†’ entails Ξ“ ⊀ (βˆ€' A $ (↑0 ∈ (^ ⟦A | Ο†βŸ§)) ⇔ Ο†)

view this post on Zulip Mario Carneiro (Jun 26 2020 at 11:35):

It's not true

view this post on Zulip Mario Carneiro (Jun 26 2020 at 11:37):

for example with phi = p, a variable of type Omega, and psi = βŠ₯, then the antecedent is true because entails [p:Ξ©] ⊀ p is false, but entails [p:Ξ©] ⊀ (p -> βŠ₯) is also false

view this post on Zulip Mario Carneiro (Jun 26 2020 at 11:39):

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

view this post on Zulip Mario Carneiro (Jun 26 2020 at 11:40):

because then you can just instantiate it with context (Ο†::Ξ“) to derive entails (Ο†::Ξ“) ⊀ ψ, after which you can use imp intro to derive entails Ξ“ ⊀ (Ο† -> ψ)

view this post on Zulip Mario Carneiro (Jun 26 2020 at 11:41):

wait, where is your imp intro?

view this post on Zulip Mario Carneiro (Jun 26 2020 at 11:42):

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

view this post on Zulip Mario Carneiro (Jun 26 2020 at 11:43):

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

view this post on Zulip Billy Price (Jun 26 2020 at 11:43):

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

lemma from_imp {Ξ“ : context} : entails Ξ“ ⊀ (q ⟹ r) β†’ entails Ξ“ q r :=
begin
  intro h₁,
  apply entails.cut _ (⊀ β‹€ q) _,
  apply_rules [entails.and_intro, entails.vac, entails.axm];
    { apply @WF.imp_left _ q r,
      exact WF.proof_right h₁
    },
  exact entails.imp_to_and h₁,
end

lemma to_imp {Ξ“ : context} : entails Ξ“ q r β†’ entails Ξ“ ⊀ (q ⟹ r) :=
begin
  intro h₁,
  apply_rules [entails.and_to_imp, entails.cut _ q _, entails.and_right _ ⊀ _, entails.axm],
  WF_prover,
  apply WF.proof_left h₁,
end

view this post on Zulip Mario Carneiro (Jun 26 2020 at 11:44):

So yeah you have to have the assumption \all p, entails Ξ“ p Ο† β†’ entails Ξ“ p ψ at which point the theorem is trivial

view this post on Zulip Billy Price (Jun 26 2020 at 11:44):

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

view this post on Zulip Billy Price (Jun 26 2020 at 11:47):

Ah that makes sense, it's strengthening the hypotheses to ensure that the function entails Ξ“ p Ο† β†’ entails Ξ“ p ψ doesn't just just rely on entails Ξ“ p Ο† being false.

view this post on Zulip Billy Price (Jul 01 2020 at 03:41):

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

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

view this post on Zulip Kevin Buzzard (Jul 01 2020 at 06:46):

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

view this post on Zulip Kevin Buzzard (Jul 01 2020 at 06:47):

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

view this post on Zulip Billy Price (Jul 01 2020 at 11:06):

the latter

view this post on Zulip Billy Price (Jul 01 2020 at 11:14):

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

view this post on Zulip Johan Commelin (Jul 01 2020 at 11:14):

Do you use elan?

view this post on Zulip Johan Commelin (Jul 01 2020 at 11:15):

I suggest using leanproject instead of leanpkg

view this post on Zulip Billy Price (Jul 01 2020 at 11:18):

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

view this post on Zulip Billy Price (Jul 01 2020 at 11:18):

What do I do instead of leanpkg configure with leanproject?

view this post on Zulip Billy Price (Jul 01 2020 at 11:24):

Just straight to leanproject build?

view this post on Zulip Billy Price (Jul 01 2020 at 11:27):

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

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

and this

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

and this

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

Is this a problem with the commit?

view this post on Zulip Billy Price (Jul 01 2020 at 11:30):

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

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

view this post on Zulip Billy Price (Jul 01 2020 at 12:03):

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

view this post on Zulip Reid Barton (Jul 01 2020 at 13:40):

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

view this post on Zulip Jannis Limperg (Jul 01 2020 at 14:00):

What Reid said. This recipe should work:

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

The Lean update may require minor changes to your code.

view this post on Zulip Reid Barton (Jul 01 2020 at 14:02):

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

view this post on Zulip Reid Barton (Jul 01 2020 at 14:03):

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

view this post on Zulip Billy Price (Jul 02 2020 at 00:19):

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

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

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

view this post on Zulip Billy Price (Jul 02 2020 at 00:20):

Oh I just saw Reid's first reply

view this post on Zulip Billy Price (Jul 07 2020 at 03:26):

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

view this post on Zulip Alex J. Best (Jul 07 2020 at 03:39):

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

view this post on Zulip Billy Price (Jul 07 2020 at 03:48):

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

view this post on Zulip Billy Price (Jul 09 2020 at 11:58):

(deleted)

view this post on Zulip Billy Price (Jul 09 2020 at 12:13):

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

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

lemma all_sub {A Ο† a} : WF (A :: Ξ“) Ξ© Ο† β†’ entails (A::Ξ“) (^ (βˆ€' A Ο†)) (φ⁅a⁆)

(the ^ means lift 1 0).

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

| all_elim   {Ξ“} {p Ο† A}   : entails Ξ“ p (βˆ€' A Ο†) β†’ entails (A::Ξ“) (^ p) Ο†
| all_intro  {Ξ“} {p Ο†} (A) : entails (A::Ξ“) (^ p) Ο† β†’ entails Ξ“ p (βˆ€' A Ο†)
| sub      {Ξ“} {p q} (B b) : WF Ξ“ B b β†’ entails (B::Ξ“) p q β†’ entails Ξ“ (p⁅b⁆) (q⁅b⁆)

This is the proof so far,

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

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

1 goal
Ξ“: context
A: type
Ο†a: term
wf: WF (A :: Ξ“) Ξ© Ο†
⊒ entails (A :: Ξ“) Ο† φ⁅a//0⁆

It was possible to prove a slight variation of this here

lemma meta_all_sub {A Ο† a} : WF Ξ“ A a β†’ entails Ξ“ ⊀ (βˆ€' A Ο†) β†’ entails Ξ“ ⊀ (φ⁅a⁆) :=
begin
  intros wfa ent_all,
  have : (⊀ : term) =  βŠ€β…a⁆, by refl, rw this,
  apply sub _ _ wfa,
  have : (⊀ : term) = ^ ⊀, by refl, rw this,
  exact all_elim ent_all
end

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

view this post on Zulip Mario Carneiro (Jul 09 2020 at 12:18):

what's the theorem?

view this post on Zulip Billy Price (Jul 09 2020 at 12:18):

lemma all_sub {A Ο† a} : WF (A :: Ξ“) Ξ© Ο† β†’ entails (A::Ξ“) (^ (βˆ€' A Ο†)) (φ⁅a⁆)

view this post on Zulip Mario Carneiro (Jul 09 2020 at 12:20):

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

lemma all_sub {A Ο† a} : WF Ξ“ a A β†’ WF (A :: Ξ“) Ξ© Ο† β†’ entails Ξ“ (βˆ€' A Ο†) (φ⁅a⁆)

view this post on Zulip Billy Price (Jul 09 2020 at 12:20):

Yep that's an oversight

view this post on Zulip Mario Carneiro (Jul 09 2020 at 12:21):

It should be provable without induction

view this post on Zulip Billy Price (Jul 09 2020 at 12:24):

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

view this post on Zulip Billy Price (Jul 09 2020 at 12:25):

(those are all entails.*)

view this post on Zulip Mario Carneiro (Jul 09 2020 at 12:25):

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

view this post on Zulip Billy Price (Jul 09 2020 at 12:47):

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

lemma all_sub {A Ο† a} : WF Ξ“ A a β†’ WF (A :: Ξ“) Ξ© Ο† β†’ entails (A::Ξ“) (^ (βˆ€' A Ο†)) (φ⁅a⁆) :=
begin
  intros wfa wfφ,
  have : (^ (βˆ€' A Ο†)) = (^ (βˆ€' A Ο†))⁅a⁆, by sorry,
  rw this,
  refine sub _ _ wfa _,
  refine all_elim _,
  refine axm _,
  WF_prover
end

view this post on Zulip Mario Carneiro (Jul 09 2020 at 22:51):

the have line should be (^ (βˆ€' A Ο†))⁅a⁆ = (βˆ€' A Ο†)

view this post on Zulip Mario Carneiro (Jul 09 2020 at 22:52):

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

view this post on Zulip Billy Price (Jul 10 2020 at 02:28):

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

view this post on Zulip Mario Carneiro (Jul 10 2020 at 02:32):

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

view this post on Zulip Mario Carneiro (Jul 10 2020 at 02:33):

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

view this post on Zulip Billy Price (Jul 10 2020 at 02:55):

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

view this post on Zulip Billy Price (Jul 10 2020 at 02:58):

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

view this post on Zulip Mario Carneiro (Jul 10 2020 at 04:02):

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

view this post on Zulip Mario Carneiro (Jul 10 2020 at 04:03):

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

view this post on Zulip Billy Price (Jul 10 2020 at 05:46):

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

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

view this post on Zulip Billy Price (Jul 10 2020 at 05:55):

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

view this post on Zulip Billy Price (Jul 10 2020 at 05:55):

(Unrelated to the proof i just posted)

view this post on Zulip Mario Carneiro (Jul 10 2020 at 06:05):

Only if h is a structure

view this post on Zulip Kenny Lau (Jul 10 2020 at 06:06):

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

view this post on Zulip Kenny Lau (Jul 10 2020 at 06:07):

let \<x\> := h in x

view this post on Zulip Mario Carneiro (Jul 10 2020 at 06:08):

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

view this post on Zulip Mario Carneiro (Jul 10 2020 at 06:09):

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

view this post on Zulip Billy Price (Jul 10 2020 at 06:39):

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

view this post on Zulip Billy Price (Jul 10 2020 at 06:55):

In light of the new substitution rule, does my axiom of comprehension still make sense?
| comp {Ξ“} (A) (Ο†) : WF (A::Ξ“) Ξ© Ο† β†’ entails Ξ“ ⊀ (βˆ€' A $ (↑0 ∈ (^ ⟦A | Ο†βŸ§)) ⇔ Ο†)

I'm lifting the set in order to prevent Russell's paradox and the like, but then when I try and prove this lemma I run into trouble

lemma elem_comp {H} {A Ο† a} : entails Ξ“ H (a ∈ (^ (⟦A | Ο†βŸ§))) β†’ entails Ξ“ H (φ⁅a⁆) :=
begin
  intro ent_elem,
  apply cut _ ent_elem,
  apply from_imp,
  have : ((a ∈ ^ (⟦ A | Ο† ⟧)) ⟹ φ⁅a//0⁆) = ((↑0 ∈ ^ (⟦ A | Ο† ⟧)) ⟹ Ο†)⁅a⁆, simp, sorry,
  sorry
end

the state before the first sorry is, in which the right conjunct isn't true.

Ξ“: context
H: term
A: type
Ο†a: term
ent_elem: entails Ξ“ H (a ∈ lift 1 0 ⟦ A | Ο† ⟧)
⊒ a = ↑0⁅a//0⁆ ∧ lift 1 1 Ο† = Ο†

Do I just need to change comp to this? (lifting the last phi)
| comp {Ξ“} (A) (Ο†) : WF (A::Ξ“) Ξ© Ο† β†’ entails Ξ“ ⊀ (βˆ€' A $ (↑0 ∈ (^ ⟦A | Ο†βŸ§)) ⇔ (lift 1 1 Ο†))

or is there a better alternative?

view this post on Zulip Mario Carneiro (Jul 10 2020 at 18:49):

What does ⟦A | Ο†βŸ§ mean?

view this post on Zulip Mario Carneiro (Jul 10 2020 at 18:51):

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

view this post on Zulip Mario Carneiro (Jul 10 2020 at 18:53):

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

view this post on Zulip Mario Carneiro (Jul 10 2020 at 18:55):

In this case a, A and live in context Ξ“ and Ο† is in context A::Ξ“ so a and ⟦A | Ο†βŸ§ live in the same context and no lifting is necessary

view this post on Zulip Billy Price (Jul 11 2020 at 04:29):

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

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

view this post on Zulip Billy Price (Jul 11 2020 at 04:52):

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

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

def lift (d : β„•) : β„• β†’ term β†’ term
| k ⁎          := ⁎
| k ⊀          := ⊀
| k βŠ₯          := βŠ₯
| k (p β‹€ q)    := (lift k p) β‹€ (lift k q)
| k (p ⋁ q)    := (lift k p) ⋁ (lift k q)
| k (p ⟹ q)   := (lift k p) ⟹ (lift k q)
| k (a ∈ α)    := (lift k a) ∈ (lift k α)
| k βŸͺa,b⟫      := βŸͺlift k a, lift k b⟫
| k (var m)    := if mβ‰₯k then var (m+d) else var m
| k ⟦A | Ο†βŸ§  :=   ⟦A | lift (k+1) Ο†βŸ§
| k (βˆ€' A Ο†)   := βˆ€' A $ lift (k+1) Ο†
| k (βˆƒ' A Ο†)   := βˆƒ' A $ lift (k+1) Ο†

def subst : β„• β†’ term β†’ term β†’ term
| n x ⁎          := ⁎
| n x ⊀          := ⊀
| n x βŠ₯          := βŠ₯
| n x (p β‹€ q)    := (subst n x p) β‹€ (subst n x q)
| n x (p ⋁ q)    := (subst n x p) ⋁ (subst n x q)
| n x (p ⟹ q)  := (subst n x p) ⟹ (subst n x q)
| n x (a ∈ α)    := (subst n x a) ∈ (subst n x α)
| n x βŸͺa,b⟫      := βŸͺsubst n x a, subst n x b⟫
| n x (var m)    := if n=m then x else (if m > n then var (m-1) else var m)
| n x ⟦ A | Ο† ⟧   := ⟦A | subst (n+1) (^ x) Ο†βŸ§
| n x (βˆ€' A Ο†)   := βˆ€' A (subst (n+1) (^ x) Ο†)
| n x (βˆƒ' A Ο†)   := βˆƒ' A (subst (n+1) (^ x) Ο†)

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

view this post on Zulip Mario Carneiro (Jul 11 2020 at 05:27):

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

view this post on Zulip Billy Price (Jul 11 2020 at 13:11):

Very interesting, thanks :)

view this post on Zulip Billy Price (Jul 12 2020 at 08:47):

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

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

view this post on Zulip Kevin Buzzard (Jul 12 2020 at 09:08):

Try the conv mode docs?

view this post on Zulip Kevin Buzzard (Jul 12 2020 at 09:09):

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

view this post on Zulip Billy Price (Jul 29 2020 at 04:04):

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

view this post on Zulip Kenny Lau (Jul 29 2020 at 07:37):

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

view this post on Zulip Kenny Lau (Jul 29 2020 at 07:38):

and I wouldn't call that theorem compactness?

view this post on Zulip Billy Price (Jul 30 2020 at 07:37):

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

inductive deduction : set Form β†’ Form β†’ Type

inductive provable (X : set Form) (A : Form) : Prop
| mk : deduction X A β†’ provable

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

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

inductive fin_provable (X : set Form) (A : Form) : Prop
| mk : fin_deduction X A β†’ fin_provable

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

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

view this post on Zulip Kenny Lau (Jul 30 2020 at 07:39):

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

view this post on Zulip Kenny Lau (Jul 30 2020 at 07:39):

so from a deduction you can produce a finite set Form

view this post on Zulip Kenny Lau (Jul 30 2020 at 07:39):

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

view this post on Zulip Kenny Lau (Jul 30 2020 at 07:41):

so you can produce:

def axioms_used : deduction X A β†’ { X' : set Form // X'.finite }

view this post on Zulip Kenny Lau (Jul 30 2020 at 07:42):

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

view this post on Zulip Kenny Lau (Jul 30 2020 at 07:42):

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

view this post on Zulip Kenny Lau (Jul 30 2020 at 07:43):

def extract_axioms : Ξ  {A : Form}, deduction X A β†’ { X' : set Form // X'.finite ∧ X' βŠ† X ∧ deduction X' A }

view this post on Zulip Kenny Lau (Jul 30 2020 at 07:44):

why not use finset?

view this post on Zulip Mario Carneiro (Jul 30 2020 at 09:27):

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

view this post on Zulip Mario Carneiro (Jul 30 2020 at 09:28):

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

view this post on Zulip Billy Price (Jul 30 2020 at 12:43):

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

view this post on Zulip Mario Carneiro (Jul 30 2020 at 13:09):

You can cast the finset to a set

view this post on Zulip Mario Carneiro (Jul 30 2020 at 13:11):

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

view this post on Zulip Billy Price (Jul 30 2020 at 13:25):

I see, not sure if I need that but maybe

view this post on Zulip Billy Price (Jul 30 2020 at 13:25):

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

failed to instantiate goal with (frozen_name has_union.union) XA' XB'
state:
X : set Form,
A B : Form,
dXA : X ≻ A,
dXB : X ≻ B,
XA' : finset Form,
AsubX : ↑XA' βŠ† X,
XA'A : ↑XA' ⊒I A,
XB' : finset Form,
BsubX : ↑XB' βŠ† X,
XB'B : ↑XB' ⊒I B
⊒ {X' // ↑X' βŠ† X ∧ ↑X' ⊒I A β‹€ B}

view this post on Zulip Mario Carneiro (Jul 30 2020 at 13:31):

try existsi