Interaction of Backtrackings and Strict Constant Mappings on PreGroundTerm

This file mainly shows two results for PreGroundTerm.

1. backtrackFacts_under_strict_constant_mapping_same_number_of_fresh_constants shows that applying a StrictConstantMapping to a PreGroundTerm does not change the total number of fresh constants introduced in the backtracking.
2. backtrackFacts_under_constant_mapping_subset_of_composing_with_subs shows that applying a StrictConstantMapping to the backtracking of a PreGroundTerm yields a subset of the backtracking for the term resulting from applying the constant mapping to the original term. However, fresh constants need to be remapped here potentially and other terms and conditions apply as well but this is at least the intuition.

If you have been looking for the most horrible theorem in this repo, then your search likely concludes here :D

theorem PreGroundTerm.backtrackFacts_under_strict_constant_mapping_same_number_of_fresh_constants {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [GetFreshInhabitant sig.C] [Inhabited sig.C] (term : PreGroundTerm sig) (term_arity_ok : arity_ok term = true) (forbidden_constants forbidden_constants_2 : List sig.C) (g : StrictConstantMapping sig) : (term.backtrackFacts term_arity_ok forbidden_constants).snd.length = ((g.toConstantMapping.apply_pre_ground_term term).backtrackFacts ⋯ forbidden_constants_2).snd.length

theorem PreGroundTerm.backtrackFacts_list_under_strict_constant_mapping_same_number_of_fresh_constants {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [GetFreshInhabitant sig.C] [Inhabited sig.C] (terms : List (PreGroundTerm sig)) (terms_arity_ok : ∀ (t : PreGroundTerm sig), t ∈ terms → arity_ok t = true) (forbidden_constants forbidden_constants_2 : List sig.C) (g : StrictConstantMapping sig) : (backtrackFacts_list terms terms_arity_ok forbidden_constants).snd.length = (backtrackFacts_list (List.map g.toConstantMapping.apply_pre_ground_term terms) ⋯ forbidden_constants_2).snd.length

theorem PreGroundTerm.backtrackFacts_under_constant_mapping_subset_of_composing_with_subs {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [GetFreshInhabitant sig.C] [Inhabited sig.C] (term : PreGroundTerm sig) (term_arity_ok : arity_ok term = true) (forbidden_constants : List sig.C) (forbidden_constants_subsumes_term : FiniteTree.leaves term ⊆ forbidden_constants) (forbidden_constants_subsumes_rules : List.flatMap (Rule.constants ∘ SkolemFS.rule) (FiniteTree.innerLabels term) ⊆ forbidden_constants) : have backtracking := term.backtrackFacts term_arity_ok forbidden_constants; ∀ (g : StrictConstantMapping sig), (∀ (d : sig.C), d ∈ List.flatMap (Rule.constants ∘ SkolemFS.rule) (FiniteTree.innerLabels term) → g d = d) → ∃ (fresh_constant_remapping : StrictConstantMapping sig), (∀ (d : sig.C), ¬d ∈ backtracking.snd → fresh_constant_remapping d = d) ∧ (StrictConstantMapping.toConstantMapping fun (c : sig.C) => if c ∈ backtracking.snd then fresh_constant_remapping c else g c).apply_fact_set backtracking.fst.toSet ⊆ ((g.toConstantMapping.apply_pre_ground_term term).backtrackFacts ⋯ (List.map g forbidden_constants)).fst.toSet ∧ List.map fresh_constant_remapping backtracking.snd = ((g.toConstantMapping.apply_pre_ground_term term).backtrackFacts ⋯ (List.map g forbidden_constants)).snd

theorem PreGroundTerm.backtrackFacts_list_under_constant_mapping_subset_of_composing_with_subs {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [GetFreshInhabitant sig.C] [Inhabited sig.C] (terms : List (PreGroundTerm sig)) (terms_arity_ok : ∀ (t : PreGroundTerm sig), t ∈ terms → arity_ok t = true) (forbidden_constants : List sig.C) (forbidden_constants_subsumes_term : List.flatMap FiniteTree.leaves terms ⊆ forbidden_constants) (forbidden_constants_subsumes_rules : List.flatMap (Rule.constants ∘ SkolemFS.rule) (List.flatMap FiniteTree.innerLabels terms) ⊆ forbidden_constants) : have backtracking := backtrackFacts_list terms terms_arity_ok forbidden_constants; ∀ (g : StrictConstantMapping sig), (∀ (d : sig.C), d ∈ List.flatMap (Rule.constants ∘ SkolemFS.rule) (List.flatMap FiniteTree.innerLabels terms) → g d = d) → ∃ (fresh_constant_remapping : StrictConstantMapping sig), (∀ (d : sig.C), ¬d ∈ backtracking.snd → fresh_constant_remapping d = d) ∧ (StrictConstantMapping.toConstantMapping fun (c : sig.C) => if c ∈ backtracking.snd then fresh_constant_remapping c else g c).apply_fact_set backtracking.fst.toSet ⊆ (backtrackFacts_list (List.map g.toConstantMapping.apply_pre_ground_term terms) ⋯ (List.map g forbidden_constants)).fst.toSet ∧ List.map fresh_constant_remapping backtracking.snd = (backtrackFacts_list (List.map g.toConstantMapping.apply_pre_ground_term terms) ⋯ (List.map g forbidden_constants)).snd