Documentation

Pdl.Tableau

PDL-Tableaux (Section 4) #

Projections #

Equations
Instances For
    Equations
    Instances For
      @[simp]
      theorem proj {A : } {X : List Formula} {g : Formula} :

      Loading and Loaded Histories #

      Equations
      Instances For
        @[reducible, inline]
        abbrev History :

        A history is a list of Sequents. This only tracks "big" steps, hoping we do not need steps within a local tableau. The head of the first list is the newest Sequent.

        Equations
        Instances For
          def rep (Hist : History) (X : Sequent) :

          We have a repeat iff the history contains a node that is setEqTo the current node.

          Equations
          Instances For
            instance instDecidableRep {H : History} {X : Sequent} :
            Equations
            def LoadedPathRepeat (Hist : History) (X : Sequent) :

            A lpr means we can go k steps back in the history to reach an equal node, and all nodes on the way are loaded. Note: k=0 means the first element of Hist is the companion.

            Equations
            Instances For
              theorem LoadedPathRepeat.to_rep {Hist : History} {X : Sequent} (lpr : LoadedPathRepeat Hist X) :
              rep Hist X

              If there is any loaded path repeat, then we can compute one. FIXME There is probably a more elegant way, avoiding Nonempty and Fin.find. Something like: def getLPR (H : History) (X : Sequent) : Option ... := ... that might also give us uniqueness of LPRs?

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem LoadedPathRepeat_comp_isLoaded {Hist : History} {X : Sequent} (lpr : LoadedPathRepeat Hist X) :
                (List.get Hist lpr).isLoaded = true

                The PDL rules #

                inductive PdlRule (X Y : Sequent) :

                A rule to go from X to Y. Note the four variants of the modal rule.

                Instances For
                  def instDecidableEqPdlRule.decEq {X✝ Y✝ : Sequent} (x✝ x✝¹ : PdlRule X✝ Y✝) :
                  Decidable (x✝ = x✝¹)
                  Instances For
                    inductive Tableau :

                    The Tableau [parent, grandparent, ...] child type.

                    A closed tableau for X is either of:

                    • a local tableau for X followed by closed tableaux for all end nodes,
                    • a PDL rule application
                    • a successful loaded repeat (MB condition six)
                    Instances For
                      def Tableau.size {Hist : History} {X : Sequent} :
                      Tableau Hist X
                      Equations
                      Instances For
                        theorem Tableau.size_next_lt_of_loc {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {nrep : ¬rep a✝ a✝¹} {nbas : ¬a✝¹.basic} {lt : LocalTableau a✝¹} {next : (Y : Sequent) → Y endNodesOf ltTableau (a✝¹ :: a✝) Y} (tab_def : tab = loc nrep nbas lt next) (Y : Sequent) (Y_in : Y endNodesOf lt) :
                        (next Y Y_in).size < tab.size
                        theorem Tableau.size_next_lt_of_pdl {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {nrep : ¬rep a✝ a✝¹} {bas : a✝¹.basic} {Y✝ : Sequent} {r : PdlRule a✝¹ Y✝} {next : Tableau (a✝¹ :: a✝) Y✝} (tab_def : tab = pdl nrep bas r next) :
                        next.size < tab.size
                        instance instDecidableExistsEndNodeOf {X : Sequent} {lt : LocalTableau X} {f : (Y : Sequent) → Y endNodesOf ltProp} {dec : (Y : Sequent) → (Y_in : Y endNodesOf lt) → Decidable (f Y Y_in)} :
                        Decidable (∃ (Y : Sequent) (Y_in : Y endNodesOf lt), f Y Y_in)
                        Equations
                        • One or more equations did not get rendered due to their size.
                        @[irreducible]
                        instance Tableau.instDecidableEq {Hist : History} {X : Sequent} {tab1 tab2 : Tableau Hist X} :
                        Decidable (tab1 = tab2)
                        Equations
                        • One or more equations did not get rendered due to their size.
                        def Tableau.isLrep {Hist : History} {X : Sequent} :
                        Tableau Hist XProp
                        Equations
                        Instances For
                          inductive provable :
                          Instances For

                            A Sequent is inconsistent if there exists a closed tableau for it.

                            Equations
                            Instances For

                              A Sequent is consistent iff it is not inconsistent.

                              Equations
                              Instances For