Sequents

Optional loaded formulas (Olfs)

@[reducible, inline]

abbrev Olf : Type

In nodes we optionally have a negated loaded formula on the left or right.

Equations

• Olf = Option (NegLoadFormula ⊕ NegLoadFormula)

def Olf.voc : Olf → Vocab

Equations

• Olf.voc none = ∅
• Olf.voc (some (Sum.inl nlf)) = nlf.voc
• Olf.voc (some (Sum.inr nlf)) = nlf.voc

def Olf.L : Olf → List Formula

Equations

• Olf.L none = []
• Olf.L (some (Sum.inl (~'lf))) = [~lf.unload]
• Olf.L (some (Sum.inr val)) = []

@[simp]

theorem Olf.L_none : L none = []

@[simp]

theorem Olf.L_inr {lf : NegLoadFormula} : L (some (Sum.inr lf)) = []

def Olf.R : Olf → List Formula

Equations

• Olf.R none = []
• Olf.R (some (Sum.inl val)) = []
• Olf.R (some (Sum.inr (~'lf))) = [~lf.unload]

@[simp]

theorem Olf.R_none : R none = []

@[simp]

theorem Olf.R_inl {lf : NegLoadFormula} : R (some (Sum.inl lf)) = []

instance Option.instHasSubsetOption {α : Type u_1} : HasSubset (Option α)

Equations

• Option.instHasSubsetOption = { Subset := fun (o1 o2 : Option α) => match o1, o2 with | none, x => True | some val, none => False | some f, some g => f = g }

@[simp]

theorem Option.some_subseteq {α : Type u_1} {x : α} {O : Option α} : some x ⊆ O ↔ some x = O

instance Option.insHasSdiff {α : Type u_1} [DecidableEq α] : SDiff (Option α)

Instance that is used to say (O : Olf) \ (O' : Olf).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Option.insHasSdiff_none {α : Type u_1} {o : Option α} [DecidableEq α] : none \ o = none

@[simp]

theorem Option.insHasSdiff_remove_none_cancel {α : Type u_1} {o : Option α} [DecidableEq α] : o \ none = o

@[simp]

theorem Option.insHasSdiff_remove_sem_eq_none {α : Type u_1} {x : α} [DecidableEq α] : some x \ some x = none

def Option.overwrite {α : Type u_1} : Option α → Option α → Option α

Equations

• x✝.overwrite none = x✝
• x✝.overwrite (some x_3) = some x_3

def Olf.change (oldO Ocond newO : Olf) : Olf

Equations

• oldO.change Ocond newO = Option.overwrite (oldO \ Ocond) newO

@[simp]

theorem Olf.change_none_none {oldO : Olf} : oldO.change none none = oldO

@[simp]

theorem Olf.change_some {oldO whatever : Olf} {wnlf : NegLoadFormula ⊕ NegLoadFormula} : oldO.change whatever (some wnlf) = some wnlf

@[simp]

theorem Olf.change_some_some_eq {nχ : NegLoadFormula ⊕ NegLoadFormula} {Onew : Olf} : change (some nχ) (some nχ) Onew = Onew

Sequents and their (multi)set quality

def Sequent : Type

A tableau node is labelled with two lists of formulas and an Olf. Each formula is placed on the left or right and up to one formula may be loaded.

Equations

• Sequent = (List Formula × List Formula × Olf)

instance instDecidableEqSequent : DecidableEq Sequent

Equations

• instDecidableEqSequent a b = instDecidableEqProd a b

instance instReprSequent : Repr Sequent

Equations

• instReprSequent = instReprProdOfReprTuple

def Sequent.setEqTo : Sequent → Sequent → Prop

Two Sequents are set-equal when their components are finset-equal. That is, we do not care about the order of the lists, but we do care about the side of the formula and what formual is loaded. Hint: use List.toFinset.ext_iff with this.

Equations

• Sequent.setEqTo (L, R, O) (L', R', O') = (L.toFinset = L'.toFinset ∧ R.toFinset = R'.toFinset ∧ O = O')

instance instDecidableRelSequentSetEqTo : DecidableRel Sequent.setEqTo

Equations

• One or more equations did not get rendered due to their size.

def Sequent.multisetEqTo : Sequent → Sequent → Prop

Two Sequents are multiset-equal when their components are multiset-equal. That is, we do not care about the order of the lists, but we do care about the side on which the formula is, whether it is loaded or not, and how often it occurs.

Equations

• Sequent.multisetEqTo (L, R, O) (L', R', O') = (↑L = ↑L' ∧ ↑R = ↑R' ∧ O = O')

instance instDecidableRelSequentMultisetEqTo : DecidableRel Sequent.multisetEqTo

Equations

• One or more equations did not get rendered due to their size.

theorem Sequent.setEqTo_of_multisetEqTo (X Y : Sequent) : X.multisetEqTo Y → X.setEqTo Y

@[simp]

theorem Sequent.setEqTo_refl (X : Sequent) : X.setEqTo X

theorem Sequent.setEqTo_symm (X Y : Sequent) : X.setEqTo Y ↔ Y.setEqTo X

@[simp]

theorem Sequent.multisetEqTo_refl (X : Sequent) : X.multisetEqTo X

theorem Sequent.multisetEqTo_symm (X Y : Sequent) : X.multisetEqTo Y ↔ Y.multisetEqTo X

def Sequent.toFinset : Sequent → Finset Formula

Equations

• Sequent.toFinset (L, R, O) = L.toFinset ∪ R.toFinset ∪ (Option.map (Sum.elim negUnload negUnload) O).toFinset

Components and sides of sequents

def Sequent.L : Sequent → List Formula

Equations

• Sequent.L (L, R, O) = L

def Sequent.R : Sequent → List Formula

Equations

• Sequent.R (L, R, O) = R

def Sequent.O : Sequent → Olf

Equations

• Sequent.O (L, R, O) = O

def Sequent.left (X : Sequent) : List Formula

Equations

• X.left = X.L ++ X.O.L

def Sequent.right (X : Sequent) : List Formula

Equations

• X.right = X.R ++ X.O.R

Formulas as elements of sequents

instance instMembershipFormulaSequent : Membership Formula Sequent

Equations

• instMembershipFormulaSequent = { mem := fun (X : Sequent) (φ : Formula) => φ ∈ X.L ∨ φ ∈ X.R }

instance instDecidableMemFormulaSequent {φ : Formula} {X : Sequent} : Decidable (φ ∈ X)

Equations

• instDecidableMemFormulaSequent = Prod.casesOn X fun (L : List Formula) (snd : List Formula × Olf) => Prod.casesOn snd fun (R : List Formula) (o : Olf) => id inferInstance

instance instFintypeSubtypeMemSequent {X : Sequent} : Fintype { x : Formula // x ∈ X }

Equations

• One or more equations did not get rendered due to their size.

def NegLoadFormula.mem_Sequent (X : Sequent) (nlf : NegLoadFormula) : Prop

Equations

• NegLoadFormula.mem_Sequent X nlf = (X.O = some (Sum.inl nlf) ∨ X.O = some (Sum.inr nlf))

instance instDecidableMem_SequentMkListFormulaProdOlf {L R : List Formula} {O : Olf} {nlf : NegLoadFormula} : Decidable (NegLoadFormula.mem_Sequent (L, R, O) nlf)

Equations

• instDecidableMem_SequentMkListFormulaProdOlf = if h : O = some (Sum.inl nlf) then isTrue ⋯ else if h2 : O = some (Sum.inr nlf) then isTrue ⋯ else isFalse ⋯

instance instMembershipNegLoadFormulaSequent : Membership NegLoadFormula Sequent

Equations

• instMembershipNegLoadFormulaSequent = { mem := NegLoadFormula.mem_Sequent }

def AnyNegFormula.mem_Sequent (X : Sequent) (anf : AnyNegFormula) : Prop

Equations

• AnyNegFormula.mem_Sequent x✝ (~''(AnyFormula.normal φ)) = (~φ ∈ x✝)
• AnyNegFormula.mem_Sequent x✝ (~''(AnyFormula.loaded χ)) = NegLoadFormula.mem_Sequent x✝ (~'χ)

instance instMembershipAnyNegFormulaSequent : Membership AnyNegFormula Sequent

Equations

• instMembershipAnyNegFormulaSequent = { mem := AnyNegFormula.mem_Sequent }

Closed, basic, loaded and free sequents

def Sequent.closed (X : Sequent) : Prop

A sequent is closed iff it contains ⊥ or contains a formula and its negation.

Equations

• X.closed = (⊥ ∈ X ∨ ∃ f ∈ X, ~f ∈ X)

def Sequent.basic : Sequent → Prop

A sequent is basic iff it only contains basic formulas and is not closed.

Equations

• Sequent.basic (L, R, O) = ((∀ f ∈ L ++ R ++ (Option.map (Sum.elim negUnload negUnload) O).toList, f.basic = true) ∧ ¬Sequent.closed (L, R, O))

instance Fintype.decidableExistsConjFintype {α : Type u_1} {p q : α → Prop} [DecidablePred p] [DecidablePred q] [Fintype (Subtype p)] : Decidable (∃ (a : α), p a ∧ q a)

A variant of Fintype.decidableExistsFintype, used by instDecidableClosed.

Equations

• Fintype.decidableExistsConjFintype = if h : ∃ (x : Subtype p), q ↑x then isTrue ⋯ else isFalse ⋯

instance Sequent.instDecidableClosed {X : Sequent} : Decidable X.closed

Equations

• Sequent.instDecidableClosed = id (if h : ⊥ ∈ X then isTrue ⋯ else if h_1 : ∃ f ∈ X, ~f ∈ X then isTrue ⋯ else isFalse ⋯)

def Sequent.isLoaded : Sequent → Bool

Equations

• Sequent.isLoaded (fst, fst_1, none) = decide False
• Sequent.isLoaded (fst, fst_1, some val) = decide True

def Sequent.isFree (Γ : Sequent) : Bool

Equations

• Γ.isFree = decide ¬Γ.isLoaded = true

@[simp]

theorem Sequent.none_isFree (L R : List Formula) : isFree (L, R, none) = true

@[simp]

theorem Sequent.some_not_isFree (L R : List Formula) (olf : NegLoadFormula ⊕ NegLoadFormula) : ¬isFree (L, R, some olf) = true

theorem setEqTo_isLoaded_iff {X Y : Sequent} (h : X.setEqTo Y) : X.isLoaded = Y.isLoaded

theorem multisetEqTo_isLoaded_iff {X Y : Sequent} (h : X.multisetEqTo Y) : X.isLoaded = Y.isLoaded

Semantics of sequents

instance modelCanSemImplySequent {W : Type} : vDash (KripkeModel W × W) Sequent

Equations

• One or more equations did not get rendered due to their size.

instance modelCanSemImplyLLO {W : Type} : vDash (KripkeModel W × W) (List Formula × List Formula × Olf)

Equations

• One or more equations did not get rendered due to their size.

instance instSequentHasSat : HasSat Sequent

Equations

• instSequentHasSat = { satisfiable := fun (Δ : Sequent) => ∃ (W : Type) (M : KripkeModel W) (w : W), (M, w)⊨Δ }

theorem tautImp_iff_SequentUnsat {φ ψ : Formula} {X : Sequent} : X = ([φ], [~ψ], none) → (tautology (~(φ⋀~ψ)) ↔ ¬HasSat.satisfiable X)

theorem vDash_setEqTo_iff {W : Type} {X Y : Sequent} (h : X.setEqTo Y) (M : KripkeModel W) (w : W) : (M, w)⊨X ↔ (M, w)⊨Y

theorem vDash_multisetEqTo_iff {W : Type} {X Y : Sequent} (h : X.multisetEqTo Y) (M : KripkeModel W) (w : W) : (M, w)⊨X ↔ (M, w)⊨Y

def Sequent.without (LRO : Sequent) (naf : AnyNegFormula) : Sequent

Removing loaded formulas from sequents

Equations

• Sequent.without (L, R, O) (~''(AnyFormula.normal f)) = (L \ {~f}, R \ {~f}, O)
• Sequent.without (L, R, O) (~''(AnyFormula.loaded lf)) = if NegLoadFormula.mem_Sequent (L, R, O) (~'lf) then (L, R, none) else (L, R, O)

@[simp]

theorem Sequent.without_normal_isFree_iff_isFree {φ : Formula} (LRO : Sequent) : (LRO.without (~''(AnyFormula.normal φ))).isFree = true ↔ LRO.isFree = true

@[simp]

theorem Sequent.isFree_then_without_isFree (LRO : Sequent) : LRO.isFree = true → ∀ (anf : AnyNegFormula), (LRO.without anf).isFree = true

theorem Sequent.without_loadBoxes_isFree_of_eq_inl {αs : List Program} {d : Program} {L R : List Formula} {δs : List Program} {χ : LoadFormula} {φ : Formula} (h : AnyFormula.loaded χ = AnyFormula.loadBoxes αs (AnyFormula.normal φ)) : (without (L, R, some (Sum.inl (~'⌊⌊d :: δs⌋⌋χ))) (~''(AnyFormula.loadBoxes (d :: (δs ++ αs)) (AnyFormula.normal φ)))).isFree = true

theorem Sequent.without_loadBoxes_isFree_of_eq_inr {αs : List Program} {d : Program} {L R : List Formula} {δs : List Program} {χ : LoadFormula} {φ : Formula} (h : AnyFormula.loaded χ = AnyFormula.loadBoxes αs (AnyFormula.normal φ)) : (without (L, R, some (Sum.inr (~'⌊⌊d :: δs⌋⌋χ))) (~''(AnyFormula.loadBoxes (d :: (δs ++ αs)) (AnyFormula.normal φ)))).isFree = true

theorem Sequent.without_loadMulti_isFree_of_splitLast_cons_inl {d : Program} {δ_β : List Program × Program} {L R : List Formula} {δs : List Program} {φ : Formula} (h : splitLast (d :: δs) = some δ_β) : (without (L, R, some (Sum.inl (~'loadMulti δ_β.1 δ_β.2 φ))) (~''(AnyFormula.loadBoxes (d :: δs) (AnyFormula.normal φ)))).isFree = true

theorem Sequent.without_loadMulti_isFree_of_splitLast_cons_inr {d : Program} {δ_β : List Program × Program} {L R : List Formula} {δs : List Program} {φ : Formula} (h : splitLast (d :: δs) = some δ_β) : (without (L, R, some (Sum.inr (~'loadMulti δ_β.1 δ_β.2 φ))) (~''(AnyFormula.loadBoxes (d :: δs) (AnyFormula.normal φ)))).isFree = true

inductive Side : Type

• LL : Side
• RR : Side

def sideOf {α : Type u_1} : α ⊕ α → Side

Equations

• sideOf (Sum.inl val) = Side.LL
• sideOf (Sum.inr val) = Side.RR

def AnyNegFormula.in_side (anf : AnyNegFormula) : Side → (X : Sequent) → Prop

Equations

• (~''(AnyFormula.normal φ)).in_side Side.LL (L, fst, snd) = (~φ ∈ L)
• (~''(AnyFormula.normal φ)).in_side Side.RR (fst, R, snd) = (~φ ∈ R)
• (~''(AnyFormula.loaded χ)).in_side Side.LL (fst, fst_1, O) = (O = some (Sum.inl (~'χ)))
• (~''(AnyFormula.loaded χ)).in_side Side.RR (fst, fst_1, O) = (O = some (Sum.inr (~'χ)))

theorem AnyNegFormula.in_side_of_setEqTo {side : Side} {X Y : Sequent} (h : X.setEqTo Y) {anf : AnyNegFormula} : anf.in_side side X ↔ anf.in_side side Y

theorem AnyNegFormula.in_side_of_multisetEqTo {side : Side} {X Y : Sequent} (h : X.multisetEqTo Y) {anf : AnyNegFormula} : anf.in_side side X ↔ anf.in_side side Y

theorem LoadFormula.in_side_of_lf_inl {X : Sequent} (lf : LoadFormula) (O_def : X.2.2 = some (Sum.inl (~'lf))) : (~''(AnyFormula.loaded lf)).in_side Side.LL X

theorem LoadFormula.in_side_of_lf_inr {X : Sequent} (lf : LoadFormula) (O_def : X.2.2 = some (Sum.inr (~'lf))) : (~''(AnyFormula.loaded lf)).in_side Side.RR X

theorem Sequent.isLoaded_of_negAnyFormula_loaded {α : Program} {ξ : AnyFormula} {side : Side} {X : Sequent} (negLoad_in : (~''(AnyFormula.loaded (⌊α⌋ξ))).in_side side X) : X.isLoaded = true

@[simp]

theorem Sequent.without_loaded_in_side_isFree (LRO : Sequent) (ξ : LoadFormula) (side : Side) : (~''(AnyFormula.loaded ξ)).in_side side LRO → (LRO.without (~''(AnyFormula.loaded ξ))).isFree = true