Documentation

Pdl.Soundness

Soundness (Section 6) #

Soundness of the PDL rules #

theorem pdlRuleSat {X Y : Sequent} (r : PdlRule X Y) (satX : HasSat.satisfiable X) :

The PDL rules are sound.

Companion, cEdge, etc. #

def companionOf {X : Sequent} {tab : Tableau [] X} (s : PathIn tab) (lpr : LoadedPathRepeat (tabAt s).fst (tabAt s).snd.fst) :
(tabAt s).snd.snd = Tableau.lrep lprPathIn tab

To get the companion of a LoadedPathRepeat we rewind the path with the lpr value. The succ is there because the lpr values are indices of the history starting with 0, but PathIn.rewind 0 would do nothing.

Equations
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
theorem companion_lt {a✝ : Sequent} {tab : Tableau [] a✝} {l c : PathIn tab} :
l cc < 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_setEq {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) :
theorem companion_loaded {a✝ : Sequent} {a✝¹ : Tableau [] a✝} {s t : PathIn a✝¹} :

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

The companion is strictly before the the repeat.

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

≡ᶜ 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
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) :
Equations
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 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
theorem before.irrefl {X : Sequent} {tab : Tableau [] X} :

The <ᶜ relation is irreflexive.

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

The <ᶜ relation is transitive.

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

The before relation in a tableau is well-founded.

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

The converse of <ᶜ is irreflexive.

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

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

≣ᶜ 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 ⋖_ ts <ᶜ t t ≡ᶜ s
theorem ePropB.b {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) :
s tt ≡ᶜ s
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 c_claim {a : Sequent} {tab : Tableau [] a} (t l c : PathIn tab) :
(nodeAt t).isFree = truet < ll ct < c
theorem ePropB.c {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) :
(nodeAt s).isFree = trues < ts <ᶜ t
theorem free_or_loaded {a : Sequent} {tab : Tableau [] a} (s : PathIn tab) :
theorem edge_is_strict_ordering {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {s t : PathIn tab} :
s ⋖_ ts t
theorem path_is_strict_ordering {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {s t : PathIn tab} :
s < ts 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) :
theorem ePropB.d {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) :
(nodeAt t).isFree = trues < ts <ᶜ t
theorem ePropB.c_single {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) :
(nodeAt s).isFree = trues ⋖_ ts <ᶜ t
theorem ePropB.e {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) :
(nodeAt s).isLoaded = true(nodeAt t).isFree = trues ⋖_ ts <ᶜ t
theorem ePropB.e_help {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) :
(nodeAt t).isLoaded = true(nodeAt s).isFree = truet ◃⁺ s¬s ◃⁺ t
theorem ePropB.f {X : Sequent} {tab : Tableau [] X} (s u t : PathIn tab) :
s <ᶜ uu <ᶜ ts <ᶜ t

<ᶜ is transitive

theorem ePropB.g {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) :
t ◃⁺ s¬t ≡ᶜ st <ᶜ s
theorem ePropB.g_tweak {X : Sequent} {tab : Tableau [] X} (s u t : PathIn tab) :
s ◃⁺ uu ◃⁺ 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 <ᶜ us ≡ᶜ tt <ᶜ u
theorem ePropB {X : Sequent} {tab : Tableau [] X} (s u t : PathIn tab) :
(s ⋖_ ts <ᶜ t t ≡ᶜ s) (s tt ≡ᶜ s) ((nodeAt s).isFree = trues < ts <ᶜ t) ((nodeAt t).isFree = trues < ts <ᶜ t) ((nodeAt s).isLoaded = true(nodeAt t).isFree = trues ⋖_ ts <ᶜ t) (s <ᶜ uu <ᶜ ts <ᶜ t) (t ◃⁺ s¬t ≡ᶜ st <ᶜ s) (s <ᶜ t¬s ≡ᶜ t) (s <ᶜ us ≡ᶜ tt <ᶜ u)

Soundness #

theorem localLoadedDiamond (α : Program) {X : Sequent} (ltab : LocalTableau X) {W : Type} {M : KripkeModel W} {v w : W} (v_α_w : relate M α v w) (v_t : (M, v)X) (ξ : AnyFormula) {side : Side} (negLoad_in : (~''(AnyFormula.loaded (αξ))).in_side side X) (w_nξ : (M, w)~''ξ) :
YendNodesOf ltab, (M, v)Y (Y.isFree = true ∃ (F : List Formula) (γ : List Program), (~''(AnyFormula.loadBoxes γ ξ)).in_side side Y relateSeq M γ v w (M, v)F (F, γ) H α (Y.without (~''(AnyFormula.loadBoxes γ ξ))).isFree = true)

Helper to deal with local tableau in loadedDiamondPaths.

theorem Sequent.isLoaded_of_negAnyFormula_loaded {α : Program} {ξ : AnyFormula} {side : Side} {X : Sequent} (negLoad_in : (~''(AnyFormula.loaded (αξ))).in_side side X) :
theorem boxes_true_at_k_of_Vector_rel {W : Type} {M : KripkeModel W} (ξ : AnyFormula) (δ : List Program) (h : ¬δ = []) (ws : List.Vector W δ.length.succ) (ws_rel : ∀ (i : Fin δ.length), relate M (δ.get i) (ws.get i) (ws.get i.succ)) (k : Fin δ.length) (w_nξ : (M, ws.last)~''ξ) :
theorem loadedDiamondPathsM (α : 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) (ξ : AnyFormula) {side : Side} (negLoad_in : (~''(AnyFormula.loaded (αξ))).in_side side (nodeAt t)) (v_α_w : relate M α v w) (w_nξ : (M, w)~''ξ) :
∃ (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)

Soundness of loading and repeats: a tableau can immitate all moves in a model.

@[irreducible]
theorem loadedDiamondPaths (α : 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) (ξ : AnyFormula) {side : Side} (negLoad_in : (~''(AnyFormula.loaded (αξ))).in_side side (nodeAt t)) (v_α_w : relate M α v w) (w_nξ : (M, w)~''ξ) :
∃ (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 simpler_equiv_simpler {a✝ : Sequent} {tab : Tableau [] a✝} {u s t : PathIn tab} :
s <ᶜ us ≡ᶜ tt <ᶜ u
theorem tableauThenNotSat {Root : Sequent} (tab : Tableau [] Root) (Root_isFree : Root.isFree = true) (t : PathIn tab) :

Any node in a closed tableau with a free root is not satisfiable. This is the main argument for soundness.

theorem soundness (φ : Formula) :

All provable formulas are semantic tautologies. See tableauThenNotSat for what the notes call soundness.