Interaction of Strict Constant Mappings and Renaming Constant Apart

For PreGroundTerm, GroundTerm, GroundSubstitution, and PreTrigger, we do the following things:

1. We define what it means for them to have the same_skeleton, which is the case if their only difference is the naming of constants in terms (but their structure is the same),
2. we show that applying a StrictConstantMapping yields something that has the same skeleton,
3. we show that for two things with the same skeleton, we can find a StrictConstantMapping that maps the renamed apart version of the first thing to the second one while mapping each constant to itself that does not occur in the renamed apart version.

def PreGroundTerm.same_skeleton {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (term term2 : PreGroundTerm sig) : Prop

Equations

• PreGroundTerm.same_skeleton (FiniteTree.leaf a) (FiniteTree.leaf a_1) = True
• PreGroundTerm.same_skeleton (FiniteTree.leaf a) (FiniteTree.inner a_1 a_2) = False
• PreGroundTerm.same_skeleton (FiniteTree.inner a a_1) (FiniteTree.leaf a_2) = False
• PreGroundTerm.same_skeleton (FiniteTree.inner a a_1) (FiniteTree.inner a_2 a_3) = (a = a_2 ∧ PreGroundTerm.same_skeleton_list a_1 a_3)

def PreGroundTerm.same_skeleton_list {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (terms terms2 : List (PreGroundTerm sig)) : Prop

Equations

• PreGroundTerm.same_skeleton_list [] [] = True
• PreGroundTerm.same_skeleton_list [] (head :: tail) = False
• PreGroundTerm.same_skeleton_list (head :: tail) [] = False
• PreGroundTerm.same_skeleton_list (head :: tail) (head_1 :: tail_1) = (head.same_skeleton head_1 ∧ PreGroundTerm.same_skeleton_list tail tail_1)

theorem PreGroundTerm.same_skeleton_refl {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (term : PreGroundTerm sig) : term.same_skeleton term

theorem PreGroundTerm.same_skeleton_list_refl {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (terms : List (PreGroundTerm sig)) : same_skeleton_list terms terms

theorem PreGroundTerm.same_skeleton_symm {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (term term2 : PreGroundTerm sig) : term.same_skeleton term2 → term2.same_skeleton term

theorem PreGroundTerm.same_skeleton_list_symm {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (terms terms2 : List (PreGroundTerm sig)) : same_skeleton_list terms terms2 → same_skeleton_list terms2 terms

@[irreducible]

theorem PreGroundTerm.same_skeleton_under_strict_constant_mapping {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (term : PreGroundTerm sig) (g : StrictConstantMapping sig) : term.same_skeleton (g.toConstantMapping.apply_pre_ground_term term)

@[irreducible]

theorem PreGroundTerm.same_skeleton_list_under_strict_constant_mapping {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (terms : List (PreGroundTerm sig)) (g : StrictConstantMapping sig) : same_skeleton_list terms (List.map g.toConstantMapping.apply_pre_ground_term terms)

theorem PreGroundTerm.exists_strict_constant_mapping_to_reverse_renaming {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [GetFreshInhabitant sig.C] (term term2 : PreGroundTerm sig) (terms_same_skeleton : term.same_skeleton term2) (forbidden_constants : List sig.C) : ∃ (g : StrictConstantMapping sig), g.toConstantMapping.apply_pre_ground_term (term.rename_constants_apart forbidden_constants) = term2 ∧ ∀ (d : sig.C), ¬d ∈ FiniteTree.leaves (term.rename_constants_apart forbidden_constants) → g d = d

theorem PreGroundTerm.exists_strict_constant_mapping_to_reverse_renaming_list {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [GetFreshInhabitant sig.C] (terms terms2 : List (PreGroundTerm sig)) (terms_same_skeleton : same_skeleton_list terms terms2) (forbidden_constants : List sig.C) : ∃ (g : StrictConstantMapping sig), List.map (fun (term : PreGroundTerm sig) => g.toConstantMapping.apply_pre_ground_term term) (rename_constants_apart.foldl_list terms forbidden_constants) = terms2 ∧ ∀ (d : sig.C), ¬d ∈ List.flatMap FiniteTree.leaves (rename_constants_apart.foldl_list terms forbidden_constants) → g d = d

def GroundTerm.same_skeleton {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (term term2 : GroundTerm sig) : Prop

Equations

• term.same_skeleton term2 = term.val.same_skeleton term2.val

theorem GroundTerm.same_skeleton_refl {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (term : GroundTerm sig) : term.same_skeleton term

theorem GroundTerm.same_skeleton_symm {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (term term2 : GroundTerm sig) : term.same_skeleton term2 → term2.same_skeleton term

theorem GroundTerm.same_skeleton_under_strict_constant_mapping {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (term : GroundTerm sig) (g : StrictConstantMapping sig) : term.same_skeleton (g.toConstantMapping.apply_ground_term term)

theorem GroundTerm.exists_strict_constant_mapping_to_reverse_renaming {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [GetFreshInhabitant sig.C] (term term2 : GroundTerm sig) (terms_same_skeleton : term.same_skeleton term2) (forbidden_constants : List sig.C) : ∃ (g : StrictConstantMapping sig), g.toConstantMapping.apply_ground_term (term.rename_constants_apart forbidden_constants) = term2 ∧ ∀ (d : sig.C), ¬d ∈ (term.rename_constants_apart forbidden_constants).constants → g d = d

def GroundSubstitution.same_skeleton_for_vars {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (subs subs2 : GroundSubstitution sig) : List sig.V → Prop

Equations

• subs.same_skeleton_for_vars subs2 [] = True
• subs.same_skeleton_for_vars subs2 (hd :: tl) = ((subs hd).same_skeleton (subs2 hd) ∧ subs.same_skeleton_for_vars subs2 tl)

theorem GroundSubstitution.same_skeleton_for_vars_refl {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (subs : GroundSubstitution sig) (vars : List sig.V) : subs.same_skeleton_for_vars subs vars

theorem GroundSubstitution.same_skeleton_for_vars_symm {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (subs subs2 : GroundSubstitution sig) (vars : List sig.V) : subs.same_skeleton_for_vars subs2 vars → subs2.same_skeleton_for_vars subs vars

theorem GroundSubstitution.same_skeleton_for_vars_under_strict_constant_mapping {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (subs : GroundSubstitution sig) (vars : List sig.V) (g : StrictConstantMapping sig) : subs.same_skeleton_for_vars (g.toConstantMapping.apply_ground_term ∘ subs) vars

theorem GroundSubstitution.exists_strict_constant_mapping_to_reverse_renaming_for_vars {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [GetFreshInhabitant sig.C] (subs subs2 : GroundSubstitution sig) (vars : List sig.V) (vars_nodup : vars.Nodup) (subs_same_skeleton : subs.same_skeleton_for_vars subs2 vars) (forbidden_constants : List sig.C) : ∃ (g : StrictConstantMapping sig), (∀ (v : sig.V), v ∈ vars → g.toConstantMapping.apply_ground_term (subs.rename_constants_apart_for_vars forbidden_constants vars v) = subs2 v) ∧ ∀ (d : sig.C), ¬d ∈ List.flatMap GroundTerm.constants (List.map (subs.rename_constants_apart_for_vars forbidden_constants vars) vars) → g d = d

def PreTrigger.same_skeleton {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg trg2 : PreTrigger sig) : Prop

Equations

• trg.same_skeleton trg2 = (trg.rule = trg2.rule ∧ trg.subs.same_skeleton_for_vars trg2.subs trg.rule.body.vars.eraseDupsKeepRight)

theorem PreTrigger.same_skeleton_refl {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) : trg.same_skeleton trg

theorem PreTrigger.same_skeleton_symm {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg trg2 : PreTrigger sig) : trg.same_skeleton trg2 → trg2.same_skeleton trg

theorem PreTrigger.same_skeleton_under_strict_constant_mapping {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (g : StrictConstantMapping sig) : trg.same_skeleton { rule := trg.rule, subs := g.toConstantMapping.apply_ground_term ∘ trg.subs }

theorem PreTrigger.exists_strict_constant_mapping_to_reverse_renaming {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] (trg trg2 : PreTrigger sig) (trgs_same_skeleton : trg.same_skeleton trg2) (forbidden_constants : List sig.C) : ∃ (g : StrictConstantMapping sig), { rule := trg.rule, subs := g.toConstantMapping.apply_ground_term ∘ (trg.rename_constants_apart forbidden_constants).subs }.strong_equiv trg2 ∧ ∀ (d : sig.C), ¬d ∈ List.flatMap GroundTerm.constants (List.map (trg.rename_constants_apart forbidden_constants).subs trg.rule.body.vars.eraseDupsKeepRight) → g d = d