import AntiDynamics.Lifting
import AntiDynamics.Counting
import AntiDynamics.Arith

/-!
# The quantificational case: the model, Lemma 1 (Section 5.2)

Fidelity notes.
* Domain: individuals are `0, …, n-1` (constant finite size `n`, as in Section 3.2);
  sets of individuals are `Nat → Bool`, cardinalities are `cnt n`.
* A generalized quantifier `Q_i` is *given by its tree of numbers* `f_i : ℕ → ℕ → Bool`
  (`Iw(Q_i)(A)(B) = f_i(|A−B|, |A∩B|)`, paper (20a)); permutation invariance, extension and
  conservativity are then built in.  No further property of `f_i` is assumed.
* Predicates: `plain k` = `P_k`; `trig k j` = `P̲_k P'_j` (presupposition `P_k`, assertion `P_j`);
  `conj k j` = `(P_k and P_j)` (the non-recursive predicate conjunction of (18)).
* Only the clause types of (18) are formalized:  `(Q P . R)` with predicates `P, R`.
* A "sentence completion" of the initial string `(Q_i P̲P'` is `. Y)` with `Y` any predicate,
  and of `(Q_i P . R̲R'`  is `)`; this is what `lvar` encodes.
-/

namespace AntiDyn
namespace Quantified

/-- Predicates of (18): `P_i`, `P̲_i P'_k`, `(P_i and P_k)`. -/
inductive Pred (ρ : Type) where
  | plain : ρ → Pred ρ
  | trig : ρ → ρ → Pred ρ
  | conj : ρ → ρ → Pred ρ
  deriving DecidableEq

/-- Clauses: propositional atoms `p_i`, `p̲_a p'_b`, and quantificational clauses `(Q_q P . R)`. -/
inductive QLeaf (ι ρ κ : Type) where
  | atom : ι → QLeaf ι ρ κ
  | trig : ι → ι → QLeaf ι ρ κ
  | quant : κ → Pred ρ → Pred ρ → QLeaf ι ρ κ

/-- A model: valuation of propositional letters, interpretation of predicate letters
(`I k w d` : `P_k` holds of individual `d` at `w`), trees of numbers of the quantifiers,
domain size `n`, and a propositional letter `i0` (to build `⊤`, `⊥`). -/
structure QModel (W ι ρ κ : Type) where
  val : W → ι → Bool
  I : ρ → W → Nat → Bool
  f : κ → Nat → Nat → Bool
  n : Nat
  i0 : ι

variable {W ι ρ κ : Type} (M : QModel W ι ρ κ)

namespace QModel

/-- Static value of a predicate (the underlined part is just conjoined). -/
def pstat : Pred ρ → W → Nat → Bool
  | .plain k, w, d => M.I k w d
  | .trig k j, w, d => M.I k w d && M.I j w d
  | .conj k j, w, d => M.I k w d && M.I j w d

/-- Assertive component. -/
def passert : Pred ρ → W → Nat → Bool
  | .plain k, w, d => M.I k w d
  | .trig _ j, w, d => M.I j w d
  | .conj k j, w, d => M.I k w d && M.I j w d

/-- Presuppositional component. -/
def ppre : Pred ρ → W → Nat → Bool
  | .plain _, _, _ => true
  | .trig k _, w, d => M.I k w d
  | .conj _ _, _, _ => true

theorem pstat_eq (P : Pred ρ) (w d) : M.pstat P w d = (M.ppre P w d && M.passert P w d) := by
  cases P <;> simp [pstat, ppre, passert]

/-- Static semantics (25) of `(Q P . R)`: `f(|P∖R|, |P∩R|)` computed with the static values. -/
def qsem (q : κ) (P R : Pred ρ) (w : W) : Bool :=
  M.f q (cnt M.n (fun d => M.pstat P w d && !M.pstat R w d))
        (cnt M.n (fun d => M.pstat P w d && M.pstat R w d))

/-- Heim's update (21) for `(Q P . R)`: only assertive components enter the counts. -/
def qupd (q : κ) (P R : Pred ρ) (C : WSet W) : WSet W := fun w =>
  C w ∧ M.f q (cnt M.n (fun d => M.passert P w d && !M.passert R w d))
              (cnt M.n (fun d => M.passert P w d && M.passert R w d)) = true

/-- Heim's definedness condition (21). -/
def qdef (P R : Pred ρ) (C : WSet W) : Prop :=
  (∀ w, C w → ∀ d, d < M.n → M.ppre P w d = true) ∧
  (∀ w, C w → ∀ d, d < M.n → M.pstat P w d = true → M.ppre R w d = true)

/-- `Expressive`: any property of individuals (possibly world-dependent) is expressed by some
predicate letter — hypothesis (b) of Lemma 1. -/
def Expressive : Prop := ∀ s : W → Nat → Bool, ∃ m : ρ, ∀ w d, M.I m w d = s w d

end QModel

/-- The Sys instance for the quantified fragment. -/
def sys : Sys W (QLeaf ι ρ κ) where
  sem := fun l w => match l with
    | .atom i => M.val w i
    | .trig a b => M.val w a && M.val w b
    | .quant q P R => M.qsem q P R w
  lupd := fun l C => match l with
    | .atom i => fun w => C w ∧ M.val w i = true
    | .trig _ b => fun w => C w ∧ M.val w b = true
    | .quant q P R => M.qupd q P R C
  ldef := fun l C => match l with
    | .atom _ => True
    | .trig a _ => ∀ w, C w → M.val w a = true
    | .quant _ P R => M.qdef P R C
  lvar := fun l φ₁ φ₂ => match l with
    | .atom _ => False
    | .trig a _ => ∃ γ, φ₁ = .conj (.leaf (.atom a)) γ ∧ φ₂ = γ
    | .quant q P R =>
        (∃ k j m Y, P = .trig k j ∧ φ₁ = .leaf (.quant q (.conj k m) Y) ∧
            φ₂ = .leaf (.quant q (.plain m) Y)) ∨
        (∃ k j m, R = .trig k j ∧ φ₁ = .leaf (.quant q P (.conj k m)) ∧
            φ₂ = .leaf (.quant q P (.plain m)))
  top := .disj (.leaf (.atom M.i0)) (.neg (.leaf (.atom M.i0)))
  bot := .conj (.leaf (.atom M.i0)) (.neg (.leaf (.atom M.i0)))
  top_ok := by intro w; simp [evalF]
  bot_ok := by intro w; simp [evalF]
  lupd_static := by
    intro l C h
    cases l with
    | atom i => rfl
    | trig a b =>
      funext w; apply propext
      simp only
      constructor
      · rintro ⟨hc, hb⟩; exact ⟨hc, by simp [h w hc, hb]⟩
      · rintro ⟨hc, hb⟩
        have hb' : (M.val w a && M.val w b) = true := hb
        simp at hb'
        exact ⟨hc, hb'.2⟩
    | quant q P R =>
      obtain ⟨h1, h2⟩ := h
      funext w; apply propext
      simp only [QModel.qupd, QModel.qsem]
      constructor
      · rintro ⟨hc, hb⟩
        refine ⟨hc, ?_⟩
        have e1 : cnt M.n (fun d => M.passert P w d && !M.passert R w d) =
            cnt M.n (fun d => M.pstat P w d && !M.pstat R w d) := by
          apply cnt_congr; intro d hd
          have hP := h1 w hc d hd
          have hs := M.pstat_eq P w d
          simp [hP] at hs
          by_cases hp : M.pstat P w d = true
          · have hR := h2 w hc d hd hp
            rw [M.pstat_eq R w d, hs]; simp [hR]
          · simp [hs] at hp; simp [hs, hp]
        have e2 : cnt M.n (fun d => M.passert P w d && M.passert R w d) =
            cnt M.n (fun d => M.pstat P w d && M.pstat R w d) := by
          apply cnt_congr; intro d hd
          have hP := h1 w hc d hd
          have hs := M.pstat_eq P w d
          simp [hP] at hs
          by_cases hp : M.pstat P w d = true
          · have hR := h2 w hc d hd hp
            rw [M.pstat_eq R w d, hs]; simp [hR]
          · simp [hs] at hp; simp [hs, hp]
        rw [← e1, ← e2]; exact hb
      · rintro ⟨hc, hb⟩
        refine ⟨hc, ?_⟩
        have e1 : cnt M.n (fun d => M.passert P w d && !M.passert R w d) =
            cnt M.n (fun d => M.pstat P w d && !M.pstat R w d) := by
          apply cnt_congr; intro d hd
          have hP := h1 w hc d hd
          have hs := M.pstat_eq P w d
          simp [hP] at hs
          by_cases hp : M.pstat P w d = true
          · have hR := h2 w hc d hd hp
            rw [M.pstat_eq R w d, hs]; simp [hR]
          · simp [hs] at hp; simp [hs, hp]
        have e2 : cnt M.n (fun d => M.passert P w d && M.passert R w d) =
            cnt M.n (fun d => M.pstat P w d && M.pstat R w d) := by
          apply cnt_congr; intro d hd
          have hP := h1 w hc d hd
          have hs := M.pstat_eq P w d
          simp [hP] at hs
          by_cases hp : M.pstat P w d = true
          · have hR := h2 w hc d hd hp
            rw [M.pstat_eq R w d, hs]; simp [hR]
          · simp [hs] at hp; simp [hs, hp]
        rw [e1, e2]; exact hb

end Quantified
end AntiDyn