Supporting results for pointwise provable equality.

Terms of first-order logic

This file defines the terms of first-order logic.

The bounded variables are denoted by #x for x : Fin n, and free variables are denoted by &x for x : ξ. t : Semiterm L ξ n is a (semi-)term of language L with bounded variables of Fin n and free variables of ξ.

inductive PointwiseComposition.FFL.FirstOrder.Semiterm (L : Language) (ξ : Type u_1) (n : ℕ) : Type (max u_1 u_2)

A semiterm of language L, with bound variables indexed by Fin n and free variables indexed by ξ. In FFL.FirstOrder.Semiformula, bound variables are de Bruijn indices with a separate type from free variables.

• bvar {L : Language} {ξ : Type u_1} {n : ℕ} : Fin n → Semiterm L ξ n
• fvar {L : Language} {ξ : Type u_1} {n : ℕ} : ξ → Semiterm L ξ n
• func {L : Language} {ξ : Type u_1} {n arity : ℕ} : L.Func arity → (Fin arity → Semiterm L ξ n) → Semiterm L ξ n

def PointwiseComposition.FFL.FirstOrder.«term&_» : Lean.ParserDescr

&x is the free variable indexed by the element x : ξ.

Equations

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

def PointwiseComposition.FFL.FirstOrder.«term#_» : Lean.ParserDescr

#x is the bound variable with de Bruijn index x.

Equations

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

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Term (L : Language) (ξ : Type u_1) : Type (max u_1 u_2)

The Term construction in FFL.FirstOrder.

Equations

• PointwiseComposition.FFL.FirstOrder.Term L ξ = PointwiseComposition.FFL.FirstOrder.Semiterm L ξ 0

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.ClosedSemiterm (L : Language) (n : ℕ) : Type u_1

The Closed Semiterm construction in FFL.FirstOrder.

Equations

• PointwiseComposition.FFL.FirstOrder.ClosedSemiterm L n = PointwiseComposition.FFL.FirstOrder.Semiterm L Empty n

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.ClosedTerm (L : Language) : Type u_1

The Closed Term construction in FFL.FirstOrder.

Equations

• PointwiseComposition.FFL.FirstOrder.ClosedTerm L = PointwiseComposition.FFL.FirstOrder.Semiterm L Empty 0

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.SyntacticSemiterm (L : Language) (n : ℕ) : Type u_1

The Syntactic Semiterm construction in FFL.FirstOrder.

Equations

• PointwiseComposition.FFL.FirstOrder.SyntacticSemiterm L n = PointwiseComposition.FFL.FirstOrder.Semiterm L ℕ n

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.SyntacticTerm (L : Language) : Type u_1

The Syntactic Term construction in FFL.FirstOrder.

Equations

• PointwiseComposition.FFL.FirstOrder.SyntacticTerm L = PointwiseComposition.FFL.FirstOrder.SyntacticSemiterm L 0

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Semiterm.instInhabited {L : Language} {ξ : Type u_1} {n : ℕ} [Inhabited ξ] : Inhabited (Semiterm L ξ n)

Equations

• PointwiseComposition.FFL.FirstOrder.Semiterm.instInhabited = { default := PointwiseComposition.FFL.FirstOrder.Semiterm.fvar default }

def PointwiseComposition.FFL.FirstOrder.Semiterm.toStr {L : Language} {ξ : Type u_1} {n : ℕ} [(k : ℕ) → ToString (L.Func k)] [ToString ξ] : Semiterm L ξ n → String

The to Str construction in FFL.FirstOrder.Semiterm.

Equations

• (PointwiseComposition.FFL.FirstOrder.Semiterm.bvar x_1).toStr = "x_{" ++ toString (n - 1 - ↑x_1) ++ "}"
• (PointwiseComposition.FFL.FirstOrder.Semiterm.fvar x_1).toStr = "z_{" ++ toString x_1 ++ "}"
• (PointwiseComposition.FFL.FirstOrder.Semiterm.func c a).toStr = toString c
• (PointwiseComposition.FFL.FirstOrder.Semiterm.func f v).toStr = ("{" ++ toString f ++ "} \\left(" ++ PointwiseComposition.String.vecToStr fun (i : Fin (n_1 + 1)) => (v i).toStr) ++ "\\right)"

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Semiterm.instRepr {L : Language} {ξ : Type u_1} {n : ℕ} [(k : ℕ) → ToString (L.Func k)] [ToString ξ] : Repr (Semiterm L ξ n)

Equations

• PointwiseComposition.FFL.FirstOrder.Semiterm.instRepr = { reprPrec := fun (t : PointwiseComposition.FFL.FirstOrder.Semiterm L ξ n) (x : ℕ) => Std.Format.text t.toStr }

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Semiterm.instToString {L : Language} {ξ : Type u_1} {n : ℕ} [(k : ℕ) → ToString (L.Func k)] [ToString ξ] : ToString (Semiterm L ξ n)

Equations

• PointwiseComposition.FFL.FirstOrder.Semiterm.instToString = { toString := PointwiseComposition.FFL.FirstOrder.Semiterm.toStr }

def PointwiseComposition.FFL.FirstOrder.Semiterm.hasDecEq {L : Language} {ξ : Type u_1} {n : ℕ} [(k : ℕ) → DecidableEq (L.Func k)] [DecidableEq ξ] (t u : Semiterm L ξ n) : Decidable (t = u)

The has Dec Eq construction in FFL.FirstOrder.Semiterm.

Equations

• One or more equations did not get rendered due to their size.
• (PointwiseComposition.FFL.FirstOrder.Semiterm.bvar x_2).hasDecEq (PointwiseComposition.FFL.FirstOrder.Semiterm.bvar y) = ⋯.mpr (decEq x_2 y)
• (PointwiseComposition.FFL.FirstOrder.Semiterm.bvar a).hasDecEq (PointwiseComposition.FFL.FirstOrder.Semiterm.fvar a_1) = isFalse ⋯
• (PointwiseComposition.FFL.FirstOrder.Semiterm.bvar a).hasDecEq (PointwiseComposition.FFL.FirstOrder.Semiterm.func a_1 a_2) = isFalse ⋯
• (PointwiseComposition.FFL.FirstOrder.Semiterm.fvar a).hasDecEq (PointwiseComposition.FFL.FirstOrder.Semiterm.bvar a_1) = isFalse ⋯
• (PointwiseComposition.FFL.FirstOrder.Semiterm.fvar x_2).hasDecEq (PointwiseComposition.FFL.FirstOrder.Semiterm.fvar y) = ⋯.mpr (decEq x_2 y)
• (PointwiseComposition.FFL.FirstOrder.Semiterm.fvar a).hasDecEq (PointwiseComposition.FFL.FirstOrder.Semiterm.func a_1 a_2) = isFalse ⋯
• (PointwiseComposition.FFL.FirstOrder.Semiterm.func a a_1).hasDecEq (PointwiseComposition.FFL.FirstOrder.Semiterm.bvar a_2) = isFalse ⋯
• (PointwiseComposition.FFL.FirstOrder.Semiterm.func a a_1).hasDecEq (PointwiseComposition.FFL.FirstOrder.Semiterm.fvar a_2) = isFalse ⋯

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Semiterm.instDecidableEq {L : Language} {ξ : Type u_1} {n : ℕ} [(k : ℕ) → DecidableEq (L.Func k)] [DecidableEq ξ] : DecidableEq (Semiterm L ξ n)

Equations

• PointwiseComposition.FFL.FirstOrder.Semiterm.instDecidableEq = PointwiseComposition.FFL.FirstOrder.Semiterm.hasDecEq

def PointwiseComposition.FFL.FirstOrder.Semiterm.complexity {L : Language} {ξ : Type u_1} {n : ℕ} : Semiterm L ξ n → ℕ

The complexity of a semiterm, taking suprema at function symbols.

Equations

• (PointwiseComposition.FFL.FirstOrder.Semiterm.bvar a).complexity = 0
• (PointwiseComposition.FFL.FirstOrder.Semiterm.fvar a).complexity = 0
• (PointwiseComposition.FFL.FirstOrder.Semiterm.func a v).complexity = (Finset.univ.sup fun (i : Fin arity) => (v i).complexity) + 1

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.complexity_bvar {L : Language} {ξ : Type u_1} {n : ℕ} (x : Fin n) : (bvar x).complexity = 0

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.complexity_fvar {L : Language} {ξ : Type u_1} {n : ℕ} (x : ξ) : (fvar x).complexity = 0

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.complexity_func {L : Language} {ξ : Type u_1} {n k : ℕ} (f : L.Func k) (v : Fin k → Semiterm L ξ n) : (func f v).complexity = (Finset.univ.sup fun (i : Fin k) => (v i).complexity) + 1

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.complexity_func_lt {L : Language} {ξ : Type u_1} {n k : ℕ} (f : L.Func k) (v : Fin k → Semiterm L ξ n) (i : Fin k) : (v i).complexity < (func f v).complexity

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Semiterm.funcWithArity {L : Language} {ξ : Type u_1} {n : ℕ} (k : ℕ) (f : L.Func k) (v : Fin k → Semiterm L ξ n) : Semiterm L ξ n

The func! construction in FFL.FirstOrder.Semiterm.

Equations

• PointwiseComposition.FFL.FirstOrder.Semiterm.funcWithArity k f v = PointwiseComposition.FFL.FirstOrder.Semiterm.func f v

def PointwiseComposition.FFL.FirstOrder.Semiterm.bv {L : Language} {ξ : Type u_1} {n : ℕ} : Semiterm L ξ n → Finset (Fin n)

The set of bound variables occurring in a semiterm.

Equations

• (PointwiseComposition.FFL.FirstOrder.Semiterm.bvar a).bv = {a}
• (PointwiseComposition.FFL.FirstOrder.Semiterm.fvar a).bv = ∅
• (PointwiseComposition.FFL.FirstOrder.Semiterm.func a v).bv = Finset.univ.biUnion fun (i : Fin arity) => (v i).bv

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.bv_bvar {L : Language} {ξ : Type u_1} {n : ℕ} {x : Fin n} : (bvar x).bv = {x}

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.bv_fvar {L : Language} {ξ : Type u_1} {n : ℕ} {x : ξ} : (fvar x).bv = ∅

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.bv_func {L : Language} {ξ : Type u_1} {n k : ℕ} (f : L.Func k) (v : Fin k → Semiterm L ξ n) : (func f v).bv = Finset.univ.biUnion fun (i : Fin k) => (v i).bv

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.bv_constant {L : Language} {ξ : Type u_1} {n : ℕ} (f : L.Func 0) (v : Fin 0 → Semiterm L ξ n) : (func f v).bv = ∅

def PointwiseComposition.FFL.FirstOrder.Semiterm.Positive {L : Language} {ξ : Type u_1} {n : ℕ} (t : Semiterm L ξ (n + 1)) : Prop

The Positive construction in FFL.FirstOrder.Semiterm.

Equations

• t.Positive = ∀ x ∈ t.bv, 0 < x

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Positive.bvar {L : Language} {ξ : Type u_1} {n : ℕ} {x : Fin (n + 1)} : (bvar x).Positive ↔ 0 < x

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Positive.fvar {L : Language} {ξ : Type u_1} {n : ℕ} {x : ξ} : (fvar x).Positive

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.Positive.func {L : Language} {ξ : Type u_1} {n k : ℕ} (f : L.Func k) (v : Fin k → Semiterm L ξ (n + 1)) : (func f v).Positive ↔ ∀ (i : Fin k), (v i).Positive

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.bv_eq_empty_of_positive {L : Language} {ξ : Type u_1} {t : Semiterm L ξ 1} (ht : t.Positive) : t.bv = ∅

def PointwiseComposition.FFL.FirstOrder.Semiterm.freeVariables {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] : Semiterm L ξ n → Finset ξ

The set of free variables occuring in a semiterm.

Equations

• (PointwiseComposition.FFL.FirstOrder.Semiterm.bvar a).freeVariables = ∅
• (PointwiseComposition.FFL.FirstOrder.Semiterm.fvar a).freeVariables = {a}
• (PointwiseComposition.FFL.FirstOrder.Semiterm.func a v).freeVariables = Finset.univ.biUnion fun (i : Fin arity) => (v i).freeVariables

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.freeVariables_bvar {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] {x : Fin n} : (bvar x).freeVariables = ∅

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.freeVariables_fvar {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] {x : ξ} : (fvar x).freeVariables = {x}

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.freeVariables_func {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] {k : ℕ} (f : L.Func k) (v : Fin k → Semiterm L ξ n) : (func f v).freeVariables = Finset.univ.biUnion fun (i : Fin k) => (v i).freeVariables

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.freeVariables_constant {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (f : L.Func 0) (v : Fin 0 → Semiterm L ξ n) : (func f v).freeVariables = ∅

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.freeVariables_empty {L : Language} {n : ℕ} {ο : Type u_6} [IsEmpty ο] {t : Semiterm L ο n} : t.freeVariables = ∅

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Semiterm.HasFreeVariable {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (t : Semiterm L ξ n) (x : ξ) : Prop

The FVar? construction in FFL.FirstOrder.Semiterm.

Equations

• t.HasFreeVariable x = (x ∈ t.freeVariables)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.hasFreeVariable_bvar {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (x : Fin n) (z : ξ) : ¬(bvar x).HasFreeVariable z

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.hasFreeVariable_fvar {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (x z : ξ) : (fvar x).HasFreeVariable z ↔ x = z

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.hasFreeVariable_func {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (x : ξ) {k : ℕ} (f : L.Func k) (v : Fin k → Semiterm L ξ n) : (func f v).HasFreeVariable x ↔ ∃ (i : Fin k), (v i).HasFreeVariable x

def PointwiseComposition.FFL.FirstOrder.Semiterm.lMap {L₁ : Language} {L₂ : Language} {ξ : Type u_1} {n : ℕ} (Φ : L₁.Hom L₂) : Semiterm L₁ ξ n → Semiterm L₂ ξ n

The map on terms induced from a homomorphism between languages.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.FirstOrder.Semiterm.lMap Φ (PointwiseComposition.FFL.FirstOrder.Semiterm.bvar a) = PointwiseComposition.FFL.FirstOrder.Semiterm.bvar a
• PointwiseComposition.FFL.FirstOrder.Semiterm.lMap Φ (PointwiseComposition.FFL.FirstOrder.Semiterm.fvar a) = PointwiseComposition.FFL.FirstOrder.Semiterm.fvar a

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.lMap_bvar {L₁ : Language} {L₂ : Language} {ξ : Type u_1} {n : ℕ} (Φ : L₁.Hom L₂) (x : Fin n) : lMap Φ (bvar x) = bvar x

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.lMap_fvar {L₁ : Language} {L₂ : Language} {ξ : Type u_1} {n : ℕ} (Φ : L₁.Hom L₂) (x : ξ) : lMap Φ (fvar x) = fvar x

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.lMap_func {L₁ : Language} {L₂ : Language} {ξ : Type u_1} {n : ℕ} (Φ : L₁.Hom L₂) {k : ℕ} (f : L₁.Func k) (v : Fin k → Semiterm L₁ ξ n) : lMap Φ (func f v) = func (Φ.func f) (lMap Φ ∘ v)

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.lMap_func' {L₁ : Language} {L₂ : Language} {ξ : Type u_1} {n : ℕ} (Φ : L₁.Hom L₂) {k : ℕ} (f : L₁.Func k) (v : Fin k → Semiterm L₁ ξ n) : lMap Φ (func f v) = func (Φ.func f) fun (i : Fin k) => lMap Φ (v i)

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.lMap_positive {L₁ : Language} {L₂ : Language} {ξ : Type u_1} {n : ℕ} (Φ : L₁.Hom L₂) (t : Semiterm L₁ ξ (n + 1)) : (lMap Φ t).Positive ↔ t.Positive

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.freeVariables_lMap {L₁ : Language} {L₂ : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (Φ : L₁.Hom L₂) (t : Semiterm L₁ ξ n) : (lMap Φ t).freeVariables = t.freeVariables

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Semiterm.instInhabited_1 {L : Language} {ξ : Type u_1} {n : ℕ} [L.ConstantInhabited] : Inhabited (Semiterm L ξ n)

Equations

• PointwiseComposition.FFL.FirstOrder.Semiterm.instInhabited_1 = { default := PointwiseComposition.FFL.FirstOrder.Semiterm.func default ![] }

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.default_def {L : Language} {ξ : Type u_1} {n : ℕ} [L.ConstantInhabited] : default = func default ![]

def PointwiseComposition.FFL.FirstOrder.Semiterm.fvarList {L : Language} {ξ : Type u_1} {n : ℕ} : Semiterm L ξ n → List ξ

The fvar List construction in FFL.FirstOrder.Semiterm.

Equations

• (PointwiseComposition.FFL.FirstOrder.Semiterm.bvar a).fvarList = []
• (PointwiseComposition.FFL.FirstOrder.Semiterm.fvar a).fvarList = [a]
• (PointwiseComposition.FFL.FirstOrder.Semiterm.func a v).fvarList = (PointwiseComposition.Matrix.toList fun (i : Fin arity) => (v i).fvarList).flatten

def PointwiseComposition.FFL.FirstOrder.Semiterm.idxOfFVar {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (t : Semiterm L ξ n) : ξ → ℕ

The idx Of FVar construction in FFL.FirstOrder.Semiterm.

Equations

• t.idxOfFVar a = List.idxOf a t.fvarList

def PointwiseComposition.FFL.FirstOrder.Semiterm.enumerateFVar {L : Language} {ξ : Type u_1} {n : ℕ} [Inhabited ξ] (t : Semiterm L ξ n) : ℕ → ξ

The enumerate FVar construction in FFL.FirstOrder.Semiterm.

Equations

• t.enumerateFVar i = if hi : i < t.fvarList.length then t.fvarList.get ⟨i, hi⟩ else default

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.enumerateFVar_idxOfFVar {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] [Inhabited ξ] {t : Semiterm L ξ n} {x : ξ} (hx : x ∈ t.fvarList) : t.enumerateFVar (t.idxOfFVar x) = x

theorem PointwiseComposition.FFL.FirstOrder.Semiterm.mem_fvarList_iff_hasFreeVariable {L : Language} {ξ : Type u_1} {n : ℕ} {x : ξ} [DecidableEq ξ] {t : Semiterm L ξ n} : x ∈ t.fvarList ↔ t.HasFreeVariable x