import KleeneTheory
/-!
# Additions (not in the paper): comparison of the symmetric theories, propositional fragment

* `kleeneAccS_transpS` : symmetric Kleene-acceptability implies symmetric Transparency.
* `exF_superAccS_not_transpS` : symmetric Super-acceptability does not (the sentence of Lemma 11).
* `and_p_separation` : `(pp' and p)` is symmetrically Kleene/Super/Transparent but not incrementally.
-/
namespace LCProp
variable {W : Type}

/-- a defined standard-Kleene value is the classical value -/
theorem sk_ev (I : Nat → W → Bool) (w : W) : ∀ (G : Form) (e : Bool), sk I G w = some e →
    ev I G w = e := by
  intro G
  induction G with
  | atom a => intro e h; simp [sk] at h; simp [ev, h]
  | trig a b k =>
    intro e h
    by_cases ha : I a w = true
    · simp [sk, ha] at h; simp [ev, ha, h]
    · simp [sk, ha] at h
  | neg F ih =>
    intro e h
    cases hF : sk I F w with
    | none => simp [sk, hF] at h
    | some b =>
      simp [sk, hF] at h
      simp [ev, ih b hF, ← h]
  | bin o F G ihF ihG =>
    intro e h
    simp only [sk] at h
    cases o <;> rcases hx : sk I F w with _ | (_ | _) <;> rcases hy : sk I G w with _ | (_ | _) <;>
      simp_all [skop, ev, Bop.eval]

/-- if a hole with undefined value sits in a context whose value is defined, the context is constant
in the hole -/
theorem sk_plug_const (I : Nat → W → Bool) (w : W) (X : Form) (hX : sk I X w = none) :
    ∀ K : List Frame, sk I (plug K X) w ≠ none → ∀ b1 b2, applyK I w K b1 = applyK I w K b2 := by
  intro K
  induction K with
  | nil => intro h; simp [plug, hX] at h
  | cons f K ih =>
    intro h b1 b2
    cases hY : sk I (plug K X) w with
    | some v =>
      have := ih (by simp [hY]) b1 b2
      simp only [applyK, this]
    | none =>
      cases f with
      | neg => simp [plug, Frame.fill, sk, hY] at h
      | left o G =>
        simp only [plug, Frame.fill, sk, hY] at h
        cases hG : sk I G w with
        | none => cases o <;> simp [skop, hG] at h
        | some e =>
          have hev := sk_ev I w G e hG
          cases o <;> cases e <;> simp_all [skop, applyK, Frame.fn, Bop.eval]
      | right o F =>
        simp only [plug, Frame.fill, sk, hY] at h
        cases hG : sk I F w with
        | none => cases o <;> simp [skop, hG] at h
        | some e =>
          have hev := sk_ev I w F e hG
          cases o <;> cases e <;> simp_all [skop, applyK, Frame.fn, Bop.eval]

/-- **A1.** Propositional fragment: `Kleene-acc_s(C,F)` implies `Transp_s(C,F)`. -/
theorem kleeneAccS_transpS (I : Nat → W → Bool) (C : W → Prop) (F : Form) :
    KleeneAccS I C F → TranspS I C F := by
  intro h t ht γ w hw
  have hF := occs_plug F t ht
  have hk := h w hw
  rw [theorem41, ← hF] at hk
  rw [ev_plug, ev_plug]
  by_cases ha : I t.2.1 w = true
  · simp [ev, ha, Bop.eval]
  · have hs : sk I (.trig t.2.1 t.2.2.1 t.2.2.2) w = none := by simp [sk, ha]
    exact sk_plug_const I w _ hs t.1 hk _ _

/-- **A2.** `(pp' or not pp')` is symmetrically super-acceptable in every `C` but, if `p` fails at a
world of `C`, not symmetrically transparent. -/
theorem exF_superAccS_not_transpS (I : Nat → W → Bool) (a b : Nat) (C : W → Prop) (w : W)
    (hw : C w) (hp : I a w = false) : SuperAccS I C (exF a b) ∧ ¬ TranspS I C (exF a b) := by
  refine ⟨lemma11_super I a b C, fun h => ?_⟩
  have := h ([Frame.right .or (.trig a b 0), Frame.neg], a, b, 0)
    (by simp [exF, occs]) Form.tt w hw
  simp [plug, Frame.fill, ev, ev_tt, hp, Bop.eval] at this

/-- `(pp' and p)` -/
def andP (a b : Nat) : Form := .bin .and (.trig a b 0) (.atom a)

/-- **A3.** `(pp' and p)` is symmetrically Kleene-, Super-acceptable and Transparent in every `C`,
but incrementally not, as soon as `p` fails somewhere in `C`. -/
theorem andP_separation (I : Nat → W → Bool) (a b : Nat) (C : W → Prop) (w : W)
    (hw : C w) (hp : I a w = false) :
    (KleeneAccS I C (andP a b) ∧ SuperAccS I C (andP a b) ∧ TranspS I C (andP a b)) ∧
    (¬ TranspI I C (andP a b) ∧ ¬ KleeneAccI I C (andP a b) ∧ ¬ SuperAccI I C (andP a b)) := by
  have hK : KleeneAccS I C (andP a b) := by
    intro v _
    rw [theorem41]
    by_cases ha : I a v = true
    · cases hb : I b v <;> simp [andP, sk, ha, hb, skop]
    · simp [andP, sk, ha, skop]
  have hT : ¬ TranspI I C (andP a b) := by
    intro h
    have := h ([Frame.left .and (.atom a)], a, b, 0) (by simp [andP, occs])
      [Frame.left .and Form.tt] (F2.cons (by simp [Frame.same]) F2.nil) Form.tt w hw
    simp [plug, Frame.fill, ev, ev_tt, hp, Bop.eval] at this
  refine ⟨⟨hK, lemma8_s_super I C _ hK, kleeneAccS_transpS I C _ hK⟩, hT, ?_, ?_⟩
  · exact fun h => hT ((prop_fragment_collapse I C _).2.1.mp h)
  · exact fun h => hT ((prop_fragment_collapse I C _).2.2.mp h)

end LCProp