KRF Definitions_Core (arXiv 2412.11855 framework layer)

/-
Core logic of the KRF formalization (arXiv 2412.11855v2, Zhang--Jiang--Quan).
Everything here corresponds to the paper's "Conventions and Notations" and the
tacit logical machinery used by Definitions 1--3 (databases, query languages,
knowledge bases): signatures, terms, first-order formulas, structures, the
satisfaction relation, entailment and tautologies, plus the renaming maps
τ(-) on terms/formulas and the embedding of formulas along a signature
extension. See FORMALIZATION_PLAN.md §2 for the encoding decisions.

Notation fixes (paper → Lean):
  Δ (constants) → Nat; the truth values {1,0,-1} → `TVal`;
  τ : Δ → Δ injective → an arbitrary injective `Nat → Nat` (no surjectivity,
  matching the paper).
-/
import Mathlib.Data.Set.Basic
import Mathlib.Data.List.Basic

namespace KRFCore

/-- The three truth values of Definition 1: `uno` = 1 (observed true),
`zero` = 0 (observed false), `neg` = -1 (not observed yet). -/
inductive TVal where
  | uno | zero | neg
  deriving DecidableEq, Repr

export TVal (uno zero neg)

/-- A fact value is *observed* if it is 1 or 0 (Definition 1: "observed fact"
means D(α) ≥ 0). -/
def obs : TVal → Prop
  | .uno | .zero => True
  | .neg => False

/-- A database is *positive* if no atom is observed false (value 0). -/
def dbPosVal (v : TVal) : Prop := v ≠ .zero

/-! ### Signatures

A signature records, for every predicate symbol (a natural number), its arity
(`none` = not in the signature; `some 0` = proposition symbol), and which
predicates are CWA-predicates. Following the paper's convention every signature
contains Δ (all constants), and database signatures have no function symbols of
arity > 0 — which is vacuous here since terms carry only constants and
variables. A *query signature* contains no CWA-predicate (`IsQrySig`). -/

structure Sig where
  arity : Nat → Option Nat
  cwa : Nat → Prop
  cwa_pred : ∀ p, cwa p → (arity p).isSome

/-- Query signature: no CWA-predicate symbol. -/
def IsQrySig (σ : Sig) : Prop := ∀ p, ¬ σ.cwa p

/-! ### Terms, atoms, formulas (the FO language of a signature)

Terms are constants (any natural number — Δ) or variables (also natural
numbers). Atoms carry a well-formedness proof tying the argument list length to
the predicate's arity. `GroundAtom` = atom whose arguments are all constants
(no variables, hence no equality concerns beyond the term structure — the
paper's Fact(σ)). Formulas include predicate atoms, equality (needed for the
appendix's PDst), negation, conjunction, universal quantification; the other
connectives and the existential quantifier are derived. -/

inductive Tm where
  | cst : Nat → Tm
  | var : Nat → Tm
  deriving DecidableEq, Repr

/-- Renaming τ applied to a term: constants are renamed, variables untouched. -/
def renameTm (τ : Nat → Nat) : Tm → Tm
  | .cst c => .cst (τ c)
  | .var x => .var x

structure Atom (σ : Sig) where
  pred : Nat
  args : List Tm
  wf : (σ.arity pred).isSome ∧ args.length = (σ.arity pred).getD 0

/-- Ground atom of σ: an atom whose arguments are all constants. This is the
paper's Fact(σ) (atoms involving no variables; the paper excludes equality from
facts, so there is no equality among atoms). -/
def GroundAtom (σ : Sig) := { a : Atom σ // ∀ t ∈ a.args, ∃ c, t = .cst c }

inductive Fm (σ : Sig) where
  | atom : Atom σ → Fm σ
  | eq : Tm → Tm → Fm σ
  | neg : Fm σ → Fm σ
  | conj : Fm σ → Fm σ → Fm σ
  | all : Nat → Fm σ → Fm σ

namespace Fm

variable {σ : Sig}

/-- Derived disjunction. -/
def or (φ ψ : Fm σ) : Fm σ := .neg (.conj (.neg φ) (.neg ψ))

/-- Derived implication. -/
def imp (φ ψ : Fm σ) : Fm σ := .neg (.conj φ (.neg ψ))

/-- Derived existential quantification. -/
def ex (x : Nat) (φ : Fm σ) : Fm σ := .neg (.all x (.neg φ))

/-- A canonical tautology (x = x, universally closed). -/
def top : Fm σ := .all 0 (.eq (.var 0) (.var 0))

/-- A canonical contradiction. -/
def bot : Fm σ := .neg top

/-- Renaming τ applied to a formula: only constants are renamed. -/
def rename (τ : Nat → Nat) : Fm σ → Fm σ
  | .atom a => .atom ⟨a.pred, a.args.map (renameTm τ),
      ⟨a.wf.1, by simp only [List.length_map]; exact a.wf.2⟩⟩
  | .eq t u => .eq (renameTm τ t) (renameTm τ u)
  | .neg φ => .neg (rename τ φ)
  | .conj φ ψ => .conj (rename τ φ) (rename τ ψ)
  | .all x φ => .all x (rename τ φ)

end Fm

/-! ### Structures and satisfaction

A σ-structure has a (necessarily inhabited) domain, an interpretation of the
constants, and for every predicate symbol a relation on the tuple space of its
arity (absent predicates get the arity 0, i.e. a dummy constant relation — such
atoms still evaluate via the arity guard below, so they are always false in the
well-formed cases). -/

structure FStruct (σ : Sig) where
  Dom : Type
  dom_ne : Nonempty Dom
  ctm : Nat → Dom
  rel : (p : Nat) → (Fin ((σ.arity p).getD 0) → Dom) → Prop

namespace FStruct

variable {σ τ : Sig}

/-- Evaluate a term under an assignment. -/
def evTm (A : FStruct σ) (s : Nat → A.Dom) : Tm → A.Dom
  | .cst c => A.ctm c
  | .var x => s x

/-- Interpretation of a predicate symbol on a list of domain elements; guards
on the arity (absent/wrong-length = false). -/
def relList (A : FStruct σ) (p : Nat) (ds : List A.Dom) : Prop :=
  if h : ds.length = (σ.arity p).getD 0 then
    A.rel p (fun i => ds.get (have hb : i.val < (σ.arity p).getD 0 := i.isLt
      ⟨i.val, by simpa [h] using hb⟩))
  else False

/-- Satisfaction with an explicit assignment. -/
def Sat (A : FStruct σ) (s : Nat → A.Dom) : Fm σ → Prop
  | .atom a => A.relList a.pred (a.args.map (A.evTm s))
  | .eq t u => A.evTm s t = A.evTm s u
  | .neg φ => ¬ Sat A s φ
  | .conj φ ψ => Sat A s φ ∧ Sat A s ψ
  | .all x φ => ∀ v, Sat A (fun y => if y = x then v else s y) φ

/-- A formula holds in a structure (over all assignments — the universal
closure reading; all formulas at the framework level are sentences). -/
def Satisfies (A : FStruct σ) (φ : Fm σ) : Prop := ∀ s, A.Sat s φ

/-- The structure renamed by τ: the same domain and relations, constant
interpretation composed with τ. -/
def renamed (A : FStruct σ) (τ : Nat → Nat) : FStruct σ where
  Dom := A.Dom
  dom_ne := A.dom_ne
  ctm := A.ctm ∘ τ
  rel := A.rel

/-- Logical entailment between formulas (read at sentence level). -/
def Entails (φ ψ : Fm σ) : Prop := ∀ A : FStruct σ, A.Satisfies φ → A.Satisfies ψ

/-- φ is a tautology. -/
def Taut (φ : Fm σ) : Prop := ∀ A : FStruct σ, A.Satisfies φ

/-- `top` really is a tautology. -/
theorem satisf_top : Taut (Fm.top : Fm σ) := by
  intro A s
  exact fun v => rfl

end FStruct

/-! ### Signature embeddings (σ₁ ⊆ σ₂) and formula lifting

A signature is a sub-signature of another when every absent-or-equal predicate
keeps or agrees on its arity (CWA flags are not compared; queries only embed up
to supersets of their signature). Used to read a σ_Q-query (or a σ_D-database)
inside a σ ⊇ σ_D ∪ σ_Q structure, as in Definition 4 / Proposition 4. -/

structure SigEmb (σ₁ σ₂ : Sig) where
  arity_agree : ∀ p, σ₁.arity p = none ∨ σ₁.arity p = σ₂.arity p

namespace SigEmb

variable {σ₁ σ₂ : Sig}

/-- Lift an atom to the bigger signature; well-formedness transfers because
arities agree wherever the smaller signature has the predicate (and the
`isSome` component of `wf` says the predicate really is present). -/
def embAtom (e : SigEmb σ₁ σ₂) (a : Atom σ₁) : Atom σ₂ :=
  ⟨a.pred, a.args, by
    rcases e.arity_agree a.pred with h | h
    · have hso : (σ₁.arity a.pred).isSome := a.wf.1
      rw [h] at hso
      cases hso
    · exact ⟨by simpa [h] using a.wf.1, by simpa [h] using a.wf.2⟩⟩

/-- Lift a formula to the bigger signature. -/
def embFm (e : SigEmb σ₁ σ₂) : Fm σ₁ → Fm σ₂
  | .atom a => .atom (e.embAtom a)
  | .eq t u => .eq t u
  | .neg φ => .neg (embFm e φ)
  | .conj φ ψ => .conj (embFm e φ) (embFm e ψ)
  | .all x φ => .all x (embFm e φ)

/-- Renaming commutes with lifting along a signature embedding. -/
theorem embFm_rename (e : SigEmb σ₁ σ₂) (τ : Nat → Nat) (φ : Fm σ₁) :
    e.embFm (φ.rename τ) = (e.embFm φ).rename τ := by
  induction φ with
  | atom a =>
      cases a with
      | mk p args wf =>
          simp only [embFm, embAtom, Fm.rename]
  | eq => rfl
  | neg φ ih => simp [Fm.rename, embFm, ih]
  | conj φ ψ ihφ ihψ => simp [Fm.rename, embFm, ihφ, ihψ]
  | all _ φ ih => simp [Fm.rename, embFm, ih]

end SigEmb

/-! ### Renaming respects satisfaction (the semantic content of τ(-))

Theorem (used by Example 2's renaming-closure and by belief mappings): for an
injective τ, `Sat` of the renamed formula in A equals `Sat` of the original
formula in the renamed structure. -/

namespace FStruct

variable {σ : Sig} {τ : Nat → Nat}

/-- Terms commute with renaming. -/
theorem evTm_rename (A : FStruct σ) (s : Nat → A.Dom) (t : Tm) :
    A.evTm s (renameTm τ t) = (A.renamed τ).evTm s t := by
  cases t <;> rfl

/-- Satisfaction is invariant under renaming (structure side vs. formula
side). Injectivity of τ is *not* needed for this direction — it holds for any
τ, since renaming only changes the constant interpretation consistently. -/
theorem sat_rename (A : FStruct σ) (s : Nat → A.Dom) (φ : Fm σ) :
    A.Sat s (φ.rename τ) ↔ (A.renamed τ).Sat s φ := by
  induction φ generalizing s with
  | atom a =>
      change A.relList a.pred ((a.args.map (renameTm τ)).map (A.evTm s)) ↔
        (A.renamed τ).relList a.pred (a.args.map ((A.renamed τ).evTm s))
      rw [List.map_map]
      have hm : a.args.map (A.evTm s ∘ renameTm τ) =
                a.args.map ((A.renamed τ).evTm s) := by
        apply List.map_congr_left
        intro t _
        exact evTm_rename A s t
      rw [hm]
      exact Iff.intro (fun h => by simpa using h) (fun h => by simpa using h)
  | eq t u =>
      change A.evTm s (renameTm τ t) = A.evTm s (renameTm τ u) ↔
        (A.renamed τ).evTm s t = (A.renamed τ).evTm s u
      rw [evTm_rename A s t, evTm_rename A s u]
      try exact Iff.intro id id
  | neg φ ih =>
      change (¬ A.Sat s (φ.rename τ)) ↔ ¬ (A.renamed τ).Sat s φ
      rw [ih s]
  | conj φ ψ ihφ ihψ =>
      change (A.Sat s (φ.rename τ) ∧ A.Sat s (ψ.rename τ)) ↔
        ((A.renamed τ).Sat s φ ∧ (A.renamed τ).Sat s ψ)
      rw [ihφ s, ihψ s]
  | all x φ ih =>
      constructor
      · intro h v
        exact (ih (fun y => if y = x then v else s y)).mp (h v)
      · intro h v
        exact (ih (fun y => if y = x then v else s y)).mpr (h v)

end FStruct

end KRFCore