Zulip Chat Archive

Stream: general

Topic: Intuitionistic Type Theory Proofs


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

Hi there,

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

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

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

view this post on Zulip Reid Barton (Apr 15 2020 at 13:49):

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

view this post on Zulip Reid Barton (Apr 15 2020 at 13:53):

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

view this post on Zulip Patrick Massot (Apr 15 2020 at 13:56):

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

view this post on Zulip Billy Price (Apr 15 2020 at 13:57):

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

view this post on Zulip Kevin Buzzard (Apr 15 2020 at 13:58):

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

view this post on Zulip Andrew Ashworth (Apr 15 2020 at 13:59):

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

view this post on Zulip Billy Price (Apr 15 2020 at 14:03):

Patrick Massot said:

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

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

view this post on Zulip Patrick Massot (Apr 15 2020 at 14:11):

@Floris van Doorn @Jesse Michael Han

view this post on Zulip Jesse Michael Han (Apr 15 2020 at 17:44):

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

view this post on Zulip Floris van Doorn (Apr 16 2020 at 05:22):

Provability is defined in the repository:

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

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

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

view this post on Zulip Billy Price (Apr 25 2020 at 03:07):

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

structure PowerSet (A : Type) : Type

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

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

view this post on Zulip Donald Sebastian Leung (Apr 25 2020 at 03:09):

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

view this post on Zulip Billy Price (Apr 25 2020 at 03:13):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 04:01):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 04:02):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 04:02):

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

view this post on Zulip Billy Price (Apr 25 2020 at 04:33):

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

view this post on Zulip Kenny Lau (Apr 25 2020 at 04:35):

elem x is different for each x : Type

view this post on Zulip Kenny Lau (Apr 25 2020 at 04:35):

what does PowerSet A do?

view this post on Zulip Kenny Lau (Apr 25 2020 at 04:36):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 04:36):

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

view this post on Zulip Billy Price (Apr 25 2020 at 04:37):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 04:37):

but the problem is that A can be anything

view this post on Zulip Kenny Lau (Apr 25 2020 at 04:37):

I claim that PowerSet A -> false for all A

view this post on Zulip Mario Carneiro (Apr 25 2020 at 04:38):

that's false, PowerSet A ~= unit

view this post on Zulip Kenny Lau (Apr 25 2020 at 04:38):

I don't understand structures

view this post on Zulip Billy Price (Apr 25 2020 at 04:39):

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

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

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 04:39):

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

view this post on Zulip Kenny Lau (Apr 25 2020 at 04:39):

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

view this post on Zulip Kenny Lau (Apr 25 2020 at 04:39):

now I can claim that type -> false

view this post on Zulip Billy Price (Apr 25 2020 at 04:40):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 04:40):

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

view this post on Zulip Kenny Lau (Apr 25 2020 at 04:40):

structure PowerSet (A : Type) : Type

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

view this post on Zulip Kenny Lau (Apr 25 2020 at 04:40):

I'm not sure if this is the intended interpretation

view this post on Zulip Kenny Lau (Apr 25 2020 at 04:41):

@Mario Carneiro I see

view this post on Zulip Mario Carneiro (Apr 25 2020 at 04:42):

Here's an easy fix:

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

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 04:42):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 04:42):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 04:43):

Also, type is empty

view this post on Zulip Mario Carneiro (Apr 25 2020 at 04:45):

Here's a more well typed version

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

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

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

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

view this post on Zulip Billy Price (Apr 25 2020 at 04:46):

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

view this post on Zulip Kenny Lau (Apr 25 2020 at 04:47):

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

view this post on Zulip Kenny Lau (Apr 25 2020 at 04:47):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 04:47):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 04:47):

because the definition of term depends on formula and vice versa

view this post on Zulip Billy Price (Apr 25 2020 at 04:51):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 04:52):

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

view this post on Zulip Kenny Lau (Apr 25 2020 at 04:53):

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

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

view this post on Zulip Kenny Lau (Apr 25 2020 at 04:53):

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

view this post on Zulip Kenny Lau (Apr 25 2020 at 04:53):

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

view this post on Zulip Kenny Lau (Apr 25 2020 at 04:53):

which is required in b3 and b5

view this post on Zulip Kenny Lau (Apr 25 2020 at 04:53):

but here's b2 formalized @Billy Price

view this post on Zulip Mario Carneiro (Apr 25 2020 at 04:55):

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

view this post on Zulip Billy Price (Apr 25 2020 at 04:56):

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

view this post on Zulip Kenny Lau (Apr 25 2020 at 04:56):

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

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

view this post on Zulip Kenny Lau (Apr 25 2020 at 04:56):

how does this look

view this post on Zulip Mario Carneiro (Apr 25 2020 at 04:57):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 04:58):

and you are still missing var

view this post on Zulip Mario Carneiro (Apr 25 2020 at 04:59):

also star,true,false

view this post on Zulip Kenny Lau (Apr 25 2020 at 05:01):

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

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

view this post on Zulip Kenny Lau (Apr 25 2020 at 05:02):

what do you mean by use de Bruijn variables?

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:02):

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

view this post on Zulip Billy Price (Apr 25 2020 at 05:03):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:03):

You have to define subst by recursion

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:04):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:04):

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

view this post on Zulip Kenny Lau (Apr 25 2020 at 05:04):

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

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

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:05):

yep

view this post on Zulip Kenny Lau (Apr 25 2020 at 05:05):

this doesn't use de Bruijn though

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:05):

no

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:05):

this is the named variables approach

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:05):

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

view this post on Zulip Kenny Lau (Apr 25 2020 at 05:06):

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

view this post on Zulip Kenny Lau (Apr 25 2020 at 05:06):

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

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

view this post on Zulip Kenny Lau (Apr 25 2020 at 05:06):

like this?

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:06):

It affects FV and subst

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:06):

but yes, in the definition itself that's all

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:07):

you need operations like lift too

view this post on Zulip Kenny Lau (Apr 25 2020 at 05:07):

what's the signature of lift?

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:08):

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

view this post on Zulip Kenny Lau (Apr 25 2020 at 05:08):

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

view this post on Zulip Kenny Lau (Apr 25 2020 at 05:08):

is this right?

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:09):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:09):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:10):

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

view this post on Zulip Billy Price (Apr 25 2020 at 05:10):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:11):

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

view this post on Zulip Billy Price (Apr 25 2020 at 05:12):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:12):

yes, that's their secret weapon

view this post on Zulip Billy Price (Apr 25 2020 at 05:14):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:15):

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

view this post on Zulip Billy Price (Apr 25 2020 at 05:15):

(deleted)

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:15):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:15):

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

view this post on Zulip Billy Price (Apr 25 2020 at 05:19):

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

view this post on Zulip Billy Price (Apr 25 2020 at 05:19):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:20):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:20):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:23):

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

view this post on Zulip Billy Price (Apr 25 2020 at 05:25):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:26):

The general lift comes up when you define lift by recursion

view this post on Zulip Billy Price (Apr 25 2020 at 05:26):

Ah okay

view this post on Zulip Billy Price (Apr 25 2020 at 05:28):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:29):

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

view this post on Zulip Billy Price (Apr 25 2020 at 05:29):

So I'm limited to only substituting variable 0?

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:30):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:30):

You should only ever have to substitute variable 0

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:30):

because of the way the binders are set up

view this post on Zulip Billy Price (Apr 25 2020 at 05:31):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:32):

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

view this post on Zulip Mario Carneiro (Apr 25 2020 at 05:34):

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

view this post on Zulip Billy Price (Apr 25 2020 at 05:35):

Cheers, will do

view this post on Zulip Billy Price (Apr 25 2020 at 05:38):

Thanks again for your help :)

view this post on Zulip Patrick Massot (Apr 25 2020 at 09:38):

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

view this post on Zulip Donald Sebastian Leung (Apr 25 2020 at 09:50):

Perhaps we could create a stream "computer science"?

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

view this post on Zulip Patrick Massot (Apr 25 2020 at 09:52):

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

view this post on Zulip Kenny Lau (Apr 25 2020 at 09:52):

Computer Science, Logic, Program Verification

view this post on Zulip Patrick Massot (Apr 25 2020 at 09:53):

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

view this post on Zulip Billy Price (Apr 25 2020 at 10:51):

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

view this post on Zulip Kevin Buzzard (Apr 25 2020 at 11:08):

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

view this post on Zulip Patrick Massot (Apr 25 2020 at 11:21):

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

view this post on Zulip Billy Price (Apr 25 2020 at 11:23):

Okay no worries :)

view this post on Zulip Patrick Massot (Apr 25 2020 at 11:29):

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

view this post on Zulip Billy Price (Apr 28 2020 at 12:56):

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

view this post on Zulip Patrick Massot (Apr 28 2020 at 12:57):

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

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

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

view this post on Zulip Mario Carneiro (Apr 28 2020 at 12:58):

Logic is also a bit unclear

view this post on Zulip Billy Price (Apr 28 2020 at 12:58):

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

view this post on Zulip Patrick Massot (Apr 28 2020 at 12:59):

Yes, same level

view this post on Zulip Mario Carneiro (Apr 28 2020 at 12:59):

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

view this post on Zulip Patrick Massot (Apr 28 2020 at 12:59):

Things inside are called topics or threads

view this post on Zulip Patrick Massot (Apr 28 2020 at 12:59):

(Zulip says topic)

view this post on Zulip Patrick Massot (Apr 28 2020 at 13:00):

Mario Carneiro said:

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

I hope that would help raise this amount

view this post on Zulip Patrick Massot (Apr 28 2020 at 13:00):

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

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

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

view this post on Zulip Johan Commelin (Apr 28 2020 at 13:01):

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

view this post on Zulip Johan Commelin (Apr 28 2020 at 13:01):

It is easier to disable a stream than to discover it

view this post on Zulip Kevin Buzzard (Apr 28 2020 at 13:02):

(deleted)


Last updated: May 14 2021 at 03:27 UTC