/-!
# Propositional fragment of L: syntax, classical semantics, syntactic contexts
(Appendix items 1-2.)

Fidelity notes.
* Atoms are *names* `Nat`, interpreted by `I : Nat → W → Bool` (type `<s,t>`).
  A presuppositional expression `p p'` is `trig a b k`: `a`,`b` are the names of `p`,`p'`,
  `k` is the superscript of item 27 (`k = 0` for formulas of L itself; used only by Strong Kleene).
* Binary connectives are one constructor `bin o F G` with `o ∈ {and, or, imp}`.
* "Every proposition is denoted by an atomic expression" (item 3) is the hypothesis
  `Expressive I`, used only where the paper uses it.
* A string `α _ β'` (hole + good final) is modelled by a syntactic context `List Frame`
  (outermost frame first).  A frame is `neg`, `left o G` (hole = left operand, right sibling `G`,
  i.e. part of the good final) or `right o F` (hole = right operand, left sibling `F`,
  i.e. part of α).  A *good final* for the incremental version is any context with the
  same frames except that right siblings of `left` frames are arbitrary
  (`Frame.same`).  See RESULTS.md for the remark about the connective of a `left` frame.
-/
namespace LCProp

inductive Bop where
  | and | or | imp
  deriving DecidableEq

def Bop.eval : Bop → Bool → Bool → Bool
  | .and, a, b => a && b
  | .or, a, b => a || b
  | .imp, a, b => !a || b

/-- value of the left operand that lets the right operand matter -/
def Bop.need : Bop → Bool
  | .and => true | .or => false | .imp => true

/-- right sibling value that makes the hole "neutral" (identity or negation) -/
def Bop.neut : Bop → Bool
  | .and => true | .or => false | .imp => false

inductive Form where
  | atom (a : Nat)
  | trig (a b k : Nat)
  | neg (F : Form)
  | bin (o : Bop) (F G : Form)

def Form.trigFree : Form → Prop
  | .atom _ => True
  | .trig .. => False
  | .neg F => F.trigFree
  | .bin _ F G => F.trigFree ∧ G.trigFree

/-- a formula that is true in every world -/
def Form.tt : Form := .bin .imp (.atom 0) (.atom 0)
/-- a formula that is false in every world -/
def Form.ff : Form := .neg Form.tt

theorem Form.tt_trigFree : Form.tt.trigFree := ⟨trivial, trivial⟩
theorem Form.ff_trigFree : Form.ff.trigFree := Form.tt_trigFree

variable {W : Type}

/-- Item 2: classical semantics `I` (a presuppositional `pp'` is the conjunction). -/
def ev (I : Nat → W → Bool) : Form → W → Bool
  | .atom a, w => I a w
  | .trig a b _, w => I a w && I b w
  | .neg F, w => !ev I F w
  | .bin o F G, w => o.eval (ev I F w) (ev I G w)

theorem ev_tt (I : Nat → W → Bool) (w : W) : ev I Form.tt w = true := by
  simp [Form.tt, ev, Bop.eval]
theorem ev_ff (I : Nat → W → Bool) (w : W) : ev I Form.ff w = false := by
  simp [Form.ff, ev_tt, ev]

/-- `Expressivity` (item 3), propositional part. -/
def Expressive (I : Nat → W → Bool) : Prop := ∀ f : W → Bool, ∃ n, I n = f

/-! ## syntactic contexts -/
inductive Frame where
  | neg
  | left (o : Bop) (G : Form)
  | right (o : Bop) (F : Form)

def Frame.fill : Frame → Form → Form
  | .neg, x => .neg x
  | .left o G, x => .bin o x G
  | .right o F, x => .bin o F x

/-- `plug K x`: fill the hole of context `K` (outermost frame first) with `x`. -/
def plug : List Frame → Form → Form
  | [], x => x
  | f :: K, x => f.fill (plug K x)

/-- Same "α" (left part), possibly different "β'" (right siblings). -/
def Frame.same : Frame → Frame → Prop
  | .neg, .neg => True
  | .left o _, .left o' _ => o = o'
  | .right o F, .right o' F' => o = o' ∧ F = F'
  | _, _ => False

/-- right siblings of the new final must not contain triggers (`β'` "without underlined material") -/
def Frame.tf : Frame → Prop
  | .left _ G => G.trigFree
  | _ => True

def Frame.sameTF (f f' : Frame) : Prop := f.same f' ∧ f'.tf

/-- pointwise relation on lists (`List.Forall₂` is not in core Lean) -/
inductive F2 {α : Type} (R : α → α → Prop) : List α → List α → Prop where
  | nil : F2 R [] []
  | cons {a b : α} {l l' : List α} : R a b → F2 R l l' → F2 R (a :: l) (b :: l')

/-- occurrences of presuppositional expressions: (context, a, b, k). -/
def occs : Form → List (List Frame × Nat × Nat × Nat)
  | .atom _ => []
  | .trig a b k => [([], a, b, k)]
  | .neg F => (occs F).map (fun t => (Frame.neg :: t.1, t.2))
  | .bin o F G => (occs F).map (fun t => (Frame.left o G :: t.1, t.2)) ++
                  (occs G).map (fun t => (Frame.right o F :: t.1, t.2))

/-- sanity: every occurrence is an actual decomposition `F = α (trig a b k) β`. -/
theorem occs_plug : ∀ (F : Form) (t : List Frame × Nat × Nat × Nat), t ∈ occs F →
    plug t.1 (.trig t.2.1 t.2.2.1 t.2.2.2) = F := by
  intro F
  induction F with
  | atom a => intro t h; simp [occs] at h
  | trig a b k => intro t h; simp [occs] at h; subst h; rfl
  | neg F ih =>
    intro t h
    simp only [occs, List.mem_map] at h
    obtain ⟨u, hu, rfl⟩ := h
    simp [plug, Frame.fill, ih u hu]
  | bin o F G ihF ihG =>
    intro t h
    simp only [occs, List.mem_append, List.mem_map] at h
    rcases h with ⟨u, hu, rfl⟩ | ⟨u, hu, rfl⟩
    · simp [plug, Frame.fill, ihF u hu]
    · simp [plug, Frame.fill, ihG u hu]

/-! ## truth value of a context at a world -/
def Frame.fn (I : Nat → W → Bool) (w : W) : Frame → Bool → Bool
  | .neg, b => !b
  | .left o G, b => o.eval b (ev I G w)
  | .right o F, b => o.eval (ev I F w) b

def applyK (I : Nat → W → Bool) (w : W) : List Frame → Bool → Bool
  | [], b => b
  | f :: K, b => f.fn I w (applyK I w K b)

theorem ev_plug (I : Nat → W → Bool) (w : W) : ∀ (K : List Frame) (x : Form),
    ev I (plug K x) w = applyK I w K (ev I x w) := by
  intro K
  induction K with
  | nil => intro x; rfl
  | cons f K ih => intro x; cases f <;> simp [plug, Frame.fill, applyK, Frame.fn, ev, ih]

theorem Frame.same_cases {f f' : Frame} (h : f.same f') :
    (f = .neg ∧ f' = .neg) ∨ (∃ o G G', f = .left o G ∧ f' = .left o G') ∨
    (∃ o F, f = .right o F ∧ f' = .right o F) := by
  cases f with
  | neg => cases f' with
    | neg => exact Or.inl ⟨rfl, rfl⟩
    | left _ _ => exact absurd h id
    | right _ _ => exact absurd h id
  | left o G => cases f' with
    | neg => exact absurd h id
    | left o' G' =>
      have h' : o = o' := h
      subst h'; exact Or.inr (Or.inl ⟨o, G, G', rfl, rfl⟩)
    | right _ _ => exact absurd h id
  | right o F => cases f' with
    | neg => exact absurd h id
    | left _ _ => exact absurd h id
    | right o' F' =>
      have h' : o = o' ∧ F = F' := h
      obtain ⟨h1, h2⟩ := h'
      subst h1; subst h2; exact Or.inr (Or.inr ⟨o, F, rfl, rfl⟩)

end LCProp