import Mathlib.Order.Basic
import Logic.Syntax

universe u

namespace Kripke

class Frame (W : Type u) extends Preorder W where
  val : W → ℕ → Prop
  le_val : ∀ {w w' : W}{i : ℕ}, w ≤ w' → val w i → val w' i

open Frame

open Syntax

open Tm

def at_world {W : Type u} [Frame W] (w : W) (tm : Tm) : Prop :=
  match tm with
  | var v => val w v
  | Tm.and p q => at_world w p ∧ at_world w q
  | Tm.or p q => at_world w p ∨ at_world w q
  | imp p q => ∀ (w' : W), w ≤ w' → at_world w' p → at_world w' q
  | tt => True
  | ff => False

attribute [simp] at_world

def mono_at {W : Type u} [Frame W] {w w' : W} {t : Tm} (le : w ≤ w') (t_at_w : at_world w t)
    : at_world w' t :=
  match t with
  | var _n => le_val le t_at_w
  | Tm.and _p _q => ⟨mono_at le t_at_w.1, mono_at le t_at_w.2⟩
  | Tm.or _p _q => match t_at_w with
      | Or.inl l => Or.inl (mono_at le l)
      | Or.inr r => Or.inr (mono_at le r)
  | Tm.imp _p _q => fun w'' w'_le_w'' p_at_w'' => t_at_w w'' (le_trans le w'_le_w'') p_at_w''
  | tt => trivial
  | ff => False.elim t_at_w

def all_at_world {W : Type u} [Frame W] (w : W) : Ctxt → Prop
  | [] => True
  | (t :: ts) => at_world w t ∧ all_at_world w ts

attribute [simp] all_at_world

lemma all_at_append_left {W : Type u} [Frame W] {w : W} (Δ Γ : Ctxt) :
    all_at_world w (Δ ++ Γ) → all_at_world w Γ := by
W : Type u
inst✝ : Frame W
w : W
Δ : Ctxt
Γ : Ctxt
⊢ all_at_world w (Δ ++ Γ) → all_at_world w Γ
  induction Δ with
  | nil =>
nil
W : Type u
inst✝ : Frame W
w : W
Γ : Ctxt
⊢ all_at_world w ([] ++ Γ) → all_at_world w Γ
      simp
  | cons t Δ ih =>
cons
W : Type u
inst✝ : Frame W
w : W
Γ : Ctxt
t : Tm
Δ : List Tm
ih : all_at_world w (Δ ++ Γ) → all_at_world w Γ
⊢ all_at_world w (t :: Δ ++ Γ) → all_at_world w Γ
      intro h
cons
W : Type u
inst✝ : Frame W
w : W
Γ : Ctxt
t : Tm
Δ : List Tm
ih : all_at_world w (Δ ++ Γ) → all_at_world w Γ
h : all_at_world w (t :: Δ ++ Γ)
⊢ all_at_world w Γ
      simp [all_at_world] at h
cons
W : Type u
inst✝ : Frame W
w : W
Γ : Ctxt
t : Tm
Δ : List Tm
ih : all_at_world w (Δ ++ Γ) → all_at_world w Γ
h : at_world w t ∧ all_at_world w (Δ ++ Γ)
⊢ all_at_world w Γ
      exact ih h.2

lemma all_at_of_suffix {W : Type u} [Frame W] {w : W} {Γ Δ : Ctxt} (h : Γ ≤ Δ) :
    all_at_world w Δ → all_at_world w Γ := by
W : Type u
inst✝ : Frame W
w : W
Γ : Ctxt
Δ : Ctxt
h : Γ ≤ Δ
⊢ all_at_world w Δ → all_at_world w Γ
  rcases h with ⟨xs, rfl⟩
W : Type u
inst✝ : Frame W
w : W
Γ : Ctxt
xs : List Tm
⊢ all_at_world w (xs ++ Γ) → all_at_world w Γ
  exact all_at_append_left xs Γ

def mono_all {W : Type u} [Frame W] {w w' : W} {Γ : Ctxt} (w_le_w' : w ≤ w')
    (Γ_at_w : all_at_world w Γ) : all_at_world w' Γ :=
  match Γ, Γ_at_w with
  | [], _ => trivial
  | _ :: _, ⟨h, t⟩ => ⟨mono_at w_le_w' h, mono_all w_le_w' t⟩

def Entails (W : Type u) [Frame W] (Γ : Ctxt) (t : Tm) : Prop :=
  ∀ (w : W), all_at_world w Γ → at_world w t

def SemEntails (Γ : Ctxt) (t : Tm) : Prop :=
  ∀ (W : Type u) [Frame W] (w : W), all_at_world w Γ → at_world w t

namespace Semantics

section ProofRules

  variable {W : Type u} [Frame W] (w : W) (t p q c : Tm) (Γ Δ : Ctxt)

  def assumption : Entails W (p :: Γ) p := fun _w all => all.1

  def wk : Γ ≤ Δ → Entails W Γ t → Entails W Δ t :=
    fun hΓΔ Γ_to_t w all => Γ_to_t w (all_at_of_suffix hΓΔ all)

  def and_I : Entails W Γ p → Entails W Γ q → Entails W Γ (p ∧ q) :=
    fun p_holds q_holds w all => ⟨p_holds w all, q_holds w all⟩

  def and_E₁ : Entails W Γ (p ∧ q) → Entails W Γ p :=
    fun pq_holds w all => (pq_holds w all).1

  def and_E₂ : Entails W Γ (p ∧ q) → Entails W Γ q :=
    fun pq_holds w all => (pq_holds w all).2

  def or_I₁ : Entails W Γ p → Entails W Γ (p ∨ q) :=
    fun p_holds w all => Or.inl (p_holds w all)

  def or_I₂ : Entails W Γ q → Entails W Γ (p ∨ q) :=
    fun q_holds w all => Or.inr (q_holds w all)

  def or_E : Entails W Γ (p ∨ q) → Entails W (p :: Γ) c → Entails W (q :: Γ) c → Entails W Γ c :=
    fun p_or_q c_ass_p c_ass_q w all => match p_or_q w all with
      | Or.inl p_at_w => c_ass_p w ⟨p_at_w, all⟩
      | Or.inr q_at_w => c_ass_q w ⟨q_at_w, all⟩

  def imp_I : Entails W (p :: Γ) q → Entails W Γ (p ⇒ q) :=
    fun q_ass_p _w all w' w_le_w' p_at_w' =>
      q_ass_p w' ⟨p_at_w', mono_all w_le_w' all⟩

  def imp_E : Entails W Γ (p ⇒ q) → Entails W Γ p → Entails W Γ q :=
    fun q_if_p p_holds w all =>
      q_if_p w all w (le_refl w) (p_holds w all)

  def tt_I : Entails W Γ tt := fun _ _ => trivial

  def ff_E : Entails W Γ ff → Entails W Γ p := by
W : Type u
inst✝ : Frame W
w : W
t : Tm
p : Tm
q : Tm
c : Tm
Γ : Ctxt
Δ : Ctxt
⊢ Entails W Γ ff → Entails W Γ p
    intro ff_at_w w
W : Type u
inst✝ : Frame W
w✝ : W
t : Tm
p : Tm
q : Tm
c : Tm
Γ : Ctxt
Δ : Ctxt
ff_at_w : Entails W Γ ff
w : W
⊢ all_at_world w Γ → at_world w p all_w
W : Type u
inst✝ : Frame W
w✝ : W
t : Tm
p : Tm
q : Tm
c : Tm
Γ : Ctxt
Δ : Ctxt
ff_at_w : Entails W Γ ff
w : W
all_w : all_at_world w Γ
⊢ at_world w p
    exfalso
W : Type u
inst✝ : Frame W
w✝ : W
t : Tm
p : Tm
q : Tm
c : Tm
Γ : Ctxt
Δ : Ctxt
ff_at_w : Entails W Γ ff
w : W
all_w : all_at_world w Γ
⊢ False
    apply ff_at_w w all_w

end ProofRules

end Semantics