Evaluating Q-formulas, the witness distance, and basic nodes

This file collects the notions needed for Lemmas 10.6, 10.7 and 10.8 in Pdl.ClusterSatDown:

• QFormula.evalQ, the evaluation of a Q-formula with an assignment for the internal variables, together with QFormula.evalQ_gfp_unfold, the unfolding of the fixpoint used at a companion node,
• Sequent.loadedSplit and friends, which read off the loaded formula ¬⌊δ⃗⌋ψ of a sequent,
• witDist, the witness distance wd_M(v,x) of the proof of Lemma 10.7, and
• QuasiTab.BasicBetween, the paper's "there is a basic node between x and z".

Internal variables

The pre-interpolants ι_x are QFormulas, i.e. they may contain internal variables q_z. The proof of Lemma 10.7 modifies the valuation of the internal variable q_x at a companion node x, keeping the relational structure of the model fixed. Instead of substituting a formula for q_x (and then appealing to the substitution lemma) we therefore evaluate a Q-formula directly with respect to an assignment g : Var → W → Prop of the internal variables. Changing the assignment leaves the model, and hence all distances, untouched, which is exactly the "M and M' have the same relational structure" of the paper.

Evaluating Q-formulas with an assignment for the internal variables

def QFormula.evalQ {Var W : Type} (M : KripkeModel W) (g : Var → W → Prop) : W → QFormula Var → Prop

Evaluate a Q-formula in a model M where the internal variables are interpreted by the assignment g.

Equations

• QFormula.evalQ M g x✝ (QFormula.fma ψ) = evaluate M x✝ ψ
• QFormula.evalQ M g x✝ (QFormula.var q) = g q x✝
• QFormula.evalQ M g x✝ (ι1.and ι2) = (QFormula.evalQ M g x✝ ι1 ∧ QFormula.evalQ M g x✝ ι2)
• QFormula.evalQ M g x✝ (QFormula.boxes as ι) = ∀ (u : W), relateSeq M as x✝ u → QFormula.evalQ M g u ι

@[simp]

theorem QFormula.evalQ_fma {Var W : Type} {M : KripkeModel W} {g : Var → W → Prop} {v : W} {ψ : Formula} : evalQ M g v (fma ψ) ↔ evaluate M v ψ

@[simp]

theorem QFormula.evalQ_var {Var W : Type} {M : KripkeModel W} {g : Var → W → Prop} {v : W} {q : Var} : evalQ M g v (var q) ↔ g q v

@[simp]

theorem QFormula.evalQ_and {Var W : Type} {M : KripkeModel W} {g : Var → W → Prop} {v : W} {ι1 ι2 : QFormula Var} : evalQ M g v (ι1.and ι2) ↔ evalQ M g v ι1 ∧ evalQ M g v ι2

@[simp]

theorem QFormula.evalQ_boxes {Var W : Type} {M : KripkeModel W} {g : Var → W → Prop} {v : W} {as : List Program} {ι : QFormula Var} : evalQ M g v (boxes as ι) ↔ ∀ (u : W), relateSeq M as v u → evalQ M g u ι

theorem QFormula.evalQ_iff_evaluate_subst {Var W : Type} {M : KripkeModel W} {σ : Var → Formula} (ι : QFormula Var) (v : W) : evalQ M (fun (q : Var) (u : W) => evaluate M u (σ q)) v ι ↔ evaluate M v (subst σ ι)

Evaluating a Q-formula with the assignment given by a substitution is the same as evaluating the substituted formula.

theorem QFormula.evalQ_congr {Var W : Type} {M : KripkeModel W} {g h : Var → W → Prop} (ι : QFormula Var) (v : W) : (∀ q ∈ ι.vars, g q = h q) → (evalQ M g v ι ↔ evalQ M h v ι)

Two assignments that agree on the internal variables of a Q-formula give the same value.

theorem QFormula.evalQ_conj {Var W : Type} {M : KripkeModel W} {g : Var → W → Prop} {v : W} (L : List (QFormula Var)) : evalQ M g v (conj L) ↔ ∀ ι ∈ L, evalQ M g v ι

Evaluating a conjunction of Q-formulas.

theorem QFormula.evalQ_toQ_prefixBoxes {Var W : Type} {M : KripkeModel W} {g : Var → W → Prop} {v : W} (as : List Program) (s : QSimple Var) : evalQ M g v (QSimple.prefixBoxes as s).toQ ↔ ∀ (u : W), relateSeq M as v u → evalQ M g u s.toQ

Prefixing a simple Q-formula with boxes, for evalQ.

theorem QFormula.evalQ_nf {Var W : Type} {M : KripkeModel W} {g : Var → W → Prop} {v : W} (ι : QFormula Var) : evalQ M g v ι.nf ↔ ∀ s ∈ ι.Spl, evalQ M g v s.toQ

Evaluating the normal form of a Q-formula: this is Fact 9.17 for evalQ.

theorem QFormula.evalQ_nf_iff {Var W : Type} {M : KripkeModel W} {g : Var → W → Prop} (ι : QFormula Var) (v : W) : evalQ M g v ι.nf ↔ evalQ M g v ι

A Q-formula is equivalent to its normal form, for evalQ.

Unfolding the fixpoint of the companion case

The pre-interpolant of a companion node x is gfp x ι for the pre-interpolant ι of its child. Interpreting the internal variable q_x by gfp x ι itself turns gfp x ι into ι; this is the semantic counterpart of the paper's observation that ι_x ≡ ι_y[q_x := ι_x].

theorem QFormula.evalQ_gfp_unfold {Var W : Type} [DecidableEq Var] {M : KripkeModel W} {g : Var → W → Prop} {v : W} {q : Var} (ι : QFormula Var) (h : evalQ M g v (gfp q ι)) : evalQ M (Function.update g q fun (u : W) => evalQ M g u (gfp q ι)) v ι

The loaded formula of a sequent

For a node x of the quasi-tableau the paper writes the unique loaded formula of Δ_x as ¬⌊δ_x⌋ψ_x with ψ_x unloaded. Here δ_x and ψ_x are Sequent.loadedProgs and Sequent.loadedFma, read off with LoadFormula.split.

def Sequent.loadedSplit : Sequent → List Program × Formula

The loaded formula of a sequent, split into its list of programs and its final, unloaded formula. For a free sequent we return ([], ⊥), which is never used.

Equations

• Sequent.loadedSplit (fst, fst_1, none) = ([], ⊥)
• Sequent.loadedSplit (fst, fst_1, some (Sum.inl (~'χ))) = χ.split
• Sequent.loadedSplit (fst, fst_1, some (Sum.inr (~'χ))) = χ.split

def Sequent.loadedProgs (X : Sequent) : List Program

The programs δ_x of the loaded formula ¬⌊δ_x⌋ψ_x.

Equations

• X.loadedProgs = X.loadedSplit.1

def Sequent.loadedFma (X : Sequent) : Formula

The unloaded formula ψ_x of the loaded formula ¬⌊δ_x⌋ψ_x.

Equations

• X.loadedFma = X.loadedSplit.2

def Sequent.isRightLoaded (X : Sequent) : Prop

The sequent has its loaded formula on the right, as all Δ ∈ Λ₂[C] do.

Equations

• X.isRightLoaded = ∃ (nlf : NegLoadFormula), X.O = some (Sum.inr nlf)

theorem LoadFormula.unload_eq_boxes_split (χ : LoadFormula) : χ.unload = ⌈⌈χ.split.1⌉⌉χ.split.2

Unloading a loaded formula gives the boxes of its split.

theorem Sequent.negBoxes_mem_right {X : Sequent} (h : X.isRightLoaded) : (~⌈⌈X.loadedProgs⌉⌉X.loadedFma) ∈ X.right

If the loaded formula of a sequent is on the right then the right component contains its unloading ¬⌈⌈δ⌉⌉ψ.

The witness distance

For a state v and a node x of the quasi-tableau, witDist M v Δ_x is the least δ_x-distance from v to a state satisfying ¬ψ_x, i.e. the paper's wd_M(v,x) in the case where M, v ⊨ Δ_x, ι_x. (In the other case the paper sets wd_M(v,x) := ∞; we do not need that, because we only ever use the value under that assumption.)

Note that witDist does not depend on the valuation of the internal variables — this is the paper's observation that M and M' have the same relational structure.

noncomputable def witDist {W : Type} (M : KripkeModel W) (v : W) (Δ : Sequent) : ℕ∞

The witness distance wd_M(v,x) of Lemma 10.7, as a function of the label Δ_x.

Equations

• witDist M v Δ = ⨅ (w : { w : W // evaluate M w (~Δ.loadedFma) }), distance_list M v (↑w) Δ.loadedProgs

theorem witDist_congr {W : Type} {M : KripkeModel W} {v : W} {Δ Y : Sequent} (h : Δ.loadedSplit = Y.loadedSplit) : witDist M v Δ = witDist M v Y

Basic nodes between two nodes of the quasi-tableau

The paper's "there is a basic node between x and z" means: a node of type 3 with a basic label on the path from x to z. Requiring type 3 is harmless (the label of a node of type 1 or 2 is the label of the node of type 3 below it) and it makes the property invariant under passing from a node of type 1 or 2 to its unique child.

def QuasiTab.BasicBetween (q : QuasiTab) (x z : List ℕ) : Prop

There is a node of type 3 with a basic label on the path from x to z.

Equations

• q.BasicBetween x z = ∃ (y : List ℕ) (Δ : Sequent), x <+: y ∧ y <+: z ∧ q.typAt y = some Typ.three ∧ q.labelAt y = some Δ ∧ Δ.basic

theorem QuasiTab.BasicBetween.mono {q : QuasiTab} {x x' z : List ℕ} (h : q.BasicBetween x' z) (hx : x <+: x') : q.BasicBetween x z

BasicBetween only grows when we move the left end towards the root.

theorem QuasiTab.BasicBetween.child {q : QuasiTab} {x y z : List ℕ} (h : q.BasicBetween x z) (hy : y <+: z) (hlen : y.length = x.length + 1) (hx : ∀ (Δ : Sequent), q.typAt x = some Typ.three → q.labelAt x = some Δ → ¬Δ.basic) : q.BasicBetween y z

If the left end x is not itself a basic node of type 3 then any basic node between x and z is also between the child of x on the path to z and z.

theorem QuasiTab.notBasic_of_typ_ne {q : QuasiTab} {x : List ℕ} {k : Typ} {Δ : Sequent} {next : List QuasiTab} (h : q.at? x = some (QNode k Δ next)) (hk : k ≠ Typ.three) (Y : Sequent) : q.typAt x = some Typ.three → q.labelAt x = some Y → ¬Y.basic

The node at address x is not a basic node of type 3, because its type is not 3.

theorem QuasiTab.notBasic_of_label {q : QuasiTab} {x : List ℕ} {k : Typ} {Δ : Sequent} {next : List QuasiTab} (h : q.at? x = some (QNode k Δ next)) (hb : ¬Δ.basic) (Y : Sequent) : q.typAt x = some Typ.three → q.labelAt x = some Y → ¬Y.basic

The node at address x is not a basic node of type 3, because its label is not basic.

theorem QuasiTab.at?_of_isRepeatLeaf {q : QuasiTab} {z : List ℕ} (h : q.isRepeatLeaf z = true) : ∃ (Z : Sequent), q.at? z = some (QNode Typ.one Z [])

A repeat leaf is a childless node of type 1.

theorem QuasiTab.prefix_of_mem_cycs {q : QuasiTab} {y z : List ℕ} (hz : z ∈ q.cycs y) : y <+: z

A cycle of y lies below y.