Documentation

LeanPool.PDL.FischerLadner

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 [HKT2000] which also was used in a Rocq formalization in [DB2018]. 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 [BRV2001]. An alternative version following the proof of Theorem 3.2 in [FL1979] but unfinished is in Unused/FischerLadnerViaPreForms.lean.

Definition #

source
def PDL.FL :
Formula → List Formula

The Fischer-Ladner closure of a formula. See Section 6.1 of [HKT2000]. 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
Instances For
    source
    def PDL.FLb :
    Program → Formula → List Formula

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

    Equations
    Instances For

      Lemmas #

      source
      def PDL.isNeg :
      Formula → Prop

      Whether a formula has an outer negation constructor.

      Equations
      Instances For
        source
        theorem PDL.FL_single_neg_closed {φ : Formula} :
        ¬isNeg φ → φ.neg ∈ FL φ
        source
        @[simp]
        theorem PDL.FL_refl {φ : Formula} :
        φ ∈ FL φ
        source
        @[simp]
        theorem PDL.FLb_refl {α : Program} {φ : Formula} :
        Formula.box α φ ∈ FLb α φ
        source
        @[simp]
        theorem PDL.neg_mem_FLb {α : Program} {ψ : Formula} :
        (Formula.box α ψ).neg ∈ FLb α ψ
        source
        theorem PDL.FL_trans {φ ψ : Formula} :
        ψ ∈ FL φ → FL ψ ⊆ FL φ

        Lemma 6.1(i) from [HKT2000]

        source
        theorem PDL.FLb_trans {α : Program} {φ ψ : Formula} :
        ψ ∈ FLb α φ → FL ψ ⊆ FLb α φ ++ FL φ.neg

        Lemma 6.1(ii) from [HKT2000]

        source
        theorem PDL.FL_box_sub {φ : Formula} {α : Program} {ψ : Formula} :
        Formula.box α ψ ∈ FL φ → ψ ∈ FL φ
        source
        theorem PDL.FL_boxes_sub {φ : Formula} {δ : List Program} {ψ : Formula} :
        Formula.boxes δ ψ ∈ FL φ → ψ ∈ FL φ
        source
        theorem PDL.FL_box_test {φ τ ψ : Formula} :
        Formula.box (Program.test τ) ψ ∈ FL φ → τ ∈ FL φ
        source
        theorem PDL.FL_box_cup {φ : Formula} {α β : Program} {ψ : Formula} :
        Formula.box (α.union β) ψ ∈ FL φ → Formula.box α ψ ∈ FL φ ∧ Formula.box β ψ ∈ FL φ
        source
        theorem PDL.FL_box_seq {φ : Formula} {α β : Program} {ψ : Formula} :
        Formula.box (α.sequence β) ψ ∈ FL φ → Formula.box α (Formula.box β ψ) ∈ FL φ ∧ Formula.box β ψ ∈ FL φ
        source
        theorem PDL.FL_box_star {φ : Formula} {α : Program} {ψ : Formula} :
        Formula.box α.star ψ ∈ FL φ → Formula.box α (Formula.box α.star ψ) ∈ FL φ

        Closure of a list #

        source
        def PDL.FLL (L : List Formula) :
        List Formula

        Concatenate the Fischer-Ladner closures of every formula in a list.

        Equations
        Instances For
          source
          @[simp]
          theorem PDL.FLL_refl_sub {L : List Formula} :
          L ⊆ FLL L
          source
          theorem PDL.FLL_sub {L1 L2 : List Formula} :
          L1 ⊆ L2 → FLL L1 ⊆ FLL L2
          source
          @[simp]
          theorem PDL.FLL_nil :
          FLL [] = []
          source
          @[simp]
          theorem PDL.FLL_singelton {φ : Formula} :
          FLL [φ] = FL φ
          source
          @[simp]
          theorem PDL.FLL_idem_ext {L : List Formula} {φ : Formula} :
          φ ∈ FLL (FLL L) ↔ φ ∈ FLL L
          source
          theorem PDL.FLL_sub_FLL_iff_sub_FLL {L K : List Formula} :
          L ⊆ FLL K ↔ FLL L ⊆ FLL K
          source
          theorem PDL.FLL_append_eq {L K : List Formula} :
          FLL (L ++ K) = FLL L ++ FLL K
          source
          theorem PDL.FLL_diff_sub {L K : List Formula} :
          FLL (L \ K) ⊆ FLL L
          source
          theorem PDL.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 Closure of a Finset of Formulas #

          source
          def Finset.FL (X : Finset PDL.Formula) :
          Finset PDL.Formula

          The union of the Fischer-Ladner closures of every formula in a finset.

          Equations
          Instances For
            source
            @[simp]
            theorem Finset.FL_refl_sub {X : Finset PDL.Formula} :
            X ⊆ X.FL
            source
            theorem Finset.FL_sub {X Y : Finset PDL.Formula} :
            X ⊆ Y → X.FL ⊆ Y.FL
            source
            @[simp]
            theorem Finset.FL_nil :
            ∅.FL = ∅
            source
            @[simp]
            theorem Finset.FL_singelton {φ : PDL.Formula} :
            {φ}.FL = (PDL.FL φ).toFinset
            source
            @[simp]
            theorem Finset.FL_idem_ext {X : Finset PDL.Formula} {φ : PDL.Formula} :
            φ ∈ X.FL.FL ↔ φ ∈ X.FL
            source
            theorem Finset.FL_sub_FL_iff_sub_FL {X Y : Finset PDL.Formula} :
            X ⊆ Y.FL ↔ X.FL ⊆ Y.FL
            source
            theorem Finset.FL_union_eq {X Y : Finset PDL.Formula} :
            (X ∪ Y).FL = X.FL ∪ Y.FL
            source
            theorem Finset.FL_diff_sub {X Y : Finset PDL.Formula} :
            (X \ Y).FL ⊆ X.FL

            FL stays in the Vocabulary #

            source
            theorem PDL.FL_stays_in_voc {φ ψ : Formula} (ψ_in_FL : ψ ∈ FL φ) :
            ψ.voc ⊆ φ.voc
            source
            theorem PDL.FLb_stays_in_voc {α : Program} {φ ψ : Formula} (ψ_in_FLb : ψ ∈ FLb α φ) :
            ψ.voc ⊆ α.voc ∪ φ.voc