import PropSyntax
/-!
# Supervaluations and Strong Kleene (propositional fragment): items 24-31, 40-41

Modelling (see RESULTS.md for fidelity remarks).
* A presuppositional expression is `trig a b k`.  An *extension* of `I` (item 24) is a valuation
  `ρ` of trigger symbols: `AdmK`: whenever `p` (name `a`) is true at `w`, `ρ(pp')(w) = I(p')(w)`;
  where `p` is false, `ρ(pp')(w)` is free.  The *key* of an occurrence says which occurrences
  share a valuation:
    - `symS`: key = symbol `(a,b)` (Supervaluations, item 24-25: all tokens of `pp'` are tied),
    - `tokS`: key = `(a,b,k)` (Strong Kleene, item 27-28: the superscript `k` makes tokens independent).
* Three-valued values are `Option Bool` (`none` = `#`).  `valOpt S` reads the trivalent value off a
  set `S` of achievable bivalent values (true iff only `true` achievable, etc.).
* `numF F n` is `F#` (item 27) but with *global* left-to-right numbering `n, n+1, ...` instead of
  numbering per symbol; since distinct superscripts already make tokens independent this gives the
  same semantics.
-/
namespace LCProp
variable {W : Type}

structure Scheme (K : Type) where
  κ : Nat → Nat → Nat → K
  π : K → Nat × Nat
  hπ : ∀ a b k, π (κ a b k) = (a, b)

def tokS : Scheme (Nat × Nat × Nat) := ⟨fun a b k => (a, b, k), fun x => (x.1, x.2.1), fun _ _ _ => rfl⟩
def symS : Scheme (Nat × Nat) := ⟨fun a b _ => (a, b), id, fun _ _ _ => rfl⟩

/-- evaluation of a formula of `L*` / `L**` under a valuation of trigger keys -/
def evK {K : Type} (I : Nat → W → Bool) (S : Scheme K) (ρ : K → W → Bool) : Form → W → Bool
  | .atom a, w => I a w
  | .trig a b k, w => ρ (S.κ a b k) w
  | .neg F, w => !evK I S ρ F w
  | .bin o F G, w => o.eval (evK I S ρ F w) (evK I S ρ G w)

/-- `ρ` is an extension of `I` (Def. 24, item 3) -/
def AdmK {K : Type} (I : Nat → W → Bool) (S : Scheme K) (ρ : K → W → Bool) : Prop :=
  ∀ a b k w, I a w = true → ρ (S.κ a b k) w = I b w

/-- `v` is a value taken by `F` at `w` in some extension -/
def VK {K : Type} (I : Nat → W → Bool) (S : Scheme K) (F : Form) (w : W) (v : Bool) : Prop :=
  ∃ ρ, AdmK I S ρ ∧ evK I S ρ F w = v

open Classical in
/-- trivalent value read from the set of achievable values (`none` = `#`) -/
noncomputable def valOpt (S : Bool → Prop) : Option Bool :=
  if S true ∧ ¬ S false then some true else if S false ∧ ¬ S true then some false else none

theorem valOpt_eq_some (S : Bool → Prop) (v : Bool) : valOpt S = some v ↔ (S v ∧ ¬ S (!v)) := by
  unfold valOpt
  cases v <;> by_cases h1 : S true <;> by_cases h2 : S false <;> simp [h1, h2]

/-- determinate = not `#` -/
def Det (S : Bool → Prop) : Prop := (S true ∧ ¬ S false) ∨ (S false ∧ ¬ S true)

theorem valOpt_ne_none (S : Bool → Prop) : valOpt S ≠ none ↔ Det S := by
  unfold valOpt Det
  by_cases h1 : S true <;> by_cases h2 : S false <;> simp [h1, h2]

theorem Det_congr {S T : Bool → Prop} (h : ∀ v, S v ↔ T v) : Det S ↔ Det T := by
  unfold Det; rw [h true, h false]

/-- Item 25 / 28 : supervaluationist (tied) value and Strong Kleene (token-independent) value -/
noncomputable def Super (I : Nat → W → Bool) (F : Form) (w : W) : Option Bool :=
  valOpt (VK I symS F w)

/-- number the trigger tokens left to right: `F#` -/
def cnt : Form → Nat
  | .atom _ => 0 | .trig .. => 1 | .neg F => cnt F | .bin _ F G => cnt F + cnt G

def numF : Form → Nat → Form
  | .atom a, _ => .atom a
  | .trig a b _, n => .trig a b n
  | .neg F, n => .neg (numF F n)
  | .bin o F G, n => .bin o (numF F n) (numF G (n + cnt F))

noncomputable def Kleene (I : Nat → W → Bool) (F : Form) (w : W) : Option Bool :=
  valOpt (VK I tokS (numF F 0) w)

/-! ### the canonical extension exists, and Super/Kleene characterisations -/
theorem exists_adm {K : Type} (I : Nat → W → Bool) (S : Scheme K) (c : Bool) :
    ∃ ρ : K → W → Bool, AdmK I S ρ ∧ ∀ x w, I (S.π x).1 w = false → ρ x w = c := by
  refine ⟨fun x w => if I (S.π x).1 w = true then I (S.π x).2 w else c, ?_, ?_⟩
  · intro a b k w h; simp [S.hπ, h]
  · intro x w h; simp [h]

theorem VK_nonempty {K : Type} (I : Nat → W → Bool) (S : Scheme K) (F : Form) (w : W) :
    ∃ v, VK I S F w v := by
  obtain ⟨ρ, hρ, _⟩ := exists_adm I S true
  exact ⟨_, ρ, hρ, rfl⟩

/-- Def. 25: `Super = some v` iff every extension gives `v` -/
theorem super_eq_some_iff (I : Nat → W → Bool) (F : Form) (w : W) (v : Bool) :
    Super I F w = some v ↔ ∀ ρ, AdmK I symS ρ → evK I symS ρ F w = v := by
  unfold Super
  rw [valOpt_eq_some]
  constructor
  · rintro ⟨h1, h2⟩ ρ hρ
    obtain ⟨ρ0, h0, h0'⟩ := h1
    by_cases hv : evK I symS ρ F w = v
    · exact hv
    · exfalso; apply h2
      exact ⟨ρ, hρ, by cases v <;> cases h : evK I symS ρ F w <;> simp_all⟩
  · intro h
    obtain ⟨ρ0, h0, _⟩ := exists_adm I symS true
    refine ⟨⟨ρ0, h0, h ρ0 h0⟩, ?_⟩
    rintro ⟨ρ, hρ, h'⟩
    have := h ρ hρ
    cases v <;> simp_all

theorem kleene_eq_some_iff (I : Nat → W → Bool) (F : Form) (w : W) (v : Bool) :
    Kleene I F w = some v ↔ ∀ ρ, AdmK I tokS ρ → evK I tokS ρ (numF F 0) w = v := by
  unfold Kleene
  rw [valOpt_eq_some]
  constructor
  · rintro ⟨h1, h2⟩ ρ hρ
    by_cases hv : evK I tokS ρ (numF F 0) w = v
    · exact hv
    · exfalso; apply h2
      exact ⟨ρ, hρ, by cases v <;> cases h : evK I tokS ρ (numF F 0) w <;> simp_all⟩
  · intro h
    obtain ⟨ρ0, h0, _⟩ := exists_adm I tokS true
    refine ⟨⟨ρ0, h0, h ρ0 h0⟩, ?_⟩
    rintro ⟨ρ, hρ, h'⟩
    have := h ρ hρ
    cases v <;> simp_all

/-! ## keys, linearity and independence -/
def keys {K : Type} (S : Scheme K) : Form → List K
  | .atom _ => []
  | .trig a b k => [S.κ a b k]
  | .neg F => keys S F
  | .bin _ F G => keys S F ++ keys S G

def LinK {K : Type} (S : Scheme K) : Form → Prop
  | .atom _ => True
  | .trig .. => True
  | .neg F => LinK S F
  | .bin _ F G => LinK S F ∧ LinK S G ∧ ∀ x, x ∈ keys S F → x ∉ keys S G

theorem evK_congr {K : Type} (I : Nat → W → Bool) (S : Scheme K) (ρ ρ' : K → W → Bool) :
    ∀ F : Form, (∀ x, x ∈ keys S F → ρ x = ρ' x) → evK I S ρ F = evK I S ρ' F := by
  intro F
  induction F with
  | atom a => intro _; rfl
  | trig a b k => intro h; funext w; simp [evK, h (S.κ a b k) (by simp [keys])]
  | neg F ih => intro h; funext w; simp [evK, ih h]
  | bin o F G ihF ihG =>
    intro h
    funext w
    have h1 := ihF (fun x hx => h x (by simp [keys, hx]))
    have h2 := ihG (fun x hx => h x (by simp [keys, hx]))
    simp only [evK]
    rw [h1, h2]

theorem vk_neg {K : Type} (I : Nat → W → Bool) (S : Scheme K) (F : Form) (w : W) (v : Bool) :
    VK I S (.neg F) w v ↔ VK I S F w (!v) := by
  constructor
  · rintro ⟨ρ, hρ, h⟩; exact ⟨ρ, hρ, by simp [evK] at h; cases v <;> simp_all⟩
  · rintro ⟨ρ, hρ, h⟩; exact ⟨ρ, hρ, by simp [evK, h]⟩

open Classical in
theorem vk_bin {K : Type} (I : Nat → W → Bool) (S : Scheme K) (o : Bop) (F G : Form)
    (hL : LinK S (.bin o F G)) (w : W) (v : Bool) :
    VK I S (.bin o F G) w v ↔ ∃ v1 v2, VK I S F w v1 ∧ VK I S G w v2 ∧ o.eval v1 v2 = v := by
  constructor
  · rintro ⟨ρ, hρ, h⟩
    exact ⟨_, _, ⟨ρ, hρ, rfl⟩, ⟨ρ, hρ, rfl⟩, h⟩
  · rintro ⟨v1, v2, ⟨ρ1, h1, e1⟩, ⟨ρ2, h2, e2⟩, rfl⟩
    refine ⟨fun x w' => if x ∈ keys S F then ρ1 x w' else ρ2 x w', ?_, ?_⟩
    · intro a b k w' hw'
      by_cases hm : S.κ a b k ∈ keys S F
      · simp [hm, h1 a b k w' hw']
      · simp [hm, h2 a b k w' hw']
    · have c1 : evK I S (fun x w' => if x ∈ keys S F then ρ1 x w' else ρ2 x w') F = evK I S ρ1 F :=
        evK_congr I S _ _ F (fun x hx => by funext w'; simp [hx])
      have c2 : evK I S (fun x w' => if x ∈ keys S F then ρ1 x w' else ρ2 x w') G = evK I S ρ2 G :=
        evK_congr I S _ _ G (fun x hx => by
          funext w'
          have hn : x ∉ keys S F := fun h => hL.2.2 x h hx
          simp [hn])
      simp only [evK]
      rw [c1, c2, e1, e2]

theorem vk_atom {K : Type} (I : Nat → W → Bool) (S : Scheme K) (a : Nat) (w : W) (v : Bool) :
    VK I S (.atom a) w v ↔ I a w = v := by
  constructor
  · rintro ⟨ρ, _, h⟩; exact h
  · intro h; obtain ⟨ρ, hρ, _⟩ := exists_adm I S true; exact ⟨ρ, hρ, h⟩

theorem vk_trig {K : Type} (I : Nat → W → Bool) (S : Scheme K) (a b k : Nat) (w : W) (v : Bool) :
    VK I S (.trig a b k) w v ↔ (I a w = true → v = I b w) := by
  constructor
  · rintro ⟨ρ, hρ, h⟩ ha
    have := hρ a b k w ha
    simp only [evK] at h; rw [this] at h; exact h.symm
  · intro h
    by_cases ha : I a w = true
    · obtain ⟨ρ, hρ, _⟩ := exists_adm I S true
      exact ⟨ρ, hρ, by simp only [evK]; rw [hρ a b k w ha]; exact (h ha).symm⟩
    · have ha' : I a w = false := by simpa using ha
      obtain ⟨ρ, hρ, hρ'⟩ := exists_adm I S v
      exact ⟨ρ, hρ, by simp only [evK]; exact hρ' _ _ (by rw [S.hπ]; exact ha')⟩

/-! ## Standard Strong Kleene (item 40) -/
def skop : Bop → Option Bool → Option Bool → Option Bool
  | .and, some false, _ => some false
  | .and, _, some false => some false
  | .and, some true, some true => some true
  | .and, _, _ => none
  | .or, some true, _ => some true
  | .or, _, some true => some true
  | .or, some false, some false => some false
  | .or, _, _ => none
  | .imp, some false, _ => some true
  | .imp, _, some true => some true
  | .imp, some true, some false => some false
  | .imp, _, _ => none

/-- Standard Strong Kleene: `pp'` is `#` iff `p` is false. -/
def sk (I : Nat → W → Bool) : Form → W → Option Bool
  | .atom a, w => some (I a w)
  | .trig a b _, w => if I a w = true then some (I b w) else none
  | .neg F, w => (sk I F w).map (fun b => !b)
  | .bin o F G, w => skop o (sk I F w) (sk I G w)

/-- the derived clauses of item 40: `or` and `if` follow from `not`/`and`. -/
theorem skop_or_def : ∀ x y : Option Bool,
    skop .or x y = (skop .and (x.map (fun b => !b)) (y.map (fun b => !b))).map (fun b => !b) := by
  intro x y
  rcases x with _ | (_ | _) <;> rcases y with _ | (_ | _) <;> decide
theorem skop_imp_def : ∀ x y : Option Bool,
    skop .imp x y = (skop .and x (y.map (fun b => !b))).map (fun b => !b) := by
  intro x y
  rcases x with _ | (_ | _) <;> rcases y with _ | (_ | _) <;> decide

def code : Option Bool → Bool → Bool
  | none, _ => true
  | some b, v => v == b

theorem code_bin : ∀ (o : Bop) (s1 s2 : Option Bool) (v : Bool),
    (∃ v1 v2, code s1 v1 = true ∧ code s2 v2 = true ∧ o.eval v1 v2 = v) ↔
      code (skop o s1 s2) v = true := by
  intro o s1 s2 v
  cases o <;> rcases s1 with _ | (_ | _) <;> rcases s2 with _ | (_ | _) <;> cases v <;> decide

theorem valOpt_code (s : Option Bool) : valOpt (fun v => code s v = true) = s := by
  cases s with
  | none => simp [valOpt, code]
  | some b => cases b <;> simp [valOpt, code]

theorem vk_sk {K : Type} (I : Nat → W → Bool) (S : Scheme K) :
    ∀ G : Form, LinK S G → ∀ w v, VK I S G w v ↔ code (sk I G w) v = true := by
  intro G
  induction G with
  | atom a => intro _ w v; rw [vk_atom]; cases v <;> cases h : I a w <;> simp [sk, code, h]
  | trig a b k =>
    intro _ w v
    rw [vk_trig]
    by_cases ha : I a w = true
    · cases v <;> cases h : I b w <;> simp [sk, ha, code, h]
    · simp [sk, ha, code]
  | neg F ih =>
    intro hL w v
    rw [vk_neg, ih hL]
    cases h : sk I F w with
    | none => simp [sk, h, code]
    | some b => cases v <;> cases b <;> simp [sk, h, code]
  | bin o F G ihF ihG =>
    intro hL w v
    rw [vk_bin I S o F G hL]
    simp only [sk]
    rw [← code_bin]
    constructor
    · rintro ⟨v1, v2, h1, h2, h⟩
      exact ⟨v1, v2, (ihF hL.1 w v1).mp h1, (ihG hL.2.1 w v2).mp h2, h⟩
    · rintro ⟨v1, v2, h1, h2, h⟩
      exact ⟨v1, v2, (ihF hL.1 w v1).mpr h1, (ihG hL.2.1 w v2).mpr h2, h⟩

theorem valOpt_vk_sk {K : Type} (I : Nat → W → Bool) (S : Scheme K) (G : Form) (hL : LinK S G) (w : W) :
    valOpt (VK I S G w) = sk I G w := by
  have : VK I S G w = fun v => code (sk I G w) v = true := by
    funext v; exact propext (vk_sk I S G hL w v)
  rw [this]; exact valOpt_code _

/-! ### numbering yields linear formulas -/
theorem keys_numF_range (F : Form) : ∀ n x, x ∈ keys tokS (numF F n) → n ≤ x.2.2 ∧ x.2.2 < n + cnt F := by
  induction F with
  | atom a => intro n x h; simp [numF, keys] at h
  | trig a b k => intro n x h; simp [numF, keys, tokS, cnt] at h; subst h; simp [cnt]
  | neg F ih => intro n x h; simpa [numF, keys, cnt] using ih n x h
  | bin o F G ihF ihG =>
    intro n x h
    simp only [numF, keys, List.mem_append] at h
    rcases h with h | h
    · have := ihF n x h; simp [cnt]; omega
    · have := ihG (n + cnt F) x h; simp [cnt]; omega

theorem linK_numF (F : Form) : ∀ n, LinK tokS (numF F n) := by
  induction F with
  | atom a => intro n; trivial
  | trig a b k => intro n; trivial
  | neg F ih => intro n; exact ih n
  | bin o F G ihF ihG =>
    intro n
    refine ⟨ihF n, ihG _, ?_⟩
    intro x hx hx'
    have h1 := keys_numF_range F n x hx
    have h2 := keys_numF_range G (n + cnt F) x hx'
    omega

theorem sk_numF (I : Nat → W → Bool) : ∀ (F : Form) (n : Nat), sk I (numF F n) = sk I F := by
  intro F
  induction F with
  | atom a => intro n; rfl
  | trig a b k => intro n; rfl
  | neg F ih => intro n; funext w; simp [numF, sk, ih n]
  | bin o F G ihF ihG => intro n; funext w; simp [numF, sk, ihF n, ihG (n + cnt F)]

/-- **Theorem 41** (propositional fragment): the supervaluationist definition of Strong Kleene
coincides with the standard one. -/
theorem theorem41 (I : Nat → W → Bool) (F : Form) (w : W) : Kleene I F w = sk I F w := by
  unfold Kleene
  rw [valOpt_vk_sk I tokS _ (linK_numF F 0) w, sk_numF]

/-! ### Lemma 6, Lemma 7 -/
/-- items 30: if each symbol occurs at most once, Super = Kleene (= standard Kleene). -/
theorem lemma6 (I : Nat → W → Bool) (F : Form) (hL : LinK symS F) (w : W) :
    Super I F w = Kleene I F w := by
  unfold Super
  rw [valOpt_vk_sk I symS F hL w, theorem41]

theorem evK_tok_sym (I : Nat → W → Bool) (ρ : Nat × Nat → W → Bool) :
    ∀ (F : Form) (n : Nat), evK I tokS (fun x => ρ (x.1, x.2.1)) (numF F n) = evK I symS ρ F := by
  intro F
  induction F with
  | atom a => intro n; rfl
  | trig a b k => intro n; rfl
  | neg F ih => intro n; funext w; simp [numF, evK, ih n]
  | bin o F G ihF ihG => intro n; funext w; simp [numF, evK, ihF n, ihG (n + cnt F)]

theorem vk_sym_sub_tok (I : Nat → W → Bool) (F : Form) (w : W) (v : Bool) :
    VK I symS F w v → VK I tokS (numF F 0) w v := by
  rintro ⟨ρ, hρ, h⟩
  refine ⟨fun x => ρ (x.1, x.2.1), ?_, ?_⟩
  · intro a b k w' h'; exact hρ a b k w' h'
  · rw [evK_tok_sym]; exact h

/-- **Lemma 7**: if `Kleene(F,w) ≠ #` then `Super(F,w) = Kleene(F,w)`. -/
theorem lemma7 (I : Nat → W → Bool) (F : Form) (w : W) (h : Kleene I F w ≠ none) :
    Super I F w = Kleene I F w := by
  cases hk : Kleene I F w with
  | none => exact absurd hk h
  | some v =>
    have h1 := (valOpt_eq_some _ _).mp hk
    unfold Super
    rw [valOpt_eq_some]
    obtain ⟨v0, hv0⟩ := VK_nonempty I symS F w
    have h0 := vk_sym_sub_tok I F w v0 hv0
    have hv : v0 = v := by
      cases v <;> cases v0 <;> simp_all
    subst hv
    exact ⟨hv0, fun h' => h1.2 (vk_sym_sub_tok I F w _ h')⟩

end LCProp