import KleeneCore
/-!
# The formula `(No P . QQ')` : Theorem 38b and Theorem 39b

Fidelity: this is a *specialised* formalisation of the single quantificational sentence
`(No P . Q Q')` on a single world and a finite domain `Fin n`; the general quantificational
language L, its dynamic/Transparency/Supervaluation semantics are NOT formalised.  What is modelled:
* Item 2: generalized quantifier = tree of numbers `f a b` with
  `a = #{d : P d ∧ ¬ S d}`, `b = #{d : P d ∧ S d}`; `fNo a b = 1 iff b = 0`.
* Item 6 (dynamic): `C[(No P . QQ')] = #` iff some `d` with `P d` has `¬ Q d` (single world context).
* Item 8a (Transparency): the only good final of `(No P . _` is `)`, so incremental = symmetric;
  `γ` ranges over all predicates (Expressivity, item 3).
* Items 24-25/28 (Supervaluations/Kleene): `Q Q'` is a predicative trigger; an extension `ρ`
  satisfies `Q d → ρ d = Q' d` and is free elsewhere.  With a single occurrence of the trigger,
  Super and Kleene coincide (Lemma 6), so one definition serves for both.
-/
namespace LCQuant
open LCProp

abbrev Pred (n : Nat) := Fin n → Bool

def fNo (_a b : Nat) : Bool := decide (b = 0)
def fEvery (a _b : Nat) : Bool := decide (a = 0)

/-- tree-of-numbers quantifier with restrictor `P` and scope `S` (single world) -/
def quant {n : Nat} (f : Nat → Nat → Bool) (P S : Pred n) : Bool :=
  f ((List.finRange n).countP (fun d => P d && !S d)) ((List.finRange n).countP (fun d => P d && S d))

theorem countP_zero_iff {n : Nat} (p : Fin n → Bool) :
    (List.finRange n).countP p = 0 ↔ ∀ d, p d = false := by
  rw [List.countP_eq_zero]
  constructor
  · intro h d; have := h d (List.mem_finRange d); simpa using this
  · intro h d _; simp [h d]

theorem quantNo_iff {n : Nat} (P S : Pred n) :
    quant fNo P S = true ↔ ∀ d, ¬ (P d = true ∧ S d = true) := by
  simp only [quant, fNo, decide_eq_true_eq, countP_zero_iff]
  constructor
  · intro h d ⟨h1, h2⟩; have := h d; simp [h1, h2] at this
  · intro h d
    cases hp : P d <;> cases hs : S d <;> simp
    exact h d ⟨hp, hs⟩

/-- Dynamic semantics, item 6: `C[(No P . QQ')] ≠ #` for `C = {w}` -/
def dynDefined {n : Nat} (P Q : Pred n) : Prop := ∀ d, P d = true → Q d = true

/-- Transparency of the trigger `QQ'` in `(No P . _)` (items 8, 57; `β' = )` is the only good final) -/
def transNo {n : Nat} (P Q : Pred n) : Prop :=
  ∀ γ : Pred n, quant fNo P (fun d => Q d && γ d) = quant fNo P γ

theorem transNo_iff {n : Nat} (P Q : Pred n) : transNo P Q ↔ dynDefined P Q := by
  constructor
  · intro H d hP
    refine Classical.byContradiction (fun hQ => ?_)
    have hQ' : Q d = false := by simpa using hQ
    have h := H (fun e => decide (e = d))
    have h1 : quant fNo P (fun e => Q e && decide (e = d)) = true := by
      rw [quantNo_iff]; intro e ⟨_, h2⟩
      simp at h2; obtain ⟨h3, h4⟩ := h2; subst h4; simp [hQ'] at h3
    rw [h1] at h
    have := (quantNo_iff P (fun e => decide (e = d))).mp h.symm d
    simp [hP] at this
  · intro H γ
    have : (fun d => P d && !(Q d && γ d)) = (fun d => P d && !γ d) := by
      funext d; by_cases hP : P d = true
      · simp [hP, H d hP]
      · simp [hP]
    have h2 : (fun d => P d && (Q d && γ d)) = (fun d => P d && γ d) := by
      funext d; by_cases hP : P d = true
      · simp [hP, H d hP]
      · simp [hP]
    simp only [quant, this, h2]

/-- extensions of the predicative trigger `QQ'` -/
def AdmP {n : Nat} (Q Q' : Pred n) (ρ : Pred n) : Prop := ∀ d, Q d = true → ρ d = Q' d

/-- values of `(No P . QQ')` over the extensions (Super = Kleene here: one trigger token) -/
def VP {n : Nat} (P Q Q' : Pred n) (v : Bool) : Prop := ∃ ρ, AdmP Q Q' ρ ∧ quant fNo P ρ = v

theorem kleeneNo_iff {n : Nat} (P Q Q' : Pred n) :
    Det (VP P Q Q') ↔ (∃ d, P d = true ∧ Q d = true ∧ Q' d = true) ∨ dynDefined P Q := by
  unfold Det
  constructor
  · intro h
    refine Classical.byContradiction (fun hne => ?_)
    have h1 : ¬ ∃ d, P d = true ∧ Q d = true ∧ Q' d = true := fun h' => hne (Or.inl h')
    have h2 : ¬ dynDefined P Q := fun h' => hne (Or.inr h')
    obtain ⟨d1, hd1P, hd1Q⟩ : ∃ d, P d = true ∧ Q d = false := by
      refine Classical.byContradiction (fun hh => h2 (fun d hP => ?_))
      by_cases hq : Q d = true
      · exact hq
      · exact absurd ⟨d, hP, by simpa using hq⟩ hh
    have t : VP P Q Q' true := by
      refine ⟨fun d => Q d && Q' d, fun d hq => by simp [hq], ?_⟩
      rw [quantNo_iff]; intro d ⟨hp, hq⟩
      simp at hq; exact h1 ⟨d, hp, hq.1, hq.2⟩
    have f : VP P Q Q' false := by
      refine ⟨fun d => if Q d then Q' d else true, fun d hq => by simp [hq], ?_⟩
      have : ¬ quant fNo P (fun d => if Q d then Q' d else true) = true := by
        rw [quantNo_iff]; intro hh; apply hh d1; simp [hd1P, hd1Q]
      simpa using this
    rcases h with ⟨_, h⟩ | ⟨_, h⟩
    · exact h f
    · exact h t
  · rintro (⟨d0, hP, hQ, hQ'⟩ | hd)
    · right
      have f : VP P Q Q' false := by
        refine ⟨fun d => Q d && Q' d, fun d hq => by simp [hq], ?_⟩
        have : ¬ quant fNo P (fun d => Q d && Q' d) = true := by
          rw [quantNo_iff]; intro hh; apply hh d0; simp [hP, hQ, hQ']
        simpa using this
      refine ⟨f, ?_⟩
      rintro ⟨ρ, hρ, hv⟩
      have : quant fNo P ρ = true := hv
      rw [quantNo_iff] at this
      exact this d0 ⟨hP, by rw [hρ d0 hQ]; exact hQ'⟩
    · -- all P are Q: the extension is determined on P
      obtain ⟨ρ0, h0, hv0⟩ : ∃ ρ, AdmP Q Q' ρ ∧ True :=
        ⟨fun d => Q d && Q' d, fun d hq => by simp [hq], trivial⟩
      have key : ∀ ρ ρ', AdmP Q Q' ρ → AdmP Q Q' ρ' → quant fNo P ρ = quant fNo P ρ' := by
        intro ρ ρ' h h'
        have : ∀ d, P d = true → ρ d = ρ' d := fun d hP => by rw [h d (hd d hP), h' d (hd d hP)]
        have e1 : (fun d => P d && !ρ d) = (fun d => P d && !ρ' d) := by
          funext d; by_cases hP : P d = true
          · simp [hP, this d hP]
          · simp [hP]
        have e2 : (fun d => P d && ρ d) = (fun d => P d && ρ' d) := by
          funext d; by_cases hP : P d = true
          · simp [hP, this d hP]
          · simp [hP]
        simp only [quant, e1, e2]
      cases hb : quant fNo P ρ0
      · right; refine ⟨⟨ρ0, h0, hb⟩, ?_⟩
        rintro ⟨ρ, hρ, hv⟩; rw [key ρ ρ0 hρ h0, hb] at hv; simp at hv
      · left; refine ⟨⟨ρ0, h0, hb⟩, ?_⟩
        rintro ⟨ρ, hρ, hv⟩; rw [key ρ ρ0 hρ h0, hb] at hv; simp at hv

/-! ## the countermodel of Theorem 38b / 39b : two P-individuals, d1 ¬Q, d2 Q and Q' -/
def P2 : Pred 2 := fun _ => true
def Q2 : Pred 2 := fun d => decide (d = 1)
def Q2' : Pred 2 := fun d => decide (d = 1)

theorem ex_dynamic_undefined : ¬ dynDefined P2 Q2 := by
  intro h; have := h 0 rfl; simp [Q2] at this

theorem ex_not_transparent : ¬ transNo P2 Q2 := fun h => ex_dynamic_undefined ((transNo_iff _ _).mp h)

theorem ex_kleene_acceptable : Det (VP P2 Q2 Q2') :=
  (kleeneNo_iff _ _ _).mpr (Or.inl ⟨1, rfl, by simp [Q2], by simp [Q2']⟩)

/-- more precisely the sentence is Kleene-false (and super-false) in the context (not `#`) -/
theorem ex_value_false : valOpt (VP P2 Q2 Q2') = some false := by
  rw [valOpt_eq_some]
  have h := (kleeneNo_iff P2 Q2 Q2').mpr (Or.inl ⟨1, rfl, by simp [Q2], by simp [Q2']⟩)
  refine ⟨⟨fun d => Q2 d && Q2' d, fun d hq => by simp [hq], ?_⟩, ?_⟩
  · have : ¬ quant fNo P2 (fun d => Q2 d && Q2' d) = true := by
      rw [quantNo_iff]; intro hh; apply hh 1; simp [P2, Q2, Q2']
    simpa using this
  · rintro ⟨ρ, hρ, hv⟩
    have : quant fNo P2 ρ = true := hv
    rw [quantNo_iff] at this
    exact this 1 ⟨rfl, by rw [hρ 1 (by simp [Q2])]; simp [Q2']⟩

/-- Theorem 38b / 39b: `(No P . QQ')` is Kleene- and Super-acceptable in the model but not
(incrementally or symmetrically) Transparent, nor dynamically defined. -/
theorem theorem38b_39b :
    Det (VP P2 Q2 Q2') ∧ ¬ transNo P2 Q2 ∧ ¬ dynDefined P2 Q2 :=
  ⟨ex_kleene_acceptable, ex_not_transparent, ex_dynamic_undefined⟩

end LCQuant