Vocabulary and other Syntax functions (part of Section 2.1)

Vocab

@[reducible, inline]

abbrev Vocab : Type

Equations

• Vocab = Finset (ℕ ⊕ ℕ)

def Vocab.atomProps : Vocab → Finset ℕ

Equations

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

def Vocab.atomProgs : Vocab → Finset ℕ

Equations

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

def Program.voc : Program → Vocab

Equations

• (·n).voc = {Sum.inr n}
• (α;'β).voc = α.voc ∪ β.voc
• (α⋓β).voc = α.voc ∪ β.voc
• (∗α).voc = α.voc
• (?'φ).voc = φ.voc

def Formula.voc : Formula → Vocab

Equations

• Formula.bottom.voc = ∅
• (·n).voc = {Sum.inl n}
• (~φ).voc = φ.voc
• (φ ⋀ ψ).voc = φ.voc ∪ ψ.voc
• (⌈α⌉φ).voc = α.voc ∪ φ.voc

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

Equations

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

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

Equations

• Vocab.fromFinset L = L.sup id

@[reducible, inline]

abbrev List.fvoc (L : List Formula) : Vocab

Equations

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

@[reducible, inline]

abbrev List.pvoc (L : List Program) : Vocab

Equations

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

@[reducible, inline]

abbrev Finset.fvoc (L : Finset Formula) : Vocab

Equations

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

@[reducible, inline]

abbrev Finset.pvoc (L : Finset Program) : Vocab

Equations

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

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

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

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

theorem Formula.voc_boxes {δ : List Program} {φ : Formula} : (⌈⌈δ⌉⌉φ).voc = δ.pvoc ∪ φ.voc

def LoadFormula.voc (lf : LoadFormula) : Vocab

Equations

• lf.voc = lf.unload.voc

def NegLoadFormula.voc (nlf : NegLoadFormula) : Vocab

Equations

• nlf.voc = (negUnload nlf).voc

Tests in a program

@[implicit_reducible]

def testsOfProgram : Program → List Formula

Test(α)

Equations

• testsOfProgram (·a) = []
• testsOfProgram (?'τ) = [τ]
• testsOfProgram (α;'β) = testsOfProgram α ++ testsOfProgram β
• testsOfProgram (α⋓β) = testsOfProgram α ++ testsOfProgram β
• testsOfProgram (∗α) = testsOfProgram α

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

Subprograms

def subprograms : Program → List Program

Prog(α)

Equations

• subprograms (·a) = [·a]
• subprograms (?'τ) = [?'τ]
• subprograms (α;'β) = [α;'β] ++ subprograms α ++ subprograms β
• subprograms (α⋓β) = [α⋓β] ++ subprograms α ++ subprograms β
• subprograms (∗α) = [∗α] ++ subprograms α

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

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

@[simp]

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

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

Fresh variables

def freshVarForm : Formula → ℕ

Get a fresh atomic proposition x not occuring in ψ.

Equations

• freshVarForm Formula.bottom = 0
• freshVarForm (·n) = n + 1
• freshVarForm (~φ) = freshVarForm φ
• freshVarForm (φ ⋀ ψ) = max (freshVarForm φ) (freshVarForm ψ)
• freshVarForm (⌈α⌉φ) = max (freshVarProg α) (freshVarForm φ)

def freshVarProg : Program → ℕ

Get a fresh atomic proposition x not occuring in α.

Equations

• freshVarProg (·n) = 0
• freshVarProg (α;'β) = max (freshVarProg α) (freshVarProg β)
• freshVarProg (α⋓β) = max (freshVarProg α) (freshVarProg β)
• freshVarProg (∗α) = freshVarProg α
• freshVarProg (?'φ) = freshVarForm φ

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

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

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

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