Flypitch.FOL.Syntax defines first-order languages, terms, and the de Bruijn-style lifting and substitution operations on them. The lemmas in this file are the basic bookkeeping tools used throughout the later semantic and proof-theoretic developments.

def Flypitch.fol.subst_realize {S : Type u} (v : ℕ → S) (x : S) (n k : ℕ) : S

Given a valuation v, replace the variable at index n by x.

Equations

• (v[x // n]) k = if k < n then v k else if n < k then v (k - 1) else x

def Flypitch.fol.«term_[_//_]» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Flypitch.fol.subst_realize_lt {S : Type u} (v : ℕ → S) (x : S) {n k : ℕ} (h : k < n) : (v[x // n]) k = v k

@[simp]

theorem Flypitch.fol.subst_realize_gt {S : Type u} (v : ℕ → S) (x : S) {n k : ℕ} (h : n < k) : (v[x // n]) k = v (k - 1)

@[simp]

theorem Flypitch.fol.subst_realize_var_eq {S : Type u} (v : ℕ → S) (x : S) (n : ℕ) : (v[x // n]) n = x

theorem Flypitch.fol.subst_realize_congr {S : Type u} {v v' : ℕ → S} (hv : ∀ (k : ℕ), v k = v' k) (x : S) (n k : ℕ) : (v[x // n]) k = (v'[x // n]) k

Pointwise-equal valuations give the same substituted valuation.

theorem Flypitch.fol.subst_realize2_0 {S : Type u} (v : ℕ → S) (x x' : S) (n k : ℕ) : (v[x' // n][x // 0]) k = (v[x // 0][x' // n + 1]) k

Commuting the substitutions at 0 and n + 1 on valuations.

structure Flypitch.fol.Language : Type (u + 1)

A first-order language is given by its function and relation symbols, indexed by arity.

• functions : ℕ → Type u
• relations : ℕ → Type u

def Flypitch.fol.Language.constants (L : Language) : Type u

Nullary function symbols of a language.

Equations

• L.constants = L.functions 0

inductive Flypitch.fol.preterm (L : Language) : ℕ → Type u

preterm L l is a partially applied term requiring l more arguments.

• var {L : Language} : ℕ → preterm L 0
• func {L : Language} {l : ℕ} : L.functions l → preterm L l
• app {L : Language} {l : ℕ} : preterm L (l + 1) → preterm L 0 → preterm L l

@[reducible, inline]

abbrev Flypitch.fol.term (L : Language) : Type u_1

Closed terms.

Equations

• Flypitch.fol.term L = Flypitch.fol.preterm L 0

def Flypitch.fol.«term&_» : Lean.ParserDescr

Equations

• Flypitch.fol.«term&_» = Lean.ParserDescr.node `Flypitch.fol.«term&_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "&") (Lean.ParserDescr.cat `term 1024))

def Flypitch.fol.apps {L : Language} {l : ℕ} : preterm L l → dvector (term L) l → term L

Fully apply a partially applied term to a tuple of arguments.

Equations

• Flypitch.fol.apps t Flypitch.dvector.nil = t
• Flypitch.fol.apps t (Flypitch.dvector.cons x_3 xs) = Flypitch.fol.apps (t.app x_3) xs

@[simp]

theorem Flypitch.fol.apps_zero {L : Language} (t : term L) (ts : dvector (term L) 0) : apps t ts = t

theorem Flypitch.fol.apps_eq_app {L : Language} {l : ℕ} (t : preterm L (l + 1)) (s : term L) (ts : dvector (term L) l) : ∃ (t' : preterm L (0 + 1)) (s' : preterm L 0), apps t (dvector.cons s ts) = t'.app s'

Applying at least one argument produces an explicit preterm.app.

noncomputable def Flypitch.fol.term.rec {L : Language} {C : term L → Sort v} (hvar : (k : ℕ) → C &k) (hfunc : {l : ℕ} → (f : L.functions l) → (ts : dvector (term L) l) → ((t : term L) → dvector.pmem t ts → C t) → C (apps (preterm.func f) ts)) (t : term L) : C t

Dependent recursor on terms that exposes the full argument vector of each function symbol.

Equations

• One or more equations did not get rendered due to their size.

def Flypitch.fol.term.elim' {L : Language} {C : Type v} (hvar : ℕ → C) (hfunc : {l : ℕ} → L.functions l → dvector (term L) l → dvector C l → C) {l : ℕ} (_t : preterm L l) (_ts : dvector (term L) l) (_ih_ts : dvector C l) : C

Non-dependent eliminator on partially applied terms with accumulated recursive results.

Equations

• One or more equations did not get rendered due to their size.
• Flypitch.fol.term.elim' hvar hfunc (&k) x_4 x_5 = hvar k
• Flypitch.fol.term.elim' hvar hfunc (Flypitch.fol.preterm.func f) x✝¹ x✝ = hfunc f x✝¹ x✝

def Flypitch.fol.term.elim {L : Language} {C : Type v} (hvar : ℕ → C) (hfunc : {l : ℕ} → L.functions l → dvector (term L) l → dvector C l → C) (_t : term L) : C

Non-dependent eliminator on closed terms.

Equations

• Flypitch.fol.term.elim hvar hfunc t = Flypitch.fol.term.elim' hvar (fun {l : ℕ} => hfunc) t Flypitch.dvector.nil Flypitch.dvector.nil

theorem Flypitch.fol.term.elim'_apps {L : Language} {C : Type v} (hvar : ℕ → C) (hfunc : {l : ℕ} → L.functions l → dvector (term L) l → dvector C l → C) {l : ℕ} (t : preterm L l) (ts : dvector (term L) l) : elim' hvar (fun {l : ℕ} => hfunc) (apps t ts) dvector.nil dvector.nil = elim' hvar (fun {l : ℕ} => hfunc) t ts (dvector.map (elim hvar fun {l : ℕ} => hfunc) ts)

Compatibility of term.elim' with apps.

theorem Flypitch.fol.term.elim_apps {L : Language} {C : Type v} (hvar : ℕ → C) (hfunc : {l : ℕ} → L.functions l → dvector (term L) l → dvector C l → C) {l : ℕ} (f : L.functions l) (ts : dvector (term L) l) : elim hvar (fun {l : ℕ} => hfunc) (apps (preterm.func f) ts) = hfunc f ts (dvector.map (elim hvar fun {l : ℕ} => hfunc) ts)

Compatibility of term.elim with function application.

def Flypitch.fol.preterm.change_arity' {L : Language} {l l' : ℕ} : l = l' → preterm L l → preterm L l'

Equations

• Flypitch.fol.preterm.change_arity' ⋯ &k = &k
• Flypitch.fol.preterm.change_arity' ⋯ (Flypitch.fol.preterm.func f) = Flypitch.fol.preterm.func f
• Flypitch.fol.preterm.change_arity' ⋯ (t₁.app t₂) = (Flypitch.fol.preterm.change_arity' ⋯ t₁).app t₂

@[simp]

theorem Flypitch.fol.preterm.change_arity'_rfl {L : Language} {l : ℕ} (t : preterm L l) : change_arity' ⋯ t = t

theorem Flypitch.fol.apps_ne_var {L : Language} {l : ℕ} {f : L.functions l} {ts : dvector (term L) l} {k : ℕ} : apps (preterm.func f) ts ≠ &k

A fully applied function symbol can never be a variable.

def Flypitch.fol.lift_term_at {L : Language} {l : ℕ} : preterm L l → ℕ → ℕ → preterm L l

lift_term_at t n m raises variables in t at or above m by n.

Equations

• (&k ↑' x✝¹ # x✝) = if x✝ ≤ k then &(k + x✝¹) else &k
• (Flypitch.fol.preterm.func f ↑' x✝¹ # x✝) = Flypitch.fol.preterm.func f
• (t₁.app t₂ ↑' x✝¹ # x✝) = (t₁ ↑' x✝¹ # x✝).app (t₂ ↑' x✝¹ # x✝)

def Flypitch.fol.lift_term {L : Language} {l : ℕ} : preterm L l → ℕ → preterm L l

Lift every free variable of a term by n.

Equations

• x✝¹ ↑ x✝ = x✝¹ ↑' x✝ # 0

def Flypitch.fol.lift_term1 {L : Language} {l : ℕ} : preterm L l → preterm L l

Lift every free variable of a term by one.

Equations

• Flypitch.fol.lift_term1 x✝ = x✝ ↑ 1

def Flypitch.fol.«term_↑'_#_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Flypitch.fol.«term_↑_» : Lean.TrailingParserDescr

Equations

• Flypitch.fol.«term_↑_» = Lean.ParserDescr.trailingNode `Flypitch.fol.«term_↑_» 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↑ ") (Lean.ParserDescr.cat `term 101))

theorem Flypitch.fol.lift_term_def {L : Language} {l : ℕ} (t : preterm L l) (n : ℕ) : (t ↑' n # 0) = t ↑ n

lift_term is lift_term_at specialized to cutoff 0.

@[simp]

theorem Flypitch.fol.lift_term_at_zero {L : Language} {l : ℕ} (t : preterm L l) (m : ℕ) : (t ↑' 0 # m) = t

@[simp]

theorem Flypitch.fol.lift_term_at_apps {L : Language} {l : ℕ} (t : preterm L l) (ts : dvector (term L) l) (n m : ℕ) : (apps t ts ↑' n # m) = apps (t ↑' n # m) (dvector.map (fun (x : preterm L 0) => x ↑' n # m) ts)

def Flypitch.fol.subst_term {L : Language} {l : ℕ} : preterm L l → term L → ℕ → preterm L l

Substitute s for variable n, lowering higher variables by one.

Equations

• &k[x✝¹ // x✝] = (Flypitch.fol.preterm.var[x✝¹ ↑' x✝ # 0 // x✝]) k
• Flypitch.fol.preterm.func f[x✝¹ // x✝] = Flypitch.fol.preterm.func f
• t₁.app t₂[x✝¹ // x✝] = t₁[x✝¹ // x✝].app (t₂[x✝¹ // x✝])

def Flypitch.fol.«term_[_//_]_1» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Flypitch.fol.subst_term_var_lt {L : Language} (s : term L) {k n : ℕ} (h : k < n) : &k[s // n] = &k

@[simp]

theorem Flypitch.fol.subst_term_var_gt {L : Language} (s : term L) {k n : ℕ} (h : n < k) : &k[s // n] = &(k - 1)

@[simp]

theorem Flypitch.fol.subst_term_var_eq {L : Language} (s : term L) (n : ℕ) : &n[s // n] = s ↑' n # 0

@[simp]

theorem Flypitch.fol.subst_term_apps {L : Language} {l : ℕ} (t : preterm L l) (ts : dvector (term L) l) (s : term L) (n : ℕ) : apps t ts[s // n] = apps (t[s // n]) (dvector.map (fun (x : preterm L 0) => x[s // n]) ts)

@[simp]

theorem Flypitch.fol.lift_term1_lift_term_at {L : Language} {l : ℕ} (t : preterm L l) (n m : ℕ) : (t ↑' n # m) ↑ 1 = t ↑ 1 ↑' n # m + 1

@[simp]

theorem Flypitch.fol.lift_term_succ {L : Language} {l : ℕ} (t : preterm L l) (n : ℕ) : (t ↑ n) ↑ 1 = t ↑ (n + 1)

@[simp]

theorem Flypitch.fol.lift_term_zero {L : Language} {l : ℕ} (t : preterm L l) : t ↑ 0 = t

theorem Flypitch.fol.lift_term_at2_small {L : Language} {l : ℕ} (t : preterm L l) (n n' : ℕ) {m m' : ℕ} : m' ≤ m → ((t ↑' n # m) ↑' n' # m') = (t ↑' n' # m') ↑' n # m + n'

Commute two lifts when the second cutoff is no larger than the first.

theorem Flypitch.fol.lift_term_at2_medium {L : Language} {l : ℕ} (t : preterm L l) {n : ℕ} (n' : ℕ) {m m' : ℕ} : m ≤ m' → m' ≤ m + n → ((t ↑' n # m) ↑' n' # m') = t ↑' n + n' # m

Collapse two lifts when the second cutoff lies inside the first lifted block.

theorem Flypitch.fol.lift_term2_medium {L : Language} {l : ℕ} (t : preterm L l) {n : ℕ} (n' : ℕ) {m' : ℕ} (h : m' ≤ n) : (t ↑ n ↑' n' # m') = t ↑ (n + n')

Global version of lift_term_at2_medium.

theorem Flypitch.fol.lift_term2 {L : Language} {l : ℕ} (t : preterm L l) (n n' : ℕ) : (t ↑ n) ↑ n' = t ↑ (n + n')

Successive global lifts add their shift amounts.

theorem Flypitch.fol.lift_term_at2_eq {L : Language} {l : ℕ} (t : preterm L l) (n n' m : ℕ) : ((t ↑' n # m) ↑' n' # m + n) = t ↑' n + n' # m

Special case of lift_term_at2_medium at the top of the lifted block.

theorem Flypitch.fol.lift_term_at2_large {L : Language} {l : ℕ} (t : preterm L l) {n : ℕ} (n' : ℕ) {m m' : ℕ} (h : m + n ≤ m') : ((t ↑' n # m) ↑' n' # m') = (t ↑' n' # m' - n) ↑' n # m

Commute two lifts when the second cutoff lies strictly above the first lifted block.

theorem Flypitch.fol.lift_at_subst_term_large {L : Language} {l : ℕ} (t : preterm L l) (s : term L) {n₁ : ℕ} (n₂ : ℕ) {m : ℕ} : m ≤ n₁ → (t ↑' n₂ # m)[s // n₁ + n₂] = t[s // n₁] ↑' n₂ # m

Substituting above the lift cutoff commutes with lifting.

theorem Flypitch.fol.lift_subst_term_large {L : Language} {l : ℕ} (t : preterm L l) (s : term L) (n₁ n₂ : ℕ) : t ↑ n₂[s // n₁ + n₂] = (t[s // n₁]) ↑ n₂

Global lifting commutes with substitution above the lifted block.

theorem Flypitch.fol.lift_subst_term_large' {L : Language} {l : ℕ} (t : preterm L l) (s : term L) (n₁ n₂ : ℕ) : t ↑ n₂[s // n₂ + n₁] = (t[s // n₁]) ↑ n₂

Commuted-index version of lift_subst_term_large.

theorem Flypitch.fol.lift_at_subst_term_medium {L : Language} {l : ℕ} (t : preterm L l) (s : term L) {n₁ n₂ m : ℕ} : m ≤ n₂ → n₂ ≤ m + n₁ → (t ↑' n₁ + 1 # m)[s // n₂] = t ↑' n₁ # m

Substituting inside the lifted block lowers the lift amount by one.

theorem Flypitch.fol.lift_subst_term_medium {L : Language} {l : ℕ} (t : preterm L l) (s : term L) (n₁ n₂ : ℕ) : t ↑ (n₁ + n₂ + 1)[s // n₁] = t ↑ (n₁ + n₂)

Global version of lift_at_subst_term_medium.

theorem Flypitch.fol.lift_at_subst_term_eq {L : Language} {l : ℕ} (t : preterm L l) (s : term L) (n : ℕ) : (t ↑' 1 # n)[s // n] = t

Lifting once and substituting at the cutoff cancels out.

theorem Flypitch.fol.subst_term2 {L : Language} {l : ℕ} (t : preterm L l) (s₁ s₂ : term L) (n₁ n₂ : ℕ) : t[s₁ // n₁][s₂ // n₁ + n₂] = t[s₂ // n₁ + n₂ + 1][s₁[s₂ // n₂] // n₁]

Composition law for two substitutions into a term.

@[simp]

theorem Flypitch.fol.lift_term1_subst_shift {L : Language} {l : ℕ} (t : preterm L l) (s : term L) (n : ℕ) : t ↑ 1[s // n + 1] = (t[s // n]) ↑ 1

@[simp]

theorem Flypitch.fol.lift_term1_subst_term {L : Language} {l : ℕ} (t : preterm L l) (s : term L) : t ↑ 1[s // 0] = t

Lifting once and then substituting at 0 recovers the original term.

@[simp]

theorem Flypitch.fol.lift_at_subst_term_small0 {L : Language} {l : ℕ} (t : preterm L l) (s : term L) (n m : ℕ) : (t ↑' n # m + 1)[s ↑' n # m // 0] = t[s // 0] ↑' n # m

Special case of lift_at_subst_term_small at variable 0.

theorem Flypitch.fol.lift_at_subst_term_small {L : Language} {l : ℕ} (t : preterm L l) (s : term L) (n₁ n₂ m : ℕ) : (t ↑' n₁ # m + n₂ + 1)[s ↑' n₁ # m // n₂] = t[s // n₂] ↑' n₁ # m + n₂

Substituting below the lift cutoff commutes with lifting the substituted term.

@[simp]

theorem Flypitch.fol.subst_term2_zero {L : Language} {l : ℕ} (t : preterm L l) (s₁ s₂ : term L) (n : ℕ) : t[s₁ // 0][s₂ // n] = t[s₂ // n + 1][s₁[s₂ // n] // 0]

Specialization of subst_term2 with the first substitution at variable 0.