import Logic.Syntax
import Beth.Semantics

universe u

namespace Beth

open Syntax

open Pf

def soundness {W : Type u}[BethFrame W] {Γ : Ctxt}{tm : Tm} : Pf Γ tm  → Entails W Γ tm
  | Pf.assume =>
W : Type u
inst✝ : BethFrame W
Γ : Ctxt
tm✝ : Tm
tm : Tm
Γ✝ : Ctxt
⊢ Entails W (tm :: Γ✝) tm by
W : Type u
inst✝ : BethFrame W
Γ : Ctxt
tm✝ : Tm
tm : Tm
Γ✝ : Ctxt
⊢ Entails W (tm :: Γ✝) tm
      apply Semantics.assumption
  | Pf.wk le pf =>
W : Type u
inst✝ : BethFrame W
Γ✝¹ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
Γ✝ : Ctxt
le : Γ✝ ≤ Γ
pf : Pf Γ✝ tm
⊢ Entails W Γ tm by
W : Type u
inst✝ : BethFrame W
Γ✝¹ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
Γ✝ : Ctxt
le : Γ✝ ≤ Γ
pf : Pf Γ✝ tm
⊢ Entails W Γ tm
      apply Semantics.wk
a
W : Type u
inst✝ : BethFrame W
Γ✝¹ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
Γ✝ : Ctxt
le : Γ✝ ≤ Γ
pf : Pf Γ✝ tm
⊢ ?Γ ≤ Γ
a
W : Type u
inst✝ : BethFrame W
Γ✝¹ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
Γ✝ : Ctxt
le : Γ✝ ≤ Γ
pf : Pf Γ✝ tm
⊢ Entails W ?Γ tm
Γ
W : Type u
inst✝ : BethFrame W
Γ✝¹ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
Γ✝ : Ctxt
le : Γ✝ ≤ Γ
pf : Pf Γ✝ tm
⊢ Ctxt
      exact le
a
W : Type u
inst✝ : BethFrame W
Γ✝¹ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
Γ✝ : Ctxt
le : Γ✝ ≤ Γ
pf : Pf Γ✝ tm
⊢ Entails W ?Γ tm
      apply soundness pf
  | Pf.and_I p q =>
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm : Tm
Γ : Ctxt
P✝ : Tm
Q✝ : Tm
p : Pf Γ P✝
q : Pf Γ Q✝
⊢ Entails W Γ (P✝ ∧ Q✝) by
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm : Tm
Γ : Ctxt
P✝ : Tm
Q✝ : Tm
p : Pf Γ P✝
q : Pf Γ Q✝
⊢ Entails W Γ (P✝ ∧ Q✝)
      apply Semantics.and_I
a
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm : Tm
Γ : Ctxt
P✝ : Tm
Q✝ : Tm
p : Pf Γ P✝
q : Pf Γ Q✝
⊢ Entails W Γ P✝
a
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm : Tm
Γ : Ctxt
P✝ : Tm
Q✝ : Tm
p : Pf Γ P✝
q : Pf Γ Q✝
⊢ Entails W Γ Q✝
      apply soundness p
a
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm : Tm
Γ : Ctxt
P✝ : Tm
Q✝ : Tm
p : Pf Γ P✝
q : Pf Γ Q✝
⊢ Entails W Γ Q✝
      apply soundness q
  | Pf.and_E₁ p =>
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
Q✝ : Tm
p : Pf Γ (tm ∧ Q✝)
⊢ Entails W Γ tm by
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
Q✝ : Tm
p : Pf Γ (tm ∧ Q✝)
⊢ Entails W Γ tm
      apply Semantics.and_E₁
a
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
Q✝ : Tm
p : Pf Γ (tm ∧ Q✝)
⊢ Entails W Γ (tm ∧ ?q)
q
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
Q✝ : Tm
p : Pf Γ (tm ∧ Q✝)
⊢ Tm
      apply soundness p
  | Pf.and_E₂ p =>
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
P✝ : Tm
p : Pf Γ (P✝ ∧ tm)
⊢ Entails W Γ tm by
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
P✝ : Tm
p : Pf Γ (P✝ ∧ tm)
⊢ Entails W Γ tm
      apply Semantics.and_E₂
a
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
P✝ : Tm
p : Pf Γ (P✝ ∧ tm)
⊢ Entails W Γ (?p ∧ tm)
p
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
P✝ : Tm
p : Pf Γ (P✝ ∧ tm)
⊢ Tm
      apply soundness p
  | or_I₁ p =>
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm : Tm
Γ : Ctxt
P✝ : Tm
Q✝ : Tm
p : Pf Γ P✝
⊢ Entails W Γ (P✝ ∨ Q✝) by
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm : Tm
Γ : Ctxt
P✝ : Tm
Q✝ : Tm
p : Pf Γ P✝
⊢ Entails W Γ (P✝ ∨ Q✝)
      apply Semantics.or_I₁
a
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm : Tm
Γ : Ctxt
P✝ : Tm
Q✝ : Tm
p : Pf Γ P✝
⊢ Entails W Γ P✝
      apply soundness p
  | or_I₂ q =>
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm : Tm
Γ : Ctxt
P✝ : Tm
Q✝ : Tm
q : Pf Γ Q✝
⊢ Entails W Γ (P✝ ∨ Q✝) by
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm : Tm
Γ : Ctxt
P✝ : Tm
Q✝ : Tm
q : Pf Γ Q✝
⊢ Entails W Γ (P✝ ∨ Q✝)
      apply Semantics.or_I₂
a
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm : Tm
Γ : Ctxt
P✝ : Tm
Q✝ : Tm
q : Pf Γ Q✝
⊢ Entails W Γ Q✝
      apply soundness q
  | or_E p_or_q c_ass_p c_ass_q =>
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
P✝ : Tm
Q✝ : Tm
p_or_q : Pf Γ (P✝ ∨ Q✝)
c_ass_p : Pf (P✝ :: Γ) tm
c_ass_q : Pf (Q✝ :: Γ) tm
⊢ Entails W Γ tm by
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
P✝ : Tm
Q✝ : Tm
p_or_q : Pf Γ (P✝ ∨ Q✝)
c_ass_p : Pf (P✝ :: Γ) tm
c_ass_q : Pf (Q✝ :: Γ) tm
⊢ Entails W Γ tm
      apply Semantics.or_E
a
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
P✝ : Tm
Q✝ : Tm
p_or_q : Pf Γ (P✝ ∨ Q✝)
c_ass_p : Pf (P✝ :: Γ) tm
c_ass_q : Pf (Q✝ :: Γ) tm
⊢ Entails W Γ (?p ∨ ?q)
a
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
P✝ : Tm
Q✝ : Tm
p_or_q : Pf Γ (P✝ ∨ Q✝)
c_ass_p : Pf (P✝ :: Γ) tm
c_ass_q : Pf (Q✝ :: Γ) tm
⊢ Entails W (?p :: Γ) tm
a
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
P✝ : Tm
Q✝ : Tm
p_or_q : Pf Γ (P✝ ∨ Q✝)
c_ass_p : Pf (P✝ :: Γ) tm
c_ass_q : Pf (Q✝ :: Γ) tm
⊢ Entails W (?q :: Γ) tm
p
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
P✝ : Tm
Q✝ : Tm
p_or_q : Pf Γ (P✝ ∨ Q✝)
c_ass_p : Pf (P✝ :: Γ) tm
c_ass_q : Pf (Q✝ :: Γ) tm
⊢ Tm
q
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
P✝ : Tm
Q✝ : Tm
p_or_q : Pf Γ (P✝ ∨ Q✝)
c_ass_p : Pf (P✝ :: Γ) tm
c_ass_q : Pf (Q✝ :: Γ) tm
⊢ Tm
      apply soundness p_or_q
a
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
P✝ : Tm
Q✝ : Tm
p_or_q : Pf Γ (P✝ ∨ Q✝)
c_ass_p : Pf (P✝ :: Γ) tm
c_ass_q : Pf (Q✝ :: Γ) tm
⊢ Entails W (?p :: Γ) tm
a
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
P✝ : Tm
Q✝ : Tm
p_or_q : Pf Γ (P✝ ∨ Q✝)
c_ass_p : Pf (P✝ :: Γ) tm
c_ass_q : Pf (Q✝ :: Γ) tm
⊢ Entails W (?q :: Γ) tm
      apply soundness c_ass_p
a
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
P✝ : Tm
Q✝ : Tm
p_or_q : Pf Γ (P✝ ∨ Q✝)
c_ass_p : Pf (P✝ :: Γ) tm
c_ass_q : Pf (Q✝ :: Γ) tm
⊢ Entails W (?q :: Γ) tm
      apply soundness c_ass_q
  | Pf.imp_I p =>
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm : Tm
Γ : Ctxt
P✝ : Tm
Q✝ : Tm
p : Pf (P✝ :: Γ) Q✝
⊢ Entails W Γ (P✝ ⇒ Q✝) by
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm : Tm
Γ : Ctxt
P✝ : Tm
Q✝ : Tm
p : Pf (P✝ :: Γ) Q✝
⊢ Entails W Γ (P✝ ⇒ Q✝)
      apply Semantics.imp_I
a
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm : Tm
Γ : Ctxt
P✝ : Tm
Q✝ : Tm
p : Pf (P✝ :: Γ) Q✝
⊢ Entails W (P✝ :: Γ) Q✝
      apply soundness p
  | Pf.imp_E p q =>
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
P✝ : Tm
p : Pf Γ (P✝ ⇒ tm)
q : Pf Γ P✝
⊢ Entails W Γ tm by
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
P✝ : Tm
p : Pf Γ (P✝ ⇒ tm)
q : Pf Γ P✝
⊢ Entails W Γ tm
      apply Semantics.imp_E
a
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
P✝ : Tm
p : Pf Γ (P✝ ⇒ tm)
q : Pf Γ P✝
⊢ Entails W Γ (?p ⇒ tm)
a
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
P✝ : Tm
p : Pf Γ (P✝ ⇒ tm)
q : Pf Γ P✝
⊢ Entails W Γ ?p
p
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
P✝ : Tm
p : Pf Γ (P✝ ⇒ tm)
q : Pf Γ P✝
⊢ Tm
      apply soundness p
a
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
P✝ : Tm
p : Pf Γ (P✝ ⇒ tm)
q : Pf Γ P✝
⊢ Entails W Γ ?p
      apply soundness q
  | Pf.tt_I => fun _ _ => trivial
  | Pf.ff_E pf =>
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
pf : Pf Γ Tm.ff
⊢ Entails W Γ tm by
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
pf : Pf Γ Tm.ff
⊢ Entails W Γ tm
      apply Semantics.ff_E
a
W : Type u
inst✝ : BethFrame W
Γ✝ : Ctxt
tm✝ : Tm
tm : Tm
Γ : Ctxt
pf : Pf Γ Tm.ff
⊢ Entails W Γ Tm.ff
      apply soundness pf