Q-formulas and their normal form (Definitions 9.15, 9.16 and Fact 9.17)

The pre-interpolants of Definition 9.18 are not arbitrary formulas: they are built from "ordinary" formulas and from internal variables q_x, one for each companion node x of the quasi-tableau Q, using only conjunction and (sequences of) boxes.

Instead of using fresh proposition letters for the internal variables we use a separate constructor QFormula.var of a new data type QFormula Var, where Var is the type of internal variables. This makes the side condition of Definition 9.15 — that the vocabulary of the ordinary formulas ψ and of the programs αs contains no internal variables — true by construction, and it avoids having to pick fresh proposition letters.

To read a QFormula as an actual Formula one has to say what the internal variables stand for. This is done by QFormula.subst σ where σ : Var → Formula. Taking σ x = ·(n x) for an injection n into unused proposition letters gives the formulas of the paper, but the extra generality is exactly what is needed later: in the correctness proof the internal variables get replaced by other formulas.

Definition 9.15: the language L_Q

inductive PDL.QFormula (Var : Type) : Type

Def 9.15: the set L_Q of Q-formulas, given by the grammar ι ::= ψ | q | ι ∧ ι | □(αs, ι). Here Var is the type of internal variables, i.e. the paper's { q_x | x ∈ K_Q }. The side condition that ψ and αs contain no internal variables is automatic here because internal variables are not Formulas.

• fma {Var : Type} : Formula → QFormula Var

  An ordinary formula ψ, containing no internal variables.

• var {Var : Type} : Var → QFormula Var

  An internal variable q_x.

• and {Var : Type} : QFormula Var → QFormula Var → QFormula Var

  A conjunction ι₁ ∧ ι₂.

• boxes {Var : Type} : List Program → QFormula Var → QFormula Var

  A box □(αs, ι) over a sequence of programs.

def PDL.instReprQFormula.repr {Var✝ : Type} [Repr Var✝] : QFormula Var✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance PDL.instReprQFormula {Var✝ : Type} [Repr Var✝] : Repr (QFormula Var✝)

Equations

• PDL.instReprQFormula = { reprPrec := PDL.instReprQFormula.repr }

def PDL.instDecidableEqQFormula.decEq {Var✝ : Type} [DecidableEq Var✝] (x✝ x✝¹ : QFormula Var✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• PDL.instDecidableEqQFormula.decEq (PDL.QFormula.fma a) (PDL.QFormula.fma b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• PDL.instDecidableEqQFormula.decEq (PDL.QFormula.fma a) (PDL.QFormula.var a_1) = isFalse ⋯
• PDL.instDecidableEqQFormula.decEq (PDL.QFormula.fma a) (a_1.and a_2) = isFalse ⋯
• PDL.instDecidableEqQFormula.decEq (PDL.QFormula.fma a) (PDL.QFormula.boxes a_1 a_2) = isFalse ⋯
• PDL.instDecidableEqQFormula.decEq (PDL.QFormula.var a) (PDL.QFormula.fma a_1) = isFalse ⋯
• PDL.instDecidableEqQFormula.decEq (PDL.QFormula.var a) (PDL.QFormula.var b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• PDL.instDecidableEqQFormula.decEq (PDL.QFormula.var a) (a_1.and a_2) = isFalse ⋯
• PDL.instDecidableEqQFormula.decEq (PDL.QFormula.var a) (PDL.QFormula.boxes a_1 a_2) = isFalse ⋯
• PDL.instDecidableEqQFormula.decEq (a.and a_1) (PDL.QFormula.fma a_2) = isFalse ⋯
• PDL.instDecidableEqQFormula.decEq (a.and a_1) (PDL.QFormula.var a_2) = isFalse ⋯
• PDL.instDecidableEqQFormula.decEq (a.and a_1) (PDL.QFormula.boxes a_2 a_3) = isFalse ⋯
• PDL.instDecidableEqQFormula.decEq (PDL.QFormula.boxes a a_1) (PDL.QFormula.fma a_2) = isFalse ⋯
• PDL.instDecidableEqQFormula.decEq (PDL.QFormula.boxes a a_1) (PDL.QFormula.var a_2) = isFalse ⋯
• PDL.instDecidableEqQFormula.decEq (PDL.QFormula.boxes a a_1) (a_2.and a_3) = isFalse ⋯

@[instance_reducible]

instance PDL.instDecidableEqQFormula {Var✝ : Type} [DecidableEq Var✝] : DecidableEq (QFormula Var✝)

Equations

• PDL.instDecidableEqQFormula = PDL.instDecidableEqQFormula.decEq

def PDL.QFormula.subst {Var : Type} (σ : Var → Formula) : QFormula Var → Formula

Replace the internal variables in a Q-formula according to σ, yielding a Formula. For σ x = ·(n x) with n injective into unused proposition letters this is the formula that the paper denotes by ι itself.

Equations

• PDL.QFormula.subst σ (PDL.QFormula.fma ψ) = ψ
• PDL.QFormula.subst σ (PDL.QFormula.var q) = σ q
• PDL.QFormula.subst σ (ι1.and ι2) = (PDL.QFormula.subst σ ι1).and (PDL.QFormula.subst σ ι2)
• PDL.QFormula.subst σ (PDL.QFormula.boxes as ι) = PDL.Formula.boxes as (PDL.QFormula.subst σ ι)

@[simp]

theorem PDL.QFormula.subst_fma {Var : Type} {σ : Var → Formula} {ψ : Formula} : subst σ (fma ψ) = ψ

@[simp]

theorem PDL.QFormula.subst_var {Var : Type} {σ : Var → Formula} {q : Var} : subst σ (var q) = σ q

@[simp]

theorem PDL.QFormula.subst_and {Var : Type} {σ : Var → Formula} {ι1 ι2 : QFormula Var} : subst σ (ι1.and ι2) = (subst σ ι1).and (subst σ ι2)

@[simp]

theorem PDL.QFormula.subst_boxes {Var : Type} {σ : Var → Formula} {as : List Program} {ι : QFormula Var} : subst σ (boxes as ι) = Formula.boxes as (subst σ ι)

def PDL.QFormula.vars {Var : Type} : QFormula Var → List Var

The internal variables occurring in a Q-formula.

Equations

• (PDL.QFormula.fma ψ).vars = []
• (PDL.QFormula.var q).vars = [q]
• (ι1.and ι2).vars = ι1.vars ++ ι2.vars
• (PDL.QFormula.boxes as ι).vars = ι.vars

@[irreducible]

def PDL.QFormula.substVar {Var : Type} [DecidableEq Var] (x : Var) (ρ ι : QFormula Var) : QFormula Var

Substitute the Q-formula ρ for the internal variable x.

Equations

• PDL.QFormula.substVar x ρ (PDL.QFormula.fma ψ) = PDL.QFormula.fma ψ
• PDL.QFormula.substVar x ρ (PDL.QFormula.var q) = if q = x then ρ else PDL.QFormula.var q
• PDL.QFormula.substVar x ρ (ι1.and ι2) = (PDL.QFormula.substVar x ρ ι1).and (PDL.QFormula.substVar x ρ ι2)
• PDL.QFormula.substVar x ρ (PDL.QFormula.boxes as ι_1) = PDL.QFormula.boxes as (PDL.QFormula.substVar x ρ ι_1)

def PDL.QFormula.conj {Var : Type} : List (QFormula Var) → QFormula Var

Big conjunction of a list of Q-formulas, mirroring con on formulas.

Equations

• PDL.QFormula.conj [] = PDL.QFormula.fma ⊤
• PDL.QFormula.conj [ι] = ι
• PDL.QFormula.conj (ι :: rest) = ι.and (PDL.QFormula.conj rest)

@[simp]

theorem PDL.QFormula.conj_nil {Var : Type} : conj [] = fma ⊤

@[simp]

theorem PDL.QFormula.conj_singleton {Var : Type} {ι : QFormula Var} : conj [ι] = ι

theorem PDL.QFormula.subst_conj {Var : Type} (σ : Var → Formula) (L : List (QFormula Var)) : subst σ (conj L) = con (List.map (subst σ) L)

Substitution commutes with big conjunction.

Simple Q-formulas and Definition 9.16: the normal form

inductive PDL.QSimple (Var : Type) : Type

A simple Q-formula (Def 9.15): either an ordinary formula ψ or a box □(αs, q_x) over an internal variable.

• fma {Var : Type} : Formula → QSimple Var
• boxVar {Var : Type} : List Program → Var → QSimple Var

def PDL.instReprQSimple.repr {Var✝ : Type} [Repr Var✝] : QSimple Var✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance PDL.instReprQSimple {Var✝ : Type} [Repr Var✝] : Repr (QSimple Var✝)

Equations

• PDL.instReprQSimple = { reprPrec := PDL.instReprQSimple.repr }

def PDL.instDecidableEqQSimple.decEq {Var✝ : Type} [DecidableEq Var✝] (x✝ x✝¹ : QSimple Var✝) : Decidable (x✝ = x✝¹)

Equations

• PDL.instDecidableEqQSimple.decEq (PDL.QSimple.fma a) (PDL.QSimple.fma b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• PDL.instDecidableEqQSimple.decEq (PDL.QSimple.fma a) (PDL.QSimple.boxVar a_1 a_2) = isFalse ⋯
• PDL.instDecidableEqQSimple.decEq (PDL.QSimple.boxVar a a_1) (PDL.QSimple.fma a_2) = isFalse ⋯
• PDL.instDecidableEqQSimple.decEq (PDL.QSimple.boxVar a a_1) (PDL.QSimple.boxVar b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance PDL.instDecidableEqQSimple {Var✝ : Type} [DecidableEq Var✝] : DecidableEq (QSimple Var✝)

Equations

• PDL.instDecidableEqQSimple = PDL.instDecidableEqQSimple.decEq

def PDL.QSimple.toQ {Var : Type} : QSimple Var → QFormula Var

A simple Q-formula is a Q-formula.

Equations

• (PDL.QSimple.fma ψ).toQ = PDL.QFormula.fma ψ
• (PDL.QSimple.boxVar as q).toQ = PDL.QFormula.boxes as (PDL.QFormula.var q)

def PDL.QSimple.prefixBoxes {Var : Type} (as : List Program) : QSimple Var → QSimple Var

Prefix a simple Q-formula with a sequence of boxes; the result is again simple.

Equations

• PDL.QSimple.prefixBoxes as (PDL.QSimple.fma ψ) = PDL.QSimple.fma (PDL.Formula.boxes as ψ)
• PDL.QSimple.prefixBoxes as (PDL.QSimple.boxVar as_1 q) = PDL.QSimple.boxVar (as ++ as_1) q

@[simp]

theorem PDL.QSimple.toQ_prefixBoxes {Var : Type} (as : List Program) (s : QSimple Var) (σ : Var → Formula) : QFormula.subst σ (prefixBoxes as s).toQ = Formula.boxes as (QFormula.subst σ s.toQ)

def PDL.QSimple.mentions {Var : Type} [DecidableEq Var] (x : Var) : QSimple Var → Bool

Does the simple Q-formula mention the internal variable x?

Equations

• PDL.QSimple.mentions x (PDL.QSimple.fma ψ) = false
• PDL.QSimple.mentions x (PDL.QSimple.boxVar as q) = decide (q = x)

def PDL.QSimple.progToOpt {Var : Type} [DecidableEq Var] (x : Var) : QSimple Var → Option Program

If the simple Q-formula is □(αs, q_x) then return the program αs as one program.

Equations

• PDL.QSimple.progToOpt x (PDL.QSimple.fma ψ) = none
• PDL.QSimple.progToOpt x (PDL.QSimple.boxVar as q) = if q = x then some (PDL.Program.steps as) else none

def PDL.QFormula.Spl {Var : Type} : QFormula Var → List (QSimple Var)

Def 9.16: the finite set Spl(ι) of simple Q-formulas of a Q-formula ι. Note that Spl(q_x) = { [⊤?]q_x }, i.e. we make the variable into a box formula.

Equations

• (PDL.QFormula.fma ψ).Spl = [PDL.QSimple.fma ψ]
• (PDL.QFormula.var q).Spl = [PDL.QSimple.boxVar [PDL.Program.test ⊤] q]
• (ι1.and ι2).Spl = ι1.Spl ++ ι2.Spl
• (PDL.QFormula.boxes as ι).Spl = List.map (PDL.QSimple.prefixBoxes as) ι.Spl

theorem PDL.QFormula.Spl_ne_nil {Var : Type} (ι : QFormula Var) : ι.Spl ≠ []

Spl(ι) is never empty.

def PDL.QFormula.nf {Var : Type} (ι : QFormula Var) : QFormula Var

Def 9.16: the normal form ι^nf of a Q-formula, the conjunction of Spl(ι).

Equations

• ι.nf = PDL.QFormula.conj (List.map PDL.QSimple.toQ ι.Spl)

def PDL.QFormula.IsNormalForm {Var : Type} (ι : QFormula Var) : Prop

Being in normal form: a conjunction of simple Q-formulas.

Equations

• ι.IsNormalForm = ∃ (L : List (PDL.QSimple Var)), ι = PDL.QFormula.conj (List.map PDL.QSimple.toQ L)

theorem PDL.QFormula.isNormalForm_nf {Var : Type} (ι : QFormula Var) : ι.nf.IsNormalForm

theorem PDL.QFormula.eval_nf_iff {Var W : Type} {M : KripkeModel W} {w : W} (σ : Var → Formula) (ι : QFormula Var) : evaluate M w (subst σ ι.nf) ↔ ∀ s ∈ ι.Spl, evaluate M w (subst σ s.toQ)

Evaluating a normal form means evaluating all its simple conjuncts.

Fact 9.17

theorem PDL.QFormula.eval_nf {Var W : Type} {M : KripkeModel W} {w : W} (σ : Var → Formula) (ι : QFormula Var) : evaluate M w (subst σ ι.nf) ↔ evaluate M w (subst σ ι)

Fact 9.17, first part: every Q-formula is equivalent to its normal form.

theorem PDL.QFormula.voc_toQ_prefixBoxes {Var : Type} (as : List Program) (s : QSimple Var) (σ : Var → Formula) : (subst σ (QSimple.prefixBoxes as s).toQ).voc = as.pdlPvoc ∪ (subst σ s.toQ).voc

The vocabulary of a simple Q-formula prefixed with boxes.

theorem PDL.QFormula.mem_voc_nf {Var : Type} {n : ℕ ⊕ ℕ} (σ : Var → Formula) (ι : QFormula Var) : n ∈ (subst σ ι.nf).voc ↔ ∃ s ∈ ι.Spl, n ∈ (subst σ s.toQ).voc

The vocabulary of a normal form is the union of the vocabularies of its conjuncts.

theorem PDL.QFormula.voc_nf {Var : Type} (σ : Var → Formula) (ι : QFormula Var) : (subst σ ι.nf).voc = (subst σ ι).voc

Fact 9.17, second part: a Q-formula and its normal form have the same vocabulary.

The fixpoint elimination used at companion nodes (part of Definition 9.18)

Given ι with normal form ⋀ᵢ [αᵢ]q_x ∧ ⋀ⱼ [βⱼ]q_{zⱼ} ∧ ψ, the pre-interpolant of the companion x is [(⋃ᵢ αᵢ)*](⋀ⱼ [βⱼ]q_{zⱼ} ∧ ψ). We implement this here as QFormula.gfp x ι, using Spl to read off the αᵢ and the remaining conjuncts.

def PDL.QFormula.loopProgs {Var : Type} [DecidableEq Var] (x : Var) (ι : QFormula Var) : List Program

The programs αᵢ such that [αᵢ]q_x is a conjunct of the normal form of ι.

Equations

• PDL.QFormula.loopProgs x ι = List.filterMap (PDL.QSimple.progToOpt x) ι.Spl

def PDL.QFormula.dropVar {Var : Type} [DecidableEq Var] (x : Var) (ι : QFormula Var) : QFormula Var

The conjunction of those conjuncts of the normal form of ι that do not mention the internal variable x.

Equations

• PDL.QFormula.dropVar x ι = PDL.QFormula.conj (List.map PDL.QSimple.toQ (List.filter (fun (s : PDL.QSimple Var) => !PDL.QSimple.mentions x s) ι.Spl))

def PDL.QFormula.gfp {Var : Type} [DecidableEq Var] (x : Var) (ι : QFormula Var) : QFormula Var

The greatest fixpoint of ι with respect to the internal variable x, i.e. the formula [(⋃ᵢ αᵢ)*](⋀ⱼ [βⱼ]q_{zⱼ} ∧ ψ) of the companion case of Definition 9.18.

Equations

• PDL.QFormula.gfp x ι = PDL.QFormula.boxes [(PDL.Program.unions (PDL.QFormula.loopProgs x ι)).star] (PDL.QFormula.dropVar x ι)

theorem PDL.QFormula.not_mem_vars_gfp {Var : Type} [DecidableEq Var] (x : Var) (ι : QFormula Var) : x ∉ (gfp x ι).vars

The internal variable x no longer occurs in gfp x ι.