/-!
# Anti-Dynamics (Schlenker 2007): generic core

Formalization of the *connective structure* shared by the propositional case
(Theorem 1) and the quantificational case (Theorem 2).

* `Fm L`      : formulas built from *leaf clauses* `L` with `not`, `and`, `or`, `if`.
                (Leaves are the atomic clauses `p`, `p̲p'` in the propositional case,
                 and the quantificational clauses `(Q P . R)` in the quantified case.)
* `Sys W L`   : the data of a model: static truth of leaves (`sem`), Heim's
                leaf-level CCP (`lupd`) and definedness (`ldef`), and the leaf-level
                replacement pairs tested by Transparency (`lvar`).
* `Upd`/`Def` : Heim's dynamic semantics (paper (21)), with Beaver's `or`.
* `Ctx`/`Compl`/`Transp` : the Transparency theory.  A *context* `π` is a formula with a
                hole; `Compl π π'` says that `π'` is a *sentence completion* of the initial
                string that ends at the hole of `π` (see `Strings.lean` for the bridge
                to literal strings and the Syntactic Lemma).
* `lift`      : the inductive proof of Theorem 1/2 for the connective steps
                (paper cases (c)-(f)); the leaf steps are supplied by the instances.
* `NT`, `Acc`, `lemma2` : Non-Triviality, accessed pairs, and the paper's Lemma 2.
* `dyn_transparency` : Dynamic Transparency (23).

No `sorry`, no Mathlib: core Lean 4 only.
-/

namespace AntiDyn

/-- Formulas over leaf clauses `L`. -/
inductive Fm (L : Type) where
  | leaf : L → Fm L
  | neg  : Fm L → Fm L
  | conj : Fm L → Fm L → Fm L
  | disj : Fm L → Fm L → Fm L
  | cond : Fm L → Fm L → Fm L

/-- Context sets are predicates on worlds. -/
abbrev WSet (W : Type) := W → Prop

/-- Bivalent (static) semantics (paper (25)); `if` is material implication. -/
def evalF {W L : Type} (sem : L → W → Bool) : Fm L → W → Bool
  | .leaf l, w => sem l w
  | .neg F, w => !(evalF sem F w)
  | .conj F G, w => evalF sem F w && evalF sem G w
  | .disj F G, w => evalF sem F w || evalF sem G w
  | .cond F G, w => !(evalF sem F w) || evalF sem G w

/-- A model for the connective fragment over leaves `L`.

* `lupd`, `ldef` : Heim's CCP of a leaf clause (update, definedness).
* `lvar l φ₁ φ₂` : the pair `(φ₁, φ₂)` is one of the pairs that Transparency
  requires to be contextually equivalent when the leaf `l` occupies the hole
  (for a trigger `p̲p'`: `φ₁ = (p and γ)`, `φ₂ = γ`).
* `top`/`bot` : the tautology and contradiction the paper assumes the language contains.
* `lupd_static` : when defined, the leaf update is the static truth set. -/
structure Sys (W L : Type) where
  sem : L → W → Bool
  lupd : L → WSet W → WSet W
  ldef : L → WSet W → Prop
  lvar : L → Fm L → Fm L → Prop
  top : Fm L
  bot : Fm L
  top_ok : ∀ w, evalF sem top w = true
  bot_ok : ∀ w, evalF sem bot w = false
  lupd_static : ∀ l C, ldef l C → lupd l C = fun w => C w ∧ sem l w = true

variable {W L : Type}

namespace Sys

def eval (S : Sys W L) (F : Fm L) (w : W) : Bool := evalF S.sem F w

@[simp] theorem eval_leaf (S : Sys W L) (l : L) (w : W) : S.eval (.leaf l) w = S.sem l w := rfl
@[simp] theorem eval_neg (S : Sys W L) (F : Fm L) (w : W) : S.eval (.neg F) w = !(S.eval F w) := rfl
@[simp] theorem eval_conj (S : Sys W L) (F G : Fm L) (w : W) :
    S.eval (.conj F G) w = (S.eval F w && S.eval G w) := rfl
@[simp] theorem eval_disj (S : Sys W L) (F G : Fm L) (w : W) :
    S.eval (.disj F G) w = (S.eval F w || S.eval G w) := rfl
@[simp] theorem eval_cond (S : Sys W L) (F G : Fm L) (w : W) :
    S.eval (.cond F G) w = (!(S.eval F w) || S.eval G w) := rfl

theorem top_true (S : Sys W L) (w : W) : S.eval S.top w = true := S.top_ok w
theorem bot_false (S : Sys W L) (w : W) : S.eval S.bot w = false := S.bot_ok w

/-- `C ⊨ A ⇔ B`: the two formulas have the same truth value at every world of `C`. -/
def CEquiv (S : Sys W L) (C : WSet W) (A B : Fm L) : Prop :=
  ∀ w, C w → S.eval A w = S.eval B w

/-- The static truth set `{w ∈ C : w ⊨ F}`. -/
def TS (S : Sys W L) (F : Fm L) (C : WSet W) : WSet W :=
  fun w => C w ∧ S.eval F w = true

/-- Heim's update `C[F]` (meaningful only where `Def` holds). Paper (21). -/
def Upd (S : Sys W L) : Fm L → WSet W → WSet W
  | .leaf l, C => S.lupd l C
  | .neg F, C => fun w => C w ∧ ¬ Upd S F C w
  | .conj F G, C => Upd S G (Upd S F C)
  | .disj F G, C => fun w => Upd S F C w ∨ Upd S G (fun v => C v ∧ ¬ Upd S F C v) w
  | .cond F G, C => fun w => C w ∧ ¬ (Upd S F C w ∧ ¬ Upd S G (Upd S F C) w)

/-- `Def S F C` iff `C[F] ≠ #`. Paper (21). -/
def Def (S : Sys W L) : Fm L → WSet W → Prop
  | .leaf l, C => S.ldef l C
  | .neg F, C => Def S F C
  | .conj F G, C => Def S F C ∧ Def S G (Upd S F C)
  | .disj F G, C => Def S F C ∧ Def S G (fun v => C v ∧ ¬ Upd S F C v)
  | .cond F G, C => Def S F C ∧ Def S G (Upd S F C)

/-- **Theorem 1(ii)/2(ii) (dynamic half).**  Where defined, Heim's update is the static
truth set.  (Independent of Transparency.) -/
theorem upd_eq_TS (S : Sys W L) : ∀ (F : Fm L) (C : WSet W), Def S F C → Upd S F C = TS S F C := by
  intro F
  induction F with
  | leaf l =>
    intro C h
    exact S.lupd_static l C h
  | neg F ih =>
    intro C h
    have h1 := ih C h
    funext w
    apply propext
    simp only [Upd, h1, TS, eval_neg]
    cases S.eval F w <;> simp
  | conj F G ihF ihG =>
    intro C ⟨h1, h2⟩
    have e1 := ihF C h1
    simp only [Upd] at *
    rw [e1] at h2 ⊢
    rw [ihG _ h2]
    funext w
    apply propext
    simp only [TS, eval_conj]
    cases S.eval F w <;> cases S.eval G w <;> simp
  | disj F G ihF ihG =>
    intro C ⟨h1, h2⟩
    have e1 := ihF C h1
    simp only [Upd] at *
    rw [e1] at h2 ⊢
    have e2 := ihG _ h2
    rw [e2]
    funext w
    apply propext
    simp only [TS, eval_disj]
    cases S.eval F w <;> cases S.eval G w <;> simp <;> grind
  | cond F G ihF ihG =>
    intro C ⟨h1, h2⟩
    have e1 := ihF C h1
    simp only [Upd] at *
    rw [e1] at h2 ⊢
    have e2 := ihG _ h2
    rw [e2]
    funext w
    apply propext
    simp only [TS, eval_cond]
    cases S.eval F w <;> cases S.eval G w <;> simp <;> grind

end Sys

/-! ## Contexts, completions, Transparency -/

/-- One-hole formula contexts.  Sibling formulas that lie to the *left* of the hole (or
the left operand when the hole is in the right operand) are part of the fixed initial
string `α`; sibling formulas to the *right* of the hole belong to the (variable)
completion `β`. -/
inductive Ctx (L : Type) where
  | hole : Ctx L
  | negC : Ctx L → Ctx L
  | conjL : Ctx L → Fm L → Ctx L
  | conjR : Fm L → Ctx L → Ctx L
  | disjL : Ctx L → Fm L → Ctx L
  | disjR : Fm L → Ctx L → Ctx L
  | condL : Ctx L → Fm L → Ctx L
  | condR : Fm L → Ctx L → Ctx L

def Ctx.plug : Ctx L → Fm L → Fm L
  | .hole, X => X
  | .negC c, X => .neg (c.plug X)
  | .conjL c r, X => .conj (c.plug X) r
  | .conjR l c, X => .conj l (c.plug X)
  | .disjL c r, X => .disj (c.plug X) r
  | .disjR l c, X => .disj l (c.plug X)
  | .condL c r, X => .cond (c.plug X) r
  | .condR l c, X => .cond l (c.plug X)

/-- `Compl π π'`: `π'` is a *sentence completion* of the initial string determined by the
hole of `π`: same left material, same number of open brackets.  When the hole is the
first operand of a bracket `(_ ... )` opened by `(` alone, the connective (`and`/`or`)
and the right operand are not yet determined by the initial string (this is exactly
what "for any sentence completion β" quantifies over); `(not ` and `(if ` are
already determined by the initial string, but not the right operand of `if`. -/
def Compl : Ctx L → Ctx L → Prop
  | .hole, π' => π' = .hole
  | .negC c, π' => ∃ c', π' = .negC c' ∧ Compl c c'
  | .conjL c _, π' => ∃ c' r', (π' = .conjL c' r' ∨ π' = .disjL c' r') ∧ Compl c c'
  | .disjL c _, π' => ∃ c' r', (π' = .conjL c' r' ∨ π' = .disjL c' r') ∧ Compl c c'
  | .conjR l c, π' => ∃ c', π' = .conjR l c' ∧ Compl c c'
  | .disjR l c, π' => ∃ c', π' = .disjR l c' ∧ Compl c c'
  | .condL c _, π' => ∃ c' r', π' = .condL c' r' ∧ Compl c c'
  | .condR l c, π' => ∃ c', π' = .condR l c' ∧ Compl c c'

namespace Sys

/-- **Principle of Transparency** (paper (26)), for a formula `F` in context set `C`:
for every occurrence of a leaf `l` in `F` (= initial string `α l`), every sentence
completion `π'`, and every replacement pair `(φ₁, φ₂)` of `l`,
`C ⊨ π'[φ₁] ⇔ π'[φ₂]`. -/
def Transp (S : Sys W L) (C : WSet W) (F : Fm L) : Prop :=
  ∀ (π : Ctx L) (l : L), π.plug (.leaf l) = F → ∀ π', Compl π π' →
    ∀ φ₁ φ₂, S.lvar l φ₁ φ₂ → S.CEquiv C (π'.plug φ₁) (π'.plug φ₂)

theorem plug_leaf_eq {π : Ctx L} {l l' : L} (h : π.plug (.leaf l) = .leaf l') :
    π = .hole ∧ l = l' := by
  cases π <;> simp [Ctx.plug] at h
  · exact ⟨rfl, h⟩

/-- Transparency of a bare leaf. -/
theorem transp_leaf (S : Sys W L) (C : WSet W) (l : L) :
    S.Transp C (.leaf l) ↔ ∀ φ₁ φ₂, S.lvar l φ₁ φ₂ → S.CEquiv C φ₁ φ₂ := by
  constructor
  · intro h φ₁ φ₂ hv
    exact h .hole l rfl .hole rfl φ₁ φ₂ hv
  · intro h π l' hπ π' hc φ₁ φ₂ hv
    obtain ⟨rfl, rfl⟩ := plug_leaf_eq hπ
    simp only [Compl] at hc
    subst hc
    exact h φ₁ φ₂ hv

theorem transp_neg (S : Sys W L) (C : WSet W) (G : Fm L) :
    S.Transp C (.neg G) ↔ S.Transp C G := by
  constructor
  · intro h π l hπ π' hc φ₁ φ₂ hv w hw
    have := h (.negC π) l (by simp [Ctx.plug, hπ]) (.negC π') ⟨π', rfl, hc⟩ φ₁ φ₂ hv w hw
    simpa [Ctx.plug] using this
  · intro h π l hπ π' hc φ₁ φ₂ hv w hw
    cases π <;> simp [Ctx.plug] at hπ
    case negC π1 =>
      obtain ⟨c', rfl, hc'⟩ := hc
      have := h π1 l hπ c' hc' φ₁ φ₂ hv w hw
      simp [Ctx.plug, this]

/-- Paper cases (d)(i) and Transparency Lemma (a) at the level of contexts:
`Transp C (G and H)` iff `Transp C G` and `Transp {w ∈ C : w ⊨ G} H`. -/
theorem transp_conj (S : Sys W L) (C : WSet W) (G H : Fm L) :
    S.Transp C (.conj G H) ↔ S.Transp C G ∧ S.Transp (S.TS G C) H := by
  constructor
  · intro h
    constructor
    · intro π l hπ π' hc φ₁ φ₂ hv w hw
      have := h (.conjL π H) l (by simp [Ctx.plug, hπ]) (.conjL π' S.top)
        ⟨π', S.top, Or.inl rfl, hc⟩ φ₁ φ₂ hv w hw
      simpa [Ctx.plug, S.top_true] using this
    · intro π l hπ π' hc φ₁ φ₂ hv w ⟨hwC, hwG⟩
      have := h (.conjR G π) l (by simp [Ctx.plug, hπ]) (.conjR G π')
        ⟨π', rfl, hc⟩ φ₁ φ₂ hv w hwC
      simpa [Ctx.plug, hwG] using this
  · intro ⟨h1, h2⟩ π l hπ π' hc φ₁ φ₂ hv w hw
    cases π <;> simp [Ctx.plug] at hπ
    case conjL π1 r =>
      obtain ⟨hG, rfl⟩ := hπ
      obtain ⟨c', r', hor, hc'⟩ := hc
      have := h1 π1 l hG c' hc' φ₁ φ₂ hv w hw
      rcases hor with rfl | rfl <;> simp [Ctx.plug, this]
    case conjR l' π2 =>
      obtain ⟨hl, hH⟩ := hπ
      subst hl
      obtain ⟨c', rfl, hc'⟩ := hc
      cases hg : S.eval l' w
      · simp [Ctx.plug, hg]
      · have := h2 π2 l hH c' hc' φ₁ φ₂ hv w ⟨hw, hg⟩
        simp [Ctx.plug, hg, this]

theorem transp_disj (S : Sys W L) (C : WSet W) (G H : Fm L) :
    S.Transp C (.disj G H) ↔ S.Transp C G ∧ S.Transp (fun w => C w ∧ S.eval G w = false) H := by
  constructor
  · intro h
    constructor
    · intro π l hπ π' hc φ₁ φ₂ hv w hw
      have := h (.disjL π H) l (by simp [Ctx.plug, hπ]) (.disjL π' S.bot)
        ⟨π', S.bot, Or.inr rfl, hc⟩ φ₁ φ₂ hv w hw
      simpa [Ctx.plug, S.bot_false] using this
    · intro π l hπ π' hc φ₁ φ₂ hv w ⟨hwC, hwG⟩
      have := h (.disjR G π) l (by simp [Ctx.plug, hπ]) (.disjR G π')
        ⟨π', rfl, hc⟩ φ₁ φ₂ hv w hwC
      simpa [Ctx.plug, hwG] using this
  · intro ⟨h1, h2⟩ π l hπ π' hc φ₁ φ₂ hv w hw
    cases π <;> simp [Ctx.plug] at hπ
    case disjL π1 r =>
      obtain ⟨hG, rfl⟩ := hπ
      obtain ⟨c', r', hor, hc'⟩ := hc
      have := h1 π1 l hG c' hc' φ₁ φ₂ hv w hw
      rcases hor with rfl | rfl <;> simp [Ctx.plug, this]
    case disjR l' π2 =>
      obtain ⟨hl, hH⟩ := hπ
      subst hl
      obtain ⟨c', rfl, hc'⟩ := hc
      cases hg : S.eval l' w
      · have := h2 π2 l hH c' hc' φ₁ φ₂ hv w ⟨hw, hg⟩
        simp [Ctx.plug, hg, this]
      · simp [Ctx.plug, hg]

theorem transp_cond (S : Sys W L) (C : WSet W) (G H : Fm L) :
    S.Transp C (.cond G H) ↔ S.Transp C G ∧ S.Transp (S.TS G C) H := by
  constructor
  · intro h
    constructor
    · intro π l hπ π' hc φ₁ φ₂ hv w hw
      have := h (.condL π H) l (by simp [Ctx.plug, hπ]) (.condL π' S.bot)
        ⟨π', S.bot, rfl, hc⟩ φ₁ φ₂ hv w hw
      simpa [Ctx.plug, S.bot_false] using this
    · intro π l hπ π' hc φ₁ φ₂ hv w ⟨hwC, hwG⟩
      have := h (.condR G π) l (by simp [Ctx.plug, hπ]) (.condR G π')
        ⟨π', rfl, hc⟩ φ₁ φ₂ hv w hwC
      simpa [Ctx.plug, hwG] using this
  · intro ⟨h1, h2⟩ π l hπ π' hc φ₁ φ₂ hv w hw
    cases π <;> simp [Ctx.plug] at hπ
    case condL π1 r =>
      obtain ⟨hG, rfl⟩ := hπ
      obtain ⟨c', r', rfl, hc'⟩ := hc
      have := h1 π1 l hG c' hc' φ₁ φ₂ hv w hw
      simp [Ctx.plug, this]
    case condR l' π2 =>
      obtain ⟨hl, hH⟩ := hπ
      subst hl
      obtain ⟨c', rfl, hc'⟩ := hc
      cases hg : S.eval l' w
      · simp [Ctx.plug, hg]
      · have := h2 π2 l hH c' hc' φ₁ φ₂ hv w ⟨hw, hg⟩
        simp [Ctx.plug, hg, this]

end Sys

end AntiDyn