import AntiDynamics.Lifting

/-!
# The propositional case: Theorem 1

* Language (18): atomic propositions `p_i` and `p̲_a p'_b` (presupposition `a`, assertion `b`),
  closed under `not`, `and`, `or`, `if`.
* Heim's dynamic semantics (21) (with Beaver's `or`): `Sys.Upd`, `Sys.Def` of `Core.lean`.
* Static semantics (25): a clause `p̲_a p'_b` is the conjunction `a ∧ b`.
* Transparency (26): `Sys.Transp` of `Core.lean` (initial strings ↔ contexts; see
  `Strings.lean` for the bridge to literal strings).
* **Theorem 1** (`theorem1_i`, `theorem1_ii`), Transparency Lemma (27) (`transparency_lemma_a/b`).
* Worked derivations (14)-(17), the discussion of (10)-(13), Dynamic Transparency (23).
-/

namespace AntiDyn
namespace Propositional

/-- Atomic propositional clauses over propositional letters `ι`:
`atom i` is `p_i`;  `trig a b` is `p̲_a p'_b` (presupposition `p_a`, assertive component `p_b`). -/
inductive PLeaf (ι : Type) where
  | atom : ι → PLeaf ι
  | trig : ι → ι → PLeaf ι

abbrev PFm (ι : Type) := Fm (PLeaf ι)

variable {W ι : Type}

/-- `p_i` -/
def at_ (i : ι) : PFm ι := .leaf (.atom i)
/-- `p̲_a p'_b` -/
def tr_ (a b : ι) : PFm ι := .leaf (.trig a b)

/-- The model: `v w i` is the truth value of `p_i` at `w`; `i0` is a letter used to build
the tautology `p ∨ ¬p` and the contradiction `p ∧ ¬p` that the paper assumes are in the
language. -/
def sys (v : W → ι → Bool) (i0 : ι) : Sys W (PLeaf ι) where
  sem := fun l w => match l with
    | .atom i => v w i
    | .trig a b => v w a && v w b
  lupd := fun l C => match l with
    | .atom i => fun w => C w ∧ v w i = true
    | .trig _ b => fun w => C w ∧ v w b = true
  ldef := fun l C => match l with
    | .atom _ => True
    | .trig a _ => ∀ w, C w → v w a = true
  lvar := fun l φ₁ φ₂ => match l with
    | .atom _ => False
    | .trig a _ => ∃ γ, φ₁ = .conj (at_ a) γ ∧ φ₂ = γ
  top := .disj (at_ i0) (.neg (at_ i0))
  bot := .conj (at_ i0) (.neg (at_ i0))
  top_ok := by intro w; simp [evalF, at_]
  bot_ok := by intro w; simp [evalF, at_]
  lupd_static := by
    intro l C h
    cases l with
    | atom i => rfl
    | trig a b =>
      funext w; apply propext
      simp only
      constructor
      · rintro ⟨hc, hb⟩; exact ⟨hc, by simp [h w hc, hb]⟩
      · rintro ⟨hc, hb⟩
        have hb' : (v w a && v w b) = true := hb
        simp at hb'
        exact ⟨hc, hb'.2⟩

variable (v : W → ι → Bool) (i0 : ι)

@[simp] theorem eval_at (i : ι) (w : W) : (sys v i0).eval (at_ i) w = v w i := rfl
@[simp] theorem eval_tr (a b : ι) (w : W) : (sys v i0).eval (tr_ a b) w = (v w a && v w b) := rfl

/-- Leaf case of Theorem 1, cases (a) and (b) of the paper's proof:
`p` is always transparent; `p̲p'` is transparent iff `C ⊨ p`. -/
theorem leaf_transp_iff_def (C : WSet W) (l : PLeaf ι) :
    (sys v i0).Transp C (.leaf l) ↔ (sys v i0).ldef l C := by
  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 (at_ a) (sys v i0).top) (sys v i0).top ⟨(sys v i0).top, rfl, rfl⟩ w hw
      simpa [Sys.eval, evalF, at_, sys, (sys v i0).top_true] using this
    · rintro h φ₁ φ₂ ⟨γ, rfl, rfl⟩ w hw
      simp [Sys.eval, evalF, at_, h w hw]

/-- **Theorem 1 (i)**: for every formula `F` and every `C ⊆ W`,
`Transp(C, F)` iff `C[F] ≠ #`. -/
theorem theorem1_i (C : WSet W) (F : PFm ι) :
    (sys v i0).Transp C F ↔ (sys v i0).Def F C :=
  Sys.transp_iff_def _ (leaf_transp_iff_def v i0) F C

/-- **Theorem 1 (ii)**: if `C[F] ≠ #` then `C[F] = {w ∈ C : w ⊨ F}`. -/
theorem theorem1_ii (C : WSet W) (F : PFm ι) (h : (sys v i0).Def F C) :
    (sys v i0).Upd F C = (sys v i0).TS F C :=
  Sys.upd_eq_TS _ F C h

/-- **Transparency Lemma (27a)**: `Transp(C, (G and δ)) → Transp(C, G)`. -/
theorem transparency_lemma_a (C : WSet W) (G δ : PFm ι)
    (h : (sys v i0).Transp C (.conj G δ)) : (sys v i0).Transp C G :=
  ((Sys.transp_conj _ C G δ).1 h).1

/-- **Transparency Lemma (27b)**: `Transp(C, (if G . δ)) → Transp(C, G)`. -/
theorem transparency_lemma_b (C : WSet W) (G δ : PFm ι)
    (h : (sys v i0).Transp C (.cond G δ)) : (sys v i0).Transp C G :=
  ((Sys.transp_cond _ C G δ).1 h).1

/-! ### The inductive clauses used in the proof of Theorem 1, cases (c)-(f) -/

theorem caseC (C : WSet W) (G : PFm ι) :
    (sys v i0).Transp C (.neg G) ↔ (sys v i0).Transp C G := Sys.transp_neg _ C G
theorem caseD (C : WSet W) (G H : PFm ι) :
    (sys v i0).Transp C (.conj G H) ↔
      (sys v i0).Transp C G ∧ (sys v i0).Transp ((sys v i0).TS G C) H := Sys.transp_conj _ C G H
theorem caseE (C : WSet W) (G H : PFm ι) :
    (sys v i0).Transp C (.disj G H) ↔
      (sys v i0).Transp C G ∧ (sys v i0).Transp (fun w => C w ∧ (sys v i0).eval G w = false) H :=
  Sys.transp_disj _ C G H
theorem caseF (C : WSet W) (G H : PFm ι) :
    (sys v i0).Transp C (.cond G H) ↔
      (sys v i0).Transp C G ∧ (sys v i0).Transp ((sys v i0).TS G C) H := Sys.transp_cond _ C G H

/-! ## Section 2.3: the worked derivations (14)-(17)

The paper derives them by direct arguments with a tautology `γ` and a completion `β`.
Here they follow from the decomposition lemmas (which do not mention Heim's semantics). -/

/-- `C ⊨ p_a` -/
def Ent (C : WSet W) (a : ι) : Prop := ∀ w, C w → v w a = true
/-- `C ⊨ p_a ⇒ p_b` -/
def EntImp (C : WSet W) (a b : ι) : Prop := ∀ w, C w → v w a = true → v w b = true

theorem transp_atomic (C : WSet W) (a b : ι) :
    (sys v i0).Transp C (tr_ a b) ↔ Ent v C a := by
  have := leaf_transp_iff_def v i0 C (.trig a b)
  exact this

theorem transp_plain (C : WSet W) (i : ι) : (sys v i0).Transp C (at_ i) := by
  have := leaf_transp_iff_def v i0 C (.atom i)
  exact this.2 trivial

/-- (14): `(p̲p' and q)` presupposes `p`. -/
theorem ex14 (C : WSet W) (a b q : ι) :
    (sys v i0).Transp C (.conj (tr_ a b) (at_ q)) ↔ Ent v C a := by
  rw [caseD, transp_atomic]
  exact ⟨fun h => h.1, fun h => ⟨h, transp_plain v i0 _ q⟩⟩

/-- (15): `(p and q̲q')` presupposes `p ⇒ q`. -/
theorem ex15 (C : WSet W) (p a b : ι) :
    (sys v i0).Transp C (.conj (at_ p) (tr_ a b)) ↔ EntImp v C p a := by
  rw [caseD]
  constructor
  · rintro ⟨_, h⟩ w hw hp
    have := (transp_atomic v i0 _ a b).1 h w ⟨hw, by simpa using hp⟩
    exact this
  · intro h
    refine ⟨transp_plain v i0 _ p, (transp_atomic v i0 _ a b).2 ?_⟩
    rintro w ⟨hw, hp⟩
    exact h w hw (by simpa using hp)

/-- (16): `(if p̲p' . q)` presupposes `p`. -/
theorem ex16 (C : WSet W) (a b q : ι) :
    (sys v i0).Transp C (.cond (tr_ a b) (at_ q)) ↔ Ent v C a := by
  rw [caseF, transp_atomic]
  exact ⟨fun h => h.1, fun h => ⟨h, transp_plain v i0 _ q⟩⟩

/-- (17): `(if p . q̲q')` presupposes `p ⇒ q`. -/
theorem ex17 (C : WSet W) (p a b : ι) :
    (sys v i0).Transp C (.cond (at_ p) (tr_ a b)) ↔ EntImp v C p a := by
  rw [caseF]
  constructor
  · rintro ⟨_, h⟩ w hw hp
    exact (transp_atomic v i0 _ a b).1 h w ⟨hw, by simpa using hp⟩
  · intro h
    refine ⟨transp_plain v i0 _ p, (transp_atomic v i0 _ a b).2 ?_⟩
    rintro w ⟨hw, hp⟩
    exact h w hw (by simpa using hp)

/-! ## Section 2.2: why the naive requirement (10) does not suffice

`F*` deletes the underlined material.  The naive condition (10) is `C ⊨ F ⇔ F*`. -/

/-- `p̲_a p'_b ↦ p'_b` -/
def star1 : PLeaf ι → PLeaf ι
  | .atom i => .atom i
  | .trig _ b => .atom b

/-- `F*` -/
def star (F : PFm ι) : PFm ι := F.map star1

theorem star_tr (a b : ι) : star (tr_ a b) = at_ b := rfl

/-- (10): the naive requirement `C ⊨ F ⇔ F*`. -/
def Naive (C : WSet W) (F : PFm ι) : Prop := (sys v i0).CEquiv C F (star F)

/-- (11)-(12): for an atomic clause the naive requirement says only `C ⊨ p' ⇒ p`. -/
theorem naive_atomic (C : WSet W) (a b : ι) :
    Naive v i0 C (tr_ a b) ↔ EntImp v C b a := by
  unfold Naive Sys.CEquiv
  rw [star_tr]
  simp only [eval_tr, eval_at]
  constructor
  · intro h w hw hb
    have := h w hw
    cases ha : v w a <;> simp_all
  · intro h w hw
    cases hb : v w b
    · simp
    · simp [h w hw hb]

/-- The naive requirement is strictly weaker than Transparency already for atomic clauses:
a one-world countermodel (`p` false, `p'` false). -/
theorem naive_strictly_weaker :
    ∃ (C : WSet Unit) (v : Unit → Bool → Bool),
      Naive v true C (tr_ false true) ∧ ¬ (sys v true).Transp C (tr_ false true) := by
  refine ⟨fun _ => True, fun _ _ => false, ?_, ?_⟩
  · rw [naive_atomic]; intro w _ hb; simp at hb
  · rw [transp_atomic]; intro h; have := h () trivial; simp at this

/-- The remark after (10): the naive requirement is symmetric in the conjuncts, so it
cannot derive the asymmetry of `and`. -/
theorem naive_conj_symmetric (C : WSet W) (G H : PFm ι) :
    Naive v i0 C (.conj G H) ↔ Naive v i0 C (.conj H G) := by
  unfold Naive Sys.CEquiv
  constructor <;> intro h w hw <;> have := h w hw <;>
    simp only [star, Fm.map, Sys.eval_conj] at this ⊢ <;> grind

/-- Transparency is asymmetric for `and`: `(p and q̲q')` vs `(q̲q' and p)`. -/
theorem transp_conj_asymmetric :
    ∃ (C : WSet Bool) (v : Bool → Bool → Bool),
      (sys v true).Transp C (.conj (at_ true) (tr_ false false)) ∧
      ¬ (sys v true).Transp C (.conj (tr_ false false) (at_ true)) := by
  -- worlds `false`/`true`; `p_true` is true only at `true`; `p_false` (= q) is true only at `true`
  refine ⟨fun _ => True, fun w _ => w, ?_, ?_⟩
  · rw [ex15]; intro w _ hp; simpa using hp
  · rw [ex14]; intro h; have := h false trivial; simp at this

/-! ## Dynamic Transparency (8), (23) -/

/-- **Dynamic Transparency (23)**: if `C[F] ≠ #` then `C[F] = C[F*]`. -/
theorem dynamic_transparency (C : WSet W) (F : PFm ι) (h : (sys v i0).Def F C) :
    (sys v i0).Upd (star F) C = (sys v i0).Upd F C :=
  Sys.dyn_transparency _ star1 (by intro l C _; cases l <;> rfl) F C h

/-- `F*` is presupposition-free, hence always defined (so (23) is not vacuous). -/
theorem star_defined (C : WSet W) (F : PFm ι) : (sys v i0).Def (star F) C :=
  Sys.def_map _ star1 (by intro l C; cases l <;> simp [star1, sys]) F C

end Propositional
end AntiDyn