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.

@[irreducible]

def PreGroundTerm.rename_constants_apart {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [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

• PreGroundTerm.rename_constants_apart (FiniteTree.leaf a) forbidden_constants = FiniteTree.leaf (GetFreshInhabitant.fresh forbidden_constants).val
• PreGroundTerm.rename_constants_apart (FiniteTree.inner func ts) forbidden_constants = FiniteTree.inner func (PreGroundTerm.rename_constants_apart.foldl_list ts forbidden_constants)

@[irreducible]

def PreGroundTerm.rename_constants_apart.foldl_list {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] (ts : List (PreGroundTerm sig)) (forbidden_constants : List sig.C) : List (PreGroundTerm sig)

Equations

• PreGroundTerm.rename_constants_apart.foldl_list ts forbidden_constants = PreGroundTerm.rename_constants_apart.foldl_list_with_init ts forbidden_constants []

@[irreducible]

def PreGroundTerm.rename_constants_apart.foldl_list_with_init {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [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.

theorem PreGroundTerm.rename_constants_apart.length_foldl_list_with_init {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [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

theorem PreGroundTerm.rename_constants_apart.foldl_list_with_init_eq {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [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 FiniteTree.leaves init) []

theorem PreGroundTerm.rename_constants_apart.length_foldl_list {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] {ts : List (PreGroundTerm sig)} {forbidden_constants : List sig.C} : (foldl_list ts forbidden_constants).length = ts.length

theorem PreGroundTerm.rename_constants_apart.foldl_list_cons {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [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 ++ FiniteTree.leaves (t.rename_constants_apart forbidden_constants))

theorem PreGroundTerm.rename_constants_apart.mem_foldl_list_implies {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [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)

theorem PreGroundTerm.rename_constants_apart_leaves_fresh {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] {term : FiniteTree (SkolemFS sig) sig.C} {forbidden_constants : List sig.C} {e : sig.C} : e ∈ FiniteTree.leaves (rename_constants_apart term forbidden_constants) → ¬e ∈ forbidden_constants

Indeed the fresh constants are fresh.

theorem PreGroundTerm.rename_constants_apart_preserves_ruleId_validity {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [GetFreshInhabitant sig.C] {term : FiniteTree (SkolemFS sig) sig.C} {forbidden_constants : List sig.C} {rl : RuleList sig} : skolem_ruleIds_valid rl term → skolem_ruleIds_valid rl (rename_constants_apart term forbidden_constants)

theorem PreGroundTerm.rename_constants_apart_preserves_disjIdx_validity {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [GetFreshInhabitant sig.C] {term : FiniteTree (SkolemFS sig) sig.C} {forbidden_constants : List sig.C} {rl : RuleList sig} (h : skolem_ruleIds_valid rl term) : skolem_disjIdx_valid rl term h → skolem_disjIdx_valid rl (rename_constants_apart term forbidden_constants) ⋯

theorem PreGroundTerm.rename_constants_apart_preserves_rule_arity_validity {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [GetFreshInhabitant sig.C] {term : FiniteTree (SkolemFS sig) sig.C} {forbidden_constants : List sig.C} {rl : RuleList sig} (h : skolem_ruleIds_valid rl term) : skolem_rule_arity_valid rl term h → skolem_rule_arity_valid rl (rename_constants_apart term forbidden_constants) ⋯