import AntiDynamics.Theorem2

/-!
# Additions (suggested extra results, not in the paper)

* `st_pointwise`, `rt_pointwise`, `transp_quant_pointwise`: exact, world-by-world characterization of
  Transparency for a quantificational clause (no constancy, no Non-Triviality).
* `theorem2'`: Theorem 2 with hypotheses (ii) and (iii) replaced by a local non-degeneracy condition
  on the quantifier; `theorem2_via_theorem2'` recovers the corrected Theorem 2 from it.
* `theorem2'_strictly_stronger`: a model with non-constant restrictor size to which `theorem2'`
  applies but Theorem 2 does not.
-/

namespace AntiDyn
namespace Quantified

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

/-- `g` is constant on the line `{(p-b, b) : b ≤ p}`. -/
def LineConst (g : Nat → Nat → Bool) (p : Nat) : Prop :=
  ∀ b₁ b₂, b₁ ≤ p → b₂ ≤ p → g (p - b₁) b₁ = g (p - b₂) b₂

/-- `g` is constant on the triangle `{(a, b) : a + b ≤ n}`. -/
def TriConst (g : Nat → Nat → Bool) (n : Nat) : Prop :=
  ∀ a b a' b', a + b ≤ n → a' + b' ≤ n → g a b = g a' b'

theorem qsem_tri (q : κ) (P R : Pred ρ) (w : W) :
    ∃ a b, a + b ≤ M.n ∧ M.qsem q P R w = M.f q a b := by
  refine ⟨_, _, ?_, rfl⟩
  rw [qsem_args_le M P R w]; exact cnt_le _ _

theorem qsem_line (q : κ) (P R : Pred ρ) (w : W) :
    ∃ b, b ≤ cnt M.n (M.pstat P w) ∧
      M.qsem q P R w = M.f q (cnt M.n (M.pstat P w) - b) b := by
  have h := qsem_args_le M P R w
  refine ⟨cnt M.n (fun d => M.pstat P w d && M.pstat R w d), by omega, ?_⟩
  have : cnt M.n (M.pstat P w) - 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) := by omega
  rw [this]; rfl

/-- **Exact characterization, nuclear-scope trigger.**  With every property expressible,
`Transp(C,(Q P . R̲_k R'))` holds iff at every `w ∈ C` either Heim's condition holds
(`P^w ⊆ R_k^w`) or `f_Q` is constant on the line `a+b = |P^w|`.  No constancy of `|P^w|`,
no Non-Triviality. -/
theorem st_pointwise (hexp : M.Expressive) (C : WSet W) (q : κ) (P : Pred ρ) (k : ρ) :
    ST M C q P k ↔ ∀ w, C w →
      ((∀ d, d < M.n → M.pstat P w d = true → M.I k w d = true) ∨
        LineConst (M.f q) (cnt M.n (M.pstat P w))) := by
  constructor
  · intro h w hw
    by_cases hl : LineConst (M.f q) (cnt M.n (M.pstat P w))
    · exact Or.inr hl
    · left
      have hne : ∃ b₁ b₂, b₁ ≤ cnt M.n (M.pstat P w) ∧ b₂ ≤ cnt M.n (M.pstat P w) ∧
          M.f q (cnt M.n (M.pstat P w) - b₁) b₁ ≠ M.f q (cnt M.n (M.pstat P w) - b₂) b₂ := by
        apply Classical.byContradiction
        intro hn
        apply hl
        intro b₁ b₂ h1 h2
        apply Classical.byContradiction
        intro hne
        exact hn ⟨b₁, b₂, h1, h2, hne⟩
      have hST : ST M (fun v => v = w) q P k := fun m v hv => by
        rw [hv]; exact h m w hw
      exact (lemma1_ii M hexp (fun v => v = w) q k P (cnt M.n (M.pstat P w))
        (fun v hv => by rw [hv]) hne).1 hST w rfl
  · intro h m w hw
    rcases h w hw with h1 | h1
    · exact st_at M q P k m w h1
    · obtain ⟨b, hb, e1⟩ := qsem_line M q P (.conj k m) w
      obtain ⟨b', hb', e2⟩ := qsem_line M q P (.plain m) w
      rw [e1, e2]
      exact h1 b b' hb hb'

/-- **Exact characterization, restrictor trigger.**  `Transp(C,(Q P̲_k P' . R))` (all `R`, all
`P_m`) holds iff at every `w ∈ C` either every individual satisfies `P_k` or `f_Q` is constant on the
whole triangle `a+b ≤ n`. -/
theorem rt_pointwise (hexp : M.Expressive) (C : WSet W) (q : κ) (k : ρ) :
    RT M C q k ↔ ∀ w, C w →
      ((∀ d, d < M.n → M.I k w d = true) ∨ TriConst (M.f q) M.n) := by
  constructor
  · intro h w hw
    by_cases hl : TriConst (M.f q) M.n
    · exact Or.inr hl
    · left
      have hne : ∃ a b a' b', a + b ≤ M.n ∧ a' + b' ≤ M.n ∧ M.f q a b ≠ M.f q a' b' := by
        apply Classical.byContradiction
        intro hn
        apply hl
        intro a b a' b' h1 h2
        apply Classical.byContradiction
        intro hne
        exact hn ⟨a, b, a', b', h1, h2, hne⟩
      have hRT : RT M (fun v => v = w) q k := fun m Y v hv => by
        rw [hv]; exact h m Y w hw
      exact (lemma1_i M hexp (fun v => v = w) q k hne).1 hRT w rfl
  · intro h m Y w hw
    rcases h w hw with h1 | h1
    · exact rt_at M q k m Y w h1
    · obtain ⟨a, b, hab, e1⟩ := qsem_tri M q (.conj k m) Y w
      obtain ⟨a', b', hab', e2⟩ := qsem_tri M q (.plain m) Y w
      rw [e1, e2]
      exact h1 a b a' b' hab hab'

/-- Transparency of a full quantificational clause, world by world. -/
theorem transp_quant_pointwise (hexp : M.Expressive) (C : WSet W) (q : κ) (P R : Pred ρ) :
    (sys M).Transp C (.leaf (.quant q P R)) ↔
      (∀ k j, P = .trig k j → ∀ w, C w →
        ((∀ d, d < M.n → M.I k w d = true) ∨ TriConst (M.f q) M.n)) ∧
      (∀ k j, R = .trig k j → ∀ w, C w →
        ((∀ d, d < M.n → M.pstat P w d = true → M.I k w d = true) ∨
          LineConst (M.f q) (cnt M.n (M.pstat P w)))) := by
  rw [transp_quant]
  constructor
  · rintro ⟨h1, h2⟩
    exact ⟨fun k j hP => (rt_pointwise M hexp C q k).1 (h1 k j hP),
           fun k j hR => (st_pointwise M hexp C q P k).1 (h2 k j hR)⟩
  · rintro ⟨h1, h2⟩
    exact ⟨fun k j hP => (rt_pointwise M hexp C q k).2 (h1 k j hP),
           fun k j hR => (st_pointwise M hexp C q P k).2 (h2 k j hR)⟩

/-- Local non-degeneracy of a clause `(Q P . R)` in context `C`: a trigger in the restrictor needs
`f_Q` non-constant on the triangle; a trigger in the scope needs `f_Q` non-constant on the line
`a+b = |P^w|` for every `w ∈ C`. -/
def NonDeg (C : WSet W) (q : κ) (P R : Pred ρ) : Prop :=
  (∀ k j, P = .trig k j → ¬ TriConst (M.f q) M.n) ∧
  (∀ k j, R = .trig k j → ∀ w, C w → ¬ LineConst (M.f q) (cnt M.n (M.pstat P w)))

/-- Lemma 1 for a clause under `NonDeg` alone. -/
theorem quant_leaf' (hexp : M.Expressive) (C : WSet W) (q : κ) (P R : Pred ρ)
    (hnd : NonDeg M C q P R) :
    (sys M).Transp C (.leaf (.quant q P R)) ↔ M.qdef P R C := by
  obtain ⟨hn1, hn2⟩ := hnd
  rw [transp_quant_pointwise M hexp]
  constructor
  · rintro ⟨h1, h2⟩
    refine ⟨?_, ?_⟩
    · intro w hw d hd
      cases P with
      | plain k => rfl
      | conj k j => rfl
      | trig k j =>
        rcases h1 k j rfl w hw with h | h
        · exact h d hd
        · exact absurd h (hn1 k j rfl)
    · intro w hw d hd hPd
      cases R with
      | plain k => rfl
      | conj k j => rfl
      | trig k j =>
        rcases h2 k j rfl w hw with h | h
        · exact h d hd hPd
        · exact absurd h (hn2 k j rfl w hw)
  · rintro ⟨d1, d2⟩
    exact ⟨fun k j hP w hw => Or.inl (fun d hd => by subst hP; exact d1 w hw d hd),
           fun k j hR w hw => Or.inl (fun d hd hPd => by subst hR; exact d2 w hw d hd hPd)⟩

/-- Non-degeneracy at every quantificational clause accessed from `⟨C, F⟩`. -/
def NondegAcc (C : WSet W) (F : Fm (QLeaf ι ρ κ)) : Prop :=
  ∀ C'' q P R, Accessed (sys M) C F C'' (.leaf (.quant q P R)) → NonDeg M C'' q P R

/-- **Theorem 2′.**  Theorem 2 with hypotheses (ii) (constant restrictor size) and (iii)
(Non-Triviality) replaced by `NondegAcc` (only expressiveness remains from Lemma 1). -/
theorem theorem2' (hexp : M.Expressive) (C : WSet W) (F : Fm (QLeaf ι ρ κ))
    (hnd : NondegAcc M C F) :
    ∀ (C' : WSet W) (F' : Fm (QLeaf ι ρ κ)), Accessed (sys M) C F C' F' →
      ((sys M).Transp C' F' ↔ (sys M).Def F' C') ∧
      ((sys M).Def F' C' → (sys M).Upd F' C' = (sys M).TS F' C') := by
  intro C' F' hacc
  refine ⟨?_, fun hd => (sys M).upd_eq_TS F' C' hd⟩
  refine (sys M).lift (C₀ := C) (F₀ := F) ?_ F' C' hacc
  intro C'' l hl
  rw [Sys.transp_leaf]
  cases l with
  | atom i => simp [sys]
  | trig a b =>
    simp only [sys]
    constructor
    · intro h w hw
      have := h (.conj (.leaf (.atom a)) (sys M).top) (sys M).top ⟨(sys M).top, rfl, rfl⟩ w hw
      simpa [Sys.eval, evalF, sys, (sys M).top_true] using this
    · rintro h φ₁ φ₂ ⟨γ, rfl, rfl⟩ w hw
      simp [Sys.eval, evalF, h w hw]
  | quant q P R =>
    have := quant_leaf' M hexp C'' q P R (hnd C'' q P R hl)
    rw [Sys.transp_leaf] at this
    exact this

/-- Theorem 2's hypotheses (ii), (iii) imply `NondegAcc`. -/
theorem nondegAcc_of_NT (C : WSet W) (F : Fm (QLeaf ι ρ κ))
    (hconst : ConstRestr M C F) (hNT : (sys M).NT IsQ C F) : NondegAcc M C F := by
  intro C'' q P R hacc
  have hNT' := (sys M).lemma2 hNT hacc
  obtain ⟨hsub, hleaf⟩ := hacc.sub
  obtain ⟨p, hp⟩ := hconst _ (hleaf _ (by simp [Fm.leaves])) q P R rfl
  have hp' : ∀ w, C'' w → cnt M.n (M.pstat P w) = p := fun w hw => hp w (hsub w hw)
  obtain ⟨a, b, a', b', h1, h2, hne⟩ := nt_corollary_i M hNT'
  obtain ⟨c₁, c₂, g1, g2, hne'⟩ := nt_corollary_ii M hNT' hp'
  refine ⟨fun k j _ hc => hne (hc a b a' b' h1 h2), fun k j _ w hw hc => ?_⟩
  rw [hp' w hw] at hc
  exact hne' (hc c₁ c₂ g1 g2)

/-- The corrected Theorem 2 is a corollary of `theorem2'`. -/
theorem theorem2_via_theorem2' (hexp : M.Expressive) (C : WSet W) (F : Fm (QLeaf ι ρ κ))
    (hconst : ConstRestr M C F) (hNT : (sys M).NT IsQ C F) :
    ∀ (C' : WSet W) (F' : Fm (QLeaf ι ρ κ)), Accessed (sys M) C F C' F' →
      ((sys M).Transp C' F' ↔ (sys M).Def F' C') ∧
      ((sys M).Def F' C' → (sys M).Upd F' C' = (sys M).TS F' C') :=
  theorem2' M hexp C F (nondegAcc_of_NT M C F hconst hNT)

/-! ### Theorem 2′ is strictly stronger: non-constant restrictor size -/

/-- Predicate letters are the properties themselves (so the model is expressive); two worlds;
domain `{0,1}`; `Q = no` (`f a b = [b = 0]`); `P` has size 2 at `true` and 1 at `false`. -/
def exModel : QModel Bool Unit (Bool → Nat → Bool) Unit where
  val := fun _ _ => true
  I := fun k w d => k w d
  f := fun _ _ b => decide (b = 0)
  n := 2
  i0 := ()

def exP : Bool → Nat → Bool := fun w d => decide (d < (if w then 2 else 1))
def exR : Bool → Nat → Bool := fun _ _ => true

def exF : Fm (QLeaf Unit (Bool → Nat → Bool) Unit) :=
  .leaf (.quant () (.plain exP) (.trig exR exR))

theorem exModel_expressive : exModel.Expressive := fun s => ⟨s, fun _ _ => rfl⟩

theorem exModel_nondeg : NondegAcc exModel (fun _ => True) exF := by
  intro C'' q P R hacc
  have hl := hacc.sub.2 (.quant q P R) (by simp [Fm.leaves])
  simp only [exF, Fm.leaves, List.mem_cons, List.not_mem_nil, or_false, QLeaf.quant.injEq] at hl
  obtain ⟨-, rfl, rfl⟩ := hl
  refine ⟨fun k j h => (nomatch h), fun k j _ w _ hc => ?_⟩
  have h01 := hc 0 1
  cases q
  cases w
  · exact absurd (h01 (by decide) (by decide)) (by decide)
  · exact absurd (h01 (by decide) (by decide)) (by decide)

/-- `theorem2'` applies to `exF`, although Theorem 2's hypothesis (ii) fails. -/
theorem theorem2'_strictly_stronger :
    ((sys exModel).Transp (fun _ => True) exF ↔ (sys exModel).Def exF (fun _ => True)) ∧
    ¬ ConstRestr exModel (fun _ => True) exF := by
  refine ⟨(theorem2' exModel exModel_expressive _ exF exModel_nondeg _ exF .refl).1, ?_⟩
  intro h
  obtain ⟨p, hp⟩ := h _ (by simp [exF, Fm.leaves]) () (.plain exP) (.trig exR exR) rfl
  have h1 := hp true trivial
  have h2 := hp false trivial
  have e1 : cnt exModel.n (exModel.pstat (.plain exP) true) = 2 := by decide
  have e2 : cnt exModel.n (exModel.pstat (.plain exP) false) = 1 := by decide
  omega

end Quantified
end AntiDyn