Soundness (Section 6)

theorem PDL.Sequent.mem_toFinset_of_O_eq {X : Sequent} {nlf : NegLoadFormula} (h : X.2.2 = some (Sum.inl nlf) ∨ X.2.2 = some (Sum.inr nlf)) : negUnload nlf ∈ X.toFinset

If the Olf of a sequent is nlf then its unloading is in the toFinset.

Soundness of the PDL rules

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

The PDL rules are sound.

Companion, cEdge, etc.

def PDL.companionOf {X : Sequent} {tab : Tableau [] X} (s : PathIn tab) (lpr : LoadedPathRepeat (tabAt s).fst (tabAt s).snd.fst) : (tabAt s).snd.snd = Tableau.lrep lpr → PathIn 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

• PDL.companionOf s lpr x✝ = s.rewind (Fin.cast ⋯ ↑lpr).succ

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

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

Equations

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

def PDL.«term_♥_» : Lean.TrailingParserDescr

The companion relation connecting a loaded repeat to its earlier node.

Equations

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

@[instance_reducible]

instance PDL.instDecidableCompanion {X : Sequent} {tab : Tableau [] X} (p q : PathIn tab) : Decidable (companion p q)

Equations

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

theorem PDL.companion_lt {X : Sequent} {tab : Tableau [] X} {l c : PathIn tab} : companion l c → c < l

theorem PDL.nodeAt_companionOf_eq_toHistory_get_lpr_val {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) = List.get s.toHistory (Fin.cast ⋯ ↑lpr)

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

theorem PDL.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) : nodeAt (companionOf s lpr h) = nodeAt s

theorem PDL.companion_loaded {a✝ : Sequent} {a✝¹ : Tableau [] a✝} {s t : PathIn a✝¹} : companion s t → (nodeAt s).isLoaded ∧ (nodeAt t).isLoaded

Any repeat and companion are both loaded.

theorem PDL.companionOf_length_lt_length {X : Sequent} {tab : Tableau [] X} {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 PDL.companion_to_repeat_all_loaded {X : Sequent} {tab : Tableau [] X} {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

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

theorem PDL.not_edge_and_heart {X : Sequent} {tab : Tableau [] X} {a b : PathIn tab} : ¬(edge a b ∧ companion b a)

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

An ordinary tableau edge or an edge to a repeat's companion.

Equations

• PDL.cEdge s t = (PDL.edge s t ∨ PDL.companion s t)

def PDL.«term_◃_» : Lean.TrailingParserDescr

One ordinary or companion edge.

Equations

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

def PDL.«term_◃⁺_» : Lean.TrailingParserDescr

A nonempty path of ordinary or companion edges.

Equations

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

def PDL.«term_◃*_» : Lean.TrailingParserDescr

A possibly empty path of ordinary or companion edges.

Equations

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

theorem PDL.cReach_of_le {X : Sequent} {tab : Tableau [] X} {s t : PathIn tab} (h : s ≤ t) : Relation.ReflTransGen cEdge s t

Any ⋖_ path is also a ◃ path.

@[instance_reducible]

instance PDL.instDecidableCEdge {X : Sequent} {tab : Tableau [] X} (p q : PathIn tab) : Decidable (cEdge p q)

Equations

• PDL.instDecidableCEdge p q = id inferInstance

@[instance_reducible]

instance PDL.instDecidablecEdgeTransGen {X : Sequent} {tab : Tableau [] X} (p q : PathIn tab) : Decidable (Relation.TransGen cEdge p q)

Equations

• PDL.instDecidablecEdgeTransGen p q = PDL.FinReach.decidableTransGen PDL.cEdge p q

≡ᶜ and Clusters

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

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

• PDL.cEquiv s t = (Relation.ReflTransGen PDL.cEdge s t ∧ Relation.ReflTransGen PDL.cEdge t s)

def PDL.«term_≡ᶜ_» : Lean.TrailingParserDescr

Membership in the same cluster.

Equations

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

theorem PDL.cEquiv.symm {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) : cEquiv s t ↔ cEquiv t s

≡ᶜ is symmetric.

def PDL.clusterOf {X : Sequent} {tab : Tableau [] X} (p : PathIn tab) : Quot cEquiv

Given a tableau node, return its cluster as an element in the cEquiv quotient. Suffices for Soundness, but for Interpolation we need something "more constructive".

Equations

• PDL.clusterOf p = Quot.mk PDL.cEquiv p

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

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

• PDL.before s t = (Relation.TransGen PDL.cEdge s t ∧ ¬Relation.TransGen PDL.cEdge t s)

def PDL.«term_<ᶜ_» : Lean.TrailingParserDescr

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

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

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

The <ᶜ relation is irreflexive.

instance PDL.before.trans {X : Sequent} {tab : Tableau [] X} : IsTrans (PathIn tab) before

The <ᶜ relation is transitive.

theorem PDL.trans_before.irrefl {X : Sequent} {tab : Tableau [] X} : Std.Irrefl (Relation.TransGen before)

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

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

The before relation in a tableau is well-founded.

theorem PDL.flip_before.irrefl {X : Sequent} {tab : Tableau [] X} : Std.Irrefl (flip before)

The converse of <ᶜ is irreflexive.

theorem PDL.trans_flip_before.irrefl {X : Sequent} {tab : Tableau [] X} : Std.Irrefl (Relation.TransGen (flip before))

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

theorem PDL.flip_before.wellFounded {X : Sequent} {tab : Tableau [] X} : WellFounded (flip before)

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

theorem PDL.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 PDL.ePropB.a {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) : edge s t → before s t ∨ cEquiv t s

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

theorem PDL.c_claim {a : Sequent} {tab : Tableau [] a} (t l c : PathIn tab) : (nodeAt t).isFree → t < l → companion l c → t < c

theorem PDL.ePropB.c {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) : (nodeAt s).isFree → s < t → before s t

theorem PDL.not_cEquiv_of_free_loaded {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) (s_free : (nodeAt s).isFree) (t_loaded : (nodeAt t).isLoaded) : ¬cEquiv s t

theorem PDL.ePropB.d {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) : (nodeAt t).isFree → s < t → before s t

theorem PDL.ePropB.c_single {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) : (nodeAt s).isFree → edge s t → before s t

theorem PDL.ePropB.e {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) : (nodeAt s).isLoaded → (nodeAt t).isFree → edge s t → before s t

theorem PDL.ePropB.e_help {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) : (nodeAt t).isLoaded → (nodeAt s).isFree → Relation.TransGen cEdge t s → ¬Relation.TransGen cEdge s t

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

<ᶜ is transitive

theorem PDL.ePropB.g {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) : Relation.TransGen cEdge t s → ¬cEquiv t s → before t s

theorem PDL.ePropB.g_tweak {X : Sequent} {tab : Tableau [] X} (s u t : PathIn tab) : Relation.TransGen cEdge s u → Relation.TransGen cEdge u t → ¬cEquiv t u → ¬cEquiv t s

theorem PDL.ePropB.h {X : Sequent} {tab : Tableau [] X} (s t : PathIn tab) : before s t → ¬cEquiv s t

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

Previously called simpler_equiv_simpler.

theorem PDL.ePropB {X : Sequent} {tab : Tableau [] X} (s u t : PathIn tab) : (edge s t → before s t ∨ cEquiv t s) ∧ (companion s t → cEquiv t s) ∧ ((nodeAt s).isFree → s < t → before s t) ∧ ((nodeAt t).isFree → s < t → before s t) ∧ ((nodeAt s).isLoaded → (nodeAt t).isFree → edge s t → before s t) ∧ (before s u → before u t → before s t) ∧ (Relation.TransGen cEdge t s → ¬cEquiv t s → before t s) ∧ (before s t → ¬cEquiv s t) ∧ (before s u → cEquiv s t → before t u)

Soundness

Specific case of loadedDiamondPaths for Tableau.pdl.

theorem PDL.loadedDiamondPathsPDL (α : Program) (X : Sequent) (tab : Tableau [] X) (t : PathIn tab) {W : Type} {M : KripkeModel W} {v w : W} (v_t : vDash.SemImplies (M, v) (nodeAt t)) (ξ : AnyFormula) {side : Side} (negLoad_in : (AnyNegFormula.neg (AnyFormula.loaded (LoadFormula.box α ξ))).inSide side (nodeAt t)) (v_α_w : relate M α v w) (w_nξ : vDash.SemImplies (M, w) (AnyNegFormula.neg ξ)) {Hist : History} {Z Y : Sequent} (bas : Z.basic) (r : PdlRule Z Y) (nflprep : ¬flprep Hist Z) (next : Tableau (Z :: Hist) Y) (tabAt_t_def : tabAt t = ⟨Hist, ⟨Z, Tableau.pdl nflprep bas r next⟩⟩) : ∃ (s : PathIn tab), Relation.TransGen cEdge t s ∧ (HasSat.satisfiable (nodeAt s) ∧ ¬cEquiv s t ∨ (AnyNegFormula.neg ξ).inSide side (nodeAt s) ∧ vDash.SemImplies (M, w) (nodeAt s) ∧ ((nodeAt s).without (AnyNegFormula.neg ξ)).isFree)

theorem PDL.SemImply_loadedNormal_ofSeqAndNormal {W✝ : Type} {w : W✝} {φ : Formula} {αs : List Program} {M : KripkeModel W✝} {u : W✝} (w_nφ : vDash.SemImplies (M, w) φ.neg) (u_αs_w : relateSeq M αs u w) : vDash.SemImplies (M, u) (AnyNegFormula.neg (AnyFormula.loadBoxes αs (AnyFormula.normal φ)))

theorem PDL.firstBox_isAtomic_of_basic {β : Program} {φ : Formula} {Y : Sequent} {side : Side} {βs : List Program} (Y_bas : Y.basic) (anf_in_Y : (AnyNegFormula.neg (AnyFormula.loadBoxes (β :: βs) (AnyFormula.normal φ))).inSide side Y) : β.isAtomic

theorem PDL.loadedDiamondPaths (α : Program) (αs : List Program) {X : Sequent} (tab : Tableau [] X) (root_free : X.isFree) (t : PathIn tab) {W : Type} {M : KripkeModel W} {v w : W} (v_t : vDash.SemImplies (M, v) (nodeAt t)) (φ : Formula) {side : Side} (negLoad_in : (AnyNegFormula.neg (AnyFormula.loaded (LoadFormula.box α (AnyFormula.loadBoxes αs (AnyFormula.normal φ))))).inSide side (nodeAt t)) (v_α_αs_w : relateSeq M (α :: αs) v w) (w_nφ : vDash.SemImplies (M, w) φ.neg) : ∃ (s : PathIn tab), Relation.TransGen cEdge t s ∧ (HasSat.satisfiable (nodeAt s) ∧ ¬cEquiv s t ∨ (AnyNegFormula.neg (AnyFormula.normal φ)).inSide side (nodeAt s) ∧ vDash.SemImplies (M, w) (nodeAt s) ∧ (nodeAt s).isFree)

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 path 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 ⟨distanceList M v w (α :: αs), lengthOfProgram α, t.length⟩. The star case is then actually handled just like the other connectives.

theorem PDL.tableauThenNotSat {Root : Sequent} (tab : Tableau [] Root) (Root_isFree : Root.isFree) (t : PathIn tab) : ¬HasSat.satisfiable (nodeAt t)

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

theorem PDL.correctness (LR : Sequent) : LR.isFree → HasSat.satisfiable LR → consistent LR

theorem PDL.soundTableau (φ : Formula) : provable φ → ¬HasSat.satisfiable {φ.neg}

theorem PDL.soundness (φ : Formula) : provable φ → tautology φ

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