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

@[instance_reducible]

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

@[simp]

theorem Option.none_subseteq {α : Type u_1} {O : Option α} : none ⊆ O

@[instance_reducible]

instance Option.instDecidableSubset {α : Type u_1} [DecidableEq α] (o1 o2 : Option α) : Decidable (o1 ⊆ o2)

The subset relation on Option α from Option.instHasSubsetOption is decidable.

Equations

• o1.instDecidableSubset o2 = Option.casesOn o1 (isTrue trivial) fun (a : α) => Option.casesOn o2 (isFalse ⋯) fun (b : α) => decidable_of_iff (a = b) ⋯

@[instance_reducible]

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 Olf.L : Olf → Finset 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)) = ∅

@[simp]

theorem Olf.L_map_inr {olf : Option NegLoadFormula} : L (Option.map Sum.inr olf) = ∅

@[simp]

theorem Olf.L_inl {lf : NegLoadFormula} : L (some (Sum.inl lf)) = {~lf.1.unload}

theorem Olf.L_subset_of_subset {O1 O2 : Olf} (h : O1 ⊆ O2) : O1.L ⊆ O2.L

theorem Olf.L_sdiff_subset {O Ocond : Olf} : (O \ Ocond).L ⊆ O.L

def Olf.R : Olf → Finset 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)) = ∅

@[simp]

theorem Olf.R_map_inl {olf : Option NegLoadFormula} : R (Option.map Sum.inl olf) = ∅

@[simp]

theorem Olf.R_inr {lf : NegLoadFormula} : R (some (Sum.inr lf)) = {~lf.1.unload}

theorem Olf.R_subset_of_subset {O1 O2 : Olf} (h : O1 ⊆ O2) : O1.R ⊆ O2.R

theorem Olf.R_sdiff_subset {O Ocond : Olf} : (O \ Ocond).R ⊆ O.R

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_old_none_none {oldO : Olf} : oldO.change none none = oldO

@[simp]

theorem Olf.change_none_none_new {newO : Olf} : change none none newO = newO

@[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

def Olf.isNone : Olf → Prop

Equations

• Olf.isNone none = True
• Olf.isNone (some (Sum.inl nlf)) = False
• Olf.isNone (some (Sum.inr nlf)) = False

def Olf.isLeft : Olf → Prop

Equations

• Olf.isLeft none = False
• Olf.isLeft (some (Sum.inl nlf)) = True
• Olf.isLeft (some (Sum.inr nlf)) = False

def Olf.isRight : Olf → Prop

Equations

• Olf.isRight none = False
• Olf.isRight (some (Sum.inl nlf)) = False
• Olf.isRight (some (Sum.inr nlf)) = True

@[instance_reducible]

instance instDecidableOlfisNone (o : Olf) : Decidable o.isNone

Equations

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

@[instance_reducible]

instance instDecidableOlfisLeft (o : Olf) : Decidable o.isLeft

Equations

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

@[instance_reducible]

instance instDecidableOlfisRight (o : Olf) : Decidable o.isRight

Equations

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

Sequents and their (multi)set quality

@[implicit_reducible]

def Sequent : Type

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

Equations

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

@[instance_reducible]

instance instDecidableEqSequent : DecidableEq Sequent

Equations

• instDecidableEqSequent = instDecidableEqSequent._aux_1

@[instance_reducible]

unsafe instance instReprSequent : Repr Sequent

Equations

• instReprSequent = { reprPrec := instReprSequent._aux_1 }

def Sequent.toFinset : Sequent → Finset Formula

Equations

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

Components and sides of sequents

def Sequent.L : Sequent → Finset Formula

Equations

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

def Sequent.R : Sequent → Finset Formula

Equations

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

def Sequent.O : Sequent → Olf

Equations

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

@[simp]

theorem Sequent.L_eq {L R : Finset Formula} {O : Olf} : Sequent.L (L, R, O) = L

@[simp]

theorem Sequent.R_eq {L R : Finset Formula} {O : Olf} : Sequent.R (L, R, O) = R

@[simp]

theorem Sequent.O_eq {L R : Finset Formula} {O : Olf} : Sequent.O (L, R, O) = O

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

Equations

• X.left = X.L ∪ X.O.L

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

Equations

• X.right = X.R ∪ X.O.R

@[simp]

theorem Sequent.left_eq {L R : Finset Formula} {O : Olf} : left (L, R, O) = L ∪ O.L

@[simp]

theorem Sequent.right_eq {L R : Finset Formula} {O : Olf} : right (L, R, O) = R ∪ O.R

(Joint) vocabulary of sequents

def onlfvoc : Option NegLoadFormula → Vocab

Like Olf.voc but without the ⊕ inside.

Equations

• onlfvoc none = ∅
• onlfvoc (some nlf) = nlf.voc

def lfovoc (L : List (List Formula × Option NegLoadFormula)) : Vocab

Equations

• lfovoc L = L.toFinset.sup fun (x : List Formula × Option NegLoadFormula) => match x with | (fs, o) => fs.fvoc ∪ onlfvoc o

def lfovocFin (L : Finset (Finset Formula × Option NegLoadFormula)) : Vocab

Finset version of lfovoc.

Equations

• lfovocFin L = L.sup fun (x : Finset Formula × Option NegLoadFormula) => match x with | (fs, o) => fs.fvoc ∪ onlfvoc o

def jvoc (X : Sequent) : Vocab

The joint vocabulary occurring on both the left and the right side.

Equations

• jvoc X = X.left.fvoc ∩ X.right.fvoc

theorem jvoc_sub_of_voc_sub {Y X : Sequent} (hl : Y.left.fvoc ⊆ X.left.fvoc) (hr : Y.right.fvoc ⊆ X.right.fvoc) : jvoc Y ⊆ jvoc X

Formulas as elements of sequents

@[instance_reducible]

instance instMembershipFormulaSequent : Membership Formula Sequent

Equations

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

@[simp]

theorem Sequent.mem_def {φ : Formula} {X : Sequent} : φ ∈ X ↔ φ ∈ X.L ∨ φ ∈ X.R

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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_reducible]

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

Equations

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

@[instance_reducible]

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 χ)) = ((~'χ) ∈ x✝)

@[instance_reducible]

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

• x✝.basic = ((∀ f ∈ x✝.toFinset, f.basic = true) ∧ ¬x✝.closed)

@[instance_reducible]

instance Fintype.decidableExistsConjFintype {α : Type u_1} {p q : α → Prop} [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_reducible]

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 ⋯)

@[instance_reducible]

instance instDecidableBasic {X : Sequent} : Decidable X.basic

Equations

• instDecidableBasic = if h : X.closed then isFalse ⋯ else id (⋯.mpr (if h : ∃ f ∈ X.toFinset, f.basic ≠ true then isFalse ⋯ else isTrue ⋯))

def Sequent.isLoaded : Sequent → Prop

Equations

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

theorem Sequent.isRight_of_not_isLeft_isLoaded {X : Sequent} (h1 : ¬X.2.2.isLeft) (h2 : X.isLoaded) : X.2.2.isRight

A loaded sequent that is not loaded on the left is loaded on the right.

@[instance_reducible]

instance instDecidableSequentisLoaded (X : Sequent) : Decidable X.isLoaded

Equations

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

def Sequent.isFree (Γ : Sequent) : Prop

Equations

• Γ.isFree = ¬Γ.isLoaded

@[instance_reducible]

instance instDecidableSequentisFree (X : Sequent) : Decidable X.isFree

Equations

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

@[simp]

theorem Sequent.none_isFree (L R : Finset Formula) : isFree (L, R, none)

@[simp]

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

Semantics of sequents

@[instance_reducible]

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

Equations

• modelCanSemImplySequent = { SemImplies := fun (x : KripkeModel W × W) (X : Sequent) => match x with | (M, w) => ∀ f ∈ X.toFinset, evaluate M w f }

@[instance_reducible]

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 = Y) (M : KripkeModel W) (w : W) : (M, w) ⊨ X ↔ (M, w) ⊨ Y

theorem Sequent.satisfiable_top_cons_right {X : Sequent} (h_left_nil : X.left = ∅) (X_unsat : ¬HasSat.satisfiable X) : ¬HasSat.satisfiable ({⊤} ∪ X.right)

Removing loaded formulas from sequents

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

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 ↔ LRO.isFree

@[simp]

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

theorem Sequent.without_loadBoxes_isFree_of_eq_inl {αs : List Program} {d : Program} {L R : Finset 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

theorem Sequent.without_loadBoxes_isFree_of_eq_inr {αs : List Program} {d : Program} {L R : Finset 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

theorem Sequent.without_loadMulti_isFree_of_splitLast_cons_inl {d : Program} {δ_β : List Program × Program} {L R : Finset 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

theorem Sequent.without_loadMulti_isFree_of_splitLast_cons_inr {d : Program} {δ_β : List Program × Program} {L R : Finset 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

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 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

@[simp]

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

Whatever formulas

A type to describe all formulas that can occur in a sequent, without losing information about whether they are loaded or not.

inductive WhateverFormula : Type

Unfortunately our AnyFormula type does not include negated loaded formulas, so this is yet another type to describe "whatever formula" can be in a sequent, without losing information.

• any : AnyFormula → WhateverFormula
• negLoad : NegLoadFormula → WhateverFormula

@[instance_reducible]

instance instReprWhateverFormula : Repr WhateverFormula

Equations

• instReprWhateverFormula = { reprPrec := instReprWhateverFormula.repr }

def instReprWhateverFormula.repr : WhateverFormula → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance instDecidableEqWhateverFormula : DecidableEq WhateverFormula

Equations

• instDecidableEqWhateverFormula = instDecidableEqWhateverFormula.decEq

def instDecidableEqWhateverFormula.decEq (x✝ x✝¹ : WhateverFormula) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqWhateverFormula.decEq (WhateverFormula.any a) (WhateverFormula.any b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqWhateverFormula.decEq (WhateverFormula.any a) (WhateverFormula.negLoad a_1) = isFalse ⋯
• instDecidableEqWhateverFormula.decEq (WhateverFormula.negLoad a) (WhateverFormula.any a_1) = isFalse ⋯
• instDecidableEqWhateverFormula.decEq (WhateverFormula.negLoad a) (WhateverFormula.negLoad b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance instCoeFormulaWhateverFormula : Coe Formula WhateverFormula

Equations

• instCoeFormulaWhateverFormula = { coe := WhateverFormula.any ∘ AnyFormula.normal }

@[instance_reducible]

instance instCoeLoadFormulaWhateverFormula : Coe LoadFormula WhateverFormula

Equations

• instCoeLoadFormulaWhateverFormula = { coe := WhateverFormula.any ∘ AnyFormula.loaded }

@[instance_reducible]

instance instCoeNegLoadFormulaWhateverFormula : Coe NegLoadFormula WhateverFormula

Equations

• instCoeNegLoadFormulaWhateverFormula = { coe := WhateverFormula.negLoad }

def Olf.wForms : Olf → Finset WhateverFormula

Equations

• Olf.wForms none = ∅
• Olf.wForms (some (Sum.inl nlf)) = {WhateverFormula.negLoad nlf}
• Olf.wForms (some (Sum.inr nlf)) = {WhateverFormula.negLoad nlf}

def Sequent.wForms : Sequent → Finset WhateverFormula

Equations

• Sequent.wForms (L, R, O) = Finset.image Coe.coe L ∪ Finset.image Coe.coe R ∪ O.wForms

theorem Sequent.mem_toFinset_iff (φ : Formula) (X : Sequent) : φ ∈ X.toFinset ↔ WhateverFormula.any (AnyFormula.normal φ) ∈ X.wForms ∨ (∃ (χ : LoadFormula), χ.unload = φ ∧ WhateverFormula.any (AnyFormula.loaded χ) ∈ X.wForms) ∨ ∃ (ψ : NegLoadFormula), negUnload ψ = φ ∧ WhateverFormula.negLoad ψ ∈ X.wForms

theorem Sequent.mem_wForms_normal_iff {ψ : Formula} {L R : Finset Formula} {O : Olf} : (WhateverFormula.any ∘ AnyFormula.normal) ψ ∈ wForms (L, R, O) ↔ ψ ∈ L ∨ ψ ∈ R

A normal formula is in X.wForms iff it is on the left or on the right of X. (Note that the Olf part of X only contributes negated loaded formulas.)

theorem Sequent.isAtomic_of_basic_of_negBox_mem_wForms {X : Sequent} {α : Program} {φ : Formula} (bas : X.basic) (h : (WhateverFormula.any ∘ AnyFormula.normal) (~⌈α⌉φ) ∈ X.wForms) : α.isAtomic

In a basic sequent all free diamonds are atomic.

theorem Sequent.mem_wForms_negLoad_iff {nlf : NegLoadFormula} {L R : Finset Formula} {O : Olf} : WhateverFormula.negLoad nlf ∈ wForms (L, R, O) ↔ O = some (Sum.inl nlf) ∨ O = some (Sum.inr nlf)

A negated loaded formula is in X.wForms iff it is the loaded formula of X.

theorem Sequent.isAtomic_of_basic_of_negLoad_mem_wForms {X : Sequent} {α : Program} {ξ : AnyFormula} (bas : X.basic) (h : WhateverFormula.negLoad (~'⌊α⌋ξ) ∈ X.wForms) : α.isAtomic

In a basic sequent all loaded diamonds are atomic.

Sorting Finsets of Sequents

Lexicographic orders on lists and pairs

NOTE: The following two definitions and their properties are general, i.e. not about PDL at all. These could be moved to a separate file (or even might be in newer versions of Mathlib?).

def listLex {α : Type} (le : α → α → Prop) : List α → List α → Prop

Lexicographic extension of a relation le to lists: shorter lists come first, and lists of the same shape are compared element-wise from left to right.

Equations

• listLex le [] x✝ = True
• listLex le (head :: tail) [] = False
• listLex le (a :: as) (b :: bs) = (le a b ∧ (a = b → listLex le as bs))

@[instance_reducible]

instance listLex.instDecidableRel {α : Type} [DecidableEq α] (le : α → α → Prop) [DecidableRel le] : DecidableRel (listLex le)

Equations

• listLex.instDecidableRel le [] x✝ = isTrue trivial
• listLex.instDecidableRel le (head :: tail) [] = isFalse not_false
• listLex.instDecidableRel le (a :: as) (b :: bs) = inferInstance

theorem listLex_refl {α : Type} {le : α → α → Prop} (hrefl : ∀ (a : α), le a a) (as : List α) : listLex le as as

theorem listLex_antisymm {α : Type} {le : α → α → Prop} (hanti : ∀ (a b : α), le a b → le b a → a = b) (as bs : List α) : listLex le as bs → listLex le bs as → as = bs

theorem listLex_trans {α : Type} {le : α → α → Prop} (hanti : ∀ (a b : α), le a b → le b a → a = b) (htrans : ∀ (a b c : α), le a b → le b c → le a c) (as bs cs : List α) : listLex le as bs → listLex le bs cs → listLex le as cs

theorem listLex_total {α : Type} {le : α → α → Prop} (hrefl : ∀ (a : α), le a a) (htotal : ∀ (a b : α), le a b ∨ le b a) (as bs : List α) : listLex le as bs ∨ listLex le bs as

def prodLex {α β : Type} (le1 : α → α → Prop) (le2 : β → β → Prop) : α × β → α × β → Prop

Lexicographic combination of two relations on a product type.

Equations

• prodLex le1 le2 (a, b) (a', b') = (le1 a a' ∧ (a = a' → le2 b b'))

@[instance_reducible]

instance prodLex.instDecidableRel {α β : Type} [DecidableEq α] (le1 : α → α → Prop) (le2 : β → β → Prop) [DecidableRel le1] [DecidableRel le2] : DecidableRel (prodLex le1 le2)

Equations

• prodLex.instDecidableRel le1 le2 (a, b) (a', b') = inferInstance

theorem prodLex_refl {α β : Type} {le1 : α → α → Prop} {le2 : β → β → Prop} (h1 : ∀ (a : α), le1 a a) (h2 : ∀ (b : β), le2 b b) (x : α × β) : prodLex le1 le2 x x

theorem prodLex_antisymm {α β : Type} {le1 : α → α → Prop} {le2 : β → β → Prop} (h1 : ∀ (a a' : α), le1 a a' → le1 a' a → a = a') (h2 : ∀ (b b' : β), le2 b b' → le2 b' b → b = b') (x y : α × β) : prodLex le1 le2 x y → prodLex le1 le2 y x → x = y

theorem prodLex_trans {α β : Type} {le1 : α → α → Prop} {le2 : β → β → Prop} (hanti1 : ∀ (a a' : α), le1 a a' → le1 a' a → a = a') (htrans1 : ∀ (a a' a'' : α), le1 a a' → le1 a' a'' → le1 a a'') (htrans2 : ∀ (b b' b'' : β), le2 b b' → le2 b' b'' → le2 b b'') (x y z : α × β) : prodLex le1 le2 x y → prodLex le1 le2 y z → prodLex le1 le2 x z

theorem prodLex_total {α β : Type} {le1 : α → α → Prop} {le2 : β → β → Prop} (hrefl1 : ∀ (a : α), le1 a a) (htotal1 : ∀ (a a' : α), le1 a a' ∨ le1 a' a) (htotal2 : ∀ (b b' : β), le2 b b' ∨ le2 b' b) (x y : α × β) : prodLex le1 le2 x y ∨ prodLex le1 le2 y x

An order on loaded formulas, via a key

def LoadFormula.key : LoadFormula → List Program × Formula

Every loaded formula is a non-empty sequence of loading boxes followed by a normal formula. The key of a loaded formula records exactly this data, and hence determines it uniquely. NOTE: This could be moved to Pdl/Syntax.lean.

Equations

• (⌊α⌋AnyFormula.normal φ).key = ([α], φ)
• (⌊α⌋AnyFormula.loaded χ).key = (α :: χ.key.1, χ.key.2)

def loadFormulaOfKey : List Program → Formula → LoadFormula

Inverse of LoadFormula.key, see LoadFormula.ofKey_key. (The value for the empty list of programs is arbitrary.) NOTE: This could be moved to Pdl/Syntax.lean.

Equations

• loadFormulaOfKey [] x✝ = ⌊?'x✝⌋AnyFormula.normal x✝
• loadFormulaOfKey [α] x✝ = ⌊α⌋AnyFormula.normal x✝
• loadFormulaOfKey (α :: β :: δ) x✝ = ⌊α⌋AnyFormula.loaded (loadFormulaOfKey (β :: δ) x✝)

theorem LoadFormula.ofKey_key (χ : LoadFormula) : loadFormulaOfKey χ.key.1 χ.key.2 = χ

The key of a loaded formula determines it.

theorem LoadFormula.key_injective {χ χ' : LoadFormula} (h : χ.key = χ'.key) : χ = χ'

An order on sequents, via a key

def Olf.key : Olf → ℕ × List Program × Formula

Key of an Olf: which side (if any) is loaded, together with the key of the loaded formula.

Equations

• Olf.key none = (0, [], Formula.bottom)
• Olf.key (some (Sum.inl (~'χ))) = (1, χ.key)
• Olf.key (some (Sum.inr (~'χ))) = (2, χ.key)

theorem Olf.key_injective {O O' : Olf} : O.key = O'.key → O = O'

def Sequent.key (X : Sequent) : List Formula × List Formula × ℕ × List Program × Formula

Key of a sequent: the sorted lists of the left and right side, and the key of the Olf.

Equations

• X.key = (X.L.fsort, X.R.fsort, X.O.key)

theorem Finset.fsort_injective {X Y : Finset Formula} (h : X.fsort = Y.fsort) : X = Y

Finsets of formulas with the same fsort are equal. NOTE: This could be moved to Pdl/Syntax.lean.

theorem Sequent.key_injective {X Y : Sequent} (h : X.key = Y.key) : X = Y

def olfKeyLe : ℕ × List Program × Formula → ℕ × List Program × Formula → Prop

Order used to compare the keys of Olfs.

Equations

• olfKeyLe = prodLex (fun (n m : ℕ) => n ≤ m) (prodLex (listLex Program.le) Formula.le)

@[instance_reducible]

instance instDecidableRelProdNatListProgramFormulaOlfKeyLe : DecidableRel olfKeyLe

Equations

• instDecidableRelProdNatListProgramFormulaOlfKeyLe = id inferInstance

theorem olfKeyLe_refl (x : ℕ × List Program × Formula) : olfKeyLe x x

theorem olfKeyLe_antisymm (x y : ℕ × List Program × Formula) (h1 : olfKeyLe x y) (h2 : olfKeyLe y x) : x = y

theorem olfKeyLe_trans (x y z : ℕ × List Program × Formula) (h1 : olfKeyLe x y) (h2 : olfKeyLe y z) : olfKeyLe x z

theorem olfKeyLe_total (x y : ℕ × List Program × Formula) : olfKeyLe x y ∨ olfKeyLe y x

def seqKeyLe : List Formula × List Formula × ℕ × List Program × Formula → List Formula × List Formula × ℕ × List Program × Formula → Prop

Order used to compare the keys of sequents.

Equations

• seqKeyLe = prodLex (listLex Formula.le) (prodLex (listLex Formula.le) olfKeyLe)

@[instance_reducible]

instance instDecidableRelProdListFormulaNatProgramSeqKeyLe : DecidableRel seqKeyLe

Equations

• instDecidableRelProdListFormulaNatProgramSeqKeyLe = id inferInstance

def Sequent.le (X Y : Sequent) : Prop

A linear order on sequents, used to define Finset.seqSort.

Equations

• X.le Y = seqKeyLe X.key Y.key

@[instance_reducible]

instance Sequent.instDecidableRelLe : DecidableRel le

Equations

• X.instDecidableRelLe Y = id inferInstance

instance Sequent.instIsTransLe : IsTrans Sequent le

instance Sequent.instAntisymmLe : Std.Antisymm le

instance Sequent.instTotalLe : Std.Total le

def Finset.seqSort : Finset Sequent → List Sequent

Sort a finite set of sequents into a list, using Sequent.le.

Equations

• A.seqSort = A.sort Sequent.le

@[simp]

theorem Finset.mem_seqSort {X : Sequent} (A : Finset Sequent) : X ∈ A.seqSort ↔ X ∈ A

theorem Finset.seqSort_nodup (A : Finset Sequent) : A.seqSort.Nodup

@[simp]

theorem Finset.length_seqSort (A : Finset Sequent) : A.seqSort.length = A.card

@[simp]

theorem Finset.seqSort_eq_nil_iff {A : Finset Sequent} : A.seqSort = [] ↔ A = ∅