import AntiDynamics.Propositional

/-!
# Over-generation of dynamic semantics and the connective `unless`

* Section 1.3, (2): the deviant conjunction `and*`; Section 3.2, (24): the deviant
  disjunction `or*` for which Dynamic Transparency fails.
* Section 6, (32)-(33): the four candidate CCPs for `unless` and the Transparency prediction.
-/

namespace AntiDyn
namespace Propositional

open Classical

variable {W ι : Type} (v : W → ι → Bool) (i0 : ι)

/-! ## Trigger-free formulas -/

/-- No presupposition trigger occurs in the formula. -/
def TrigFree : PFm ι → Prop
  | .leaf (.atom _) => True
  | .leaf (.trig _ _) => False
  | .neg F => TrigFree F
  | .conj F G => TrigFree F ∧ TrigFree G
  | .disj F G => TrigFree F ∧ TrigFree G
  | .cond F G => TrigFree F ∧ TrigFree G

theorem trigFree_def (F : PFm ι) (hF : TrigFree F) (C : WSet W) : (sys v i0).Def F C := by
  induction F generalizing C with
  | leaf l => cases l <;> simp_all [TrigFree, Sys.Def, sys]
  | neg F ih => exact ih hF C
  | conj F G ihF ihG => exact ⟨ihF hF.1 C, ihG hF.2 _⟩
  | disj F G ihF ihG => exact ⟨ihF hF.1 C, ihG hF.2 _⟩
  | cond F G ihF ihG => exact ⟨ihF hF.1 C, ihG hF.2 _⟩

/-! ## (2): the deviant conjunction `and*` -/

/-- `C[F and* G] = # iff C[G] = # or (C[G] ≠ # and C[G][F] = #)`. -/
def andStarDef (F G : PFm ι) (C : WSet W) : Prop :=
  (sys v i0).Def G C ∧ (sys v i0).Def F ((sys v i0).Upd G C)

/-- `C[F and* G] = C[G][F]`. -/
def andStarUpd (F G : PFm ι) (C : WSet W) : WSet W :=
  (sys v i0).Upd F ((sys v i0).Upd G C)

/-- `C[F and* G] = C[G and F]` (definitionally). -/
theorem andStar_eq_swap (F G : PFm ι) (C : WSet W) :
    (andStarDef v i0 F G C ↔ (sys v i0).Def (.conj G F) C) ∧
    andStarUpd v i0 F G C = (sys v i0).Upd (.conj G F) C := ⟨Iff.rfl, rfl⟩

/-- When neither conjunct contains a trigger, `and*` and `and` agree (definedness and update). -/
theorem andStar_agrees_trigfree (F G : PFm ι) (hF : TrigFree F) (hG : TrigFree G) (C : WSet W) :
    andStarDef v i0 F G C ∧ (sys v i0).Def (.conj F G) C ∧
    andStarUpd v i0 F G C = (sys v i0).Upd (.conj F G) C := by
  refine ⟨⟨trigFree_def v i0 G hG C, trigFree_def v i0 F hF _⟩,
    ⟨trigFree_def v i0 F hF C, trigFree_def v i0 G hG _⟩, ?_⟩
  have h1 := (sys v i0).upd_eq_TS (.conj G F) C ⟨trigFree_def v i0 G hG C, trigFree_def v i0 F hF _⟩
  have h2 := (sys v i0).upd_eq_TS (.conj F G) C ⟨trigFree_def v i0 F hF C, trigFree_def v i0 G hG _⟩
  show (sys v i0).Upd (.conj G F) C = _
  rw [h1, h2]
  funext w; apply propext
  simp only [Sys.TS, Sys.eval_conj]
  cases (sys v i0).eval F w <;> cases (sys v i0).eval G w <;> simp

/-- `and*` predicts the opposite projection from `and` (Moldavia example).  With
`F = p̲p'` and `G = q` in the one-world-type context `C = {w₀}` where `q` is false, `and*`
is defined (the update of the *second* conjunct empties the context) whereas `and`, hence
Transparency (Theorem 1), requires `C ⊨ p`, which fails. -/
theorem andStar_not_transparency :
    ¬ ∀ (v : Bool → Bool → Bool) (C : WSet Bool) (F G : PFm Bool),
      andStarDef v true F G C ↔ (sys v true).Transp C (.conj F G) := by
  intro h
  have := h (fun _ _ => false) (fun w => w = false) (tr_ false true) (at_ true)
  have h1 : andStarDef (fun (_ : Bool) (_ : Bool) => false) true (tr_ false true) (at_ true)
      (fun w => w = false) := by
    refine ⟨trivial, ?_⟩
    intro w hw
    simp [Sys.Upd, sys, at_] at hw
  have h2 := this.1 h1
  rw [ex14] at h2
  have := h2 false rfl
  simp at this

/-- Conversely with `F = q`, `G = p̲p'` (`Moldavia is a monarchy and* the king ...`), `and*`
requires `C ⊨ p` whereas Transparency requires only `C ⊨ q ⇒ p`. -/
theorem andStar_too_strong :
    ∃ (v : Bool → Bool → Bool) (C : WSet Bool),
      (sys v true).Transp C (.conj (at_ true) (tr_ false true)) ∧
      ¬ andStarDef v true (at_ true) (tr_ false true) C := by
  refine ⟨fun _ _ => false, fun w => w = false, ?_, ?_⟩
  · rw [ex15]; intro w _ hq; simp at hq
  · rintro ⟨h, -⟩
    have := h false rfl
    simp [sys] at this

/-! ## (24): the deviant disjunction `or*` and failure of Dynamic Transparency -/

/-- `C[F or* G]` (paper (24)): the same as `or` when `C[G] = #`; otherwise
`C[(not G)][F] ∪ C[(not F)][G]`. (Definedness is that of `or`.) -/
noncomputable def orStarUpd (F G : PFm ι) (C : WSet W) : WSet W := fun w =>
  if (sys v i0).Def G C then
    ((sys v i0).Upd F (fun x => C x ∧ ¬ (sys v i0).Upd G C x) w ∨
     (sys v i0).Upd G (fun x => C x ∧ ¬ (sys v i0).Upd F C x) w)
  else
    ((sys v i0).Upd F C w ∨
     (sys v i0).Upd G (fun x => C x ∧ ¬ (sys v i0).Upd F C x) w)

/-- Dynamic Transparency fails for `or*`: for `H = ((not p) or* p̲p')`, in the context of all
four valuations of `p, p'`, `C[H]` is defined (indeed `C[p̲p'] = #`, so the first rule
applies) but `C[H] ≠ C[H*]`. -/
theorem or_star_breaks_dynamic_transparency :
    ∃ (v : Bool × Bool → Bool → Bool) (C : WSet (Bool × Bool)),
      let F : PFm Bool := .neg (at_ false)
      (sys v true).Def (.disj F (tr_ false true)) C ∧
      ¬ (sys v true).Def (tr_ false true) C ∧
      ∃ w, C w ∧ orStarUpd v true F (tr_ false true) C w ∧
        ¬ orStarUpd v true F (star (tr_ false true)) C w := by
  refine ⟨fun w i => if i then w.2 else w.1, fun _ => True, ?_⟩
  intro F
  refine ⟨?_, ?_, ((false, true)), trivial, ?_, ?_⟩
  · simp only [Sys.Def, Sys.Upd, sys, F, at_, tr_]
    refine ⟨trivial, fun w hw => ?_⟩
    simpa using hw
  · simp only [Sys.Def, sys, tr_]
    intro h
    have := h (false, true) trivial
    simp at this
  · have hd : ¬ (sys (fun (w : Bool × Bool) (i : Bool) => if i then w.2 else w.1) true).Def
        (tr_ false true) (fun _ => True) := by
      simp only [Sys.Def, sys, tr_]
      intro h
      have := h (false, true) trivial
      simp at this
    simp only [orStarUpd, hd, ite_false]
    left
    simp [Sys.Upd, sys, F, at_]
  · simp only [orStarUpd, star_tr]
    have hd : (sys (fun (w : Bool × Bool) (i : Bool) => if i then w.2 else w.1) true).Def
        (at_ true) (fun _ => True) := by
      simp [Sys.Def, sys, at_]
    simp only [hd, ite_true]
    simp [Sys.Upd, sys, F, at_]

/-! ## Section 6, (32)-(33): candidate CCPs for `unless` -/

section Unless
variable (F G : PFm ι) (C : WSet W)

/-- (32a): `C[unless F,G] = # iff C[F] = # or (C[F] ≠ # and C[(not F)][G] = #)`;
update `C − C[(not F)][(not G)]`. -/
def unlessA_def : Prop := (sys v i0).Def F C ∧ (sys v i0).Def G ((sys v i0).Upd (.neg F) C)
def unlessA_upd : WSet W := fun w =>
  C w ∧ ¬ ((sys v i0).Upd (.neg F) C w ∧ ¬ (sys v i0).Upd G ((sys v i0).Upd (.neg F) C) w)
/-- (32b): `# iff C[F] = # or C[F][G] = #`. -/
def unlessB_def : Prop := (sys v i0).Def F C ∧ (sys v i0).Def G ((sys v i0).Upd F C)
/-- (32c): `# iff C[F] = # or C[G] = #`. -/
def unlessC_def : Prop := (sys v i0).Def F C ∧ (sys v i0).Def G C
/-- (32d): `# iff C[G] = # or (C[G] ≠ # and C[(not G)][F] = #)`;
update `C − C[(not G)][F]`. -/
def unlessD_def : Prop := (sys v i0).Def G C ∧ (sys v i0).Def F (fun x => C x ∧ ¬ (sys v i0).Upd G C x)
def unlessD_upd_paper : WSet W := fun w =>
  C w ∧ ¬ (sys v i0).Upd F (fun x => C x ∧ ¬ (sys v i0).Upd G C x) w
/-- (32d) with the update rule corrected to `C − C[(not G)][(not F)]` (= Heim's
`if not G, F`), which is what the surrounding text ("`if not G, F`") requires. -/
def unlessD_upd : WSet W := fun w =>
  C w ∧ ¬ ((fun x => C x ∧ ¬ (sys v i0).Upd G C x) w ∧
      ¬ (sys v i0).Upd F (fun x => C x ∧ ¬ (sys v i0).Upd G C x) w)

/-- (32a) is exactly Heim's `if not F, G`. -/
theorem unlessA_is_if_not :
    (unlessA_def v i0 F G C ↔ (sys v i0).Def (.cond (.neg F) G) C) ∧
    unlessA_upd v i0 F G C = (sys v i0).Upd (.cond (.neg F) G) C := ⟨Iff.rfl, rfl⟩

/-- For trigger-free `F, G` the four candidate rules are all defined and all have the same
update: the bivalent content of `unless F, G`. -/
theorem unless_variants_agree_trigfree (hF : TrigFree F) (hG : TrigFree G) :
    unlessA_def v i0 F G C ∧ unlessB_def v i0 F G C ∧ unlessC_def v i0 F G C ∧
      unlessD_def v i0 F G C ∧ unlessD_upd v i0 F G C = unlessA_upd v i0 F G C := by
  have dF := trigFree_def v i0 F hF
  have dG := trigFree_def v i0 G hG
  refine ⟨⟨dF C, dG _⟩, ⟨dF C, dG _⟩, ⟨dF C, dG C⟩, ⟨dG C, dF _⟩, ?_⟩
  have hU : ∀ (H : PFm ι), TrigFree H → ∀ (D : WSet W), (sys v i0).Upd H D = (sys v i0).TS H D :=
    fun H hH D => (sys v i0).upd_eq_TS H D (trigFree_def v i0 H hH D)
  have hFn : TrigFree (.neg F : PFm ι) := hF
  unfold unlessD_upd unlessA_upd
  funext w; apply propext
  simp only [hU F hF, hU G hG, hU _ hFn, Sys.TS, Sys.eval_neg]
  cases (sys v i0).eval F w <;> cases (sys v i0).eval G w <;> simp <;> grind

/-- **Typo in (32d)** (p. 352): the update rule as printed, `C − C[(not G)][F]`, equals
`{w ∈ C : F → G}` for trigger-free `F, G`, whereas the bivalent content of `unless F, G`
is `F ∨ G`.  So the printed (32d) contradicts the claim that all four rules "make exactly the
same predictions when F and G contain no presupposition triggers". -/
theorem unlessD_paper_is_wrong :
    ∃ (v : Unit → Bool → Bool) (C : WSet Unit) (F G : PFm Bool), TrigFree F ∧ TrigFree G ∧
      unlessD_upd_paper v true F G C ≠ unlessA_upd v true F G C := by
  refine ⟨fun _ i => !i, fun _ => True, at_ false, at_ true, trivial, trivial, ?_⟩
  -- letter `false` is true, letter `true` is false: F true, G false
  intro h
  have := congrFun h ()
  simp [unlessD_upd_paper, unlessA_upd, Sys.Upd, sys, at_] at this

/-- Transparency treats `unless F,G` like `if not F, G`: they have the same static
content (`F ∨ G`) and (for the purposes of Transparency) the same syntax shape. -/
theorem transp_unless_eq_if_not (F G : PFm ι) (C : WSet W) :
    (sys v i0).Transp C (.disj F G) ↔ (sys v i0).Transp C (.cond (.neg F) G) := by
  rw [caseE, caseF, caseC]
  constructor <;> rintro ⟨h1, h2⟩ <;> refine ⟨h1, ?_⟩
  · have : (fun w => C w ∧ (sys v i0).eval F w = false) = (sys v i0).TS (.neg F) C := by
      funext w; apply propext; simp only [Sys.TS, Sys.eval_neg]; cases (sys v i0).eval F w <;> simp
    rw [← this]; exact h2
  · have : (fun w => C w ∧ (sys v i0).eval F w = false) = (sys v i0).TS (.neg F) C := by
      funext w; apply propext; simp only [Sys.TS, Sys.eval_neg]; cases (sys v i0).eval F w <;> simp
    rw [this]; exact h2

/-- (33): `F = c` (plain, "John didn't come"), `G = h̲h'` ("Mary knows he is here").
The four rules give four different presuppositions; Transparency (= Theorem 1 applied to
`if not F, G`) selects (a): "if John came, he is here". -/
theorem unless_33 (c h h' : ι) (C : WSet W) :
    (unlessA_def v i0 (at_ c) (tr_ h h') C ↔ ∀ w, C w → v w c = false → v w h = true) ∧
    (unlessB_def v i0 (at_ c) (tr_ h h') C ↔ ∀ w, C w → v w c = true → v w h = true) ∧
    (unlessC_def v i0 (at_ c) (tr_ h h') C ↔ ∀ w, C w → v w h = true) ∧
    (unlessD_def v i0 (at_ c) (tr_ h h') C ↔ ∀ w, C w → v w h = true) ∧
    ((sys v i0).Transp C (.cond (.neg (at_ c)) (tr_ h h')) ↔
        ∀ w, C w → v w c = false → v w h = true) := by
  have hT := transp_atomic v i0
  refine ⟨?_, ?_, ?_, ?_, ?_⟩
  · simp only [unlessA_def, Sys.Def, Sys.Upd, sys, at_, tr_]
    constructor
    · rintro ⟨-, h⟩ w hw hc; exact h w ⟨hw, by simp [hc]⟩
    · intro h; exact ⟨trivial, fun w ⟨hw, hn⟩ => h w hw (by simp_all)⟩
  · simp only [unlessB_def, Sys.Def, Sys.Upd, sys, at_, tr_]
    constructor
    · rintro ⟨-, h⟩ w hw hc; exact h w ⟨hw, hc⟩
    · intro h; exact ⟨trivial, fun w ⟨hw, hn⟩ => h w hw hn⟩
  · simp only [unlessC_def, Sys.Def, sys, tr_]
    exact ⟨fun h => h.2, fun h => ⟨trivial, h⟩⟩
  · simp only [unlessD_def, Sys.Def, sys, tr_]
    exact ⟨fun h => h.1, fun h => ⟨h, trivial⟩⟩
  · rw [theorem1_i]
    simp only [Sys.Def, Sys.Upd, sys, at_, tr_]
    constructor
    · rintro ⟨-, h⟩ w hw hc; exact h w ⟨hw, by simp [hc]⟩
    · intro h; exact ⟨trivial, fun w ⟨hw, hn⟩ => h w hw (by simp_all)⟩

/-- The rules (a) vs (b), (c), (d) really differ: in a one-world context where `c` is true
and `h` false, (a) is satisfied while (b), (c), (d) fail. -/
theorem unless_rules_differ :
    ∃ (v : Unit → Bool → Bool),
      (unlessA_def v true (at_ false) (tr_ true true) (fun _ => True)) ∧
      ¬ (unlessB_def v true (at_ false) (tr_ true true) (fun _ => True)) ∧
      ¬ (unlessC_def v true (at_ false) (tr_ true true) (fun _ => True)) ∧
      ¬ (unlessD_def v true (at_ false) (tr_ true true) (fun _ => True)) := by
  refine ⟨fun _ i => !i, ?_⟩
  -- letter `false` = c is true, letter `true` = h is false
  have := unless_33 (fun (_ : Unit) (i : Bool) => !i) true false true true (fun _ => True)
  obtain ⟨a, b, c, d, -⟩ := this
  refine ⟨a.2 (by intro w _ hc; simp at hc), ?_, ?_, ?_⟩
  · intro h; have := b.1 h () trivial (by simp); simp at this
  · intro h; have := c.1 h () trivial; simp at this
  · intro h; have := d.1 h () trivial; simp at this

/-- (32b): the definedness condition of (b) does not guarantee that the update rule "as in (a)"
(which needs `C[(not F)][G] ≠ #`) is defined: (b) is not a well-formed CCP as stated. -/
theorem unlessB_update_ill_defined :
    ∃ (v : Unit → Bool → Bool),
      unlessB_def v true (at_ false) (tr_ true true) (fun _ => True) ∧
      ¬ unlessA_def v true (at_ false) (tr_ true true) (fun _ => True) := by
  refine ⟨fun _ _ => false, ?_, ?_⟩
  · have := unless_33 (fun (_ : Unit) (_ : Bool) => false) true false true true (fun _ => True)
    exact this.2.1.2 (by intro w _ hc; simp at hc)
  · have := unless_33 (fun (_ : Unit) (_ : Bool) => false) true false true true (fun _ => True)
    intro h
    have := this.1.1 h () trivial rfl
    simp at this

end Unless

end Propositional
end AntiDyn