Documentation

LeanPool.MatchingLogic.ProofSystem

MatchingLogic.ProofSystem #

Rule (1): substitution instances of propositional tautologies #

source
inductive MatchingLogic.PForm :
Type

Propositional formulas over → and ⊥.

Instances For
    source
    @[instance_reducible]
    instance MatchingLogic.instDecidableEqPForm :
    DecidableEq PForm
    Equations
    source
    def MatchingLogic.instDecidableEqPForm.decEq (x✝ x✝¹ : PForm) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      def MatchingLogic.PForm.eval (v : ℕ → Bool) :
      PForm → Bool

      Boolean evaluation under an assignment to the atoms.

      Equations
      Instances For
        source
        def MatchingLogic.PForm.Taut (p : PForm) :
        Prop

        A propositional tautology.

        Equations
        Instances For
          source
          def MatchingLogic.PForm.subst {S : Signature} {Var : Type} (θ : ℕ → Pattern S Var) :
          PForm → Pattern S Var

          Substituting patterns for the propositional atoms.

          Equations
          Instances For

            Rule (3): variable-for-variable substitution, capture-avoiding #

            source
            def MatchingLogic.substVar {S : Signature} {Var : Type} [DecidableEq Var] (x y : Var) :
            Pattern S Var → Pattern S Var

            φ[y/x], replacing the element variable x by y. Naive: it stops at a binder for x, but does not itself avoid capture of y.

            Equations
            Instances For
              source
              def MatchingLogic.CaptureFree {S : Signature} {Var : Type} (x y : Var) :
              Pattern S Var → Prop

              substVar x y φ is capture-avoiding: no binder on the way to a substituted occurrence of x binds y. This is the paper's side condition on rule (3).

              The binder clause has three alternatives, and all three are needed:

              • z = x — the substitution stops here, since x is rebound;
              • x ∉ FV a — substVar changes nothing under this binder, so it cannot introduce a y for z to capture, even when z = y;
              • z ≠ y and recursively — y may be introduced, but z does not bind it.

              The middle alternative was missing in the first version of this definition, and two independent audits caught it. Its absence made the predicate SOUND but strictly TOO STRONG: it rejected genuinely capture-safe substitutions, which would have made rule (3) weaker than Figure 2 and could have left Corollary 15 unprovable, with nothing failing to compile anywhere. See captureFree_needs_notFree below for a substitution the old version rejected.

              Equations
              Instances For
                source
                theorem MatchingLogic.captureFree_needs_notFree {S : Signature} :
                CaptureFree 0 1 (Pattern.ex 1 (Pattern.var 2)) ∧ substVar 0 1 (Pattern.ex 1 (Pattern.var 2)) = Pattern.ex 1 (Pattern.var 2)

                The x ∉ FV a alternative is not vacuous. Substituting y for x in ∃y. z, where x does not occur, is harmless — substVar leaves the pattern alone — yet the binder is y itself. Only the middle alternative admits it.

                Rule (10): application contexts #

                source
                inductive MatchingLogic.AppCtx (S : Signature) (Var : Type) :
                Type

                C ::= □ | σ(φ₁, …, C, …, φₙ).

                Instances For
                  source
                  def MatchingLogic.AppCtx.plug {S : Signature} {Var : Type} :
                  AppCtx S Var → Pattern S Var → Pattern S Var

                  C[φ].

                  Equations
                  Instances For

                    Figure 2 #

                    source
                    inductive MatchingLogic.Provable {S : Signature} {Var : Type} [DecidableEq Var] (Γ : Set (Pattern S Var)) :
                    Pattern S Var → Prop

                    Γ ⊢ φ. The ten schemes and rules of Figure 2, restricted to one sort.

                    Instances For

                      Small public Hilbert toolkit #

                      source
                      theorem MatchingLogic.Provable.weaken {S : Signature} {Var : Type} [DecidableEq Var] {Γ Δ : Set (Pattern S Var)} {φ : Pattern S Var} (hΓΔ : Γ ⊆ Δ) (h : Provable Γ φ) :
                      Provable Δ φ

                      Provability is monotone in its hypotheses.

                      source
                      theorem MatchingLogic.Provable.weaken_empty {S : Signature} {Var : Type} [DecidableEq Var] {Γ : Set (Pattern S Var)} {φ : Pattern S Var} (h : Provable ∅ φ) :
                      Provable Γ φ

                      A theorem is usable under arbitrary hypotheses.

                      source
                      theorem MatchingLogic.provable_top {S : Signature} {Var : Type} [DecidableEq Var] (Γ : Set (Pattern S Var)) :
                      Provable Γ Pattern.tp

                      ⊤ is derivable in every theory.

                      source
                      theorem MatchingLogic.Provable.and_intro {S : Signature} {Var : Type} [DecidableEq Var] {Γ : Set (Pattern S Var)} {φ ψ : Pattern S Var} (hφ : Provable Γ φ) (hψ : Provable Γ ψ) :
                      Provable Γ (φ.and ψ)

                      Derived conjunction introduction.

                      Lemma 5 #

                      source
                      def MatchingLogic.doubleNegIntro :
                      PForm

                      The propositional tautology introducing double negation.

                      Equations
                      Instances For
                        source
                        def MatchingLogic.implicationTransitivity :
                        PForm

                        The propositional tautology expressing transitivity of implication.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          theorem MatchingLogic.necessitation {S : Signature} {Var : Type} [DecidableEq Var] {Γ : Set (Pattern S Var)} {ψ : Pattern S Var} (h : Provable Γ ψ) (p : List (Coord S)) :
                          Provable Γ (boxes p ψ)

                          Lemma 5 (necessitation). If Γ ⊢ ψ then Γ ⊢ [p]ψ for every word p.

                          The paper's proof, for a single coordinate e: the tautology ψ → ((ψ → ⊥) → ⊥) with modus ponens gives Γ ⊢ ¬ψ → ⊥; framing in position i with ⊤ elsewhere gives Γ ⊢ ⟨e⟩¬ψ → σ(⊤,…,⊥,…,⊤); propagation of ⊥ gives ⊢ σ(⊤,…,⊥,…,⊤) → ⊥; composing is propositional. Then iterate along p.

                          The two black boxes #

                          source
                          def MatchingLogic.conj {S : Signature} {Var : Type} :
                          List (Pattern S Var) → Pattern S Var

                          Finite conjunction, ⋀ l.

                          Equations
                          Instances For
                            source
                            theorem MatchingLogic.provable_conj {S : Signature} {Var : Type} [DecidableEq Var] {Γ : Set (Pattern S Var)} (l : List (Pattern S Var)) (h : ∀ δ ∈ l, Provable Γ δ) :
                            Provable Γ (conj l)

                            Introduce the pinned finite conjunction of a list of derivable patterns.

                            source
                            def MatchingLogic.StrongLocalCompleteness (S : Signature) (Var : Type) [DecidableEq Var] :
                            Prop

                            (L) Strong local completeness. If Δ ⊨loc φ then ⊢ (⋀Δ₀) → φ for some finite Δ₀ ⊆ Δ. The paper uses this as a black box, citing Definition 3.3 and "Theorem 3.8" of its reference [4] -- but Theorem 3.8 there is the WEAK statement; strong local completeness is Theorem 3.7 (Theorem 83 of Chen and Rosu, Matching μ-Logic, 2019 technical report, https://hdl.handle.net/2142/102281). See FINDINGS.md.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              def MatchingLogic.Soundness (S : Signature) (Var : Type) [DecidableEq Var] :
                              Prop

                              (S) Soundness. Γ ⊢ φ implies Γ ⊨ φ. The paper uses this as a black box too, but unlike (L) it is within reach here: see soundness below.

                              Equations
                              Instances For