Documentation

ExistentialRules.ChaseSequence.Termination.RenameConstantsApart.PreGroundTerm

Renaming Constants apart in a PreGroundTerm #

For MFA we need to be able to rename constants apart in terms. For example, for $f(g(c,c),d)$, we want to consider $f(g(c,e),d)$ instead. Actually, we are way more radical and just consider $f(g(c_1, c_2), c_3)$, so we blindly introduce a fresh constant for each leaf in the term. We show that the new constants are indeed fresh rename_constants_apart_leaves_fresh and we also prove that the renaming does not mess with term validity as required for backtrackings.

source
@[irreducible]
def PreGroundTerm.rename_constants_apart {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [CustomBasicDatastructures.GetFreshInhabitant sig.C] (term : PreGroundTerm sig) (forbidden_constants : List sig.C) :
PreGroundTerm sig

We rename constants apart by introducing a fresh constant for each leaf position in the term.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[irreducible]
    def PreGroundTerm.rename_constants_apart.foldl_list {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [CustomBasicDatastructures.GetFreshInhabitant sig.C] (ts : List (PreGroundTerm sig)) (forbidden_constants : List sig.C) :
    List (PreGroundTerm sig)
    Equations
    Instances For
      source
      @[irreducible]
      def PreGroundTerm.rename_constants_apart.foldl_list_with_init {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [CustomBasicDatastructures.GetFreshInhabitant sig.C] (ts : List (PreGroundTerm sig)) (forbidden_constants : List sig.C) (init : List (PreGroundTerm sig)) :
      List (PreGroundTerm sig)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem PreGroundTerm.rename_constants_apart.length_foldl_list_with_init {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [CustomBasicDatastructures.GetFreshInhabitant sig.C] {ts : List (PreGroundTerm sig)} {forbidden_constants : List sig.C} {init : List (PreGroundTerm sig)} :
        (foldl_list_with_init ts forbidden_constants init).length = init.length + ts.length
        source
        theorem PreGroundTerm.rename_constants_apart.foldl_list_with_init_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [CustomBasicDatastructures.GetFreshInhabitant sig.C] {ts : List (PreGroundTerm sig)} {forbidden_constants : List sig.C} {init : List (PreGroundTerm sig)} :
        foldl_list_with_init ts forbidden_constants init = init ++ foldl_list_with_init ts (forbidden_constants ++ List.flatMap CustomBasicDatastructures.FiniteTree.leaves init) []
        source
        theorem PreGroundTerm.rename_constants_apart.length_foldl_list {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [CustomBasicDatastructures.GetFreshInhabitant sig.C] {ts : List (PreGroundTerm sig)} {forbidden_constants : List sig.C} :
        (foldl_list ts forbidden_constants).length = ts.length
        source
        theorem PreGroundTerm.rename_constants_apart.foldl_list_cons {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [CustomBasicDatastructures.GetFreshInhabitant sig.C] {t : PreGroundTerm sig} {ts : List (PreGroundTerm sig)} {forbidden_constants : List sig.C} :
        foldl_list (t :: ts) forbidden_constants = t.rename_constants_apart forbidden_constants :: foldl_list ts (forbidden_constants ++ CustomBasicDatastructures.FiniteTree.leaves (t.rename_constants_apart forbidden_constants))
        source
        theorem PreGroundTerm.rename_constants_apart.mem_foldl_list_implies {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [CustomBasicDatastructures.GetFreshInhabitant sig.C] {ts : List (PreGroundTerm sig)} {forbidden_constants : List sig.C} {t : PreGroundTerm sig} :
        t ∈ foldl_list ts forbidden_constants → ∃ (t' : PreGroundTerm sig), ∃ (new_consts : List sig.C), t' ∈ ts ∧ t = t'.rename_constants_apart (forbidden_constants ++ new_consts)
        source
        theorem PreGroundTerm.rename_constants_apart_leaves_fresh {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [CustomBasicDatastructures.GetFreshInhabitant sig.C] {term : CustomBasicDatastructures.FiniteTree (SkolemFS sig) sig.C} {forbidden_constants : List sig.C} {e : sig.C} :
        e ∈ CustomBasicDatastructures.FiniteTree.leaves (rename_constants_apart term forbidden_constants) → ¬e ∈ forbidden_constants

        Indeed the fresh constants are fresh.