Fischer-Ladner Closure

Here we define a closure on sets (well, actually lists) of formulas. Our main reference for this closure is Section 6.1 of [HKT00] which also was used in a Rocq formalization in [DB18]. The code for that work can be found at github.com/chdoc/comp-dec-pdl and their FL closure definition starts at line 472 of PDL_def.v.

See also Definition 4.79 and Exercise 4.8.2 in [BdRV01]. An alternative version following the proof of Theorem 3.2 in [FL79] but unfinished is in Unused/FischerLadnerViaPreForms.lean.

Definition

def FL : Formula → List Formula

The Fischer-Ladner closure of a formula. See Section 6.1 of [HKT00]. Note that there only implication is given. For our Formula type we also need to cover conjunction and negation. Also note that we are closing under single negations as well here. The main work is done by FLb, which also ensures termination.

Equations

• FL Formula.bottom = [⊥, ~⊥]
• FL (·p) = [·p, ~·p]
• FL (φ ⋀ ψ) = [φ ⋀ ψ, ~(φ ⋀ ψ), ~φ, ~ψ] ++ FL φ ++ FL ψ
• FL (⌈α⌉φ) = [~⌈α⌉φ, ~φ] ++ FLb α φ ++ FL φ
• FL (~φ) = [~φ] ++ FL φ

def FLb : Program → Formula → List Formula

The Fischer-Ladner closure of a box formula, not recursing into the formula after the box.

Equations

• FLb (·a) x✝ = [⌈·a⌉x✝, ~⌈·a⌉x✝]
• FLb (α⋓β) x✝ = [⌈α⋓β⌉x✝, ~⌈α⋓β⌉x✝] ++ FLb α x✝ ++ FLb β x✝
• FLb (α;'β) x✝ = [⌈α;'β⌉x✝, ~⌈α;'β⌉x✝] ++ FLb α (⌈β⌉x✝) ++ FLb β x✝
• FLb (∗α) x✝ = [⌈∗α⌉x✝, ~⌈∗α⌉x✝] ++ FLb α (⌈∗α⌉x✝)
• FLb (?'τ) x✝ = [⌈?'τ⌉x✝, ~⌈?'τ⌉x✝, ~τ] ++ FL τ

Lemmas

def isNeg : Formula → Prop

Equations

• isNeg (~a) = True
• isNeg x✝ = False

theorem FL_single_neg_closed {φ : Formula} : ¬isNeg φ → ~φ ∈ FL φ

@[simp]

theorem FL_refl {φ : Formula} : φ ∈ FL φ

@[simp]

theorem FLb_refl {α : Program} {φ : Formula} : (⌈α⌉φ) ∈ FLb α φ

@[simp]

theorem neg_mem_FLb {α : Program} {ψ : Formula} : (~⌈α⌉ψ) ∈ FLb α ψ

theorem FL_trans {φ ψ : Formula} : ψ ∈ FL φ → FL ψ ⊆ FL φ

Lemma 6.1(i) from [HKT00]

theorem FLb_trans {α : Program} {φ ψ : Formula} : ψ ∈ FLb α φ → FL ψ ⊆ FLb α φ ++ FL (~φ)

Lemma 6.1(ii) from [HKT00]

theorem FL_box_sub {φ : Formula} {α : Program} {ψ : Formula} : (⌈α⌉ψ) ∈ FL φ → ψ ∈ FL φ

theorem FL_boxes_sub {φ : Formula} {δ : List Program} {ψ : Formula} : (⌈⌈δ⌉⌉ψ) ∈ FL φ → ψ ∈ FL φ

theorem FL_box_test {φ τ ψ : Formula} : (⌈?'τ⌉ψ) ∈ FL φ → τ ∈ FL φ

theorem FL_box_cup {φ : Formula} {α β : Program} {ψ : Formula} : (⌈α⋓β⌉ψ) ∈ FL φ → (⌈α⌉ψ) ∈ FL φ ∧ (⌈β⌉ψ) ∈ FL φ

theorem FL_box_seq {φ : Formula} {α β : Program} {ψ : Formula} : (⌈α;'β⌉ψ) ∈ FL φ → (⌈α⌉⌈β⌉ψ) ∈ FL φ ∧ (⌈β⌉ψ) ∈ FL φ

theorem FL_box_star {φ : Formula} {α : Program} {ψ : Formula} : (⌈∗α⌉ψ) ∈ FL φ → (⌈α⌉⌈∗α⌉ψ) ∈ FL φ

Closure of a list

def FLL (L : List Formula) : List Formula

Equations

• FLL L = List.flatMap FL L

@[simp]

theorem FLL_refl_sub {L : List Formula} : L ⊆ FLL L

theorem FLL_sub {L1 L2 : List Formula} : L1 ⊆ L2 → FLL L1 ⊆ FLL L2

@[simp]

theorem FLL_nil : FLL [] = []

@[simp]

theorem FLL_singelton {φ : Formula} : FLL [φ] = FL φ

@[simp]

theorem FLL_idem_ext {L : List Formula} {φ : Formula} : φ ∈ FLL (FLL L) ↔ φ ∈ FLL L

theorem FLL_sub_FLL_iff_sub_FLL {L K : List Formula} : L ⊆ FLL K ↔ FLL L ⊆ FLL K

theorem FLL_append_eq {L K : List Formula} : FLL (L ++ K) = FLL L ++ FLL K

theorem FLL_diff_sub {L K : List Formula} : FLL (L \ K) ⊆ FLL L

theorem FLL_ext {L1 L2 : List Formula} (h : ∀ (φ : Formula), φ ∈ L1 ↔ φ ∈ L2) (φ : Formula) : φ ∈ FLL L1 ↔ φ ∈ FLL L2

Being a member of the FL closure of a list does not depend on the position.

FL stays in the Vocabulary

theorem FL_stays_in_voc {φ ψ : Formula} (ψ_in_FL : ψ ∈ FL φ) : ψ.voc ⊆ φ.voc

theorem FLb_stays_in_voc {α : Program} {φ ψ : Formula} (ψ_in_FLb : ψ ∈ FLb α φ) : ψ.voc ⊆ α.voc ∪ φ.voc