/-!
# Abstract theory of transparent restrictions and local contexts
(Appendix of "Local Contexts", items 10-21.)

Modelling.  Worlds `W`, individuals `D`.  A "restriction" `x : Val W D` is an
intension of type `<s,<e,t>>` (for a propositional restriction take `D = Unit`).
A *good final* / syntactic environment `α _ β'` is modelled by its semantic
effect `Ψ : Val W D → W → Bool`: `Ψ x w` is the truth value at `w` of
`α c'X β'` when the hole is filled with a restriction denoting `x`.
The only property of environments used by the appendix is *extensionality*
(`Ext`): `Ψ x w` depends only on `x w`.  A set of environments `Envs`
is
  * the set of all good finals `β'` (incremental version, `tr_i`),
  * the single actual final `β` (symmetric version, `tr_s`).
`Tr Envs C x` is membership of `x` in `tr(C, d, α_β)`:
  for every env Ψ, every expression γ (any `Val`, by Expressivity), every w ∈ C,
  `α (x ∧ γ) β' ⇔ α γ β'` at w.
-/
namespace LC

variable {W D : Type}

abbrev Val (W D : Type) := W → D → Bool
abbrev Env (W D : Type) := Val W D → W → Bool

def meet (x y : Val W D) : Val W D := fun w d => x w d && y w d
def top : Val W D := fun _ _ => true
def bot : Val W D := fun _ _ => false
/-- global generalized entailment `x ≤ y` (Def. 4a) -/
def le (x y : Val W D) : Prop := ∀ w d, x w d = true → y w d = true
/-- `C |= c' → x  c' ≤ y` : entailment relative to the context set -/
def cle (C : W → Prop) (x y : Val W D) : Prop := ∀ w, C w → ∀ d, x w d = true → y w d = true

def Ext (Ψ : Env W D) : Prop := ∀ x y w, x w = y w → Ψ x w = Ψ y w

/-- Def. 10: transparent restrictions (`x ∈ tr_v(C, d, α_β)`). -/
def Tr (Envs : Env W D → Prop) (C : W → Prop) (x : Val W D) : Prop :=
  ∀ Ψ, Envs Ψ → ∀ γ w, C w → Ψ (meet x γ) w = Ψ γ w

/-- Def. 11: `x` is the bottom element of `tr`, i.e. `x = lc`. -/
def IsLC (Envs : Env W D → Prop) (C : W → Prop) (x : Val W D) : Prop :=
  Tr Envs C x ∧ ∀ y, Tr Envs C y → le x y

theorem le_refl (x : Val W D) : le x x := fun _ _ h => h
theorem le_trans {x y z : Val W D} (h1 : le x y) (h2 : le y z) : le x z :=
  fun w d h => h2 w d (h1 w d h)

theorem meet_assoc (x y z : Val W D) : meet (meet x y) z = meet x (meet y z) := by
  funext w d; simp [meet, Bool.and_assoc]

theorem meet_top (γ : Val W D) : meet top γ = γ := by
  funext w d; simp [meet, top]

theorem le_meet_left (x y : Val W D) : le (meet x y) x := by
  intro w d h; simp [meet] at h; exact h.1
theorem le_meet_right (x y : Val W D) : le (meet x y) y := by
  intro w d h; simp [meet] at h; exact h.2

/-! ## Lemma 2 : closure under finite conjunction -/
theorem tr_top (Envs : Env W D → Prop) (C : W → Prop) : Tr Envs C top := by
  intro Ψ _ γ w _; rw [meet_top]

theorem lemma2 {Envs : Env W D → Prop} {C : W → Prop} {x y : Val W D}
    (h1 : Tr Envs C x) (h2 : Tr Envs C y) : Tr Envs C (meet x y) := by
  intro Ψ hΨ γ w hw
  rw [meet_assoc, h1 Ψ hΨ _ w hw, h2 Ψ hΨ γ w hw]

/-! ## generic "bottom of a finite set" lemma -/
theorem fold_bottom {α : Type} (m : α → α → α) (t : α) (P : α → Prop) (r : α → α → Prop)
    (hTop : P t) (hm : ∀ x y, P x → P y → P (m x y))
    (hml : ∀ x y, r (m x y) x) (hmr : ∀ x y, r (m x y) y)
    (htr : ∀ x y z, r x y → r y z → r x z) :
    ∀ L : List α, ∃ b, P b ∧ ∀ y, y ∈ L → P y → r b y := by
  intro L
  induction L with
  | nil => exact ⟨t, hTop, by intro y hy; cases hy⟩
  | cons a L ih =>
    obtain ⟨b, hb, hbL⟩ := ih
    by_cases ha : P a
    · refine ⟨m a b, hm a b ha hb, ?_⟩
      intro y hy hPy
      cases List.mem_cons.mp hy with
      | inl h => subst h; exact hml _ _
      | inr h => exact htr _ _ _ (hmr a b) (hbL y h hPy)
    · refine ⟨b, hb, ?_⟩
      intro y hy hPy
      cases List.mem_cons.mp hy with
      | inl h => subst h; exact absurd hPy ha
      | inr h => exact hbL y h hPy

/-! ## Lemma 3 : finite sets have a bottom -/
theorem lemma3 {Envs : Env W D → Prop} {C : W → Prop}
    (hfin : ∃ L : List (Val W D), ∀ x, Tr Envs C x → x ∈ L) :
    ∃ x, IsLC Envs C x := by
  obtain ⟨L, hL⟩ := hfin
  obtain ⟨b, hb, hbL⟩ := fold_bottom (α := Val W D) meet top (Tr Envs C) le
    (tr_top Envs C) (fun _ _ h1 h2 => lemma2 h1 h2) le_meet_left le_meet_right
    (fun _ _ _ => le_trans) L
  exact ⟨b, hb, fun y hy => hbL y (hL y hy) hy⟩

/-! ## Lemma 1 (propositional fragment, D = Unit) -/
open Classical in
/-- The paper's candidate `LCi` of Lemma 1, CORRECTED: `w ∈ C` is added. -/
noncomputable def lc1 (Envs : Env W Unit → Prop) (C : W → Prop) : Val W Unit :=
  fun w _ => decide (C w ∧ ∃ Ψ, Envs Ψ ∧ ∃ γ : Val W Unit, Ψ (meet bot γ) w ≠ Ψ γ w)

open Classical in
/-- The paper's candidate `LCi` of Lemma 1 EXACTLY as written (no restriction to `C`). -/
noncomputable def lc1Paper (Envs : Env W Unit → Prop) : Val W Unit :=
  fun w _ => decide (∃ Ψ, Envs Ψ ∧ ∃ γ : Val W Unit, Ψ (meet bot γ) w ≠ Ψ γ w)

theorem lemma1_step1 {Envs : Env W Unit → Prop} (hE : ∀ Ψ, Envs Ψ → Ext Ψ) (C : W → Prop) :
    Tr Envs C (lc1 Envs C) := by
  intro Ψ hΨ γ w hw
  by_cases h : lc1 Envs C w () = true
  · apply hE Ψ hΨ
    funext d; cases d
    simp [meet, h]
  · have hn : ¬ (C w ∧ ∃ Ψ, Envs Ψ ∧ ∃ γ : Val W Unit, Ψ (meet bot γ) w ≠ Ψ γ w) := by
      intro hc; apply h; simp [lc1]; exact hc
    have : Ψ (meet bot γ) w = Ψ γ w := by
      exact Classical.byContradiction (fun hne => hn ⟨hw, Ψ, hΨ, γ, hne⟩)
    rw [← this]
    have hl : lc1 Envs C w () = false := Bool.eq_false_iff.mpr h
    apply hE Ψ hΨ
    funext d; cases d
    simp [meet, bot, hl]

theorem lemma1_step2 {Envs : Env W Unit → Prop} (hE : ∀ Ψ, Envs Ψ → Ext Ψ) (C : W → Prop)
    (y : Val W Unit) (hy : Tr Envs C y) : le (lc1 Envs C) y := by
  intro w d h
  cases d
  refine Classical.byContradiction (fun hne => ?_)
  have hf : y w () = false := by simpa using hne
  simp [lc1] at h
  obtain ⟨hw, Ψ, hΨ, γ, hg⟩ := h
  apply hg
  have e : Ψ (meet y γ) w = Ψ (meet bot γ) w := by
    apply hE Ψ hΨ
    funext d; cases d
    simp [meet, bot, hf]
  rw [← e]; exact hy Ψ hΨ γ w hw

/-- Lemma 1 (corrected proof): in the propositional fragment the local context exists. -/
theorem lemma1 {Envs : Env W Unit → Prop} (hE : ∀ Ψ, Envs Ψ → Ext Ψ) (C : W → Prop) :
    IsLC Envs C (lc1 Envs C) :=
  ⟨lemma1_step1 hE C, lemma1_step2 hE C⟩

/-- The candidate in the paper's proof is NOT the bottom element in general:
with the empty context every `x` is transparent (in particular `bot`), yet the
paper's `LCi` is true everywhere, so it does not entail `bot`. -/
theorem lemma1_paper_candidate_fails :
    ∃ (Envs : Env Unit Unit → Prop) (C : Unit → Prop),
      (∀ Ψ, Envs Ψ → Ext Ψ) ∧ Tr Envs C bot ∧ ¬ le (lc1Paper Envs) bot := by
  refine ⟨fun Ψ => Ψ = (fun x w => x w ()), fun _ => False, ?_, ?_, ?_⟩
  · intro Ψ hΨ x y w h; subst hΨ; simp [h]
  · intro Ψ _ γ w hw; exact absurd hw id
  · intro h
    have hp : lc1Paper (fun Ψ : Env Unit Unit => Ψ = (fun x w => x w ())) () () = true := by
      simp only [lc1Paper, decide_eq_true_eq]
      refine ⟨(fun (x : Val Unit Unit) (w : Unit) => x w ()), rfl, top, ?_⟩
      simp [meet, bot, top]
    have := h () () hp
    simp [bot] at this

/-! ## Lemma 4 : point-wise construction of local contexts -/
theorem lemma4 {Envs : Env W D → Prop} (hE : ∀ Ψ, Envs Ψ → Ext Ψ) {C : W → Prop}
    (hloc : ∀ w, C w → ∃ s : D → Bool,
      Tr Envs (fun v => v = w) (fun _ => s) ∧
      ∀ y, Tr Envs (fun v => v = w) y → ∀ d, s d = true → y w d = true) :
    ∃ x, IsLC Envs C x := by
  classical
  have hex : ∀ w, ∃ s : D → Bool, C w → (Tr Envs (fun v => v = w) (fun _ => s) ∧
      ∀ y, Tr Envs (fun v => v = w) y → ∀ d, s d = true → y w d = true) := by
    intro w
    by_cases h : C w
    · obtain ⟨s, hs⟩ := hloc w h
      exact ⟨s, fun _ => hs⟩
    · exact ⟨fun _ => false, fun h' => absurd h' h⟩
  let f : W → D → Bool := fun w => Classical.choose (hex w)
  have hf : ∀ w, C w → (Tr Envs (fun v => v = w) (fun _ => f w) ∧
      ∀ y, Tr Envs (fun v => v = w) y → ∀ d, f w d = true → y w d = true) :=
    fun w => Classical.choose_spec (hex w)
  let x : Val W D := fun w d => if C w then f w d else false
  refine ⟨x, ?_, ?_⟩
  · intro Ψ hΨ γ w hw
    have h1 := (hf w hw).1 Ψ hΨ γ w rfl
    rw [← h1]
    apply hE Ψ hΨ
    funext d
    simp [meet, x, hw]
  · intro y hy w d hxd
    by_cases hw : C w
    · simp [x, hw] at hxd
      apply (hf w hw).2 y _ d hxd
      intro Ψ hΨ γ v hv
      subst hv
      exact hy Ψ hΨ γ v hw
    · simp [x, hw] at hxd

/-! ## Existence theorem 16(b), abstract form -/
theorem existence {Envs : Env W D → Prop} (hE : ∀ Ψ, Envs Ψ → Ext Ψ)
    (hD : ∃ L : List (D → Bool), ∀ s, s ∈ L) (C : W → Prop) :
    ∃ x, IsLC Envs C x := by
  obtain ⟨L, hL⟩ := hD
  apply lemma4 hE
  intro w _
  obtain ⟨s, hs, hmin⟩ := fold_bottom (α := D → Bool) (fun a b d => a d && b d) (fun _ => true)
    (fun s => Tr Envs (fun v => v = w) (fun _ => s)) (fun a b => ∀ d, a d = true → b d = true)
    (tr_top Envs (fun v => v = w))
    (by
      intro a b ha hb
      exact lemma2 ha hb)
    (by intro a b d h; simp at h; exact h.1)
    (by intro a b d h; simp at h; exact h.2)
    (by intro a b c h1 h2 d h; exact h2 d (h1 d h)) L
  refine ⟨s, hs, ?_⟩
  intro y hy d hd
  have hyc : Tr Envs (fun v => v = w) (fun _ => y w) := by
    intro Ψ hΨ γ v hv
    subst hv
    rw [← hy Ψ hΨ γ v rfl]
    apply hE Ψ hΨ
    funext d'; simp [meet]
  exact hmin (y w) (hL _) hyc d hd

/-! ## Definitions 17/18, Lemma 5, Theorem 21 -/
/-- Def. 18a (`Sat'`) for a trigger with presupposition `d`. -/
def SatP (Envs : Env W D → Prop) (C : W → Prop) (d : Val W D) : Prop :=
  ∃ X, Tr Envs C X ∧ ∀ X', le X' X → Tr Envs C X' → cle C X' d

/-- Def. 17a (`Sat`), stated for a bottom element `x = lc`. -/
def SatLC (x d : Val W D) : Prop := le x d

/-- Theorem 21(i): `Sat' ⇔ Transp`, where `Transp` is `Tr Envs C d`. -/
theorem thm21 {Envs : Env W D → Prop} (hE : ∀ Ψ, Envs Ψ → Ext Ψ) {C : W → Prop}
    (d : Val W D) : SatP Envs C d ↔ Tr Envs C d := by
  constructor
  · rintro ⟨X, hX, hX'⟩
    have hle : cle C X d := hX' X (le_refl X) hX
    intro Ψ hΨ γ w hw
    have h1 := hX Ψ hΨ (meet d γ) w hw
    have h2 := hX Ψ hΨ γ w hw
    rw [← h2, ← h1]
    apply hE Ψ hΨ
    funext e
    have := hle w hw e
    by_cases hx : X w e = true
    · have := this hx; simp [meet, hx, this]
    · have : X w e = false := by simpa using hx
      simp [meet, this]
  · intro h
    refine ⟨d, h, ?_⟩
    intro X' hle _ w _ e hx
    exact hle w e hx

/-- Lemma 5: when the local context `x` exists, `Sat ⇔ Sat'`. -/
theorem lemma5 {Envs : Env W D → Prop} (hE : ∀ Ψ, Envs Ψ → Ext Ψ) {C : W → Prop}
    {x : Val W D} (hx : IsLC Envs C x) (d : Val W D) : SatLC x d ↔ SatP Envs C d := by
  constructor
  · intro h
    refine ⟨x, hx.1, ?_⟩
    intro X' hle _ w _ e hX'
    exact h w e (hle w e hX')
  · intro h
    exact hx.2 d ((thm21 hE d).mp h)

/-! ## Theorem 20 : incremental vs symmetric -/
/-- 20a : `tr_i ⊆ tr_s` (the symmetric environments are among the incremental ones). -/
theorem thm20a {Es Ei : Env W D → Prop} (h : ∀ Ψ, Es Ψ → Ei Ψ) {C : W → Prop} {x : Val W D}
    (hx : Tr Ei C x) : Tr Es C x :=
  fun Ψ hΨ => hx Ψ (h Ψ hΨ)

/-- 20b/20c : if both local contexts exist, `lc_s ≤ lc_i`, and `Sat_i → Sat_s`. -/
theorem thm20bc {Es Ei : Env W D → Prop} (h : ∀ Ψ, Es Ψ → Ei Ψ) {C : W → Prop}
    {xs xi : Val W D} (hs : IsLC Es C xs) (hi : IsLC Ei C xi) (d : Val W D) :
    le xs xi ∧ (SatLC xi d → SatLC xs d) :=
  ⟨hs.2 xi (thm20a h hi.1), fun H => le_trans (hs.2 xi (thm20a h hi.1)) H⟩

end LC