Zulip Chat Archive

Stream: maths

Topic: I don't understand forall in flypitch


view this post on Zulip Abhimanyu Pallavi Sudhir (Jul 29 2020 at 07:01):

I'm reading flypitch, and in the definition of preformula, we have:

inductive preformula :   Type u
...
| all (f : preformula 0) : preformula 0

I must be missing something -- don't we need to specify which variable we're quantifying over? How do we distinguish forall x, x < y from forall y, x < y?

view this post on Zulip Johan Commelin (Jul 29 2020 at 07:04):

I guess it uses de Bruijn indices, and so f contains the info

view this post on Zulip Abhimanyu Pallavi Sudhir (Jul 29 2020 at 07:09):

I see, so the x < y in forall x, x < y is different from the x < y in forall y, x < y.

view this post on Zulip Johan Commelin (Jul 29 2020 at 07:10):

Yup (that's my guess)

view this post on Zulip Kenny Lau (Jul 29 2020 at 07:19):

/- preterm L l is a partially applied term. if applied to n terms, it becomes a term.
* Every element of preterm L 0 is a well-formed term.
* We use this encoding to avoid mutual or nested inductive types, since those are not too convenient to work with in Lean. -/
inductive preterm :   Type u
| var {} :  (k : ), preterm 0
| func :  {l : } (f : L.functions l), preterm l
| app :  {l : } (t : preterm (l + 1)) (s : preterm 0), preterm l
export preterm

@[reducible] def term := preterm L 0

/- preformula l is a partially applied formula. if applied to n terms, it becomes a formula.
  * We only have implication as binary connective. Since we use classical logic, we can define
    the other connectives from implication and falsum.
  * Similarly, universal quantification is our only quantifier.
  * We could make `falsum` and `equal` into elements of rel. However, if we do that, then we cannot make the interpretation of them in a model definitionally what we want.
-/
variable (L)
inductive preformula :   Type u
| falsum {} : preformula 0
| equal (t₁ t₂ : term L) : preformula 0
| rel {l : } (R : L.relations l) : preformula l
| apprel {l : } (f : preformula (l + 1)) (t : term L) : preformula l
| imp (f₁ f₂ : preformula 0) : preformula 0
| all (f : preformula 0) : preformula 0
export preformula
@[reducible] def formula := preformula L 0

view this post on Zulip Kenny Lau (Jul 29 2020 at 07:21):

so presumably x,x<y\forall x, x < y is all (apprel (apprel (rel ()) (var 0)) (var 1)) and y,x<y\forall y, x < y is with 0 and 1 swapped

view this post on Zulip Kenny Lau (Jul 29 2020 at 07:22):

more evidence is:

/- subst_term t s n substitutes s for (&n) and reduces the level of all variables above n by 1 -/
def subst_term :  {l}, preterm L l  term L    preterm L l
| _ &k          s n := subst_realize var (s  n) n k
| _ (func f)    s n := func f
| _ (app t₁ t₂) s n := app (subst_term t₁ s n) (subst_term t₂ s n)

@[simp] def subst_formula :  {l}, preformula L l  term L    preformula L l
| _ falsum       s n := falsum
| _ (t₁  t₂)    s n := subst_term t₁ s n  subst_term t₂ s n
| _ (rel R)      s n := rel R
| _ (apprel f t) s n := apprel (subst_formula f s n) (subst_term t s n)
| _ (f₁  f₂)   s n := subst_formula f₁ s n  subst_formula f₂ s n
| _ (' f)       s n := ' subst_formula f s (n+1)

view this post on Zulip Abhimanyu Pallavi Sudhir (Jul 29 2020 at 07:31):

Right -- so we always quantify over var 0.

So if we want to say forall z, x < y, we'd write the same thing with 0 and 1 replaced with 1 and 2, etc.

view this post on Zulip Kenny Lau (Jul 29 2020 at 07:32):

you would actually need to look at how a formula is interpreted, but the file is too big and causes performance issues for my humble chrome browser so I'm afraid I can't help you with that

view this post on Zulip Abhimanyu Pallavi Sudhir (Jul 29 2020 at 07:33):

ok, thanks

view this post on Zulip Mario Carneiro (Jul 29 2020 at 07:52):

@Abhimanyu Pallavi Sudhir The answer to your question is yes

view this post on Zulip Mario Carneiro (Jul 29 2020 at 07:53):

@Kenny Lau I don't think formula interpretation comes into it? He's just talking about writing formulae

view this post on Zulip Kenny Lau (Jul 29 2020 at 07:54):

well to know what formula a term of pre_formula 0 represents, one needs to look at the code where they define interpretation of a pre_formula 0

view this post on Zulip Kenny Lau (Jul 29 2020 at 07:54):

/- realization of formulas -/
@[simp] def realize_formula {S : Structure L} : {l}, (  S)  preformula L l  dvector S l  Prop
| _ v falsum       xs := false
| _ v (t₁  t₂)    xs := realize_term v t₁ xs = realize_term v t₂ xs
| _ v (rel R)      xs := S.rel_map R xs
| _ v (apprel f t) xs := realize_formula v f $ realize_term v t ([])::xs
| _ v (f₁  f₂)   xs := realize_formula v f₁ xs  realize_formula v f₂ xs
| _ v (' f)       xs := (x : S), realize_formula (v [x // 0]) f xs

Last updated: May 06 2021 at 18:20 UTC