KRF Definitions_Data (arXiv 2412.11855 framework layer)

/-
Data layer of the KRF formalization (Definition 1 -- Definition 4 of the
paper): databases (total-function encoding, see FORMALIZATION_PLAN.md §2.6),
extensions, the renaming machinery τ(D), query languages, knowledge bases (the
five closure properties), Example 2's K_Σ, belief mappings and the KB they
induce. Ambient parameters: a database signature σ_D, a query signature σ_Q
and the ambient σ ⊇ σ_D ∪ σ_Q.

Renaming conventions replicated from the paper:
  - τ : Δ → Δ is injective but NOT assumed surjective (the paper never asks
    for more);
  - τ(D) is the "preimage-pull" database: an atom whose constants are not all
    in the range of τ gets the value -1 (= unobserved). Whether τ(D) lies in
    the database class 𝒟 is NOT asserted here — the paper uses this closure
    implicitly; where a theorem needs it, that theorem states it explicitly
    (plan §2.7). CWA-completeness of τ(D) follows from that of D since the
    pull keeps the predicate, and is proved below.
-/
import Definitions.Def_KRF_Core
import Mathlib.Data.Set.Finite.Basic

noncomputable section

open KRFCore

local instance (p : Prop) : Decidable p := Classical.propDecidable p
open KRFCore.FStruct

namespace KRF

variable {σD σQ σ : Sig}

/-! ### Databases (Definition 1) -/

/-- A pre-database: the total-map-with-finitely-many-observations part of
Definition 1 (its first condition). Renamings τ(D) for injective τ land here
in full generality — see the plan §2.7 (the paper needs τ(D) ∈ 𝒟 implicitly;
we do not assert it). -/
structure PreDatabase (σD : Sig) where
  val : GroundAtom σD → TVal
  finite_observed : Set.Finite { α : GroundAtom σD | obs (val α) }

/-- A σ-database is a pre-database satisfying Definition 1's second condition:
completeness on CWA-predicates (every atom involving a CWA-predicate is
observed; unobserved = -1). -/
structure Database (σD : Sig) extends PreDatabase σD where
  cwa_complete : ∀ α : GroundAtom σD, σD.cwa α.val.pred → val α ≠ .neg

/-- Databases coerce to their pre-database part. -/
instance : Coe (Database σD) (PreDatabase σD) := ⟨fun D => D.toPreDatabase⟩

/-- The class of all σ-databases (𝒟_All^σ). -/
def DBAll (σD : Sig) : Set (Database σD) := Set.univ

/-- Positive database: no atom observed false. -/
def Positive (D : Database σD) : Prop := ∀ α : GroundAtom σD, D.val α ≠ .zero

/-- The class of positive σ-databases (𝒟_Pos^σ). -/
def DBPos (σD : Sig) : Set (Database σD) := { D | Positive D }

/-- The constant part of a term (0 on variables; ground atoms have none). -/
def stripCst : Tm → Nat
  | .cst c => c
  | .var _ => 0

/-- The constants occurring in a ground atom — extracted computably. -/
def gargs (β : GroundAtom σD) : List Nat := β.val.args.map stripCst

theorem arg_eq_cst (β : GroundAtom σD) (t : Tm) (ht : t ∈ β.val.args) :
    t = Tm.cst (stripCst t) := by
  rcases β.property t ht with ⟨c, hc⟩
  rw [hc]
  rfl

/-- The argument list recovers as the constant list re-wrapped. -/
theorem args_eq_map_gargs (β : GroundAtom σD) :
    β.val.args = (gargs β).map (fun c => Tm.cst c) := by
  rw [gargs]
  have hmg : β.val.args.map (fun t => Tm.cst (stripCst t)) = β.val.args.map id := by
    apply List.map_congr_left
    intro t ht
    exact (arg_eq_cst β t ht).symm
  rw [List.map_map]
  exact (List.map_id β.val.args).symm.trans hmg.symm

theorem Atom.ext' {σD : Sig} {a b : Atom σD} (h1 : a.pred = b.pred) (h2 : a.args = b.args) :
    a = b := by
  rcases a with ⟨p, args, wf⟩
  rcases b with ⟨p', args', wf'⟩
  rcases h1 with rfl
  rcases h2 with rfl
  exact congrArg (Atom.mk p args) (proof_irrel wf wf')

/-- D is an extension of D₀ when every fact observed in D₀ keeps its value in
D ("D₀ is a restriction of D"). Direction matches Definition 3, Property 4
and the appendix proof of Prop 2 ("D extends D₀"). -/
def Extends (D D₀ : PreDatabase σD) : Prop :=
  ∀ α : GroundAtom σD, obs (D₀.val α) → D.val α = D₀.val α

/-- A (σ ⊇ σ_D)-structure models a σ_D-database (the paper's A ⊨ D; atoms are
read through the embedding). -/
def SatDB (eD : SigEmb σD σ) (A : FStruct σ) (D : PreDatabase σD) : Prop :=
  (∀ α, obs (D.val α) → D.val α = .uno → A.Satisfies (Fm.atom (eD.embAtom α.val))) ∧
  (∀ α, obs (D.val α) → D.val α = .zero → ¬ A.Satisfies (Fm.atom (eD.embAtom α.val)))

/-! ### The renaming machinery τ(D) -/

/-- `c` is in the range of τ. -/
def InRange (τ : Nat → Nat) (c : Nat) : Prop := ∃ c', τ c' = c

/-- Pull a constant back through τ (a chosen preimage; injectivity identifies
it where needed). -/
def invOf (τ : Nat → Nat) (c : Nat) (h : InRange τ c) : Nat := Classical.choose h

theorem invOf_spec (τ : Nat → Nat) {c : Nat} (h : InRange τ c) : τ (invOf τ c h) = c :=
  Classical.choose_spec h

/-- Raw list pull: every constant is pulled to a chosen preimage when one
exists, and to 0 otherwise. The dite makes the value proof-independent, so
premise-alignment is never needed downstream. -/
def pullConstsRaw (τ : Nat → Nat) : List Nat → List Nat :=
  fun cs => cs.map (fun c => if h : InRange τ c then invOf τ c h else 0)

/-- Pulled and re-pushed constants are the originals (injective τ). -/
theorem pullConstsRaw_fwd (τ : Nat → Nat) (hinj : Function.Injective τ) (cs : List Nat) :
    pullConstsRaw τ (cs.map τ) = cs := by
  rw [pullConstsRaw]
  have hmg : (cs.map τ).map (fun c => if h : InRange τ c then invOf τ c h else 0) = cs.map id := by
    rw [List.map_map]
    apply List.map_congr_left
    intro c hc
    change (if h : ∃ c', τ c' = τ c then invOf τ (τ c) h else 0) = c
    rw [dif_pos ⟨c, rfl⟩]
    exact hinj (invOf_spec τ ⟨c, rfl⟩)
  exact hmg.trans (List.map_id cs)

/-- In-range constants satisfy the roundtrip through the raw pull. -/
theorem pullConstsRaw_spec (τ : Nat → Nat) (c : Nat) (h : InRange τ c) :
    τ ((if h' : InRange τ c then invOf τ c h' else 0)) = c := by
  rw [dif_pos h]
  exact invOf_spec τ h

/-- Pushing pulled constants back recovers the in-range configuration. -/
theorem pullConstsRaw_push (τ : Nat → Nat) (hinj : Function.Injective τ) (cs : List Nat)
    (h : ∀ c ∈ cs, InRange τ c) : (pullConstsRaw τ cs).map τ = cs := by
  rw [pullConstsRaw]
  have hmg : (cs.map (fun c => if h : InRange τ c then invOf τ c h else 0)).map τ = cs.map id := by
    rw [List.map_map]
    apply List.map_congr_left
    intro c hc
    exact pullConstsRaw_spec τ c (h c hc)
  exact hmg.trans (List.map_id cs)

/-- The atom obtained by pulling every constant of β (given all are in
range). -/
def pullGAΩ (τ : Nat → Nat) {β : GroundAtom σD} (h : ∀ c ∈ gargs β, InRange τ c) :
    GroundAtom σD :=
  ⟨⟨β.val.pred, (pullConstsRaw τ (gargs β)).map (fun c => Tm.cst c), ⟨β.val.wf.1, by
      have hm : ((pullConstsRaw τ (gargs β)).map (fun c => Tm.cst c)).length =
          (pullConstsRaw τ (gargs β)).length := by rw [List.length_map]
      have hl : (pullConstsRaw τ (gargs β)).length = (gargs β).length := by
        rw [pullConstsRaw, List.length_map]
      have hl' : (gargs β).length = β.val.args.length := by rw [gargs, List.length_map]
      calc
        ((pullConstsRaw τ (gargs β)).map (fun c => Tm.cst c)).length
            = (pullConstsRaw τ (gargs β)).length := hm
        _ = (gargs β).length := hl
        _ = β.val.args.length := hl'
        _ = (σD.arity β.val.pred).getD 0 := β.val.wf.2⟩⟩, by
    intro t ht
    rcases List.mem_map.mp ht with ⟨c, _, rfl⟩
    exact ⟨c, rfl⟩⟩

/-- Pull a ground atom back through τ when all its constants are in the
range; `none` otherwise. -/
def pullGA (τ : Nat → Nat) (β : GroundAtom σD) : Option (GroundAtom σD) :=
  if h : ∀ c ∈ gargs β, InRange τ c then some (pullGAΩ τ h) else none

/-- The canonical unfolding of `pullGA` under an in-range hypothesis. -/
theorem pullGA_eq_some (τ : Nat → Nat) (β : GroundAtom σD) (h : ∀ c ∈ gargs β, InRange τ c) :
    pullGA τ β = some (pullGAΩ τ h) := by
  unfold pullGA
  rw [dif_pos h]

/-- Push a ground atom forward through τ (no injectivity needed). -/
def fwdGA (τ : Nat → Nat) (β : GroundAtom σD) : GroundAtom σD :=
  ⟨⟨β.val.pred, (gargs β).map (fun c => Tm.cst (τ c)), ⟨β.val.wf.1, by
      rw [show ((gargs β).map (fun c => Tm.cst (τ c))).length = β.val.args.length by
        simp [gargs]]
      exact β.val.wf.2⟩⟩, by
    intro t ht
    rcases List.mem_map.mp ht with ⟨c, _, rfl⟩
    exact ⟨τ c, rfl⟩⟩

/-- Forward pushing recovers the constants' image. -/
theorem gargs_fwd (τ : Nat → Nat) (β : GroundAtom σD) :
    gargs (fwdGA τ β) = (gargs β).map τ := by
  unfold gargs fwdGA
  rw [List.map_map]
  apply List.map_congr_left
  intro c hc
  rfl

/-- Pulling a forward image returns the original atom. -/
theorem pullGA_fwd (τ : Nat → Nat) (hinj : Function.Injective τ) (α : GroundAtom σD) :
    pullGA τ (fwdGA τ α) = some α := by
  have hg : gargs (fwdGA τ α) = (gargs α).map τ := gargs_fwd τ α
  have h' : ∀ c ∈ gargs (fwdGA τ α), InRange τ c := by
    intro c hc
    rw [hg] at hc
    rcases List.mem_map.mp hc with ⟨d, _, hd⟩
    exact ⟨d, hd⟩
  unfold pullGA
  change (if h : ∀ c ∈ gargs (fwdGA τ α), InRange τ c then some (pullGAΩ τ h) else none) = some α
  rw [dif_pos h']
  congr 1
  apply Subtype.ext
  apply Atom.ext'
  · rfl
  · change (pullConstsRaw τ (gargs (fwdGA τ α))).map (fun c => Tm.cst c) = α.val.args
    have hraw : pullConstsRaw τ (gargs (fwdGA τ α)) = gargs α := by
      rw [gargs_fwd τ α]
      exact pullConstsRaw_fwd τ hinj (gargs α)
    rw [hraw]
    exact (args_eq_map_gargs α).symm

lemma gargs_pullGAΩ {σD : Sig} (τ : Nat → Nat) {β : GroundAtom σD}
    (h : ∀ c ∈ gargs β, InRange τ c) :
    gargs (pullGAΩ (σD := σD) τ h) = pullConstsRaw τ (gargs β) := by
  unfold gargs pullGAΩ
  rw [List.map_map]
  change (pullConstsRaw τ (gargs β)).map (stripCst ∘ (fun c => Tm.cst c)) =
    pullConstsRaw τ (gargs β)
  have hm : (pullConstsRaw τ (gargs β)).map (stripCst ∘ (fun c => Tm.cst c)) =
      (pullConstsRaw τ (gargs β)).map id := by
    apply List.map_congr_left
    intro c hc
    rfl
  exact hm.trans (List.map_id _)

/-- Pushing the pulled atom back up recovers the original atom. -/
theorem fwdGA_pull (τ : Nat → Nat) (hinj : Function.Injective τ) (β : GroundAtom σD)
    (h : ∀ c ∈ gargs β, InRange τ c) : fwdGA τ (pullGAΩ τ h) = β := by
  apply Subtype.ext
  apply Atom.ext'
  · rfl
  · rw [show (fwdGA τ (pullGAΩ τ h)).val.args = (gargs (pullGAΩ τ h)).map (fun c => Tm.cst (τ c)) by
        rfl]
    rw [gargs_pullGAΩ (σD := σD) τ h]
    rw [(show (pullConstsRaw τ (gargs β)).map (fun c => Tm.cst (τ c)) =
        ((pullConstsRaw τ (gargs β)).map τ).map (fun c => Tm.cst c) by
      rw [List.map_map]
      apply List.map_congr_left
      intro c hc
      rfl)]
    rw [pullConstsRaw_push τ hinj (gargs β) h]
    exact (args_eq_map_gargs β).symm

/-- The renamed database τ(D): preimage-pull, with -1 on atoms whose
constants do not all lie in the range of τ. This is a *pre*-database: full
CWA-completeness would need τ to reach the CWA facts' constants, which the
paper implicitly assumes and we do not (plan §2.7). -/
def renameDB (τ : Nat → Nat) (hinj : Function.Injective τ) (D : PreDatabase σD) : PreDatabase σD where
  val := fun β => ((pullGA τ β).map D.val).getD .neg
  finite_observed := by
    have heq : { β : GroundAtom σD | obs ((((pullGA τ β).map D.val).getD .neg : TVal)) } =
        fwdGA τ '' { α : GroundAtom σD | obs (D.val α) } := by
      ext β
      constructor
      · intro hobs
        have h' : ∀ c ∈ gargs β, InRange τ c := by
          by_contra h
          have hnone : pullGA τ β = none := by
            unfold pullGA
            rw [dif_neg h]
          simpa [hnone, obs] using hobs
        let α : GroundAtom σD := pullGAΩ τ h'
        refine ⟨α, ?_, ?_⟩
        · have hx : pullGA τ β = some α := by
            rw [pullGA_eq_some τ β h']
          change obs ((((some α).map D.val).getD .neg))
          simpa [hx] using hobs
        · exact fwdGA_pull τ hinj β h'
      · intro hmem
        rcases hmem with ⟨α, hαobs, rfl⟩
        have hret : pullGA τ (fwdGA τ α) = some α := pullGA_fwd τ hinj α
        change obs ((((pullGA τ (fwdGA τ α)).map D.val).getD .neg))
        simpa [hret] using hαobs
    rw [heq]
    exact Set.Finite.image (fwdGA τ) D.finite_observed

/-! ### Query languages (Definition 2) -/

/-- A query language of σ_Q: a recursive class (here: a decidable predicate,
standing in for recursive under the plan's §2.8 coding discipline) of
FO-sentences closed under conjunctions and constant renamings, containing a
non-tautological sentence. -/
structure QueryLanguage (σQ : Sig) where
  q : Fm σQ → Prop
  closed_conj : ∀ {φ ψ : Fm σQ}, q φ → q ψ → q (Fm.conj φ ψ)
  closed_ren : ∀ {φ : Fm σQ} {τ : Nat → Nat}, Function.Injective τ → q φ → q (φ.rename τ)
  has_nontaut : ∃ φ : Fm σQ, q φ ∧ ¬ FStruct.Taut φ
  dec : DecidablePred q

/-! ### Knowledge bases (Definition 3) -/

/-- A KB over (𝒟, 𝒬): a subclass of 𝒟 × 𝒬 — read here as a predicate carrying
the five closure properties with their domain side-conditions as premises
(plan §2.7). -/
structure KB (𝒟 : Set (Database σD)) (Q : QueryLanguage σQ) where
  mem : PreDatabase σD → Fm σQ → Prop
  p1 : ∀ {D φ}, D ∈ 𝒟 → Q.q φ → FStruct.Taut φ → mem D φ
  p2 : ∀ {D φ ψ}, mem D φ → Q.q ψ → FStruct.Entails φ ψ → mem D ψ
  p3 : ∀ {D φ ψ}, mem D φ → mem D ψ → mem D (Fm.conj φ ψ)
  p4 : ∀ {D φ D₀}, mem D φ → D₀ ∈ 𝒟 → Extends D₀ D → mem D₀ φ
  p5 : ∀ {D φ} {τ : Nat → Nat} (hinj : Function.Injective τ),
      mem D φ → mem (renameDB τ hinj D) (φ.rename τ)

/-! ### Example 2: K_Σ (logic-induced knowledge bases) -/

/-- K_Σ := { (D,φ) ∈ 𝒟×𝒬 : D ∪ Σ ⊨ φ }, over an ambient σ ⊇ σ_D ∪ σ_Q.
Faithfulness note (plan §2.7): the paper claims K_Σ is a KB for arbitrary Σ;
the renaming closure actually needs Σ itself to be renaming-closed, which the
Solution adds as a hypothesis (see Solutions/Ex_KSigma.lean). -/
def KSigma (eD : SigEmb σD σ) (eQ : SigEmb σQ σ) (Sigma : Set (Fm σ))
    (Q : QueryLanguage σQ) : PreDatabase σD → Fm σQ → Prop :=
  fun D φ =>
    ∀ A : FStruct σ, SatDB eD A D → (∀ ψ, ψ ∈ Sigma → A.Satisfies ψ) → A.Satisfies (eQ.embFm φ)

/-! ### Belief mappings (Definition 4) and the induced KB -/

/-- A belief mapping of (σ_D, σ) maps each σ_D-database to a class of
σ-structures satisfying consistency with the observation (condition 1),
renaming invariance over σ-sentences (condition 2), and extension
monotonicity (condition 3). -/
structure BeliefMapping (σD σ : Sig) where
  eD : SigEmb σD σ
  M : PreDatabase σD → Set (FStruct σ)
  sound : ∀ {D} {A : FStruct σ}, A ∈ M D → SatDB eD A D
  rename : ∀ {D : PreDatabase σD} {τ : Nat → Nat} (hinj : Function.Injective τ) {φ : Fm σ},
      (∀ A, A ∈ M D → A.Satisfies φ) ↔ (∀ A, A ∈ M (renameDB τ hinj D) → A.Satisfies (φ.rename τ))
  mono : ∀ {D D₀ : PreDatabase σD} {φ : Fm σ},
      Extends D₀ D → (∀ A, A ∈ M D → A.Satisfies φ) →
      ∀ A, A ∈ M D₀ → A.Satisfies φ

/-- kb(𝕄,𝒟,𝒬) := { (D,φ) : 𝕄(D) ⊨ φ } — the KB induced by a belief mapping. -/
def kbOfBM (𝕄 : BeliefMapping σD σ) (eQ : SigEmb σQ σ) (Q : QueryLanguage σQ) :
    PreDatabase σD → Fm σQ → Prop :=
  fun D φ => ∀ A : FStruct σ, A ∈ 𝕄.M D → A.Satisfies (eQ.embFm φ)

end KRF