import AntiDynamics.Lemma1

/-!
# Theorem 2 (Section 5.3), with the hypotheses it really needs

* `nt_corollary_i/ii` : the Non-Triviality Corollary (29).
* `quant_leaf` : Lemma 1 for a quantificational clause under NT and Constancy.
* `theorem2` : for every pair accessed by `⟨C, F⟩`, `Transp ↔ Def` and `C'[F'] = {w ∈ C' : w ⊨ F'}`.

**Correction to the statement.**  The paper's Theorem 2 lists three hypotheses
(constant domain size, constant restrictor size, Non-Triviality).  The proof of Lemma 1, which
Theorem 2 invokes, also uses hypothesis (b) of Lemma 1: *every property of individuals is
expressed by some predicate* (`Expressive`).  Without it Theorem 2 is false: see
`Counterexamples.lean`.  Here `hexp` is an explicit hypothesis.
-/

namespace AntiDyn

/-- All leaves occurring in a formula. -/
def Fm.leaves {L : Type} : Fm L → List L
  | .leaf l => [l]
  | .neg F => F.leaves
  | .conj F G => F.leaves ++ G.leaves
  | .disj F G => F.leaves ++ G.leaves
  | .cond F G => F.leaves ++ G.leaves

/-- Accessed pairs only shrink the context set and pass to subformulas. -/
theorem Accessed.sub {W L : Type} {S : Sys W L} {C₀ : WSet W} {F₀ : Fm L} {C : WSet W}
    {F : Fm L} (h : Accessed S C₀ F₀ C F) :
    (∀ w, C w → C₀ w) ∧ ∀ l, l ∈ F.leaves → l ∈ F₀.leaves := by
  induction h with
  | refl => exact ⟨fun _ h => h, fun _ h => h⟩
  | neg _ ih => exact ⟨ih.1, fun l hl => ih.2 l (by simpa [Fm.leaves] using hl)⟩
  | conjL _ ih => exact ⟨ih.1, fun l hl => ih.2 l (by simp [Fm.leaves, hl])⟩
  | disjL _ ih => exact ⟨ih.1, fun l hl => ih.2 l (by simp [Fm.leaves, hl])⟩
  | condL _ ih => exact ⟨ih.1, fun l hl => ih.2 l (by simp [Fm.leaves, hl])⟩
  | @conjR C G H _ hd ih =>
    refine ⟨fun w hw => ih.1 w ?_, fun l hl => ih.2 l (by simp [Fm.leaves, hl])⟩
    rw [S.upd_eq_TS G C hd] at hw; exact hw.1
  | @condR C G H _ hd ih =>
    refine ⟨fun w hw => ih.1 w ?_, fun l hl => ih.2 l (by simp [Fm.leaves, hl])⟩
    rw [S.upd_eq_TS G C hd] at hw; exact hw.1
  | @disjR C G H _ hd ih =>
    exact ⟨fun w hw => ih.1 w hw.1, fun l hl => ih.2 l (by simp [Fm.leaves, hl])⟩

namespace Quantified

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

/-- The quantificational clauses. -/
def IsQ : QLeaf ι ρ κ → Prop
  | .quant _ _ _ => True
  | _ => False

/-- Non-Triviality at a bare clause: `A` is true somewhere and false somewhere in `C`. -/
theorem nt_leaf_values {C : WSet W} {q : κ} {P R : Pred ρ}
    (h : (sys M).NT IsQ C (.leaf (.quant q P R))) :
    ∃ w₁ w₂, C w₁ ∧ C w₂ ∧ M.qsem q P R w₁ = false ∧ M.qsem q P R w₂ = true := by
  obtain ⟨π', hc, ⟨w₁, hw₁, h₁⟩, ⟨w₂, hw₂, h₂⟩⟩ :=
    h .hole _ rfl (by trivial)
  simp only [Compl] at hc
  subst hc
  refine ⟨w₁, w₂, hw₁, hw₂, ?_, ?_⟩
  · simp only [Ctx.plug, eval_quant] at h₁
    rw [(sys M).top_true] at h₁
    cases hh : M.qsem q P R w₁ <;> simp_all
  · simp only [Ctx.plug, eval_quant] at h₂
    rw [(sys M).bot_false] at h₂
    cases hh : M.qsem q P R w₂ <;> simp_all

theorem qsem_args_le (P R : Pred ρ) (w : 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) = cnt M.n (M.pstat P w) := by
  have := cnt_split M.n (M.pstat P w) (M.pstat R w)
  omega

/-- **Non-Triviality Corollary (29)(i)**: if `⟨C, (Q P . R)⟩` satisfies Non-Triviality (and
the domain has constant size `n`, which is built into the model), then `f_Q` is not constant
on `{(a, b) : a + b ≤ n}`. -/
theorem nt_corollary_i {C : WSet W} {q : κ} {P R : Pred ρ}
    (h : (sys M).NT IsQ C (.leaf (.quant q P R))) :
    ∃ a b a' b', a + b ≤ M.n ∧ a' + b' ≤ M.n ∧ M.f q a b ≠ M.f q a' b' := by
  obtain ⟨w₁, w₂, -, -, h1, h2⟩ := nt_leaf_values M h
  refine ⟨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),
    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), ?_, ?_, ?_⟩
  · rw [qsem_args_le M P R w₁]; exact cnt_le _ _
  · rw [qsem_args_le M P R w₂]; exact cnt_le _ _
  · simp only [QModel.qsem] at h1 h2
    rw [h1, h2]; simp

/-- **Non-Triviality Corollary (29)(ii)**: if moreover the extension of the restrictor has
constant size `p` over `C`, then `f_Q` is not constant on `{(a, b) : a + b = p}`
(here in the form used by `lemma1_ii`). -/
theorem nt_corollary_ii {C : WSet W} {q : κ} {P R : Pred ρ} {p : Nat}
    (h : (sys M).NT IsQ C (.leaf (.quant q P R))) (hp : ∀ w, C w → cnt M.n (M.pstat P w) = p) :
    ∃ b₁ b₂, b₁ ≤ p ∧ b₂ ≤ p ∧ M.f q (p - b₁) b₁ ≠ M.f q (p - b₂) b₂ := by
  obtain ⟨w₁, w₂, hw₁, hw₂, h1, h2⟩ := nt_leaf_values M h
  have e1 := qsem_args_le M P R w₁
  have e2 := qsem_args_le M P R w₂
  rw [hp w₁ hw₁] at e1
  rw [hp w₂ hw₂] at e2
  refine ⟨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, by omega, ?_⟩
  simp only [QModel.qsem] at h1 h2
  have a1 : p - 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
  have a2 : p - 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 [a1, a2, h1, h2]
  simp

/-- Lemma 1 for a whole clause `(Q P . R)` under Non-Triviality and Constancy:
`Transp` holds iff Heim's definedness condition holds. -/
theorem quant_leaf (hexp : M.Expressive) (C : WSet W) (q : κ) (P R : Pred ρ)
    (hNT : (sys M).NT IsQ C (.leaf (.quant q P R)))
    (hconst : ∃ p, ∀ w, C w → cnt M.n (M.pstat P w) = p) :
    (sys M).Transp C (.leaf (.quant q P R)) ↔ M.qdef P R C := by
  obtain ⟨p, hp⟩ := hconst
  have htri := nt_corollary_i M hNT
  have hline := nt_corollary_ii M hNT hp
  rw [transp_quant]
  constructor
  · rintro ⟨h1, h2⟩
    refine ⟨?_, ?_⟩
    · intro w hw d hd
      cases P with
      | plain k => rfl
      | conj k j => rfl
      | trig k j => exact (lemma1_i M hexp C q k htri).1 (h1 k j rfl) w hw d hd
    · intro w hw d hd hPd
      cases R with
      | plain k => rfl
      | conj k j => rfl
      | trig k j => exact (lemma1_ii M hexp C q k P p hp hline).1 (h2 k j rfl) w hw d hd hPd
  · rintro ⟨d1, d2⟩
    refine ⟨?_, ?_⟩
    · rintro k j rfl
      exact (lemma1_i M hexp C q k htri).2 (fun w hw d hd => d1 w hw d hd)
    · rintro k j rfl
      exact (lemma1_ii M hexp C q k P p hp hline).2 (fun w hw d hd hPd => d2 w hw d hd hPd)

/-- The hypothesis (ii) of Theorem 2: every restrictor in `F` has an extension of constant
size over `C`. -/
def ConstRestr (C : WSet W) (F : Fm (QLeaf ι ρ κ)) : Prop :=
  ∀ l, l ∈ F.leaves → ∀ q P R, l = .quant q P R → ∃ p, ∀ w, C w → cnt M.n (M.pstat P w) = p

/-- **Theorem 2** (with the expressiveness hypothesis (b) made explicit).
Let `C` be a context set and `F` a formula.  Suppose (i) the domain has constant finite size
(built into `M`), (ii) each restrictor in `F` has constant size over `C`, (iii) `⟨C, F⟩` satisfies
Non-Triviality, and (iv) every property is expressible.  Then for every `⟨C', F'⟩` accessed by
`⟨C, F⟩`: (i) `Transp(C', F') ↔ C'[F'] ≠ #`; (ii) if `C'[F'] ≠ #` then
`C'[F'] = {w ∈ C' : w ⊨ F'}`. -/
theorem 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') := 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
  have hNT' := (sys M).lemma2 hNT hl
  obtain ⟨hsub, hleaf⟩ := hl.sub
  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 hc : ∃ p, ∀ w, C'' w → cnt M.n (M.pstat P w) = p := by
      obtain ⟨p, hp⟩ := hconst _ (hleaf _ (by simp [Fm.leaves])) q P R rfl
      exact ⟨p, fun w hw => hp w (hsub w hw)⟩
    have := quant_leaf M hexp C'' q P R hNT' hc
    rw [Sys.transp_leaf] at this
    exact this


/-! ### Heim's claims for generalized quantifiers (Section 5, first paragraph) -/

/-- (i) `(Q P̲P' . R)` presupposes that every individual satisfies `P`. -/
theorem heim_claim_i (k j : ρ) (R : Pred ρ) (C : WSet W) :
    M.qdef (.trig k j) R C ↔ (∀ w, C w → ∀ d, d < M.n → M.I k w d = true) ∧
      (∀ w, C w → ∀ d, d < M.n → M.pstat (.trig k j) w d = true → M.ppre R w d = true) := by
  simp [QModel.qdef, QModel.ppre]

/-- (ii) `(Q P . R̲R')` presupposes that every individual satisfying `P` satisfies `R`. -/
theorem heim_claim_ii (P : Pred ρ) (k j : ρ) (C : WSet W) (hP : ∀ w d, M.ppre P w d = true) :
    M.qdef P (.trig k j) C ↔ ∀ w, C w → ∀ d, d < M.n → M.pstat P w d = true → M.I k w d = true := by
  constructor
  · rintro ⟨-, h⟩; exact h
  · intro h
    exact ⟨fun w _ d _ => hP w d, h⟩

/-- With a presuppositional restrictor `P̲P'`, the scope presupposition is
`∀d [(P ∧ P')(d) ⇒ R(d)]` (static restrictor), *not* `∀d [P(d) ⇒ R(d)]` with `P` the
presupposition alone (see RESULTS.md, issue Q5). -/
theorem qdef_both (k j k' j' : ρ) (C : WSet W) :
    M.qdef (.trig k j) (.trig k' j') C ↔
      (∀ w, C w → ∀ d, d < M.n → M.I k w d = true) ∧
      (∀ w, C w → ∀ d, d < M.n → (M.I k w d && M.I j w d) = true → M.I k' w d = true) := by
  simp [QModel.qdef, QModel.ppre, QModel.pstat]


/-! ### Dynamic Transparency (23) for the quantified fragment -/

/-- Delete the underlined material of a predicate: `P̲_k P'_j ↦ P'_j`. -/
def starP : Pred ρ → Pred ρ
  | .trig _ j => .plain j
  | P => P

/-- `F ↦ F*` on leaves. -/
def starL : QLeaf ι ρ κ → QLeaf ι ρ κ
  | .atom i => .atom i
  | .trig _ b => .atom b
  | .quant q P R => .quant q (starP P) (starP R)

theorem passert_starP (P : Pred ρ) (w : W) (d : Nat) :
    M.passert (starP P) w d = M.passert P w d := by cases P <;> rfl

theorem ppre_starP (P : Pred ρ) (w : W) (d : Nat) : M.ppre (starP P) w d = true := by
  cases P <;> rfl

/-- **Dynamic Transparency (23)** for the language with quantifiers: `C[F] ≠ #` implies
`C[F] = C[F*]`, and `F*` is always defined. -/
theorem dynamic_transparency_quant (C : WSet W) (F : Fm (QLeaf ι ρ κ))
    (h : (sys M).Def F C) : (sys M).Upd (F.map starL) C = (sys M).Upd F C ∧
      (sys M).Def (F.map starL) C := by
  refine ⟨Sys.dyn_transparency _ starL ?_ F C h, Sys.def_map _ starL ?_ F C⟩
  · intro l C' _
    cases l with
    | atom i => rfl
    | trig a b => rfl
    | quant q P R =>
      show M.qupd q (starP P) (starP R) C' = M.qupd q P R C'
      funext w
      simp only [QModel.qupd, passert_starP]
  · intro l C'
    cases l with
    | atom i => trivial
    | trig a b => trivial
    | quant q P R =>
      exact ⟨fun w _ d _ => ppre_starP M P w d, fun w _ d _ _ => ppre_starP M R w d⟩

end Quantified
end AntiDyn