import AntiDynamics.Core

/-!
# Lifting leaf-level results through the connectives

* `Accessed` : the paper's "accessed pairs" `⟨C', F'⟩` (Section 5.3 Definition).
* `lift`     : the connective steps (c)-(f) of the proofs of Theorems 1 and 2.
* `NT`       : Non-Triviality (28); `lemma2` : Lemma 2.
* `dyn_transparency` : Dynamic Transparency (23) for an arbitrary leaf-level "star" map.
-/

namespace AntiDyn

variable {W L : Type}

/-- Paper, Section 5.3: `Accessed S C₀ F₀ C F` iff `⟨C, F⟩` is accessed by `⟨C₀, F₀⟩`. -/
inductive Accessed (S : Sys W L) (C₀ : WSet W) (F₀ : Fm L) : WSet W → Fm L → Prop
  | refl : Accessed S C₀ F₀ C₀ F₀
  | neg {C G} : Accessed S C₀ F₀ C (.neg G) → Accessed S C₀ F₀ C G
  | conjL {C G H} : Accessed S C₀ F₀ C (.conj G H) → Accessed S C₀ F₀ C G
  | conjR {C G H} : Accessed S C₀ F₀ C (.conj G H) → S.Def G C →
      Accessed S C₀ F₀ (S.Upd G C) H
  | disjL {C G H} : Accessed S C₀ F₀ C (.disj G H) → Accessed S C₀ F₀ C G
  | disjR {C G H} : Accessed S C₀ F₀ C (.disj G H) → S.Def G C →
      Accessed S C₀ F₀ (fun v => C v ∧ ¬ S.Upd G C v) H
  | condL {C G H} : Accessed S C₀ F₀ C (.cond G H) → Accessed S C₀ F₀ C G
  | condR {C G H} : Accessed S C₀ F₀ C (.cond G H) → S.Def G C →
      Accessed S C₀ F₀ (S.Upd G C) H

namespace Sys

/-- **Connective steps of Theorems 1 and 2** (paper cases (c)-(f), and the "otherwise"
parts of (d)-(f) in the proof of Theorem 2).  If the leaf-level equivalence
`Transp ↔ Def` holds at every accessed leaf pair, it holds at every accessed pair. -/
theorem lift (S : Sys W L) {C₀ : WSet W} {F₀ : Fm L}
    (hleaf : ∀ C l, Accessed S C₀ F₀ C (.leaf l) → (S.Transp C (.leaf l) ↔ S.ldef l C)) :
    ∀ (F : Fm L) (C : WSet W), Accessed S C₀ F₀ C F → (S.Transp C F ↔ S.Def F C) := by
  intro F
  induction F with
  | leaf l => intro C h; exact hleaf C l h
  | neg G ih =>
    intro C h
    rw [transp_neg]
    exact ih C (.neg h)
  | conj G H ihG ihH =>
    intro C h
    have hG := ihG C (.conjL h)
    rw [transp_conj]
    simp only [Def]
    constructor
    · rintro ⟨t1, t2⟩
      have d1 := hG.1 t1
      have e := upd_eq_TS S G C d1
      have hH := ihH _ (.conjR h d1)
      rw [e] at hH ⊢
      exact ⟨d1, hH.1 t2⟩
    · rintro ⟨d1, d2⟩
      have e := upd_eq_TS S G C d1
      have hH := ihH _ (.conjR h d1)
      rw [e] at hH d2
      exact ⟨hG.2 d1, hH.2 d2⟩
  | disj G H ihG ihH =>
    intro C h
    have hG := ihG C (.disjL h)
    rw [transp_disj]
    simp only [Def]
    constructor
    · rintro ⟨t1, t2⟩
      have d1 := hG.1 t1
      have e := upd_eq_TS S G C d1
      have hH := ihH _ (.disjR h d1)
      have e' : (fun v => C v ∧ ¬ S.Upd G C v) = (fun w => C w ∧ S.eval G w = false) := by
        funext v; apply propext; rw [e]; simp only [TS]; cases S.eval G v <;> simp
      rw [e'] at hH ⊢
      exact ⟨d1, hH.1 t2⟩
    · rintro ⟨d1, d2⟩
      have e := upd_eq_TS S G C d1
      have hH := ihH _ (.disjR h d1)
      have e' : (fun v => C v ∧ ¬ S.Upd G C v) = (fun w => C w ∧ S.eval G w = false) := by
        funext v; apply propext; rw [e]; simp only [TS]; cases S.eval G v <;> simp
      rw [e'] at hH d2
      exact ⟨hG.2 d1, hH.2 d2⟩
  | cond G H ihG ihH =>
    intro C h
    have hG := ihG C (.condL h)
    rw [transp_cond]
    simp only [Def]
    constructor
    · rintro ⟨t1, t2⟩
      have d1 := hG.1 t1
      have e := upd_eq_TS S G C d1
      have hH := ihH _ (.condR h d1)
      rw [e] at hH ⊢
      exact ⟨d1, hH.1 t2⟩
    · rintro ⟨d1, d2⟩
      have e := upd_eq_TS S G C d1
      have hH := ihH _ (.condR h d1)
      rw [e] at hH d2
      exact ⟨hG.2 d1, hH.2 d2⟩

/-- Unrestricted form (Theorem 1's induction): if `Transp ↔ Def` holds for all leaves in
all context sets, then it holds for all formulas in all context sets. -/
theorem transp_iff_def (S : Sys W L)
    (hleaf : ∀ C l, S.Transp C (.leaf l) ↔ S.ldef l C) (F : Fm L) (C : WSet W) :
    S.Transp C F ↔ S.Def F C :=
  S.lift (C₀ := C) (F₀ := F) (fun C' l _ => hleaf C' l) F C .refl

end Sys

/-! ## Non-Triviality (paper (28)) and Lemma 2 -/

namespace Sys

/-- `NT S isQ C F`: `⟨C, F⟩` satisfies Non-Triviality, for the class `isQ` of
quantificational leaves: for every occurrence `α A` of such a leaf there is a completion
`β` (here `π'`) with `C ⊭ αAβ ⇔ αTβ` and `C ⊭ αAβ ⇔ αFβ`. -/
def NT (S : Sys W L) (isQ : L → Prop) (C : WSet W) (F : Fm L) : Prop :=
  ∀ (π : Ctx L) (l : L), π.plug (.leaf l) = F → isQ l → ∃ π', Compl π π' ∧
    (∃ w, C w ∧ S.eval (π'.plug (.leaf l)) w ≠ S.eval (π'.plug S.top) w) ∧
    (∃ w, C w ∧ S.eval (π'.plug (.leaf l)) w ≠ S.eval (π'.plug S.bot) w)

theorem nt_neg (S : Sys W L) {q : L → Prop} {C : WSet W} {G : Fm L}
    (h : S.NT q C (.neg G)) : S.NT q C G := by
  intro π l hπ hq
  obtain ⟨π', hc, ⟨w1, hw1, h1⟩, ⟨w2, hw2, h2⟩⟩ :=
    h (.negC π) l (by simp [Ctx.plug, hπ]) hq
  obtain ⟨c', rfl, hc'⟩ := hc
  exact ⟨c', hc', ⟨w1, hw1, by intro e; apply h1; simp [Ctx.plug, e]⟩,
    ⟨w2, hw2, by intro e; apply h2; simp [Ctx.plug, e]⟩⟩

theorem nt_conjL (S : Sys W L) {q : L → Prop} {C : WSet W} {G H : Fm L}
    (h : S.NT q C (.conj G H)) : S.NT q C G := by
  intro π l hπ hq
  obtain ⟨π', hc, ⟨w1, hw1, h1⟩, ⟨w2, hw2, h2⟩⟩ :=
    h (.conjL π H) l (by simp [Ctx.plug, hπ]) hq
  obtain ⟨c', r', hor, hc'⟩ := hc
  refine ⟨c', hc', ⟨w1, hw1, fun e => h1 ?_⟩, ⟨w2, hw2, fun e => h2 ?_⟩⟩
  · rcases hor with rfl | rfl <;> simp [Ctx.plug, e]
  · rcases hor with rfl | rfl <;> simp [Ctx.plug, e]

theorem nt_disjL (S : Sys W L) {q : L → Prop} {C : WSet W} {G H : Fm L}
    (h : S.NT q C (.disj G H)) : S.NT q C G := by
  intro π l hπ hq
  obtain ⟨π', hc, ⟨w1, hw1, h1⟩, ⟨w2, hw2, h2⟩⟩ :=
    h (.disjL π H) l (by simp [Ctx.plug, hπ]) hq
  obtain ⟨c', r', hor, hc'⟩ := hc
  refine ⟨c', hc', ⟨w1, hw1, fun e => h1 ?_⟩, ⟨w2, hw2, fun e => h2 ?_⟩⟩
  · rcases hor with rfl | rfl <;> simp [Ctx.plug, e]
  · rcases hor with rfl | rfl <;> simp [Ctx.plug, e]

theorem nt_condL (S : Sys W L) {q : L → Prop} {C : WSet W} {G H : Fm L}
    (h : S.NT q C (.cond G H)) : S.NT q C G := by
  intro π l hπ hq
  obtain ⟨π', hc, ⟨w1, hw1, h1⟩, ⟨w2, hw2, h2⟩⟩ :=
    h (.condL π H) l (by simp [Ctx.plug, hπ]) hq
  obtain ⟨c', r', rfl, hc'⟩ := hc
  refine ⟨c', hc', ⟨w1, hw1, fun e => h1 ?_⟩, ⟨w2, hw2, fun e => h2 ?_⟩⟩
  · simp [Ctx.plug, e]
  · simp [Ctx.plug, e]

theorem nt_conjR (S : Sys W L) {q : L → Prop} {C : WSet W} {G H : Fm L}
    (h : S.NT q C (.conj G H)) : S.NT q (S.TS G C) H := by
  intro π l hπ hq
  obtain ⟨π', hc, ⟨w1, hw1, h1⟩, ⟨w2, hw2, h2⟩⟩ :=
    h (.conjR G π) l (by simp [Ctx.plug, hπ]) hq
  obtain ⟨c', rfl, hc'⟩ := hc
  refine ⟨c', hc', ⟨w1, ⟨hw1, ?_⟩, ?_⟩, ⟨w2, ⟨hw2, ?_⟩, ?_⟩⟩
  · cases hg : S.eval G w1 <;> simp_all [Ctx.plug]
  · cases hg : S.eval G w1 <;> simp_all [Ctx.plug]
  · cases hg : S.eval G w2 <;> simp_all [Ctx.plug]
  · cases hg : S.eval G w2 <;> simp_all [Ctx.plug]

theorem nt_condR (S : Sys W L) {q : L → Prop} {C : WSet W} {G H : Fm L}
    (h : S.NT q C (.cond G H)) : S.NT q (S.TS G C) H := by
  intro π l hπ hq
  obtain ⟨π', hc, ⟨w1, hw1, h1⟩, ⟨w2, hw2, h2⟩⟩ :=
    h (.condR G π) l (by simp [Ctx.plug, hπ]) hq
  obtain ⟨c', rfl, hc'⟩ := hc
  refine ⟨c', hc', ⟨w1, ⟨hw1, ?_⟩, ?_⟩, ⟨w2, ⟨hw2, ?_⟩, ?_⟩⟩
  · cases hg : S.eval G w1 <;> simp_all [Ctx.plug]
  · cases hg : S.eval G w1 <;> simp_all [Ctx.plug]
  · cases hg : S.eval G w2 <;> simp_all [Ctx.plug]
  · cases hg : S.eval G w2 <;> simp_all [Ctx.plug]

theorem nt_disjR (S : Sys W L) {q : L → Prop} {C : WSet W} {G H : Fm L}
    (h : S.NT q C (.disj G H)) : S.NT q (fun w => C w ∧ S.eval G w = false) H := by
  intro π l hπ hq
  obtain ⟨π', hc, ⟨w1, hw1, h1⟩, ⟨w2, hw2, h2⟩⟩ :=
    h (.disjR G π) l (by simp [Ctx.plug, hπ]) hq
  obtain ⟨c', rfl, hc'⟩ := hc
  refine ⟨c', hc', ⟨w1, ⟨hw1, ?_⟩, ?_⟩, ⟨w2, ⟨hw2, ?_⟩, ?_⟩⟩
  · cases hg : S.eval G w1 <;> simp_all [Ctx.plug]
  · cases hg : S.eval G w1 <;> simp_all [Ctx.plug]
  · cases hg : S.eval G w2 <;> simp_all [Ctx.plug]
  · cases hg : S.eval G w2 <;> simp_all [Ctx.plug]

/-- **Lemma 2** (paper p. 348): Non-Triviality is inherited by accessed pairs.
(The paper's proof tacitly uses `w ∈ C, w ⊨ G ⇒ w ∈ C[G]`, i.e. Heim-update = static
truth set on defined pairs; here that is `upd_eq_TS`, which does not depend on any
Transparency result.) -/
theorem lemma2 (S : Sys W L) {q : L → Prop} {C₀ : WSet W} {F₀ : Fm L}
    (h0 : S.NT q C₀ F₀) :
    ∀ {C : WSet W} {F : Fm L}, Accessed S C₀ F₀ C F → S.NT q C F := by
  intro C F h
  induction h with
  | refl => exact h0
  | neg _ ih => exact nt_neg S ih
  | conjL _ ih => exact nt_conjL S ih
  | disjL _ ih => exact nt_disjL S ih
  | condL _ ih => exact nt_condL S ih
  | @conjR C G H _ hd ih =>
    have := nt_conjR S ih
    rw [← upd_eq_TS S G C hd] at this
    exact this
  | @condR C G H _ hd ih =>
    have := nt_condR S ih
    rw [← upd_eq_TS S G C hd] at this
    exact this
  | @disjR C G H _ hd ih =>
    have := nt_disjR S ih
    have e' : (fun v => C v ∧ ¬ S.Upd G C v) = (fun w => C w ∧ S.eval G w = false) := by
      funext v; apply propext; rw [upd_eq_TS S G C hd]; simp only [TS]; cases S.eval G v <;> simp
    rw [e']
    exact this

end Sys

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

/-- Map a function over all leaves (for the `F ↦ F*` operation "delete underlined
material"). -/
def Fm.map (f : L → L) : Fm L → Fm L
  | .leaf l => .leaf (f l)
  | .neg F => .neg (F.map f)
  | .conj F G => .conj (F.map f) (G.map f)
  | .disj F G => .disj (F.map f) (G.map f)
  | .cond F G => .cond (F.map f) (G.map f)

namespace Sys

/-- `F*` is always defined when every starred leaf is. -/
theorem def_map (S : Sys W L) (f : L → L) (hf : ∀ l C, S.ldef (f l) C) :
    ∀ (F : Fm L) (C : WSet W), S.Def (F.map f) C := by
  intro F
  induction F with
  | leaf l => intro C; exact hf l C
  | neg F ih => intro C; exact ih C
  | conj F G ihF ihG => intro C; exact ⟨ihF C, ihG _⟩
  | disj F G ihF ihG => intro C; exact ⟨ihF C, ihG _⟩
  | cond F G ihF ihG => intro C; exact ⟨ihF C, ihG _⟩

/-- **Dynamic Transparency** (23): if `C[F] ≠ #` then `C[F] = C[F*]`.
Hypothesis: at leaf level, `f` deletes presuppositional material without changing the
update (`lupd (f l) = lupd l` where `l` is defined). -/
theorem dyn_transparency (S : Sys W L) (f : L → L)
    (hf : ∀ l C, S.ldef l C → S.lupd (f l) C = S.lupd l C) :
    ∀ (F : Fm L) (C : WSet W), S.Def F C → S.Upd (F.map f) C = S.Upd F C := by
  intro F
  induction F with
  | leaf l => intro C h; exact hf l C h
  | neg F ih =>
    intro C h
    have := ih C h
    funext w; apply propext
    simp only [Fm.map, Upd, this]
  | conj F G ihF ihG =>
    intro C ⟨h1, h2⟩
    have e1 := ihF C h1
    simp only [Fm.map, Upd]
    rw [e1, ihG _ h2]
  | disj F G ihF ihG =>
    intro C ⟨h1, h2⟩
    have e1 := ihF C h1
    simp only [Fm.map, Upd]
    rw [e1, ihG _ h2]
  | cond F G ihF ihG =>
    intro C ⟨h1, h2⟩
    have e1 := ihF C h1
    simp only [Fm.map, Upd]
    rw [e1, ihG _ h2]

end Sys

end AntiDyn