import Logic.Syntax
import Kripke.Frame
import Beth.Semantics
import Beth.Soundness
import Beth.Coverage
import Mathlib.Order.Basic
import Mathlib.Data.Finset.Basic
namespace Beth
namespace Completeness
instance : Preorder World where
le Γ Δ := Γ.carrier ≤ Δ.carrier
le_refl _ := le_rfl
le_trans _ _ _ := le_trans
def context_sieve (Γ : World) (L : List Tm) : Sieve Γ where
carrier := { Δ : World | (Γ.carrier ≤ Δ.carrier) ∧ (∃ A ∈ L, Pf Δ.carrier A) }
bounded := by
intro Δ hΔ
exact hΔ.1
upward_closed := by
intro Δ Θ hΔ hle
constructorleft
· exact List.IsSuffix.trans hΔ.1 hle
· rcases hΔ.2 with ⟨A, hA, hPf⟩
exact ⟨A, hA, Pf.wk hle hPf⟩
def mk_disjunction : Ctxt → Tm
| [] => Tm.ff
| t :: ts => Tm.or t (mk_disjunction ts)
theorem disjunction_intro {t : Tm} {Γ Δ : Ctxt}
(t_in : t ∈ Δ) (pf : Pf Γ t) : Pf Γ (mk_disjunction Δ) := by
induction Δ with
| nil =>
cases t_in
| cons a Δ ih =>
simp at t_in
rcases t_in with rfl | htcons.inl
· exact Pf.or_I₁ pf
· simpa [mk_disjunction] using Pf.or_I₂ (ih ht)
theorem disjunction_elim {p : Tm} {Γ : Ctxt} (Δ : Ctxt) :
(∀ {t : Tm}, t ∈ Δ → Pf (t :: Γ) p) →
Pf Γ (mk_disjunction Δ) → Pf Γ p := by
intro htcase hΔ
induction Δ generalizing Γ with
| nil =>
simp [mk_disjunction] at hΔ
exact Pf.ff_E hΔ
| cons a Δ ih =>
simp [mk_disjunction] at hΔ
apply Pf.or_E hΔcons.a
· exact htcase (by simp)
· have htail : ∀ {t : Tm}, t ∈ Δ → Pf (t :: mk_disjunction Δ :: Γ) p := by
intro t ht
apply Syntax.Pf.monotone_mem (Γ := t :: Γ)
(Δ := t :: mk_disjunction Δ :: Γ) (P := p)hmem
· intro Q hQ
have : Q = t ∨ Q ∈ Γ := by simpa using hQ
rcases this with rfl | hmemhmem.inl
· simp
· simp [hmem]
· exact htcase (by simpa using Or.inr ht)
exact ih htail Pf.assume
theorem disjunction_two {Γ : Ctxt} {φ ψ : Tm} :
Pf Γ (Tm.or φ ψ) → Pf Γ (mk_disjunction [φ, ψ]) := by
intro h
simp [mk_disjunction]
apply Pf.or_E h
· exact Pf.or_I₁ Pf.assume
· exact Pf.or_I₂ (Pf.or_I₁ Pf.assume)
inductive ContextCovers : (Γ : World) → Sieve Γ → Prop where
| basic (Γ : World) (L : List Tm) {S : Sieve Γ} :
Pf Γ.carrier (mk_disjunction L) →
(context_sieve Γ L).carrier ⊆ S.carrier →
ContextCovers Γ S
| maximal (Γ : World) :
ContextCovers Γ (maximal_sieve Γ)
| trans (Γ : World) (U V : Sieve Γ) :
ContextCovers Γ U →
(∀ q : U.carrier, ContextCovers (q : World) (pullback (U.bounded q.property) V)) →
ContextCovers Γ V
theorem ContextCovers.stable {Γ Δ : World} {U : Sieve Γ} (h : Γ ≤ Δ) :
ContextCovers Γ U → ContextCovers Δ (pullback h U) := by
intro hU
induction hU with
| basic Γ L hpf hsub =>
apply ContextCovers.basic Δ Lbasic.a
· exact Pf.wk h hpf
· intro Θ hΘ
constructorbasic.a.left
· apply hsub
constructorbasic.a.left.a.left
· exact List.IsSuffix.trans h hΘ.1
· exact hΘ.2
· exact hΘ.1
| maximal Γ =>maximal
have hEq : pullback h (maximal_sieve Γ) = maximal_sieve Δ := by
apply Sieve.ext
funext Θ
apply propext
constructorh.h.a.mp
· intro hΘ
exact hΘ.2
· intro hΘ
constructorh.h.a.mpr.left
· exact List.IsSuffix.trans h hΘ
· exact hΘ
simpa [hEq] using ContextCovers.maximal Δ
| trans Γ U V hU hV ihU ihV =>trans
apply ContextCovers.trans Δ (pullback h U)trans.atrans.a
·trans.a exact ihU h
·trans.a intro qtrans.a
have hq : (q : World) ∈ U.carrier := q.property.1trans.a
have q_le : Δ ≤ q := q.property.2trans.a
have hEq :
pullback ((pullback h U).bounded q.property) (pullback h V) =
pullback (U.bounded hq) V := by
apply Sieve.exth
funext rh.h
apply propexth.h.a
constructorh.h.a.mph.h.a.mpr
·h.h.a.mp intro hrh.h.a.mp
exact ⟨hr.1.1, hr.2⟩
·h.h.a.mpr intro hrh.h.a.mpr
simp [pullback] at hrh.h.a.mpr
constructorh.h.a.mpr.lefth.h.a.mpr.right
·h.h.a.mpr.left simp [pullback]h.h.a.mpr.left
exact ⟨hr.1, List.IsSuffix.trans q_le hr.2⟩
·h.h.a.mpr.right exact hr.2
simpa [hEq] using hV ⟨(q : World), hq⟩
def contextCoverage : Coverage World where
covers := ContextCovers
maximal := ContextCovers.maximal
transitive := by⊢ ∀ (p : World) (U V : Sieve p),
ContextCovers p U → (∀ (q : ↑U.carrier), ContextCovers (↑q) (pullback ⋯ V)) → ContextCovers p V
intro p U⊢ ∀ (V : Sieve p), ContextCovers p U → (∀ (q : ↑U.carrier), ContextCovers (↑q) (pullback ⋯ V)) → ContextCovers p V V hU hV
exact ContextCovers.trans p U V hU hV
stability := by⊢ ∀ {p q : World} {U : Sieve p}, ContextCovers p U → ∀ (p_le_q : p ≤ q), ContextCovers q (pullback p_le_q U)
intro p q U hU hpq
exact ContextCovers.stable hpq hU
theorem pf_sheaf {Γ : World} {S : Sieve Γ} {r : Tm} :
ContextCovers Γ S →
(∀ Δ ∈ S.carrier, Pf Δ.carrier r) →
Pf Γ.carrier r := by
intro hCov hS
induction hCovbasicmaximaltrans
case basic Γ0 L S0 hPf hSub =>
refine disjunction_elim (Γ := Γ0.carrier) L ?_ hPf
intro t ht
by_cases hff : Pf (t :: Γ0.carrier) Tm.ffpos
· exact Pf.ff_E hff
· let Δ : World := ⟨t :: Γ0.carrier, hff⟩neg
have hin : Δ ∈ (context_sieve Γ0 L).carrier := by
constructorleftright
·left exact List.suffix_cons t Γ0.carrier
·right exact ⟨t, ht, Pf.assume⟩
exact hS Δ (hSub hin)
case maximal Γ =>
exact hS Γ (show Γ ≤ Γ from le_rfl)
case trans Γ U V hU hV ihU ihV =>
apply ihU
intro Δ hΔ
exact ihV ⟨Δ, hΔ⟩ (fun Θ hΘ => hS Θ hΘ.1)
instance : BethFrame World where
coverage := contextCoverage
val w i := Pf w.carrier (Tm.var i)
le_val hle hPf := Pf.wk hle hPf
sheaf_condition := by
intro i w S S_cov var_on_S
exact pf_sheaf S_cov var_on_S
nonempty_covers := by
intro w S hS
change ContextCovers w S at hS
by_contra hne
apply w.consistent
apply pf_sheaf hS
intro Δ hΔ
exact False.elim (hne ⟨Δ, hΔ⟩)
theorem truth_lemma (w : World) : ∀ φ : Tm, at_world w φ ↔ Pf w.carrier φ
| Tm.var i => by
rfl
| Tm.and φ ψ => by
constructor
· intro h
exact Pf.and_I ((truth_lemma w φ).1 h.1) ((truth_lemma w ψ).1 h.2)
· intro h
constructor
· rw [truth_lemma w φ]
exact Pf.and_E₁ h
· rw [truth_lemma w ψ]
exact Pf.and_E₂ h
| Tm.or φ ψ => by
constructor
· intro h
rcases h with ⟨S, hS, hLocal⟩
change ContextCovers w S at hS
apply pf_sheaf hS
intro Δ hΔ
rcases hLocal Δ hΔ with hφ | hψmp.inl
· apply Pf.or_I₁
rw [<- truth_lemma Δ φ]
exact hφ
· apply Pf.or_I₂
rw [<- truth_lemma Δ ψ]
exact hψ
· intro h
refine ⟨context_sieve w [φ, ψ], ?_, ?_⟩
· change ContextCovers w (context_sieve w [φ, ψ])
apply ContextCovers.basic w [φ, ψ]
· exact disjunction_two h
· apply subset_rfl
· intro Δ hΔ
rcases hΔ.2 with ⟨A, hA, hPf⟩
simp at hA
rcases hA with hA | hAmpr.refine_2.inl
· subst A
apply Or.inl
rw [truth_lemma Δ φ]
exact hPf
· subst A
apply Or.inr
rw [truth_lemma Δ ψ]
exact hPf
| Tm.imp φ ψ => by
constructor
· intro hImp
by_cases hff : Pf (φ :: w.carrier) Tm.ffpos
· exact Pf.imp_I (Pf.ff_E hff)
· let v : World := ⟨φ :: w.carrier, hff⟩
have hwv : w ≤ v := List.suffix_cons φ w.carrier
have hφv : at_world v φ := (truth_lemma v φ).2 Pf.assume
have hψv : at_world v ψ := hImp v hwv hφv
exact Pf.imp_I ((truth_lemma v ψ).1 hψv)
· intro hImp v hwv hφv
have hImpv : Pf v.carrier (Tm.imp φ ψ) := Pf.wk hwv hImp
have hφp : Pf v.carrier φ := (truth_lemma v φ).1 hφv
exact (truth_lemma v ψ).2 (Pf.imp_E hImpv hφp)
| Tm.tt => by
constructor
· intro _
exact Pf.tt_I
· intro _
trivial
| Tm.ff => by
constructor
· intro h
exact False.elim h
· intro h
exact False.elim (w.consistent h)
theorem all_at_world_self : ∀ w : World, all_at_world w w.carrier := by
intro w
cases w with
| mk carrier consistent =>
induction carrier with
| nil =>
simp
| cons φ Γ ih =>
have htail : ¬ Pf Γ Tm.ff := by
intro hff
exact consistent (Pf.wk (List.suffix_cons φ Γ) hff)
constructor
· rw [truth_lemma ⟨φ :: Γ, consistent⟩ φ]
apply Pf.assume
· have Γ_le : Γ ≤ φ :: Γ := by
apply List.suffix_cons
have w_le : (⟨Γ, htail⟩ : World) ≤ ⟨(φ :: Γ), consistent⟩ := by
exact Γ_le
apply mono_all w_le
apply ih htail
theorem completeness {Γ : Ctxt} {P : Tm} : Beth.SemEntails.{0} Γ P → Pf Γ P := by
intro hsem
by_cases hff : Pf Γ Tm.ff
· exact Pf.ff_E hff
· let w : World := ⟨Γ, hff⟩
have hΓ : all_at_world w Γ := all_at_world_self w
have hP : at_world w P := hsem World w hΓ
rw [<- truth_lemma w P]
exact hP
end Completeness
end Beth