KRF Definitions_RenamingProps (arXiv 2412.11855 framework layer)

/-
Renaming soundness for database modeling: the atom-level correspondence
(evaluating the forward-pushed atom in A is evaluating the original atom in
the renamed structure) and the SatDB-level invariance

  SatDB eD A (τ(D)) ↔ SatDB eD (A.renamed τ) D

These are the missing links for K_Σ's Property 5 (Example 2) and for the
renaming condition of belief mappings. Sorry-free; they build on the
pullGA_fwd / fwdGA_pull roundtrips of Definitions/Data.
-/
import Definitions.Def_KRF_Data

noncomputable section

open KRFCore
open KRFCore.FStruct

namespace KRF

variable {σD σ : Sig}

/-- The observed atoms of τ(D) are exactly the forward images of the observed
atoms of D — extracted from the finiteness proof of `renameDB`. -/
theorem renameDB_observed_eq (τ : Nat → Nat) (hinj : Function.Injective τ)
    (D : PreDatabase σD) (β : GroundAtom σD) :
    obs ((renameDB τ hinj D).val β) ↔ ∃ α, obs (D.val α) ∧ β = fwdGA τ α := by
  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 [renameDB, hnone, obs] using hobs
    let α : GroundAtom σD := pullGAΩ τ h'
    refine ⟨α, ?_, ?_⟩
    · have hx : pullGA τ β = some α := by
        rw [pullGA_eq_some τ β h']
      have hvβ : (renameDB τ hinj D).val β = D.val α := by
        dsimp [renameDB]
        rw [hx]
        rfl
      simpa [hvβ] using hobs
    · exact (fwdGA_pull τ hinj β h').symm
  · 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

/-- The renamed value at a forward image is the original value. -/
theorem renameDB_val_fwd (τ : Nat → Nat) (hinj : Function.Injective τ)
    (D : PreDatabase σD) (α : GroundAtom σD) :
    (renameDB τ hinj D).val (fwdGA τ α) = D.val α := by
  change ((pullGA τ (fwdGA τ α)).map D.val).getD .neg = D.val α
  rw [pullGA_fwd τ hinj α]
  rfl

/-- Forward-pushed argument lists equal the renamed original lists. -/
lemma args_rename_fwd {σD : Sig} (τ : Nat → Nat) (α : GroundAtom σD) :
    (gargs α).map (fun c => Tm.cst (τ c)) = α.val.args.map (renameTm τ) := by
  have ha : (gargs α).map (fun c => Tm.cst c) = α.val.args := (args_eq_map_gargs α).symm
  have h₂ : ((gargs α).map (fun c => Tm.cst c)).map (renameTm τ) = α.val.args.map (renameTm τ) :=
    congrArg (fun l : List Tm => l.map (renameTm τ)) ha
  rw [List.map_map] at h₂
  calc
    (gargs α).map (fun c => Tm.cst (τ c)) = (gargs α).map (renameTm τ ∘ fun c => Tm.cst c) := by rfl
    _ = α.val.args.map (renameTm τ) := h₂

/-- Atom-level correspondence between A and A compiled with τ on constants. -/
theorem sat_atom_fwd (eD : SigEmb σD σ) (τ : Nat → Nat) (A : FStruct σ)
    (α : GroundAtom σD) (s : Nat → A.Dom) :
    A.Sat s (Fm.atom (SigEmb.embAtom eD (fwdGA τ α).val)) ↔
      (A.renamed τ).Sat s (Fm.atom (SigEmb.embAtom eD α.val)) := by
  have hlead : Fm.atom (SigEmb.embAtom eD (fwdGA τ α).val) =
      (Fm.atom (SigEmb.embAtom eD α.val)).rename τ := by
    apply congrArg Fm.atom
    apply Atom.ext'
    · rfl
    · change (SigEmb.embAtom eD (fwdGA τ α).val).args =
          (SigEmb.embAtom eD α.val).args.map (renameTm τ)
      change (gargs α).map (fun c => Tm.cst (τ c)) =
          ((SigEmb.embAtom eD α.val).args).map (renameTm τ)
      change (gargs α).map (fun c => Tm.cst (τ c)) = α.val.args.map (renameTm τ)
      exact args_rename_fwd τ α
  rw [hlead]
  exact (FStruct.sat_rename A s (Fm.atom (SigEmb.embAtom eD α.val)))

/-- Database modeling is invariant under the synchronized renaming of
structure constants and database atoms. -/
theorem satDB_rename (eD : SigEmb σD σ) (τ : Nat → Nat) (hinj : Function.Injective τ)
    (A : FStruct σ) (D : PreDatabase σD) :
    SatDB eD A (renameDB τ hinj D) ↔ SatDB eD (A.renamed τ) D := by
  constructor
  · intro hA
    constructor
    · intro α ho hv
      have hobs' : obs ((renameDB τ hinj D).val (fwdGA τ α)) := by
        rw [renameDB_val_fwd τ hinj D α]
        exact ho
      have hf : A.Satisfies (Fm.atom (SigEmb.embAtom eD (fwdGA τ α).val)) :=
        hA.1 (fwdGA τ α) hobs' (by simpa [renameDB_val_fwd τ hinj D α] using hv)
      intro s
      exact ((sat_atom_fwd eD τ A α s).mp (hf s))
    · intro α ho hz
      have hobs' : obs ((renameDB τ hinj D).val (fwdGA τ α)) := by
        rw [renameDB_val_fwd τ hinj D α]
        exact ho
      have hf : ¬ A.Satisfies (Fm.atom (SigEmb.embAtom eD (fwdGA τ α).val)) :=
        hA.2 (fwdGA τ α) hobs' (by simpa [renameDB_val_fwd τ hinj D α] using hz)
      intro hsat
      exact hf (fun s => ((sat_atom_fwd eD τ A α s).mpr (hsat s)))
  · intro hA
    constructor
    · intro β ho hv
      rcases (renameDB_observed_eq τ hinj D β).mp ho with ⟨α, hαobs, rfl⟩
      intro s
      exact ((sat_atom_fwd eD τ A α s).mpr
        (hA.1 α hαobs (by simpa [renameDB_val_fwd τ hinj D α] using hv) s))
    · intro β ho hz
      rcases (renameDB_observed_eq τ hinj D β).mp ho with ⟨α, hαobs, rfl⟩
      intro hsat
      exact hA.2 α hαobs (by simpa [renameDB_val_fwd τ hinj D α] using hz)
        (fun s => ((sat_atom_fwd eD τ A α s).mp (hsat s)))

end KRF