import PropTheory
import KleeneCore
/-!
# Acceptability, comparison of theories (propositional fragment): items 26, 29, 32, 36-39

Main results proved here (all for the propositional fragment):
* Lemma 8, Lemma 11, Theorem 38a, Theorem 39a;
* Theorem 36 (Kleene-accept_i <-> Super-accept_i), and *more*: in the propositional fragment
  Transp_i <-> Kleene-accept_i <-> Super-accept_i <-> C[F] defined (so the converse of Theorem 38
  can only fail for quantificational sentences, cf. Quantifier.lean).
-/
namespace LCProp
variable {W : Type}

/-! ## definitions (items 26, 29) -/
/-- Incremental super-acceptability: for every trigger occurrence `α dd' β`, every good final `β'`
without triggers, every world of `C`, `Super(α dd' β') ≠ #`. -/
def SuperAccI (I : Nat → W → Bool) (C : W → Prop) (F : Form) : Prop :=
  ∀ t ∈ occs F, ∀ K', F2 Frame.sameTF t.1 K' → ∀ w, C w →
    Super I (plug K' (.trig t.2.1 t.2.2.1 t.2.2.2)) w ≠ none

def KleeneAccI (I : Nat → W → Bool) (C : W → Prop) (F : Form) : Prop :=
  ∀ t ∈ occs F, ∀ K', F2 Frame.sameTF t.1 K' → ∀ w, C w →
    Kleene I (plug K' (.trig t.2.1 t.2.2.1 t.2.2.2)) w ≠ none

/-- symmetric acceptability (26b/29b; the quantifier over triggers is vacuous/redundant) -/
def SuperAccS (I : Nat → W → Bool) (C : W → Prop) (F : Form) : Prop :=
  ∀ w, C w → Super I F w ≠ none
def KleeneAccS (I : Nat → W → Bool) (C : W → Prop) (F : Form) : Prop :=
  ∀ w, C w → Kleene I F w ≠ none

/-- "every trigger's presupposition holds throughout its incremental local context" -/
def LcCond (I : Nat → W → Bool) (C : W → Prop) (F : Form) : Prop :=
  ∀ t ∈ occs F, ∀ w, lcK I C t.1 w → I t.2.1 w = true

theorem transpI_iff_lcCond (I : Nat → W → Bool) (C : W → Prop) (F : Form) :
    TranspI I C F ↔ LcCond I C F :=
  ⟨fun H t ht => (local_iff I C t.1 t.2.1).mp (H t ht),
   fun H t ht => (local_iff I C t.1 t.2.1).mpr (H t ht)⟩

/-! ## small syntactic lemmas -/
theorem occs_bin_forall (o : Bop) (F G : Form) (P : List Frame × Nat × Nat × Nat → Prop) :
    (∀ t ∈ occs (Form.bin o F G), P t) ↔
      ((∀ t ∈ occs F, P (Frame.left o G :: t.1, t.2)) ∧
       (∀ t ∈ occs G, P (Frame.right o F :: t.1, t.2))) := by
  simp only [occs, List.mem_append, List.mem_map]
  constructor
  · intro h
    exact ⟨fun t ht => h _ (Or.inl ⟨t, ht, rfl⟩), fun t ht => h _ (Or.inr ⟨t, ht, rfl⟩)⟩
  · rintro ⟨h1, h2⟩ t (⟨u, hu, rfl⟩ | ⟨u, hu, rfl⟩)
    · exact h1 u hu
    · exact h2 u hu

theorem occs_neg_forall (F : Form) (P : List Frame × Nat × Nat × Nat → Prop) :
    (∀ t ∈ occs (Form.neg F), P t) ↔ (∀ t ∈ occs F, P (Frame.neg :: t.1, t.2)) := by
  simp only [occs, List.mem_map]
  constructor
  · intro h t ht; exact h _ ⟨t, ht, rfl⟩
  · rintro h t ⟨u, hu, rfl⟩; exact h u hu

theorem lcCond_neg (I : Nat → W → Bool) (C : W → Prop) (F : Form) :
    LcCond I C (.neg F) ↔ LcCond I C F := by
  unfold LcCond
  rw [occs_neg_forall]
  exact Iff.rfl

theorem lcCond_bin (I : Nat → W → Bool) (C : W → Prop) (o : Bop) (F G : Form) :
    LcCond I C (.bin o F G) ↔ LcCond I C F ∧ LcCond I (Frame.step I C (.right o F)) G := by
  unfold LcCond
  rw [occs_bin_forall]
  exact Iff.rfl

theorem F2_cons_inv {α : Type} {R : α → α → Prop} {a : α} {l K' : List α}
    (h : F2 R (a :: l) K') : ∃ b l', K' = b :: l' ∧ R a b ∧ F2 R l l' := by
  cases h with
  | cons hr hl => exact ⟨_, _, rfl, hr, hl⟩

theorem F2_nil_inv {α : Type} {R : α → α → Prop} {K' : List α} (h : F2 R [] K') : K' = [] := by
  cases h; rfl

/-! ## table facts for standard Strong Kleene -/
theorem skop_some : ∀ (o : Bop) (a b : Bool), skop o (some a) (some b) = some (o.eval a b) := by
  intro o a b; cases o <;> cases a <;> cases b <;> rfl

theorem skop_need : ∀ (o : Bop) (Y : Option Bool), skop o (some o.need) Y = Y := by
  intro o Y; cases o <;> rcases Y with _ | (_ | _) <;> rfl

theorem skop_const : ∀ (o : Bop) (e : Bool) (Y : Option Bool) (b : Bool), e ≠ o.need →
    skop o (some e) Y = some (o.eval e b) := by
  intro o e Y b h
  cases o <;> cases e <;> rcases Y with _ | (_ | _) <;> cases b <;> simp_all [Bop.need, skop, Bop.eval]

theorem sk_tf (I : Nat → W → Bool) : ∀ (F : Form), F.trigFree → ∀ w, sk I F w = some (ev I F w) := by
  intro F
  induction F with
  | atom a => intro _ w; rfl
  | trig a b k => intro h; exact absurd h id
  | neg F ih => intro h w; simp [sk, ev, ih h w]
  | bin o F G ihF ihG => intro h w; simp [sk, ev, ihF h.1 w, ihG h.2 w, skop_some]

/-- If every trigger is satisfied in its local context, Strong Kleene is defined and classical. -/
theorem lemmaY (I : Nat → W → Bool) : ∀ (F : Form) (C : W → Prop), LcCond I C F →
    ∀ w, C w → sk I F w = some (ev I F w) := by
  intro F
  induction F with
  | atom a => intro C _ w _; rfl
  | trig a b k =>
    intro C h w hw
    have := h ([], a, b, k) (by simp [occs]) w hw
    simp [sk, ev, this]
  | neg F ih =>
    intro C h w hw
    rw [lcCond_neg] at h
    simp [sk, ev, ih C h w hw]
  | bin o F G ihF ihG =>
    intro C h w hw
    rw [lcCond_bin] at h
    have h1 := ihF C h.1 w hw
    simp only [sk, ev]
    rw [h1]
    by_cases he : ev I F w = o.need
    · have h2 := ihG _ h.2 w ⟨hw, he⟩
      rw [h2, skop_some]
    · rw [skop_const o _ _ (ev I G w) he]

/-- **key lemma for Theorem 38a**: incremental local-context condition implies Kleene-acceptability
(stated with the standard definition `sk`). -/
theorem lcCond_sk_acc (I : Nat → W → Bool) : ∀ (F : Form) (C : W → Prop), LcCond I C F →
    ∀ t ∈ occs F, ∀ K', F2 Frame.sameTF t.1 K' → ∀ w, C w →
      sk I (plug K' (.trig t.2.1 t.2.2.1 t.2.2.2)) w ≠ none := by
  intro F
  induction F with
  | atom a => intro C _ t ht; simp [occs] at ht
  | trig a b k =>
    intro C h t ht K' hK w hw
    simp [occs] at ht; subst ht
    have hK' := F2_nil_inv hK; subst hK'
    have := h ([], a, b, k) (by simp [occs]) w hw
    simp [plug, sk, this]
  | neg F ih =>
    intro C h t ht K' hK w hw
    rw [lcCond_neg] at h
    simp only [occs, List.mem_map] at ht
    obtain ⟨u, hu, rfl⟩ := ht
    obtain ⟨f', K1, rfl, hf, hK1⟩ := F2_cons_inv hK
    rcases Frame.same_cases hf.1 with ⟨_, rfl⟩ | ⟨o, G, G', h1, _⟩ | ⟨o, F', h1, _⟩
    · have := ih C h u hu K1 hK1 w hw
      simp only [plug, Frame.fill, sk]
      intro hc
      apply this
      cases h' : sk I (plug K1 (.trig u.2.1 u.2.2.1 u.2.2.2)) w <;> simp_all
    · cases h1
    · cases h1
  | bin o F G ihF ihG =>
    intro C h t ht K' hK w hw
    rw [lcCond_bin] at h
    simp only [occs, List.mem_append, List.mem_map] at ht
    rcases ht with ⟨u, hu, rfl⟩ | ⟨u, hu, rfl⟩
    · obtain ⟨f', K1, rfl, hf, hK1⟩ := F2_cons_inv hK
      rcases Frame.same_cases hf.1 with ⟨h1, _⟩ | ⟨o', G0, G', h1, h2⟩ | ⟨o', F', h1, _⟩
      · cases h1
      · cases h1
        subst h2
        have htf : G'.trigFree := hf.2
        have := ihF C h.1 u hu K1 hK1 w hw
        simp only [plug, Frame.fill, sk]
        rw [sk_tf I G' htf w]
        cases hs : sk I (plug K1 (.trig u.2.1 u.2.2.1 u.2.2.2)) w with
        | none => exact absurd hs this
        | some x => rw [skop_some]; simp
      · cases h1
    · obtain ⟨f', K1, rfl, hf, hK1⟩ := F2_cons_inv hK
      rcases Frame.same_cases hf.1 with ⟨h1, _⟩ | ⟨o', G0, G', h1, h2⟩ | ⟨o', F', h1, h2⟩
      · cases h1
      · cases h1
      · cases h1
        subst h2
        have h1 := lemmaY I F C h.1 w hw
        simp only [plug, Frame.fill, sk]
        rw [h1]
        by_cases he : ev I F w = o.need
        · have := ihG _ h.2 u hu K1 hK1 w ⟨hw, he⟩
          rw [he, skop_need]
          exact this
        · rw [skop_const o _ _ true he]; simp

theorem lcCond_kleeneAccI (I : Nat → W → Bool) (C : W → Prop) (F : Form) (h : LcCond I C F) :
    KleeneAccI I C F := by
  intro t ht K' hK w hw
  rw [theorem41]
  exact lcCond_sk_acc I F C h t ht K' hK w hw

/-! ## super-facts for the converse -/
theorem det_of_inj {S T : Bool → Prop} (f : Bool → Bool) (hf : ∀ a b, f a = f b → a = b)
    (hT : ∀ v, T v ↔ ∃ v1, S v1 ∧ f v1 = v) : Det T ↔ Det S := by
  unfold Det
  rw [hT true, hT false]
  simp only [Bool.exists_bool]
  cases h1 : f true <;> cases h2 : f false
  · have := hf true false (by rw [h1, h2]); simp at this
  · by_cases a : S true <;> by_cases b : S false <;> simp [a, b, h1, h2]
  · by_cases a : S true <;> by_cases b : S false <;> simp [a, b, h1, h2]
  · have := hf true false (by rw [h1, h2]); simp at this

theorem evK_tf {K : Type} (I : Nat → W → Bool) (S : Scheme K) (ρ : K → W → Bool) :
    ∀ F : Form, F.trigFree → evK I S ρ F = ev I F := by
  intro F
  induction F with
  | atom a => intro _; rfl
  | trig a b k => intro h; exact absurd h id
  | neg F ih => intro h; funext w; simp [evK, ev, ih h]
  | bin o F G ihF ihG => intro h; funext w; simp [evK, ev, ihF h.1, ihG h.2]

theorem evK_nform {K : Type} (I : Nat → W → Bool) (S : Scheme K) (ρ : K → W → Bool) (o : Bop) (w : W) :
    evK I S ρ (nform o) w = o.neut := by
  rw [evK_tf I S ρ _ (nform_trigFree o), ev_nform]

theorem super_trig_ne (I : Nat → W → Bool) (a b k : Nat) (w : W) :
    Super I (.trig a b k) w ≠ none ↔ I a w = true := by
  unfold Super
  rw [valOpt_ne_none]
  unfold Det
  simp only [vk_trig]
  by_cases h : I a w = true
  · cases hb : I b w <;> simp [h, hb]
  · simp [h]

theorem super_neg_ne (I : Nat → W → Bool) (X : Form) (w : W) :
    Super I (.neg X) w ≠ none ↔ Super I X w ≠ none := by
  unfold Super
  rw [valOpt_ne_none, valOpt_ne_none]
  unfold Det
  simp only [vk_neg]
  by_cases a : VK I symS X w true <;> by_cases b : VK I symS X w false <;> simp [a, b]

/-- if `Z` is an injective function of `X` in every extension, they are equally (in)determinate -/
theorem super_ne_of (I : Nat → W → Bool) (Z X : Form) (w : W) (f : Bool → Bool)
    (hf : ∀ a b, f a = f b → a = b)
    (hev : ∀ ρ, AdmK I symS ρ → evK I symS ρ Z w = f (evK I symS ρ X w)) :
    Super I Z w ≠ none ↔ Super I X w ≠ none := by
  unfold Super
  rw [valOpt_ne_none, valOpt_ne_none]
  apply det_of_inj f hf
  intro v
  constructor
  · rintro ⟨ρ, hρ, h⟩; exact ⟨_, ⟨ρ, hρ, rfl⟩, by rw [← hev ρ hρ]; exact h⟩
  · rintro ⟨v1, ⟨ρ, hρ, rfl⟩, rfl⟩; exact ⟨ρ, hρ, hev ρ hρ⟩

theorem inj_neut (o : Bop) : ∀ a b, o.eval a o.neut = o.eval b o.neut → a = b := by
  intro a b; cases o <;> cases a <;> cases b <;> simp [Bop.eval, Bop.neut]

theorem inj_need (o : Bop) : ∀ a b, o.eval o.need a = o.eval o.need b → a = b := by
  intro a b; cases o <;> cases a <;> cases b <;> simp [Bop.eval, Bop.need]

/-- `Kleene`/`Super` of a formula whose triggers are all satisfied are classical -/
theorem super_of_lcCond (I : Nat → W → Bool) (C : W → Prop) (F : Form) (h : LcCond I C F)
    (w : W) (hw : C w) : Super I F w = some (ev I F w) := by
  have h1 : Kleene I F w = some (ev I F w) := by rw [theorem41, lemmaY I F C h w hw]
  rw [lemma7 I F w (by rw [h1]; simp), h1]

/-- **Converse direction**: super-acceptability forces the local-context condition. -/
theorem superAcc_lcCond (I : Nat → W → Bool) : ∀ (F : Form) (C : W → Prop), SuperAccI I C F →
    LcCond I C F := by
  intro F
  induction F with
  | atom a => intro C _ t ht; simp [occs] at ht
  | trig a b k =>
    intro C h t ht w hw
    simp [occs] at ht; subst ht
    have := h ([], a, b, k) (by simp [occs]) [] F2.nil w hw
    simp only [plug] at this
    exact (super_trig_ne I a b k w).mp this
  | neg F ih =>
    intro C h
    rw [lcCond_neg]
    apply ih
    intro t ht K1 hK1 w hw
    have := h (Frame.neg :: t.1, t.2) (by simp only [occs]; exact List.mem_map.mpr ⟨t, ht, rfl⟩)
      (Frame.neg :: K1) (F2.cons ⟨trivial, trivial⟩ hK1) w hw
    simp only [plug, Frame.fill] at this
    exact (super_neg_ne I _ w).mp this
  | bin o F G ihF ihG =>
    intro C h
    rw [lcCond_bin]
    -- (1) the first argument is super-acceptable
    have hF : SuperAccI I C F := by
      intro t ht K1 hK1 w hw
      have := h (Frame.left o G :: t.1, t.2)
        (by simp only [occs]; exact List.mem_append.mpr (Or.inl (List.mem_map.mpr ⟨t, ht, rfl⟩)))
        (Frame.left o (nform o) :: K1) (F2.cons ⟨rfl, nform_trigFree o⟩ hK1) w hw
      simp only [plug, Frame.fill] at this
      refine (super_ne_of I (.bin o _ (nform o)) _ w (fun b => o.eval b o.neut) (inj_neut o) ?_).mp this
      intro ρ _
      simp [evK, evK_nform]
    have hlc := ihF C hF
    refine ⟨hlc, ?_⟩
    apply ihG
    intro t ht K2 hK2 w hw
    have hwC : C w := hw.1
    have hev : ev I F w = o.need := hw.2
    have := h (Frame.right o F :: t.1, t.2)
      (by simp only [occs]; exact List.mem_append.mpr (Or.inr (List.mem_map.mpr ⟨t, ht, rfl⟩)))
      (Frame.right o F :: K2) (F2.cons ⟨⟨rfl, rfl⟩, trivial⟩ hK2) w hwC
    simp only [plug, Frame.fill] at this
    have hs := super_of_lcCond I C F hlc w hwC
    have hall := (super_eq_some_iff I F w _).mp hs
    refine (super_ne_of I (.bin o F _) _ w (fun b => o.eval o.need b) (inj_need o) ?_).mp this
    intro ρ hρ
    simp only [evK]
    rw [hall ρ hρ, hev]

/-! ## Lemma 8, Theorem 36, Theorem 38a -/
/-- Lemma 8(i) (incremental) -/
theorem lemma8_i_super (I : Nat → W → Bool) (C : W → Prop) (F : Form) :
    KleeneAccI I C F → SuperAccI I C F := by
  intro h t ht K' hK w hw
  have := h t ht K' hK w hw
  rw [lemma7 I _ w this]; exact this

/-- Lemma 8(i) (symmetric) -/
theorem lemma8_s_super (I : Nat → W → Bool) (C : W → Prop) (F : Form) :
    KleeneAccS I C F → SuperAccS I C F := by
  intro h w hw
  have := h w hw
  rw [lemma7 I _ w this]; exact this

theorem superAccI_lcCond (I : Nat → W → Bool) (C : W → Prop) (F : Form) :
    SuperAccI I C F → LcCond I C F := superAcc_lcCond I F C

/-- Lemma 8(ii), symmetric -/
theorem lemma8_s_eq (I : Nat → W → Bool) (C : W → Prop) (F : Form) (h : KleeneAccS I C F) :
    ∀ w, C w → Kleene I F w = Super I F w :=
  fun w hw => (lemma7 I F w (h w hw)).symm

/-- `Kleene-accept_i ⇒ Kleene-accept_s` (used in the proof of Lemma 8(ii) for `v = i`). -/
theorem kleeneAccI_S (I : Nat → W → Bool) (C : W → Prop) (F : Form) :
    KleeneAccI I C F → KleeneAccS I C F := by
  intro h w hw
  have hl := superAcc_lcCond I F C (lemma8_i_super I C F h)
  rw [theorem41, lemmaY I F C hl w hw]; simp

/-- Lemma 8(ii), incremental -/
theorem lemma8_i_eq (I : Nat → W → Bool) (C : W → Prop) (F : Form) (h : KleeneAccI I C F) :
    ∀ w, C w → Kleene I F w = Super I F w :=
  lemma8_s_eq I C F (kleeneAccI_S I C F h)

/-- **Theorem 36** (propositional fragment): Kleene-accept_i ⇔ Super-accept_i, and the
values agree. -/
theorem theorem36 (I : Nat → W → Bool) (C : W → Prop) (F : Form) :
    (KleeneAccI I C F ↔ SuperAccI I C F) ∧
    (KleeneAccI I C F → ∀ w, C w → Kleene I F w = Super I F w) :=
  ⟨⟨lemma8_i_super I C F, fun h => lcCond_kleeneAccI I C F (superAcc_lcCond I F C h)⟩,
   lemma8_i_eq I C F⟩

/-- **Theorem 38a** (propositional fragment): `Transp_i ⇒ Kleene-accept_i` (and Super-accept_i). -/
theorem theorem38a (I : Nat → W → Bool) (C : W → Prop) (F : Form) :
    TranspI I C F → KleeneAccI I C F ∧ SuperAccI I C F := by
  intro h
  have h1 := lcCond_kleeneAccI I C F ((transpI_iff_lcCond I C F).mp h)
  exact ⟨h1, lemma8_i_super I C F h1⟩

/-- NEW (not in the paper): in the propositional fragment the converse of Theorem 38 also holds;
all four incremental notions coincide with Heim's dynamic definedness. -/
theorem prop_fragment_collapse (I : Nat → W → Bool) (C : W → Prop) (F : Form) :
    (TranspI I C F ↔ dyn I F C ≠ none) ∧ (KleeneAccI I C F ↔ TranspI I C F) ∧
    (SuperAccI I C F ↔ TranspI I C F) := by
  refine ⟨(theorem1 I C F).1, ⟨fun h => ?_, fun h => (theorem38a I C F h).1⟩,
    ⟨fun h => ?_, fun h => (theorem38a I C F h).2⟩⟩
  · exact (transpI_iff_lcCond I C F).mpr (superAcc_lcCond I F C (lemma8_i_super I C F h))
  · exact (transpI_iff_lcCond I C F).mpr (superAcc_lcCond I F C h)

/-! ## Lemma 11 -/
/-- `(pp' or (not pp'))` -/
def exF (a b : Nat) : Form := .bin .or (.trig a b 0) (.neg (.trig a b 0))

/-- Lemma 11, positive half: `(pp' or not pp')` is symmetrically super-acceptable everywhere. -/
theorem lemma11_super (I : Nat → W → Bool) (a b : Nat) (C : W → Prop) :
    SuperAccS I C (exF a b) := by
  intro w _
  have : Super I (exF a b) w = some true := by
    rw [super_eq_some_iff]
    intro ρ _
    simp only [exF, evK, Bop.eval]
    cases ρ (symS.κ a b 0) w <;> rfl
  rw [this]; simp

/-- Lemma 11, negative half: if `p` is false somewhere in `C` it is not Kleene-acceptable. -/
theorem lemma11_not_kleene (I : Nat → W → Bool) (a b : Nat) (C : W → Prop) (w : W)
    (hw : C w) (hp : I a w = false) : ¬ KleeneAccS I C (exF a b) := by
  intro h
  have := h w hw
  rw [theorem41] at this
  simp [exF, sk, hp, skop] at this

/-! ## Theorem 39a -/
def I39 : Nat → Bool → Bool
  | 0, w => w      -- p  (false at w1 = false, true at w2 = true)
  | 1, _ => true   -- p'
  | 2, w => w      -- q
  | _, _ => true   -- q'

/-- `(pp' and qq')` -/
def F39 : Form := .bin .and (.trig 0 1 0) (.trig 2 3 0)

theorem theorem39a :
    TranspS I39 (fun _ => True) F39 ∧ ¬ KleeneAccS I39 (fun _ => True) F39 ∧
    ¬ SuperAccS I39 (fun _ => True) F39 := by
  refine ⟨?_, ?_, ?_⟩
  · intro t ht γ w _
    simp only [F39, occs, List.mem_append, List.mem_map, List.mem_singleton] at ht
    rcases ht with ⟨u, hu, rfl⟩ | ⟨u, hu, rfl⟩
    · have hu' : u = ([], 0, 1, 0) := by simpa [occs] using hu
      subst hu'
      cases w <;> simp [plug, Frame.fill, ev, I39, Bop.eval]
    · have hu' : u = ([], 2, 3, 0) := by simpa [occs] using hu
      subst hu'
      cases w <;> simp [plug, Frame.fill, ev, I39, Bop.eval]
  · intro h
    have := h false trivial
    rw [theorem41] at this
    simp [F39, sk, I39, skop] at this
  · intro h
    have := h false trivial
    have hL : LinK symS F39 := by
      simp [F39, LinK, keys, symS]
    unfold SuperAccS at h
    rw [show Super I39 F39 false = Kleene I39 F39 false from lemma6 I39 F39 hL false,
      theorem41] at this
    simp [F39, sk, I39, skop] at this

end LCProp