Shared syntax for pulling operator formulas back to tuples

A full-tuple interpretation represents each target element by d source elements. Pulling an operator formula back along it replaces each target variable by d coordinates and each relation argument by a block of d coordinates. This module holds the operator-independent part of that translation: named term values, existential coordinate blocks, scaled relation variables, and the block bijection between flattened tuples and target tuples. The least-fixed-point and transitive-closure pullbacks build on it.

Main definitions

• Operator.RelVar.scale: multiply the arity of every relation variable by d.
• Operator.Tuple.FOMap: an ordinary first-order tuple pullback.
• Operator.Tuple.termGraph, Operator.Tuple.applyTerms: name target term values by fresh coordinates.
• Operator.Tuple.exBlock: bind the d coordinates of a newly quantified target variable.
• Operator.Tuple.blockEquiv: read a flattened tuple of k coordinate blocks as k targets.

Main results

• Operator.Tuple.realize_applyTerms: the named coordinates have a unique witness.
• Operator.Tuple.realize_applyTerms_rel: pulled-back relation atoms read the related tuple.
• Operator.Tuple.realize_exBlock: a coordinate block quantifies over the target universe.

def Cslib.Logic.FO.Operator.RelVar.scale (d : ℕ) {Γ : List ℕ} {k : ℕ} : RelVar Γ k → RelVar (List.map (fun (x : ℕ) => x * d) Γ) (k * d)

Replace each argument of a scoped relation variable by d coordinates.

@[reducible, inline]

abbrev Cslib.Logic.FO.Operator.Tuple.FOMap (L : FirstOrder.Language) (L' : FirstOrder.Language) (d : ℕ) : Type (max (max (max (max (max 1 u_4) u_3) 0) u_2) u_1)

The ordinary first-order part of a full-tuple syntax translation.

def Cslib.Logic.FO.Operator.Tuple.scopeMap {d : ℕ} {α : Type w} {k : ℕ} : (α ⊕ Fin k) × Fin d → α × Fin d ⊕ Fin (k * d)

Distribute coordinates over old and newly bound variables, flattening the latter.

noncomputable def Cslib.Logic.FO.Operator.Tuple.termGraph {L : FirstOrder.Language} {L' : FirstOrder.Language} {d : ℕ} (f : FOMap L L' d) {α : Type} {k : ℕ} (args : Fin k → L'.Term α) : L.Formula (α × Fin d ⊕ Fin (k * d))

Translate the graph of a tuple of terms, using fresh coordinates for their values.

noncomputable def Cslib.Logic.FO.Operator.Tuple.applyTerms {L : FirstOrder.Language} {L' : FirstOrder.Language} {O : Type s} {shape : O → Shape} {d : ℕ} (f : FOMap L L' d) {Γ : List ℕ} {α : Type} {k : ℕ} (args : Fin k → L'.Term α) (φ : Formula L shape Γ (α × Fin d ⊕ Fin (k * d))) : Formula L shape Γ (α × Fin d)

Apply a formula with fresh coordinate arguments to translated target terms.

def Cslib.Logic.FO.Operator.Tuple.exBlock {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {d : ℕ} {Γ : List ℕ} {α : Type w} (φ : Formula L shape Γ (Option α × Fin d)) : Formula L shape Γ (α × Fin d)

Bind the d coordinates of a newly quantified target variable.

@[simp]

theorem Cslib.Logic.FO.Operator.Tuple.checkPolarity_applyTerms {L : FirstOrder.Language} {L' : FirstOrder.Language} {O : Type s} {shape : O → Shape} {d : ℕ} {Γ : List ℕ} {α : Type} (variance : Variances shape) (f : FOMap L L' d) {k : ℕ} (args : Fin k → L'.Term α) (φ : Formula L shape Γ (α × Fin d ⊕ Fin (k * d))) (sign : Bool) (mark : Marking Γ) : (Formula.checkPolarity variance (applyTerms (fun {α : Type} => f) args φ) sign fun {k : ℕ} => mark) = Formula.checkPolarity variance φ sign fun {k : ℕ} => mark

Naming term values does not change dependence on scoped relations.

@[simp]

theorem Cslib.Logic.FO.Operator.Tuple.wellFormed_applyTerms {L : FirstOrder.Language} {L' : FirstOrder.Language} {O : Type s} {shape : O → Shape} {d : ℕ} {Γ : List ℕ} {α : Type} (policy : Policy shape) (f : FOMap L L' d) {k : ℕ} (args : Fin k → L'.Term α) (φ : Formula L shape Γ (α × Fin d ⊕ Fin (k * d))) : Formula.wellFormed policy (applyTerms (fun {α : Type} => f) args φ) = Formula.wellFormed policy φ

Naming term values does not change formation conditions.

@[simp]

theorem Cslib.Logic.FO.Operator.Tuple.checkPolarity_exBlock {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {d : ℕ} {Γ : List ℕ} {β : Type w} (variance : Variances shape) (φ : Formula L shape Γ (Option β × Fin d)) (sign : Bool) (mark : Marking Γ) : (Formula.checkPolarity variance (exBlock φ) sign fun {k : ℕ} => mark) = Formula.checkPolarity variance φ sign fun {k : ℕ} => mark

Binding a coordinate block does not change dependence on scoped relations.

@[simp]

theorem Cslib.Logic.FO.Operator.Tuple.wellFormed_exBlock {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {d : ℕ} {Γ : List ℕ} {β : Type w} (policy : Policy shape) (φ : Formula L shape Γ (Option β × Fin d)) : Formula.wellFormed policy (exBlock φ) = Formula.wellFormed policy φ

Binding a coordinate block does not change formation conditions.

def Cslib.Logic.FO.Operator.Tuple.blockEquiv {d : ℕ} {M : Type u_1} {N : Type u_2} (e : (Fin d → M) ≃ N) (k : ℕ) : (Fin (k * d) → M) ≃ (Fin k → N)

Apply an element bijection independently to the blocks of a flattened relation tuple.

theorem Cslib.Logic.FO.Operator.Tuple.blockEquiv_apply {d : ℕ} {M : Type u_1} {N : Type u_2} (e : (Fin d → M) ≃ N) {k : ℕ} (xs : Fin (k * d) → M) (i : Fin k) : (blockEquiv e k) xs i = e fun (j : Fin d) => xs (finProdFinEquiv (i, j))

Each target of blockEquiv is the image of one coordinate block.

theorem Cslib.Logic.FO.Operator.Tuple.realize_termGraph {L : FirstOrder.Language} {L' : FirstOrder.Language} {d : ℕ} {α M N : Type} [L.Structure M] [L'.Structure N] (f : FOMap L L' d) (e : (Fin d → M) ≃ N) (hf : ∀ {α : Type} (φ : L'.Formula α) (v : α × Fin d → M), (f φ).Realize v ↔ φ.Realize fun (a : α) => e fun (i : Fin d) => v (a, i)) {k : ℕ} (args : Fin k → L'.Term α) (v : α × Fin d → M) (xs : Fin (k * d) → M) : (termGraph (fun {α : Type} => f) args).Realize (Sum.elim v xs) ↔ ∀ (i : Fin k), (blockEquiv e k) xs i = FirstOrder.Language.Term.realize (fun (a : α) => e fun (j : Fin d) => v (a, j)) (args i)

The translated term graph identifies precisely the encoded values of its arguments.

theorem Cslib.Logic.FO.Operator.Tuple.realize_applyTerms {L : FirstOrder.Language} {L' : FirstOrder.Language} {O : Type s} {shape : O → Shape} {d : ℕ} {Γ : List ℕ} {α M N : Type} [L.Structure M] [L'.Structure N] (f : FOMap L L' d) (e : (Fin d → M) ≃ N) (hf : ∀ {α : Type} (φ : L'.Formula α) (v : α × Fin d → M), (f φ).Realize v ↔ φ.Realize fun (a : α) => e fun (i : Fin d) => v (a, i)) (I : Interpretation shape M) {k : ℕ} (args : Fin k → L'.Term α) (φ : Formula L shape Γ (α × Fin d ⊕ Fin (k * d))) (ρ : RelEnv Γ M) (v : α × Fin d → M) : Formula.Realize I (applyTerms (fun {α : Type} => f) args φ) (fun {k : ℕ} => ρ) v ↔ Formula.Realize I φ (fun {k : ℕ} => ρ) (Sum.elim v ((blockEquiv e k).symm fun (i : Fin k) => FirstOrder.Language.Term.realize (fun (a : α) => e fun (j : Fin d) => v (a, j)) (args i)))

Existential term naming has a unique coordinate witness, even for constants and nullary argument tuples.

theorem Cslib.Logic.FO.Operator.Tuple.realize_applyTerms_rel {L : FirstOrder.Language} {L' : FirstOrder.Language} {O : Type s} {shape : O → Shape} {d : ℕ} {Γ : List ℕ} {α M N : Type} [L.Structure M] [L'.Structure N] (f : FOMap L L' d) (e : (Fin d → M) ≃ N) (hf : ∀ {α : Type} (φ : L'.Formula α) (v : α × Fin d → M), (f φ).Realize v ↔ φ.Realize fun (a : α) => e fun (i : Fin d) => v (a, i)) {O' : Type s} {shape' : O' → Shape} (I : Interpretation shape M) (I' : Interpretation shape' N) {k : ℕ} (r : RelVar Γ k) (args : Fin k → L'.Term α) (ρs : RelEnv (List.map (fun (x : ℕ) => x * d) Γ) M) (ρt : RelEnv Γ N) (hρ : ∀ (xs : Fin (k * d) → M), xs ∈ ρs (RelVar.scale d r) ↔ (blockEquiv e k) xs ∈ ρt r) (v : α × Fin d → M) : Formula.Realize I (applyTerms (fun {α : Type} => f) args (Formula.rel (RelVar.scale d r) fun (i : Fin (k * d)) => FirstOrder.Language.var (Sum.inr i))) (fun {k : ℕ} => ρs) v ↔ Formula.Realize I' (Formula.rel r args) (fun {k : ℕ} => ρt) fun (a : α) => e fun (i : Fin d) => v (a, i)

A pulled-back relation atom holds exactly when the related target valuation contains the evaluated target arguments.

theorem Cslib.Logic.FO.Operator.Tuple.realize_exBlock {L : FirstOrder.Language} {O : Type s} {shape : O → Shape} {d : ℕ} {Γ : List ℕ} {M N : Type} [L.Structure M] (e : (Fin d → M) ≃ N) {β : Type} (I : Interpretation shape M) (φ : Formula L shape Γ (Option β × Fin d)) (ρ : RelEnv Γ M) (v : β × Fin d → M) (P : (Option β → N) → Prop) (hφ : ∀ (w : Option β × Fin d → M), Formula.Realize I φ (fun {k : ℕ} => ρ) w ↔ P fun (a : Option β) => e fun (i : Fin d) => w (a, i)) : Formula.Realize I (exBlock φ) (fun {k : ℕ} => ρ) v ↔ ∃ (x : N), P fun (x_1 : Option β) => x_1.elim x fun (a : β) => e fun (i : Fin d) => v (a, i)

A coordinate block ranges over the target universe through the element bijection.