Vocabulary and other Syntax functions (part of Section 2.1)

Vocab

@[reducible, inline]

abbrev PDL.Vocab : Type

The finite set of proposition and program indices occurring in syntax.

Equations

• PDL.Vocab = Finset (ℕ ⊕ ℕ)

def PDL.Vocab.atomProps : Vocab → Finset ℕ

The atomic proposition indices in a vocabulary.

Equations

• X.atomProps = Finset.biUnion X fun (x : ℕ ⊕ ℕ) => match x with | Sum.inl n => {n} | Sum.inr val => ∅

def PDL.Vocab.atomProgs : Vocab → Finset ℕ

The atomic program indices in a vocabulary.

Equations

• X.atomProgs = Finset.biUnion X fun (x : ℕ ⊕ ℕ) => match x with | Sum.inl val => ∅ | Sum.inr n => {n}

def PDL.Program.voc : Program → Vocab

The proposition and program vocabulary occurring in a program.

Equations

• (PDL.Program.atom_prog n).voc = {Sum.inr n}
• (α.sequence β).voc = α.voc ∪ β.voc
• (α.union β).voc = α.voc ∪ β.voc
• α.star.voc = α.voc
• (PDL.Program.test φ).voc = φ.voc

def PDL.Formula.voc : Formula → Vocab

The proposition and program vocabulary occurring in a formula.

Equations

• PDL.Formula.bottom.voc = ∅
• (PDL.Formula.atom_prop n).voc = {Sum.inl n}
• φ.neg.voc = φ.voc
• (φ.and ψ).voc = φ.voc ∪ ψ.voc
• (PDL.Formula.box α φ).voc = α.voc ∪ φ.voc

def PDL.Vocab.fromList (L : List Vocab) : Vocab

The union of the vocabularies in a list.

Equations

• PDL.Vocab.fromList L = L.toFinset.sup id

def PDL.Vocab.fromFinset (L : Finset Vocab) : Vocab

The union of the vocabularies in a finset.

Equations

• PDL.Vocab.fromFinset L = L.sup id

@[reducible, inline]

abbrev List.pdlFvoc (L : List PDL.Formula) : PDL.Vocab

The combined vocabulary of a list of formulas.

Equations

• L.pdlFvoc = PDL.Vocab.fromList (List.map PDL.Formula.voc L)

@[reducible, inline]

abbrev List.pdlPvoc (L : List PDL.Program) : PDL.Vocab

The combined vocabulary of a list of programs.

Equations

• L.pdlPvoc = PDL.Vocab.fromList (List.map PDL.Program.voc L)

@[reducible, inline]

abbrev Finset.pdlFvoc (L : Finset PDL.Formula) : PDL.Vocab

The combined vocabulary of a finset of formulas.

Equations

• L.pdlFvoc = PDL.Vocab.fromFinset (Finset.image PDL.Formula.voc L)

@[reducible, inline]

abbrev Finset.pdlPvoc (L : Finset PDL.Program) : PDL.Vocab

The combined vocabulary of a finset of programs.

Equations

• L.pdlPvoc = PDL.Vocab.fromFinset (Finset.image PDL.Program.voc L)

theorem PDL.Finset.mem_fvoc {X : Finset Formula} {x : ℕ ⊕ ℕ} : x ∈ X.pdlFvoc ↔ ∃ φ ∈ X, x ∈ φ.voc

theorem PDL.Finset.fvoc_union {X Y : Finset Formula} : (X ∪ Y).pdlFvoc = X.pdlFvoc ∪ Y.pdlFvoc

theorem PDL.Finset.fvoc_mono {X Y : Finset Formula} (h : X ⊆ Y) : X.pdlFvoc ⊆ Y.pdlFvoc

theorem PDL.fvoc_subset_of_mem_voc {L L' : Finset Formula} (h : ∀ f ∈ L, ∃ g ∈ L', f.voc ⊆ g.voc) : L.pdlFvoc ⊆ L'.pdlFvoc

The vocabulary of a finset of formulas only grows when we add formulas with larger vocabularies.

theorem PDL.Vocab.fromList_append {L R : List Vocab} : fromList (L ++ R) = fromList L ∪ fromList R

theorem PDL.Vocab.fromList_map_iff {α : Type u_1} (n : ℕ ⊕ ℕ) (L : List α) (f : α → Vocab) : n ∈ fromList (List.map f L) ↔ ∃ x ∈ L, n ∈ f x

theorem PDL.Vocab.fromListFormula_map_iff (n : ℕ ⊕ ℕ) (L : List Formula) : n ∈ fromList (List.map Formula.voc L) ↔ ∃ φ ∈ L, n ∈ φ.voc

theorem PDL.Vocab.fromListProgram_map_iff {vocabOfProgram : Program → Vocab} (n : ℕ ⊕ ℕ) (L : List Program) : n ∈ fromList (List.map vocabOfProgram L) ↔ ∃ α ∈ L, n ∈ vocabOfProgram α

theorem PDL.Formula.voc_boxes {δ : List Program} {φ : Formula} : (boxes δ φ).voc = δ.pdlPvoc ∪ φ.voc

def PDL.LoadFormula.voc (lf : LoadFormula) : Vocab

The vocabulary of a loaded formula after erasing its loading annotations.

Equations

• lf.voc = lf.unload.voc

def PDL.NegLoadFormula.voc (nlf : NegLoadFormula) : Vocab

The vocabulary of a negated loaded formula after erasing its loading annotations.

Equations

• nlf.voc = (PDL.negUnload nlf).voc

Tests in a program

@[implicit_reducible]

def PDL.testsOfProgram : Program → List Formula

Test(α)

Equations

• PDL.testsOfProgram (PDL.Program.atom_prog a) = []
• PDL.testsOfProgram (PDL.Program.test τ) = [τ]
• PDL.testsOfProgram (α.sequence β) = PDL.testsOfProgram α ++ PDL.testsOfProgram β
• PDL.testsOfProgram (α.union β) = PDL.testsOfProgram α ++ PDL.testsOfProgram β
• PDL.testsOfProgram α.star = PDL.testsOfProgram α

theorem PDL.testsOfProgram.voc (α : Program) {τ : Formula} (τ_in : τ ∈ testsOfProgram α) : τ.voc ⊆ α.voc

Subprograms

def PDL.subprograms : Program → List Program

Prog(α)

Equations

• PDL.subprograms (PDL.Program.atom_prog a) = [PDL.Program.atom_prog a]
• PDL.subprograms (PDL.Program.test τ) = [PDL.Program.test τ]
• PDL.subprograms (α.sequence β) = [α.sequence β] ++ PDL.subprograms α ++ PDL.subprograms β
• PDL.subprograms (α.union β) = [α.union β] ++ PDL.subprograms α ++ PDL.subprograms β
• PDL.subprograms α.star = [α.star] ++ PDL.subprograms α

theorem PDL.subprograms_length {α β : Program} : β ∈ subprograms α → lengthOfProgram β ≤ lengthOfProgram α

theorem PDL.length_lt_of_mem_subprograms_erase {α β : Program} : β ∈ (subprograms α).erase α → lengthOfProgram β < lengthOfProgram α

@[simp]

theorem PDL.subprograms.refl {α : Program} : α ∈ subprograms α

theorem PDL.subprograms_voc {α β : Program} : β ∈ subprograms α → β.voc ⊆ α.voc

Fresh variables

def PDL.freshVarForm : Formula → ℕ

Get a fresh atomic proposition x not occuring in ψ.

Equations

• PDL.freshVarForm PDL.Formula.bottom = 0
• PDL.freshVarForm (PDL.Formula.atom_prop n) = n + 1
• PDL.freshVarForm φ.neg = PDL.freshVarForm φ
• PDL.freshVarForm (φ.and ψ) = max (PDL.freshVarForm φ) (PDL.freshVarForm ψ)
• PDL.freshVarForm (PDL.Formula.box α φ) = max (PDL.freshVarProg α) (PDL.freshVarForm φ)

def PDL.freshVarProg : Program → ℕ

Get a fresh atomic proposition x not occuring in α.

Equations

• PDL.freshVarProg (PDL.Program.atom_prog n) = 0
• PDL.freshVarProg (α.sequence β) = max (PDL.freshVarProg α) (PDL.freshVarProg β)
• PDL.freshVarProg (α.union β) = max (PDL.freshVarProg α) (PDL.freshVarProg β)
• PDL.freshVarProg α.star = PDL.freshVarProg α
• PDL.freshVarProg (PDL.Program.test φ) = PDL.freshVarForm φ

theorem PDL.freshVarForm_is_larger (φ : Formula) (n : ℕ) : n ∈ φ.voc.atomProps → n < freshVarForm φ

theorem PDL.freshVarProg_is_larger (α : Program) (n : ℕ) : n ∈ α.voc.atomProps → n < freshVarProg α

theorem PDL.freshVarForm_is_fresh (φ : Formula) : Sum.inl (freshVarForm φ) ∉ φ.voc

theorem PDL.freshVarProg_is_fresh (α : Program) : Sum.inl (freshVarProg α) ∉ α.voc