Documentation

LeanPool.MatchingLogic.EntryIII.SignatureRestriction

MatchingLogic.EntryIII.SignatureRestriction #

source
def MatchingLogic.Signature.restrict {S : Signature} (F : Finset S.Sym) :
Signature

The sub-signature containing exactly the symbols in F.

Equations
Instances For
    source
    def MatchingLogic.Pattern.liftSignature {S : Signature} {Var : Type} [DecidableEq S.Sym] (F : Finset S.Sym) :
    Pattern (Signature.restrict F) Var → Pattern S Var

    Regard a pattern over a finite sub-signature as a pattern over S.

    Equations
    Instances For
      source
      def MatchingLogic.Pattern.restrictSignature {S : Signature} {Var : Type} [DecidableEq S.Sym] (F : Finset S.Sym) (p : Pattern S Var) :
      p.symbolSupport ⊆ F → Pattern (Signature.restrict F) Var

      Restrict a pattern whose symbol support lies in F to the sub-signature.

      Equations
      Instances For
        source
        theorem MatchingLogic.Pattern.lift_restrictSignature {S : Signature} {Var : Type} [DecidableEq S.Sym] (F : Finset S.Sym) (p : Pattern S Var) (h : p.symbolSupport ⊆ F) :
        liftSignature F (restrictSignature F p h) = p

        Lifting a restricted pattern recovers the original ambient pattern.

        source
        theorem MatchingLogic.Pattern.liftSignature_substVar {S : Signature} {Var : Type} [DecidableEq Var] [DecidableEq S.Sym] (F : Finset S.Sym) (x y : Var) (p : Pattern (Signature.restrict F) Var) :
        liftSignature F (substVar x y p) = substVar x y (liftSignature F p)

        Lifting commutes with the raw variable-for-variable substitution.

        source
        theorem MatchingLogic.Pattern.FV_liftSignature {S : Signature} {Var : Type} [DecidableEq S.Sym] (F : Finset S.Sym) (p : Pattern (Signature.restrict F) Var) :
        FV (liftSignature F p) = FV p

        Free variables are unchanged by signature lifting.

        source
        theorem MatchingLogic.Pattern.captureFree_liftSignature {S : Signature} {Var : Type} [DecidableEq S.Sym] (F : Finset S.Sym) {x y : Var} {p : Pattern (Signature.restrict F) Var} :
        CaptureFree x y p → CaptureFree x y (liftSignature F p)

        Capture-freedom is preserved when a pattern is lifted to a larger signature.

        source
        theorem MatchingLogic.Pattern.liftSignature_update {S : Signature} {Var : Type} [DecidableEq S.Sym] (F : Finset S.Sym) {n : ℕ} (args : Fin n → Pattern (Signature.restrict F) Var) (i : Fin n) (p : Pattern (Signature.restrict F) Var) :
        (fun (j : Fin n) => liftSignature F (Function.update args i p j)) = Function.update (fun (j : Fin n) => liftSignature F (args j)) i (liftSignature F p)

        Lifting commutes with replacing an argument of an application.

        source
        theorem MatchingLogic.Pattern.liftSignature_app_update {S : Signature} {Var : Type} [DecidableEq S.Sym] (F : Finset S.Sym) (sigma : (Signature.restrict F).Sym) (args : Fin ((Signature.restrict F).arity sigma) → Pattern (Signature.restrict F) Var) (i : Fin ((Signature.restrict F).arity sigma)) (p : Pattern (Signature.restrict F) Var) :
        liftSignature F (app sigma (Function.update args i p)) = app (↑sigma) (Function.update (fun (j : Fin (S.arity ↑sigma)) => liftSignature F (args j)) i (liftSignature F p))

        The lifted form of an application with one replaced argument.

        source
        theorem MatchingLogic.PForm.subst_liftSignature {S : Signature} {Var : Type} [DecidableEq S.Sym] (F : Finset S.Sym) (p : PForm) (theta : ℕ → Pattern (Signature.restrict F) Var) :
        Pattern.liftSignature F (subst theta p) = subst (fun (n : ℕ) => Pattern.liftSignature F (theta n)) p

        Lifting commutes with propositional-pattern substitution.

        source
        def MatchingLogic.AppCtx.liftSignature {S : Signature} {Var : Type} [DecidableEq S.Sym] (F : Finset S.Sym) :
        AppCtx (Signature.restrict F) Var → AppCtx S Var

        Regard an application context over a finite sub-signature as one over S.

        Equations
        Instances For
          source
          theorem MatchingLogic.AppCtx.plug_liftSignature {S : Signature} {Var : Type} [DecidableEq S.Sym] (F : Finset S.Sym) (C : AppCtx (Signature.restrict F) Var) (p : Pattern (Signature.restrict F) Var) :
          Pattern.liftSignature F (C.plug p) = (liftSignature F C).plug (Pattern.liftSignature F p)
          source
          noncomputable def MatchingLogic.Pattern.signatureNatCode {T : Signature} [Encodable T.Sym] :
          Pattern T ℕ → ℕ

          A natural-number serialization retaining every application argument.

          Equations
          Instances For
            source
            theorem MatchingLogic.Pattern.signatureNatCode_injective {T : Signature} [Encodable T.Sym] :
            Function.Injective signatureNatCode

            The natural serialization is injective whenever the symbol type is encodable.

            source
            theorem MatchingLogic.restrictedPatternNatCountable {S : Signature} (F : Finset S.Sym) :
            Countable (Pattern (Signature.restrict F) ℕ)

            A finite signature yields a countable type of natural-variable patterns.

            source
            theorem MatchingLogic.Provable.liftSignature {S : Signature} {Var : Type} [DecidableEq Var] [DecidableEq S.Sym] (F : Finset S.Sym) {Gamma : Set (Pattern (Signature.restrict F) Var)} {phi : Pattern (Signature.restrict F) Var} (h : Provable Gamma phi) :
            Provable (Pattern.liftSignature F '' Gamma) (Pattern.liftSignature F phi)

            A derivation over a finite sub-signature can be replayed over S.