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 α⃗ 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 QFormula (Var : Type) : Type

Def 9.15: the set L_Q of Q-formulas, given by the grammar ι ::= ψ | q | ι ∧ ι | □(α⃗, ι). Here Var is the type of internal variables, i.e. the paper's { q_x | x ∈ K_Q }. The side condition that ψ and α⃗ 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 □(α⃗, ι) over a sequence of programs.

@[instance_reducible]

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

Equations

• instReprQFormula = { reprPrec := instReprQFormula.repr }

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

Equations

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

def 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.
• instDecidableEqQFormula.decEq (QFormula.fma a) (QFormula.fma b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqQFormula.decEq (QFormula.fma a) (QFormula.var a_1) = isFalse ⋯
• instDecidableEqQFormula.decEq (QFormula.fma a) (a_1.and a_2) = isFalse ⋯
• instDecidableEqQFormula.decEq (QFormula.fma a) (QFormula.boxes a_1 a_2) = isFalse ⋯
• instDecidableEqQFormula.decEq (QFormula.var a) (QFormula.fma a_1) = isFalse ⋯
• instDecidableEqQFormula.decEq (QFormula.var a) (QFormula.var b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqQFormula.decEq (QFormula.var a) (a_1.and a_2) = isFalse ⋯
• instDecidableEqQFormula.decEq (QFormula.var a) (QFormula.boxes a_1 a_2) = isFalse ⋯
• instDecidableEqQFormula.decEq (a.and a_1) (QFormula.fma a_2) = isFalse ⋯
• instDecidableEqQFormula.decEq (a.and a_1) (QFormula.var a_2) = isFalse ⋯
• instDecidableEqQFormula.decEq (a.and a_1) (QFormula.boxes a_2 a_3) = isFalse ⋯
• instDecidableEqQFormula.decEq (QFormula.boxes a a_1) (QFormula.fma a_2) = isFalse ⋯
• instDecidableEqQFormula.decEq (QFormula.boxes a a_1) (QFormula.var a_2) = isFalse ⋯
• instDecidableEqQFormula.decEq (QFormula.boxes a a_1) (a_2.and a_3) = isFalse ⋯

@[instance_reducible]

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

Equations

• instDecidableEqQFormula = instDecidableEqQFormula.decEq

def 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

• QFormula.subst σ (QFormula.fma a) = a
• QFormula.subst σ (QFormula.var a) = σ a
• QFormula.subst σ (a.and a_1) = QFormula.subst σ a ⋀ QFormula.subst σ a_1
• QFormula.subst σ (QFormula.boxes a a_1) = ⌈⌈a⌉⌉QFormula.subst σ a_1

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The internal variables occurring in a Q-formula.

Equations

• (QFormula.fma a).vars = []
• (QFormula.var a).vars = [a]
• (a.and a_1).vars = a.vars ++ a_1.vars
• (QFormula.boxes a a_1).vars = a_1.vars

@[irreducible]

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

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

Equations

• QFormula.substVar x ρ (QFormula.fma a) = QFormula.fma a
• QFormula.substVar x ρ (QFormula.var a) = if a = x then ρ else QFormula.var a
• QFormula.substVar x ρ (a.and a_1) = (QFormula.substVar x ρ a).and (QFormula.substVar x ρ a_1)
• QFormula.substVar x ρ (QFormula.boxes a a_1) = QFormula.boxes a (QFormula.substVar x ρ a_1)

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

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

Equations

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

@[simp]

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

@[simp]

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

theorem 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 QSimple (Var : Type) : Type

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

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

def 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 instReprQSimple {Var✝ : Type} [Repr Var✝] : Repr (QSimple Var✝)

Equations

• instReprQSimple = { reprPrec := instReprQSimple.repr }

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

Equations

• instDecidableEqQSimple.decEq (QSimple.fma a) (QSimple.fma b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqQSimple.decEq (QSimple.fma a) (QSimple.boxVar a_1 a_2) = isFalse ⋯
• instDecidableEqQSimple.decEq (QSimple.boxVar a a_1) (QSimple.fma a_2) = isFalse ⋯
• instDecidableEqQSimple.decEq (QSimple.boxVar a a_1) (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 instDecidableEqQSimple {Var✝ : Type} [DecidableEq Var✝] : DecidableEq (QSimple Var✝)

Equations

• instDecidableEqQSimple = instDecidableEqQSimple.decEq

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

A simple Q-formula is a Q-formula.

Equations

• (QSimple.fma a).toQ = QFormula.fma a
• (QSimple.boxVar a a_1).toQ = QFormula.boxes a (QFormula.var a_1)

def 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

• QSimple.prefixBoxes as (QSimple.fma a) = QSimple.fma (⌈⌈as⌉⌉a)
• QSimple.prefixBoxes as (QSimple.boxVar a a_1) = QSimple.boxVar (as ++ a) a_1

@[simp]

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

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

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

Equations

• QSimple.mentions x (QSimple.fma a) = false
• QSimple.mentions x (QSimple.boxVar a a_1) = decide (a_1 = x)

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

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

Equations

• QSimple.progTo? x (QSimple.fma a) = none
• QSimple.progTo? x (QSimple.boxVar a a_1) = if a_1 = x then some (Program.steps a) else none

def 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

• (QFormula.fma a).Spl = [QSimple.fma a]
• (QFormula.var a).Spl = [QSimple.boxVar [?'⊤] a]
• (a.and a_1).Spl = a.Spl ++ a_1.Spl
• (QFormula.boxes a a_1).Spl = List.map (QSimple.prefixBoxes a) a_1.Spl

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

Spl(ι) is never empty.

def 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 = QFormula.conj (List.map QSimple.toQ ι.Spl)

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

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

Equations

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

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

theorem 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 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 QFormula.voc_toQ_prefixBoxes {Var : Type} (as : List Program) (s : QSimple Var) (σ : Var → Formula) : (subst σ (QSimple.prefixBoxes as s).toQ).voc = as.pvoc ∪ (subst σ s.toQ).voc

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

theorem 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 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 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

• QFormula.loopProgs x ι = List.filterMap (QSimple.progTo? x) ι.Spl

def 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

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

def 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

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

theorem 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 ι.