Documentation

def companion {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) :

s ♥ t means s is a LoadedPathRepeat and the companionOf s is t.

Equations

s ♥ t = ∃ (lpr : LoadedPathRepeat (tabAt s).fst (tabAt s).snd.fst) (h : (tabAt s).snd.snd = Tableau.lrep lpr), t = companionOf s lpr h

Instances For

def «term_♥_» :

Equations

«term_♥_» = Lean.ParserDescr.trailingNode `«term_♥_» 1022 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ♥ ") (Lean.ParserDescr.cat `term 1023))

Instances For

theorem companion_lt {a✝ : Sequent} {tab : Tableau [] a✝} {l c : PathIn tab} :

l ♥ c → c < l

theorem nodeAt_companionOf_eq_toHistory_get_lpr_val {a✝ : Sequent} {tab : Tableau [] a✝} (s : PathIn tab) (lpr : LoadedPathRepeat (tabAt s).fst (tabAt s).snd.fst) (h : (tabAt s).snd.snd = Tableau.lrep lpr) :

nodeAt (companionOf s lpr h) = List.get s.toHistory (Fin.cast ⋯ ↑lpr)

The node at a companion is the same as the one in the history.

theorem nodeAt_companionOf_multisetEq {X : Sequent} {tab : Tableau [] X} (s : PathIn tab) (lpr : LoadedPathRepeat (tabAt s).fst (tabAt s).snd.fst) (h : (tabAt s).snd.snd = Tableau.lrep lpr) :

(nodeAt (companionOf s lpr h)).multisetEqTo (nodeAt s)

theorem companion_loaded {a✝ : Sequent} {a✝¹ : Tableau [] a✝} {s t : PathIn a✝¹} :

s ♥ t → (nodeAt s).isLoaded = true ∧ (nodeAt t).isLoaded = true

Any repeat and companion are both loaded.

theorem companionOf_length_lt_length {a✝ : Sequent} {tab : Tableau [] a✝} {t : PathIn tab} (lpr : LoadedPathRepeat (tabAt t).fst (tabAt t).snd.fst) (h : (tabAt t).snd.snd = Tableau.lrep lpr) :

(companionOf t lpr h).length < t.length

The companion is strictly before the the repeat.

theorem companion_to_repeat_all_loaded {a✝ : Sequent} {tab : Tableau [] a✝} {l c : PathIn tab} (lpr : LoadedPathRepeat (tabAt l).fst (tabAt l).snd.fst) (tabAt_l_def : (tabAt l).snd.snd = Tableau.lrep lpr) (c_def : c = companionOf l lpr tabAt_l_def) (k : Fin (List.length l.toHistory + 1)) :

↑k ≤ (↑↑lpr).succ → (nodeAt (l.rewind k)).isLoaded = true

Not using ♥ here because we need to refer to the lpr.

theorem not_edge_and_heart {a✝ : Sequent} {tab : Tableau [] a✝} {a b : PathIn tab} :

¬(a ⋖_ b ∧ b ♥ a)

def cEdge {X : Sequent} {ctX : Tableau [] X} (s t : PathIn ctX) :

Equations

s ◃ t = (s ⋖_ t ∨ s ♥ t)

Instances For

def «term_◃_» :

Equations

«term_◃_» = Lean.ParserDescr.trailingNode `«term_◃_» 1022 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ◃ ") (Lean.ParserDescr.cat `term 1023))

Instances For

def «term_◃⁺_» :

Equations

«term_◃⁺_» = Lean.ParserDescr.trailingNode `«term_◃⁺_» 1022 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ◃⁺ ") (Lean.ParserDescr.cat `term 1023))

Instances For

def «term_◃*_» :

Equations

«term_◃*_» = Lean.ParserDescr.trailingNode `«term_◃*_» 1022 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ◃* ") (Lean.ParserDescr.cat `term 1023))

Instances For

≡ᶜ and Clusters #

def cEquiv {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) :

Nodes are c-equivalent iff there are ◃ paths both ways. Note that this is not a closure, so we do not want Relation.EqvGen here.

Equations

s ≡ᶜ t = (s ◃* t ∧ t ◃* s)

Instances For

def «term_≡ᶜ_» :

Equations

«term_≡ᶜ_» = Lean.ParserDescr.trailingNode `«term_≡ᶜ_» 1022 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≡ᶜ ") (Lean.ParserDescr.cat `term 1023))

Instances For

theorem cEquiv.symm {a✝ : Sequent} {tab : Tableau [] a✝} (s t : PathIn tab) :

s ≡ᶜ t ↔ t ≡ᶜ s

≡ᶜ is symmetric.

def clusterOf {X : Sequent} {tab : Tableau [] X} (p : PathIn tab) :

Quot cEquiv

Equations

clusterOf p = Quot.mk cEquiv p

Instances For

def before {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) :

We have before s t iff there is a path from s to t but not from t to s. This means the cluster of s comes before the cluster of t in tab. NB: The notes use ◃* here but we use ◃⁺. The definitions are equivalent.

Equations

s <ᶜ t = (s ◃⁺ t ∧ ¬t ◃⁺ s)

Instances For

def «term_<ᶜ_» :

s <ᶜ t means there is a ◃-path from s to t but not from t to s. This means t is simpler to deal with first.

Equations

«term_<ᶜ_» = Lean.ParserDescr.trailingNode `«term_<ᶜ_» 1022 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <ᶜ ") (Lean.ParserDescr.cat `term 1023))

Instances For

theorem before.irrefl {X : Sequent} {tab : Tableau [] X} :

IsIrrefl (PathIn tab) before

The <ᶜ relation is irreflexive.

theorem before.trans {X : Sequent} {tab : Tableau [] X} :

Transitive before

The <ᶜ relation is transitive.

theorem trans_before.irrefl {X : Sequent} {tab : Tableau [] X} :

IsIrrefl (PathIn tab) (Relation.TransGen before)

The transitive closure of <ᶜ (which in fact is the same as <ᶜ) is irreflexive.

theorem before.wellFounded {X : Sequent} {tab : Tableau [] X} :

WellFounded before

The before relation in a tableau is well-founded.

theorem flip_before.irrefl {X : Sequent} {tab : Tableau [] X} :

IsIrrefl (PathIn tab) (flip before)

The converse of <ᶜ is irreflexive.

theorem trans_flip_before.irrefl {X : Sequent} {tab : Tableau [] X} :

IsIrrefl (PathIn tab) (Relation.TransGen (flip before))

The transtive closure of the converse of <ᶜ is irreflexive.

theorem flip_before.wellFounded {X : Sequent} {tab : Tableau [] X} :

WellFounded (flip before)

The before relation in a tableau is converse well-founded.

theorem eProp {X : Sequent} (tab : Tableau [] X) :

Equivalence cEquiv ∧ WellFounded before ∧ WellFounded (flip before)

≣ᶜ is an equivalence relation and <ᶜ is well-founded and converse well-founded. The converse well-founded is what we really need for induction proofs.

theorem ePropB.a {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) :

s ⋖_ t → s <ᶜ t ∨ t ≡ᶜ s

theorem ePropB.b {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) :

s ♥ t → t ≡ᶜ s

theorem c_claim {a : Sequent} {tab : Tableau [] a} (t l c : PathIn tab) :

(nodeAt t).isFree = true → t < l → l ♥ c → t < c

theorem ePropB.c {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) :

(nodeAt s).isFree = true → s < t → s <ᶜ t

theorem not_cEquiv_of_free_loaded {a✝ : Sequent} {tab : Tableau [] a✝} (s t : PathIn tab) (s_free : (nodeAt s).isFree = true) (t_loaded : (nodeAt t).isLoaded = true) :

¬s ≡ᶜ t

theorem ePropB.d {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) :

(nodeAt t).isFree = true → s < t → s <ᶜ t

theorem ePropB.c_single {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) :

(nodeAt s).isFree = true → s ⋖_ t → s <ᶜ t

theorem ePropB.e {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) :

(nodeAt s).isLoaded = true → (nodeAt t).isFree = true → s ⋖_ t → s <ᶜ t

theorem ePropB.e_help {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) :

(nodeAt t).isLoaded = true → (nodeAt s).isFree = true → t ◃⁺ s → ¬s ◃⁺ t

theorem ePropB.f {X : Sequent} {tab : Tableau [] X} (s u t : PathIn tab) :

s <ᶜ u → u <ᶜ t → s <ᶜ t

<ᶜ is transitive

theorem ePropB.g {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) :

t ◃⁺ s → ¬t ≡ᶜ s → t <ᶜ s

theorem ePropB.g_tweak {X : Sequent} {tab : Tableau [] X} (s u t : PathIn tab) :

s ◃⁺ u → u ◃⁺ t → ¬t ≡ᶜ u → ¬t ≡ᶜ s

theorem ePropB.h {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) :

s <ᶜ t → ¬s ≡ᶜ t

theorem ePropB.i {X : Sequent} {tab : Tableau [] X} (s u t : PathIn tab) :

s <ᶜ u → s ≡ᶜ t → t <ᶜ u

Previously called simpler_equiv_simpler.

theorem ePropB {X : Sequent} {tab : Tableau [] X} (s u t : PathIn tab) :

(s ⋖_ t → s <ᶜ t ∨ t ≡ᶜ s) ∧ (s ♥ t → t ≡ᶜ s) ∧ ((nodeAt s).isFree = true → s < t → s <ᶜ t) ∧ ((nodeAt t).isFree = true → s < t → s <ᶜ t) ∧ ((nodeAt s).isLoaded = true → (nodeAt t).isFree = true → s ⋖_ t → s <ᶜ t) ∧ (s <ᶜ u → u <ᶜ t → s <ᶜ t) ∧ (t ◃⁺ s → ¬t ≡ᶜ s → t <ᶜ s) ∧ (s <ᶜ t → ¬s ≡ᶜ t) ∧ (s <ᶜ u → s ≡ᶜ t → t <ᶜ u)

Soundness #

Specific case of loadedDiamondPaths for Tableau.pdl.

theorem loadedDiamondPathsPDL (α : Program) (X : Sequent) (tab : Tableau [] X) (t : PathIn tab) {W : Type} {M : KripkeModel W} {v w : W} (v_t : (M, v)⊨nodeAt t) (ξ : AnyFormula) {side : Side} (negLoad_in : (~''(AnyFormula.loaded (⌊α⌋ξ))).in_side side (nodeAt t)) (v_α_w : relate M α v w) (w_nξ : (M, w)⊨~''ξ) {Hist : History} {Z Y : Sequent} (bas : Z.basic) (r : PdlRule Z Y) (nrep : ¬rep Hist Z) (next : Tableau (Z :: Hist) Y) (tabAt_t_def : tabAt t = ⟨Hist, ⟨Z, Tableau.pdl nrep bas r next⟩⟩) :

∃ (s : PathIn tab), t ◃⁺ s ∧ (HasSat.satisfiable (nodeAt s) ∧ ¬s ≡ᶜ t ∨ (~''ξ).in_side side (nodeAt s) ∧ (M, w)⊨nodeAt s ∧ ((nodeAt s).without (~''ξ)).isFree = true)

theorem SemImply_loadedNormal_ofSeqAndNormal {W✝ : Type} {w : W✝} {φ : Formula} {αs : List Program} {M : KripkeModel W✝} {u : W✝} (w_nφ : (M, w)⊨(~φ)) (u_αs_w : relateSeq M αs u w) :

(M, u)⊨~''(AnyFormula.loadBoxes αs (AnyFormula.normal φ))

theorem firstBox_isAtomic_of_basic {β : Program} {βs : List Program} {φ : Formula} {side : Side} {Y : Sequent} (Y_bas : Y.basic) (anf_in_Y : (~''(AnyFormula.loadBoxes (β :: βs) (AnyFormula.normal φ))).in_side side Y) :

β.isAtomic

@[irreducible]

theorem loadedDiamondPaths (α : Program) (αs : List Program) {X : Sequent} (tab : Tableau [] X) (root_free : X.isFree = true) (t : PathIn tab) {W : Type} {M : KripkeModel W} {v w : W} (v_t : (M, v)⊨nodeAt t) (φ : Formula) {side : Side} (negLoad_in : (~''(AnyFormula.loaded (⌊α⌋AnyFormula.loadBoxes αs (AnyFormula.normal φ)))).in_side side (nodeAt t)) (v_α_αs_w : relateSeq M (α :: αs) v w) (w_nφ : (M, w)⊨(~φ)) :

∃ (s : PathIn tab), t ◃⁺ s ∧ (HasSat.satisfiable (nodeAt s) ∧ ¬s ≡ᶜ t ∨ (~''(AnyFormula.normal φ)).in_side side (nodeAt s) ∧ (M, w)⊨nodeAt s ∧ (nodeAt s).isFree = true)

Key helper lemma to show the soundness of loading and repeats. Intutively, it says that a tableau starting with a loaded diamond can immitate all possible ways in which a Kripke model can satisfy that diamond.

The lemma statement differs slightly from the paper version:

Our paths cannot stop "inside" a LocalTableau and they may take apart more than one loaded box, hence we need access to all of the boxes αs in front of the normal formula φ.
We do not say that the from t to s has to be satisfiable.
We only demand s to be satisfiable in the free case. For the other disjunct this is implied.

The paper proof uses three nested induction levels, one of them only in the star case. Instead of that here we use recursive calls and show that they terminate via the lexicographic order on the ℕ∞ × Nat × Nat triple ⟨distance_list M v w (α :: αs), lengthOfProgram α, t.length⟩. The star case is then actually handled just like the other connectives.