PdlTestFree.Basic

PdlTestFree
Basic

Imports

module

public import Pdl.Semantics
public import Pdl.Vocab

@[expose] public section

Basics

The definitions from Section 3 of the paper that are not already in lean4-pdl: test-free formulas and programs, modal depth, depth-bounded agreement of two states, and interpolants.

Test-free formulas and programs

A formula is test-free if no test occurs in it.

A program is test-free if no test occurs in it.

mutual  @[simp]
  def Formula.testFree : Formula → Prop
    | ⊥ => True
    | ·_ => True
    | ~φ => φ.testFree
    | φ ⋀ ψ => φ.testFree ∧ ψ.testFree
    | ⌈α⌉ φ => α.testFree ∧ φ.testFree  @[simp]
  def Program.testFree : Program → Prop
    | ·_ => True
    | α ;' β => α.testFree ∧ β.testFree
    | α ⋓ β => α.testFree ∧ β.testFree
    | ∗α => α.testFree
    | ?'_ => False
end

The vocabulary of a test-free program consists of atomic programs only.

theorem Program.testFree_voc : ∀ (α : Program), α.testFree → ∀ x ∈ α.voc, ∃ c, x = Sum.inr c
  | ·c, _, x, hx => ⟨c, byc:ℕx✝:(·c).testFreex:ℕ ⊕ ℕhx:x ∈ (·c).voc⊢ x = Sum.inr c simpa using hxAll goals completed! 🐙⟩
  | α ;' β, h, x, hx =>α:Programβ:Programh:(α;'β).testFreex:ℕ ⊕ ℕhx:x ∈ (α;'β).voc⊢ ∃ c, x = Sum.inr c byα:Programβ:Programh:(α;'β).testFreex:ℕ ⊕ ℕhx:x ∈ (α;'β).voc⊢ ∃ c, x = Sum.inr c
      simp only [Program.testFree] at hα:Programβ:Programh:α.testFree ∧ β.testFreex:ℕ ⊕ ℕhx:x ∈ (α;'β).voc⊢ ∃ c, x = Sum.inr c
      simp only [Program.voc, Finset.mem_union] at hxα:Programβ:Programh:α.testFree ∧ β.testFreex:ℕ ⊕ ℕhx:x ∈ α.voc ∨ x ∈ β.voc⊢ ∃ c, x = Sum.inr c
      rcases hx with hx | hxinlα:Programβ:Programh:α.testFree ∧ β.testFreex:ℕ ⊕ ℕhx:x ∈ α.voc⊢ ∃ c, x = Sum.inr cinrα:Programβ:Programh:α.testFree ∧ β.testFreex:ℕ ⊕ ℕhx:x ∈ β.voc⊢ ∃ c, x = Sum.inr c
      ·inlα:Programβ:Programh:α.testFree ∧ β.testFreex:ℕ ⊕ ℕhx:x ∈ α.voc⊢ ∃ c, x = Sum.inr c exact Program.testFree_voc α h.1 x hxAll goals completed! 🐙
      ·inrα:Programβ:Programh:α.testFree ∧ β.testFreex:ℕ ⊕ ℕhx:x ∈ β.voc⊢ ∃ c, x = Sum.inr c exact Program.testFree_voc β h.2 x hxAll goals completed! 🐙
  | α ⋓ β, h, x, hx =>α:Programβ:Programh:(α⋓β).testFreex:ℕ ⊕ ℕhx:x ∈ (α⋓β).voc⊢ ∃ c, x = Sum.inr c byα:Programβ:Programh:(α⋓β).testFreex:ℕ ⊕ ℕhx:x ∈ (α⋓β).voc⊢ ∃ c, x = Sum.inr c
      simp only [Program.testFree] at hα:Programβ:Programh:α.testFree ∧ β.testFreex:ℕ ⊕ ℕhx:x ∈ (α⋓β).voc⊢ ∃ c, x = Sum.inr c
      simp only [Program.voc, Finset.mem_union] at hxα:Programβ:Programh:α.testFree ∧ β.testFreex:ℕ ⊕ ℕhx:x ∈ α.voc ∨ x ∈ β.voc⊢ ∃ c, x = Sum.inr c
      rcases hx with hx | hxinlα:Programβ:Programh:α.testFree ∧ β.testFreex:ℕ ⊕ ℕhx:x ∈ α.voc⊢ ∃ c, x = Sum.inr cinrα:Programβ:Programh:α.testFree ∧ β.testFreex:ℕ ⊕ ℕhx:x ∈ β.voc⊢ ∃ c, x = Sum.inr c
      ·inlα:Programβ:Programh:α.testFree ∧ β.testFreex:ℕ ⊕ ℕhx:x ∈ α.voc⊢ ∃ c, x = Sum.inr c exact Program.testFree_voc α h.1 x hxAll goals completed! 🐙
      ·inrα:Programβ:Programh:α.testFree ∧ β.testFreex:ℕ ⊕ ℕhx:x ∈ β.voc⊢ ∃ c, x = Sum.inr c exact Program.testFree_voc β h.2 x hxAll goals completed! 🐙
  | ∗α, h, x, hx => Program.testFree_voc α h x hx
  | ?'_, h, _, _ =>a✝:Formulah:(?'a✝).testFreex✝¹:ℕ ⊕ ℕx✝:x✝¹ ∈ (?'a✝).voc⊢ ∃ c, x✝¹ = Sum.inr c bya✝:Formulah:(?'a✝).testFreex✝¹:ℕ ⊕ ℕx✝:x✝¹ ∈ (?'a✝).voc⊢ ∃ c, x✝¹ = Sum.inr c simp only [Program.testFree] at hAll goals completed! 🐙

The modal depth of a (test-free) formula. It is shallow in the sense that it does not care about the structure of programs: ⟨a ⋓ b⟩p and ⟨a ;' (∗b ⋓ c)⟩p both have depth 1.

def mdepth : Formula → ℕ
  | ⊥ => 0
  | ·_ => 0
  | ~φ => mdepth φ
  | φ ⋀ ψ => max (mdepth φ) (mdepth ψ)
  | ⌈_⌉ φ => mdepth φ + 1

agree M A j w₁ w₂: the states w₁ and w₂ agree test-free on A up to j, i.e. they satisfy the same test-free formulas with vocabulary in A and modal depth at most j.

def agree {W : Type} (M : KripkeModel W) (A : Vocab) (j : ℕ) (w₁ w₂ : W) : Prop :=
  ∀ φ : Formula, φ.testFree → φ.voc ⊆ A → mdepth φ ≤ j →
    (evaluate M w₁ φ ↔ evaluate M w₂ φ)

Basics

Test-free formulas and programs

Modal depth and depth-bounded agreement