I don't understand forall in flypitch

Stream: maths

[Abhimanyu Pallavi Sudhir]

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?

[Johan Commelin]

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

[Abhimanyu Pallavi Sudhir]

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

[Johan Commelin]

Yup (that's my guess)

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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)

[Abhimanyu Pallavi Sudhir]

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.

[Kenny Lau]

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

[Abhimanyu Pallavi Sudhir]

ok, thanks

[Mario Carneiro]

@Abhimanyu Pallavi Sudhir The answer to your question is yes

[Mario Carneiro]

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

[Kenny Lau]

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

[Kenny Lau]

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