Bml.Tableau

source

instance instHasSubsetProdFinsetFormula :

HasSubset (Finset Formula × Finset Formula)

Equations

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

source

instance instUnionProdFinsetFormula :

Union (Finset Formula × Finset Formula)

Equations

instUnionProdFinsetFormula = { union := fun (x x_1 : Finset Formula × Finset Formula) => match x with | (L1, R1) => match x_1 with | (L2, R2) => (L1 ∪ L2, R1 ∪ R2) }

source

def TNode :

Type

Equations

TNode = (Finset Formula × Finset Formula)

Instances For

source

instance instTNodeDecidableEq :

DecidableEq TNode

Equations

instTNodeDecidableEq a b = instDecidableEqProd a b

source

instance instTNodeHasSubset :

HasSubset TNode

Equations

instTNodeHasSubset = instHasSubsetProdFinsetFormula

source

instance instTNodeUnion :

Union TNode

Equations

instTNodeUnion = instUnionProdFinsetFormula

source

def lengthOfTNode :

TNode → ℕ

Equations

lengthOfTNode (L, R) = lengthOfSet L + lengthOfSet R

Instances For

source

instance TNodeHasLength :

HasLength TNode

Equations

TNodeHasLength = { lengthOf := lengthOfTNode }

source

instance TNodeHasSat :

HasSat TNode

Equations

TNodeHasSat = { Satisfiable := fun (x : TNode) => match x with | (L, R) => HasSat.Satisfiable (L ∪ R) }

source

def f_in_TNode (f : Formula) (LR : TNode) :

Prop

Equations

f_in_TNode f LR = (f ∈ LR.1 ∪ LR.2)

Instances For

source

def Closed :

Finset Formula → Prop

Definition 9, page 15. A set X is closed iff it contains ⊥ or contains a formula and its negation.

Equations

Closed X = (⊥ ∈ X ∨ ∃ f ∈ X, ~f ∈ X)

Instances For

source

def SimpleForm :

Formula → Prop

A set X is simple iff all P ∈ X are (negated) atoms or □φ or ¬□φ.

Equations

Instances For

source

def SimpleSet :

Finset Formula → Prop

Equations

SimpleSet x✝ = ∀ P ∈ x✝.attach, SimpleForm ↑P

Instances For

source

instance instDecidableSimpleSet {X : Finset Formula} :

Decidable (SimpleSet X)

Equations

instDecidableSimpleSet = Finset.decidableDforallFinset

source

structure notSimpleFormOf (X : Finset Formula) :

Type

φ : Formula
φinX : self.φ ∈ X
not_simple : ¬SimpleForm self.φ

Instances For

source

noncomputable def notSimpleSetToForm {X : Finset Formula} :

¬SimpleSet X → notSimpleFormOf X

Equations

notSimpleSetToForm not_simple = { φ := Classical.choose ⋯, φinX := ⋯, not_simple := ⋯ }

Instances For

source

def Simple (LR : TNode) :

Prop

Equations

Simple LR = (SimpleSet LR.1 ∧ SimpleSet LR.2)

Instances For

source

instance instDecidableSimple {LR : TNode} :

Decidable (Simple LR)

Equations

instDecidableSimple = if L_simple : SimpleSet LR.1 then if R_simple : SimpleSet LR.2 then isTrue ⋯ else isFalse ⋯ else isFalse ⋯

source

def formProjection :

Formula → Option Formula

Let X_A := { R | [A]R ∈ X }.

Equations

formProjection (□f) = some f
formProjection x✝ = none

Instances For

source

def projection :

Finset Formula → Finset Formula

Equations

projection x✝ = x✝.biUnion fun (x : Formula) => (formProjection x).toFinset

Instances For

source

def projectTNode :

TNode → TNode

Equations

projectTNode (L, R) = (projection L, projection R)

Instances For

source

@[simp]

theorem projectionUnion {X Y : Finset Formula} :

projection (X ∪ Y) = projection X ∪ projection Y

source

theorem proj {g : Formula} {X : Finset Formula} :

g ∈ projection X ↔ □g ∈ X

source

theorem projSet {X : Finset Formula} :

↑(projection X) = {ϕ : Formula | □ϕ ∈ X}

source

theorem projection_length_leq (f : Formula) :

(projection {f}).sum lengthOfFormula ≤ lengthOfFormula f

source

theorem projection_set_length_leq (X : Finset Formula) :

lengthOfSet (projection X) ≤ lengthOfSet X

source

inductive OneSidedLocalRule :

Finset Formula → List (Finset Formula) → Type

bot : OneSidedLocalRule {⊥} ∅
not (φ : Formula) : OneSidedLocalRule {φ, ~φ} ∅
neg (φ : Formula) : OneSidedLocalRule {~~φ} [{φ}]
con (φ ψ : Formula) : OneSidedLocalRule {φ⋀ψ} [{φ, ψ}]
ncon (φ ψ : Formula) : OneSidedLocalRule {~(φ⋀ψ)} [{~φ}, {~ψ}]

Instances For

source

def SubPair :

Type

Equations

SubPair = (Finset Formula × Finset Formula)

Instances For

source

instance instSubPairDecidableEq :

DecidableEq SubPair

Equations

instSubPairDecidableEq a b = instDecidableEqProd a b

source

inductive LocalRule :

SubPair → List SubPair → Type

oneSidedL {precond : Finset Formula} {ress : List (Finset Formula)} (orule : OneSidedLocalRule precond ress) : LocalRule (precond, ∅) (List.map (fun (res : Finset Formula) => (res, ∅)) ress)
oneSidedR {precond : Finset Formula} {ress : List (Finset Formula)} (orule : OneSidedLocalRule precond ress) : LocalRule (∅, precond) (List.map (fun (res : Finset Formula) => (∅, res)) ress)
LRnegL (ϕ : Formula) : LocalRule ({ϕ}, {~ϕ}) ∅
LRnegR (ϕ : Formula) : LocalRule ({~ϕ}, {ϕ}) ∅

Instances For

source

def jvoc (LR : TNode) :

Finset Char

Equations

jvoc LR = HasVocabulary.voc LR.1 ∩ HasVocabulary.voc LR.2

Instances For

source

def applyLocalRule {Lcond Rcond : Finset Formula} {ress : List SubPair} :

LocalRule (Lcond, Rcond) ress → TNode → List TNode

Equations

applyLocalRule x✝ (L, R) = List.map (fun (c : SubPair) => (L \ Lcond ∪ c.1, R \ Rcond ∪ c.2)) ress

Instances For

source

inductive LocalRuleApp :

TNode → List TNode → Type

mk {L R : Finset Formula} {C : List TNode} (ress : List SubPair) (Lcond Rcond : Finset Formula) (rule : LocalRule (Lcond, Rcond) ress) {hC : C = applyLocalRule rule (L, R)} (preconditionProof : Lcond ⊆ L ∧ Rcond ⊆ R) : LocalRuleApp (L, R) C

Instances For

source

theorem oneSidedRule_preserves_other_side_L {L R : Finset Formula} {C : List TNode} {fst✝ : Finset Formula} {a✝ : List (Finset Formula)} {rule : LocalRule (fst✝, ∅) (List.map (fun (res : Finset Formula) => (res, ∅)) a✝)} {hC : C = applyLocalRule rule (L, R)} {preproof : fst✝ ⊆ L ∧ ∅ ⊆ R} {orule : OneSidedLocalRule fst✝ a✝} {ruleApp : LocalRuleApp (L, R) C} :

ruleApp = LocalRuleApp.mk (List.map (fun (res : Finset Formula) => (res, ∅)) a✝) fst✝ ∅ rule preproof → ∀ (rule_is_left : rule = LocalRule.oneSidedL orule), ∀ c ∈ C, c.2 = R

source

theorem oneSidedRule_preserves_other_side_R {L R : Finset Formula} {C : List TNode} {snd✝ : Finset Formula} {a✝ : List (Finset Formula)} {rule : LocalRule (∅, snd✝) (List.map (fun (res : Finset Formula) => (∅, res)) a✝)} {hC : C = applyLocalRule rule (L, R)} {preproof : ∅ ⊆ L ∧ snd✝ ⊆ R} {orule : OneSidedLocalRule snd✝ a✝} {ruleApp : LocalRuleApp (L, R) C} :

ruleApp = LocalRuleApp.mk (List.map (fun (res : Finset Formula) => (∅, res)) a✝) ∅ snd✝ rule preproof → ∀ (rule_is_right : rule = LocalRule.oneSidedR orule), ∀ c ∈ C, c.1 = L

source

theorem localRule_does_not_increase_vocab_L {Lcond Rcond : Finset Formula} {ress : List SubPair} (rule : LocalRule (Lcond, Rcond) ress) (res : SubPair) :

res ∈ ress → HasVocabulary.voc res.1 ⊆ HasVocabulary.voc Lcond

source

theorem localRule_does_not_increase_vocab_R {Lcond Rcond : Finset Formula} {ress : List SubPair} (rule : LocalRule (Lcond, Rcond) ress) (res : SubPair) :

res ∈ ress → HasVocabulary.voc res.2 ⊆ HasVocabulary.voc Rcond

source

theorem localRuleApp_does_not_increase_vocab {C : List TNode} {L R : Finset Formula} (ruleA : LocalRuleApp (L, R) C) (cLR : TNode) :

cLR ∈ C → jvoc cLR ⊆ jvoc (L, R)

source

theorem LocalRuleUniqueL {L : Finset Formula} {α : Formula} {R : Finset Formula} {C : List TNode} {precond : Finset Formula} {ress : List (Finset Formula)} (α_in_L : α ∈ L) (lrApp : LocalRuleApp (L, R) C) (orule : OneSidedLocalRule precond ress) (precond_eq : precond = {α}) (c : TNode) :

c ∈ C → α ∈ c.1 ∨ ∃ res ∈ ress, res ⊆ c.1

If a local rule replaces formula α by some set res when applied to some node LR, then all children of LR in any LocalTableau contain α or res. This is used to prove that all paths are saturated.

source

theorem LocalRuleUniqueR {R : Finset Formula} {α : Formula} {L : Finset Formula} {C : List TNode} {precond : Finset Formula} {ress : List (Finset Formula)} (α_in_R : α ∈ R) (lrApp : LocalRuleApp (L, R) C) (orule : OneSidedLocalRule precond ress) (precond_eq : precond = {α}) (c : TNode) :

c ∈ C → α ∈ c.2 ∨ ∃ res ∈ ress, res ⊆ c.2

Almost exactly the same as LocalRuleUniqueL.

source

inductive LocalTableau :

TNode → Type

fromRule {LR : TNode} {C : List TNode} (ruleA : LocalRuleApp LR C) (subTabs : (c : TNode) → c ∈ C → LocalTableau c) : LocalTableau LR
fromSimple {LR : TNode} (isSimple : Simple LR) : LocalTableau LR

Instances For

source

noncomputable def notSimpleToRuleApp {L R : Finset Formula} :

¬Simple (L, R) → (C : List TNode) × LocalRuleApp (L, R) C

If X is not simple, then a local rule can be applied (page 13).

Equations

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

Instances For

source

theorem notSimpleThenLocalRule {L R : Finset Formula} :

¬Simple (L, R) → ∃ (Lcond : Finset Formula) (Rcond : Finset Formula) (ress : List SubPair) (x : LocalRule (Lcond, Rcond) ress), Lcond ⊆ L ∧ Rcond ⊆ R

source

theorem conDecreasesLength {φ ψ : Formula} :

∑ x ∈ {φ, ψ}, lengthOfFormula x < 1 + lengthOfFormula φ + lengthOfFormula ψ

source

theorem localRuleDecreasesLengthSide {Lcond Rcond : Finset Formula} {ress : List SubPair} (rule : LocalRule (Lcond, Rcond) ress) (res : SubPair) :

res ∈ ress → HasLength.lengthOf res.1 < HasLength.lengthOf Lcond ∧ res.2 = ∅ ∨ HasLength.lengthOf res.2 < HasLength.lengthOf Rcond ∧ res.1 = ∅

source

@[simp]

theorem notnot_notSelfContain {φ : Formula} :

~~φ ≠ φ

source

@[simp]

theorem conNotSelfContainL {φ1 φ2 : Formula} :

φ1⋀φ2 ≠ φ1

source

@[simp]

theorem conNotSelfContainR {φ1 φ2 : Formula} :

φ1⋀φ2 ≠ φ2

source

theorem localRuleNoOverlap {Lcond Rcond : Finset Formula} {ress : List SubPair} (rule : LocalRule (Lcond, Rcond) ress) (res : SubPair) :

res ∈ ress → Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅

Rules never re-insert the same formula(s).

source

def zlengthOf :

Formula → ℤ

Equations

zlengthOf f = ↑(lengthOfFormula f)

Instances For

source

theorem zlengthOf.pos {φ : Formula} :

0 ≤ zlengthOf φ

source

def zlengthOfSet :

Finset Formula → ℤ

Equations

zlengthOfSet X = X.sum zlengthOf

Instances For

source

theorem zlen_iff {X Y : Finset Formula} :

HasLength.lengthOf X < HasLength.lengthOf Y ↔ zlengthOfSet X < zlengthOfSet Y

source

theorem zlengthOfSet.pos {X : Finset Formula} :

zlengthOfSet X ≥ 0

source

theorem localRuleAppDecreasesLengthSide (X Cond Res : Finset Formula) (hyp : HasLength.lengthOf Res < HasLength.lengthOf Cond) (precondProof : Cond ⊆ X) :

HasLength.lengthOf (X \ Cond ∪ Res) < HasLength.lengthOf X

source

theorem localRuleAppDecreasesLength {C : List TNode} {L R : Finset Formula} (lrApp : LocalRuleApp (L, R) C) (c : TNode) :

c ∈ C → lengthOfTNode c < lengthOfTNode (L, R)

source

def diamondProjectTNode :

Formula ⊕ Formula → TNode → TNode

Lift definition of projection to TNodes, including the diamond formula left or right.

Equations

diamondProjectTNode (Sum.inl φ) (L, R) = (projection L ∪ {~φ}, projection R)
diamondProjectTNode (Sum.inr φ) (L, R) = (projection L, projection R ∪ {~φ})

Instances For

source

theorem proj_does_not_increase_vocab {X : Finset Formula} :

HasVocabulary.voc (projection X) ⊆ HasVocabulary.voc X

source

theorem vocProj (X : Finset Formula) :

HasVocabulary.voc (projection X) ⊆ HasVocabulary.voc X

source

theorem diamondproj_does_not_increase_vocab_L {L : Finset Formula} {φ : Formula} {R : Finset Formula} (valid_proj : ~(□φ) ∈ L) :

jvoc (diamondProjectTNode (Sum.inl φ) (L, R)) ⊆ jvoc (L, R)

source

theorem diamondproj_does_not_increase_vocab_R {R : Finset Formula} {φ : Formula} {L : Finset Formula} (valid_proj : ~(□φ) ∈ R) :

jvoc (diamondProjectTNode (Sum.inr φ) (L, R)) ⊆ jvoc (L, R)

source

instance localTableauHasLength :

HasLength ((LR : TNode) × LocalTableau LR)

Equations

localTableauHasLength = { lengthOf := fun (x : (LR : TNode) × LocalTableau LR) => match x with | ⟨(L, R), snd⟩ => lengthOfTNode (L, R) }

source

@[irreducible]

def endNodesOf :

(LR : TNode) × LocalTableau LR → List TNode

Open end nodes of a given LocalTableau.

Equations

One or more equations did not get rendered due to their size.
endNodesOf ⟨LR, LocalTableau.fromSimple isSimple⟩ = [LR]

Instances For

source

@[simp]

theorem endNodesOfSimple {LR : TNode} {hyp : Simple LR} :

endNodesOf ⟨LR, LocalTableau.fromSimple hyp⟩ = [LR]

source

noncomputable def endNodeIsEndNodeOfChild {LR : TNode} {C : List TNode} {subTabs : (c : TNode) → c ∈ C → LocalTableau c} {E : TNode} (ruleA : LocalRuleApp LR C) (E_in : E ∈ endNodesOf ⟨LR, LocalTableau.fromRule ruleA subTabs⟩) :

{ x : TNode // ∃ (h : x ∈ C), E ∈ endNodesOf ⟨x, subTabs x h⟩ }

Equations

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

Instances For

source

@[simp]

theorem lrEndNodes {LR : TNode} {C : List TNode} {ruleA : LocalRuleApp LR C} {subTabs : (c : TNode) → c ∈ C → LocalTableau c} :

endNodesOf ⟨LR, LocalTableau.fromRule ruleA subTabs⟩ = (List.map (fun (x : { x : TNode // x ∈ C }) => match x with | ⟨c, c_in⟩ => endNodesOf ⟨c, subTabs c c_in⟩) C.attach).flatten

source

@[irreducible]

theorem endNodesOfLEQ {LR Z : TNode} {ltLR : LocalTableau LR} :

Z ∈ endNodesOf ⟨LR, ltLR⟩ → lengthOfTNode Z ≤ lengthOfTNode LR

source

theorem endNodesOfLocalRuleLT {LR : TNode} {a✝ : List TNode} {lrApp : LocalRuleApp LR a✝} {subTabs : (c : TNode) → c ∈ a✝ → LocalTableau c} {Z : TNode} :

Z ∈ endNodesOf ⟨LR, LocalTableau.fromRule lrApp subTabs⟩ → lengthOfTNode Z < lengthOfTNode LR

source

inductive ClosedTableau :

TNode → Type

Definition 16, page 29. Notes:

"loc" may actually make no progress (by using "LocalTableau.fromSimple"), but that seems okay.
base case for simple tableaux is part of "atm" which can be applied to L or to R.