import Mathlib.Order.Basic
import Mathlib.Tactic
import Logic.Syntax
import Kripke.Frame
import Beth.Coverage
universe u
namespace Beth
class BethFrame (W : Type u) extends HasCoverage W, Kripke.Frame W where
sheaf_condition : ∀ {i : ℕ} {w : W} {S : Sieve w} (_S_covers : covers w S), (∀ q ∈ S , val q i) → val w i
nonempty_covers : ∀ {w : W} {S : Sieve w}, covers w S → Nonempty S.carrier
open BethFrame
open Frame
open Syntax
open Tm
def at_world {W : Type u} [BethFrame 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 =>
∃ (S : Sieve w), covers w S ∧ (∀ w' ∈ S, 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} [BethFrame 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 => by
simp
obtain ⟨S, cov, pf⟩ := t_at_w
let covers_w' : covers w' (pullback le S) := covers_stable cov le
exists pullback le S
constructorleftW : Type uw : Ww' : W
· exact covers_w'
· intro v hv
simp [pullback] at hvrightW : Type uw : Ww' : Wv : W
apply pf
exact hv.1
| 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 sheaf_term {W : Type u} [BethFrame W] {w : W} {S : Sieve w} (S_covers : covers w S) (tm : Tm) : (∀ w' ∈ S , at_world w' tm) → at_world w tm :=
match tm with
| var n => sheaf_condition S_covers
| Tm.and p q => by
intro pq_on_S
constructorleftW : Type uw : W
· apply sheaf_term S_covers p
intro s s_in_S
exact (pq_on_S s s_in_S).1
· apply sheaf_term S_covers q
intro s s_in_S
exact (pq_on_S s s_in_S).2
| Tm.or p q => by
intro p_or_q_on_S
have h_ex (w' : S.carrier) : ∃ (S' : Sieve (w' : W)), covers (w' : W) S' ∧
(∀ v ∈ S', at_world v p ∨ at_world v q) := p_or_q_on_S w' w'.property
choose f_sieve f_spec using h_ex
let S_gl := glue_sieves S f_sieve
simp
exists S_gl
constructorleft
· apply covers_glue f_sieve S_covers (fun q => (f_spec q).1)
· intro v hv
let ⟨q, hgv⟩ := hv
exact (f_spec q).2 v hgv
| Tm.imp p q => by
intro hS w' w_le_w' p_at_w'
have pullback_covers : covers w' (pullback w_le_w' S) := by
apply covers_stable
exact S_covers
apply sheaf_term pullback_covers q
intro w'' hw''
simp [pullback] at hw''W : Type uw : Ww' : Ww'' : W
apply hS w'' hw''.1 w'' (le_refl w'')W : Type uw : Ww' : Ww'' : W
apply mono_at hw''.2 p_at_w'
| tt => by
intro _
trivial
| ff => by
intro ff_on_S
obtain ⟨⟨w', hw'⟩⟩ := nonempty_covers S_covers
exact ff_on_S w' hw'
def all_at_world {W : Type u} [BethFrame 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} [BethFrame W] {w : W} (Δ Γ : Ctxt) :
all_at_world w (Δ ++ Γ) → all_at_world w Γ := by
induction Δ with
| nil =>
simp
| cons t Δ ih =>consW : Type uw : W
intro hconsW : Type uw : W
simp [all_at_world] at hconsW : Type uw : W
exact ih h.2
lemma all_at_of_suffix {W : Type u} [BethFrame W] {w : W} {Γ Δ : Ctxt} (h : Γ ≤ Δ) :
all_at_world w Δ → all_at_world w Γ := by
rcases h with ⟨xs, rfl⟩
exact all_at_append_left xs Γ
def mono_all {W : Type u} [BethFrame 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) [BethFrame W] (Γ : Ctxt) (t : Tm) : Prop :=
∀ (w : W), all_at_world w Γ → at_world w t
def SemEntails (Γ : Ctxt) (t : Tm) : Prop :=
∀ (W : Type u) [BethFrame W] (w : W), all_at_world w Γ → at_world w t
namespace Semantics
section ProofRules
def assumption : Entails W (p :: Γ) p := fun _ 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 or_I₁ : Entails W Γ p → Entails W Γ (p ∨ q) := by
intro p_holds w' all_w'
simp
exists maximal_sieve w'W : Type uw' : W
constructorleftW : Type uw' : W
·leftW : Type uw' : W apply covers_maximal
· intro v hv
have le : w' ≤ v := hv
left
apply p_holds vright.hW : Type uw' : Wv : W
apply mono_all le all_w'
def or_I₂ : Entails W Γ q → Entails W Γ (p ∨ q) := by
intro q_holds w' all_w'
simp
exists maximal_sieve w'W : Type uw' : W
constructorleftW : Type uw' : W
·leftW : Type uw' : W apply covers_maximal
· intro v hv
have le : w' ≤ v := hv
right
apply q_holds vright.hW : Type uw' : Wv : W
apply mono_all le all_w'
def or_E : Entails W Γ (p ∨ q) → Entails W (p :: Γ) c → Entails W (q :: Γ) c → Entails W Γ c := by
intro p_or_q c_ass_p c_ass_q w' all_w'
let ⟨S, S_cov, pq_sem⟩ := p_or_q w' all_w'
apply sheaf_term S_cov
intro v hv
let le : w' ≤ v := S.bounded hvaW : Type uw' : Wv : W
match pq_sem v hv with
| Or.inl p_holds =>W : Type uw' : Wv : W
apply c_ass_p vW : Type uw' : Wv : W
constructorleftW : Type uw' : Wv : WrightW : Type uw' : Wv : W
·leftW : Type uw' : Wv : W exact p_holds
·rightW : Type uw' : Wv : W exact (mono_all le all_w')
| Or.inr q_holds =>W : Type uw' : Wv : W
apply c_ass_q vW : Type uw' : Wv : W
constructorleftW : Type uw' : Wv : WrightW : Type uw' : Wv : W
·leftW : Type uw' : Wv : W exact q_holds
·rightW : Type uw' : Wv : W exact (mono_all le all_w')
def imp_I : Entails W (p :: Γ) q → Entails W Γ (p ⇒ q) :=
fun q_ass_p _w' all_w' v w_le_v p_at_v =>
q_ass_p v ⟨p_at_v, mono_all w_le_v all_w'⟩
def imp_E : Entails W Γ (p ⇒ q) → Entails W Γ p → Entails W Γ q :=
fun q_if_p p_holds w' all_w' =>
q_if_p w' all_w' w' (le_refl w') (p_holds w' all_w')
end ProofRules
end Semantics