import AntiDynamics.Theorem2

/-!
# Section 5.1 scenarios, Section 6 point 5, and a countermodel to Theorem 2 as stated

1. `less_than_three_scenario`: the paper's first scenario (only worlds with 2 P-individuals):
   Transparency holds trivially but Heim's presupposition fails; Non-Triviality rules it out.
2. `constancy_needed`: the paper's second scenario (`C = {w, w', w''}`, restrictor sizes 2, 4, 4).
3. `soccer_example`: the (34) example: Transp holds, Heim predicts presupposition failure.
4. `theorem2_needs_expressiveness`: **new**: with the paper's three hypotheses but a
   vocabulary that does not express every property, Transparency holds and Heim fails.
-/

namespace AntiDyn
namespace Quantified

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

/-- Trivial-scope lemma for `Q = less than three` (`f a b = [b < 3]`, which depends on `b` only):
scope-trigger Transparency holds as soon as, in each world, either the restrictor is included
in the presupposed predicate or the restrictor has fewer than three elements. -/
theorem st_lt3 (C : WSet W) (q : κ) (P : Pred ρ) (k : ρ)
    (hf : ∀ a b, M.f q a b = decide (b < 3))
    (h : ∀ w, C w → (∀ d, d < M.n → M.pstat P w d = true → M.I k w d = true) ∨
      cnt M.n (M.pstat P w) < 3) : ST M C q P k := by
  intro m w hw
  rcases h w hw with h1 | h2
  · exact st_at M q P k m w h1
  · simp only [QModel.qsem, hf]
    have b1 : cnt M.n (fun d => M.pstat P w d && M.pstat (.conj k m) w d) ≤ cnt M.n (M.pstat P w) :=
      cnt_mono _ (fun x hx => by simp_all)
    have b2 : cnt M.n (fun d => M.pstat P w d && M.pstat (.plain m) w d) ≤ cnt M.n (M.pstat P w) :=
      cnt_mono _ (fun x hx => by simp_all)
    simp only [decide_eq_decide]
    omega


/-- Non-Triviality fails when every world has fewer than three restrictor individuals
(paper, Section 5.1 (i)): `(Q P . R)` is then true everywhere. -/
theorem not_nt_of_lt3 (C : WSet W) (q : κ) (P R : Pred ρ)
    (hf : ∀ a b, M.f q a b = decide (b < 3)) (h : ∀ w, C w → cnt M.n (M.pstat P w) < 3) :
    ¬ (sys M).NT IsQ C (.leaf (.quant q P R)) := by
  intro hnt
  obtain ⟨w₁, w₂, hw₁, hw₂, h1, h2⟩ := nt_leaf_values M hnt
  have b1 : cnt M.n (fun d => M.pstat P w₁ d && M.pstat R w₁ d) ≤ cnt M.n (M.pstat P w₁) :=
    cnt_mono _ (fun x hx => by simp_all)
  have := h w₁ hw₁
  simp only [QModel.qsem, hf] at h1
  simp at h1
  omega

/-- A fully expressive model over worlds `W` and domain size `n`, with the single quantifier
`Q = less than three` (`f(a,b) = [b < 3]`).  Predicate letters *are* the properties
`W → ℕ → Bool`. -/
def lt3Model (W : Type) (n : Nat) : QModel W Unit (W → Nat → Bool) Unit where
  val := fun _ _ => true
  I := fun s w d => s w d
  f := fun _ _ b => decide (b < 3)
  n := n
  i0 := ()

theorem lt3Model_expressive (W : Type) (n : Nat) : (lt3Model W n).Expressive :=
  fun s => ⟨s, fun _ _ => rfl⟩

/-- Transparency of a scope trigger `R̲R'` (letter `R`) in `less than three` clauses. -/
theorem transp_lt3 (W : Type) (n : Nat) (C : WSet W) (P R R' : W → Nat → Bool)
    (h : ∀ w, C w → (∀ d, d < n → P w d = true → R w d = true) ∨
      cnt n (fun d => P w d) < 3) :
    (sys (lt3Model W n)).Transp C (.leaf (.quant () (.plain P) (.trig R R'))) := by
  rw [transp_quant]
  refine ⟨(fun k j hh => by cases hh), ?_⟩
  intro k j hh
  cases hh
  exact st_lt3 (lt3Model W n) C () (.plain P) R (fun _ _ => rfl) h

/-! ### Section 5.1, first scenario -/

/-- Paper 5.1 (i): one world, exactly two `P`-individuals (one satisfies `R`), `Q = less than
three`.  Transparency holds, Heim's presupposition fails, and Non-Triviality is violated. -/
theorem less_than_three_scenario :
    ∃ (C : WSet Unit) (P R R' : Unit → Nat → Bool),
      let M := lt3Model Unit 4
      M.Expressive ∧ (∀ w, C w → cnt M.n (M.pstat (.plain P) w) = 2) ∧
      (sys M).Transp C (.leaf (.quant () (.plain P) (.trig R R'))) ∧
      ¬ M.qdef (.plain P) (.trig R R') C ∧
      ¬ (sys M).NT IsQ C (.leaf (.quant () (.plain P) (.trig R R'))) := by
  refine ⟨fun _ => True, fun _ d => decide (d < 2), fun _ d => decide (d = 0), fun _ _ => true,
    lt3Model_expressive _ _, ?_, ?_, ?_, ?_⟩
  · intro w _; cases w; decide
  · apply transp_lt3
    intro w _
    cases w; right; decide
  · rintro ⟨-, h2⟩
    have := h2 () trivial 1 (by decide) (by decide)
    revert this; decide
  · apply not_nt_of_lt3 _ _ _ _ _ (fun _ _ => rfl)
    intro w _; cases w; decide

/-! ### Section 5.1, second scenario: Constancy is needed -/

/-- Paper 5.1 (ii): `C = {w₀, w₁, w₂}`; two `P`-individuals in `w₀` (one satisfies `R`), four in
`w₁`, `w₂` (all satisfy `R`; all satisfy `R'` in `w₁`, none in `w₂`).  Non-Triviality holds,
Transparency holds, Heim's presupposition fails.  Only Constancy (restrictor sizes 2, 4, 4) fails. -/
theorem constancy_needed :
    ∃ (C : WSet (Fin 3)) (P R R' : Fin 3 → Nat → Bool),
      let M := lt3Model (Fin 3) 4
      M.Expressive ∧
      (sys M).NT IsQ C (.leaf (.quant () (.plain P) (.trig R R'))) ∧
      (sys M).Transp C (.leaf (.quant () (.plain P) (.trig R R'))) ∧
      ¬ M.qdef (.plain P) (.trig R R') C ∧
      ¬ (∃ p, ∀ w, C w → cnt M.n (M.pstat (.plain P) w) = p) := by
  refine ⟨fun _ => True,
    fun w d => decide (d < (if w = 0 then 2 else 4)),
    fun w d => if w = 0 then decide (d = 0) else decide (d < 4),
    fun w d => if w = 1 then decide (d < 4) else if w = 2 then false else true,
    lt3Model_expressive _ _, ?_, ?_, ?_, ?_⟩
  · intro π l hπ _
    obtain ⟨rfl, rfl⟩ := Sys.plug_leaf_eq hπ
    refine ⟨.hole, rfl, ⟨1, trivial, ?_⟩, ⟨2, trivial, ?_⟩⟩ <;>
      simp [Ctx.plug, Sys.eval, evalF, sys, QModel.qsem, lt3Model, QModel.pstat, cnt] <;> decide
  · apply transp_lt3
    intro w _
    revert w; decide
  · rintro ⟨-, h2⟩
    have := h2 0 trivial 1 (by decide) (by decide)
    revert this; decide
  · rintro ⟨p, hp⟩
    have e := (hp 0 trivial).trans (hp 1 trivial).symm
    revert e; decide

/-! ### Section 6, point 5: the soccer example (34) -/

/-- Paper (34): worlds `false` (team A wins) and `true` (team B wins); six individuals:
`0..3` Frenchmen of team A, `4, 5` Frenchmen of team B.  `P` = Frenchman of the winning team,
`R` = has decided to retire (all of A; only `4` of B), `Q` = less than three.
Transparency holds although Heim predicts a presupposition failure (in `true`, Frenchman `5` has
not decided to retire). -/
theorem soccer_example :
    ∃ (P R R' : Bool → Nat → Bool),
      let M := lt3Model Bool 6
      M.Expressive ∧
      (sys M).Transp (fun _ => True) (.leaf (.quant () (.plain P) (.trig R R'))) ∧
      ¬ M.qdef (.plain P) (.trig R R') (fun _ => True) := by
  refine ⟨fun w d => if w = false then decide (d < 4) else decide (4 ≤ d ∧ d < 6),
    fun w d => if w = false then decide (d < 4) else decide (d = 4),
    fun _ _ => true, lt3Model_expressive _ _, ?_, ?_⟩
  · apply transp_lt3
    intro w _
    revert w; decide
  · rintro ⟨-, h2⟩
    have := h2 true trivial 5 (by decide) (by decide)
    revert this; decide


/-! ### Theorem 2 needs the expressiveness hypothesis (new) -/

/-- Two worlds (`false`, `true`), two individuals, three predicate letters
`0 = P`, `1 = P'`, `2 = R`, all with extension `⊆ {0}`; `Q = at least one`.
`P` holds only of individual `0` (so individual `1` violates the presupposition of the
restrictor), `R` holds of `0` in world `false` only. -/
def exprModel : QModel Bool Unit (Fin 3) Unit where
  val := fun _ _ => true
  I := fun k w d => if k = 2 then (!w && decide (d = 0)) else decide (d = 0)
  f := fun _ _ b => decide (1 ≤ b)
  n := 2
  i0 := ()

theorem exprModel_not_expressive : ¬ exprModel.Expressive := by
  intro h
  obtain ⟨m, hm⟩ := h (fun _ d => decide (d = 1))
  have h1 := hm false 1
  clear hm
  revert h1; revert m; decide

/-- **Theorem 2 as stated (hypotheses (i)-(iii) only) is false.**  In `exprModel` with
`C` = both worlds and `F = (Q P̲P' . R)`: the domain has constant size 2, the restrictor has
constant extension size 1, Non-Triviality holds, `F` satisfies Transparency (every *available*
predicate is included in `P`) although Heim's presupposition (`∀d P(d)`) fails. -/
theorem theorem2_needs_expressiveness :
    let M := exprModel
    let C : WSet Bool := fun _ => True
    let F : Fm (QLeaf Unit (Fin 3) Unit) := .leaf (.quant () (.trig 0 1) (.plain 2))
    ConstRestr M C F ∧ (sys M).NT IsQ C F ∧ ¬ M.Expressive ∧
      (sys M).Transp C F ∧ ¬ (sys M).Def F C := by
  intro M C F
  refine ⟨?_, ?_, exprModel_not_expressive, ?_, ?_⟩
  · intro l hl q P R hlq
    simp [F, Fm.leaves] at hl
    subst hl
    cases hlq
    exact ⟨1, by intro w _; cases w <;> decide⟩
  · intro π l hπ _
    obtain ⟨rfl, rfl⟩ := Sys.plug_leaf_eq hπ
    refine ⟨.hole, rfl, ⟨true, trivial, ?_⟩, ⟨false, trivial, ?_⟩⟩ <;>
      simp [Ctx.plug, Sys.eval, evalF, sys, QModel.qsem, M, exprModel, QModel.pstat, cnt] <;> decide
  · show (sys exprModel).Transp _ _
    rw [transp_quant]
    refine ⟨?_, (fun k j h => by cases h)⟩
    intro k j h
    cases h
    intro m Y w _
    rcases Y with a | ⟨a, b⟩ | ⟨a, b⟩
    · revert a m w; decide
    · revert a b m w; decide
    · revert a b m w; decide
  · intro h
    have := h.1 false trivial 1 (by decide)
    revert this; decide

end Quantified
end AntiDyn