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

@[irreducible]

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] (rl : RuleList sig) (term : PreGroundTerm sig) (term_arity_ok : arity_ok term = true) (term_ruleIds_valid : skolem_ruleIds_valid rl term) (term_disjIdx_valid : skolem_disjIdx_valid rl term term_ruleIds_valid) (term_rule_arity_valid : skolem_rule_arity_valid rl term term_ruleIds_valid) (forbidden_constants forbidden_constants_2 : List sig.C) (g : StrictConstantMapping sig) : (backtrackFacts rl term term_arity_ok term_ruleIds_valid term_disjIdx_valid term_rule_arity_valid forbidden_constants).snd.length = (backtrackFacts rl (g.toConstantMapping.apply_pre_ground_term term) ⋯ ⋯ ⋯ ⋯ forbidden_constants_2).snd.length

@[irreducible]

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] (rl : RuleList sig) (terms : List (PreGroundTerm sig)) (terms_arity_ok : ∀ (t : PreGroundTerm sig), t ∈ terms → arity_ok t = true) (terms_ruleIds_valid : ∀ (t : PreGroundTerm sig), t ∈ terms → skolem_ruleIds_valid rl t) (terms_disjIdx_valid : ∀ (t : PreGroundTerm sig) (t_mem : t ∈ terms), skolem_disjIdx_valid rl t ⋯) (terms_rule_arity_valid : ∀ (t : PreGroundTerm sig) (t_mem : t ∈ terms), skolem_rule_arity_valid rl t ⋯) (forbidden_constants forbidden_constants_2 : List sig.C) (g : StrictConstantMapping sig) : (backtrackFacts_list rl terms terms_arity_ok terms_ruleIds_valid terms_disjIdx_valid terms_rule_arity_valid forbidden_constants).snd.length = (backtrackFacts_list rl (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] (rl : RuleList sig) (term : PreGroundTerm sig) (term_arity_ok : arity_ok term = true) (term_ruleIds_valid : skolem_ruleIds_valid rl term) (term_disjIdx_valid : skolem_disjIdx_valid rl term term_ruleIds_valid) (term_rule_arity_valid : skolem_rule_arity_valid rl term term_ruleIds_valid) (forbidden_constants : List sig.C) (forbidden_constants_subsumes_term : FiniteTree.leaves term ⊆ forbidden_constants) (forbidden_constants_subsumes_rules : List.flatMap Rule.constants rl.rules ⊆ forbidden_constants) : have backtracking := backtrackFacts rl term term_arity_ok term_ruleIds_valid term_disjIdx_valid term_rule_arity_valid forbidden_constants; ∀ (g : StrictConstantMapping sig), (∀ (d : sig.C), d ∈ List.flatMap Rule.constants rl.rules → 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 rl (g.toConstantMapping.apply_pre_ground_term term) ⋯ ⋯ ⋯ ⋯ (List.map g forbidden_constants)).fst.toSet ∧ List.map fresh_constant_remapping backtracking.snd = (backtrackFacts rl (g.toConstantMapping.apply_pre_ground_term term) ⋯ ⋯ ⋯ ⋯ (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] (rl : RuleList sig) (terms : List (PreGroundTerm sig)) (terms_arity_ok : ∀ (t : PreGroundTerm sig), t ∈ terms → arity_ok t = true) (terms_ruleIds_valid : ∀ (t : PreGroundTerm sig), t ∈ terms → skolem_ruleIds_valid rl t) (terms_disjIdx_valid : ∀ (t : PreGroundTerm sig) (t_mem : t ∈ terms), skolem_disjIdx_valid rl t ⋯) (terms_rule_arity_valid : ∀ (t : PreGroundTerm sig) (t_mem : t ∈ terms), skolem_rule_arity_valid rl t ⋯) (forbidden_constants : List sig.C) (forbidden_constants_subsumes_term : List.flatMap FiniteTree.leaves terms ⊆ forbidden_constants) (forbidden_constants_subsumes_rules : List.flatMap Rule.constants rl.rules ⊆ forbidden_constants) : have backtracking := backtrackFacts_list rl terms terms_arity_ok terms_ruleIds_valid terms_disjIdx_valid terms_rule_arity_valid forbidden_constants; ∀ (g : StrictConstantMapping sig), (∀ (d : sig.C), d ∈ List.flatMap Rule.constants rl.rules → 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 rl (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 rl (List.map g.toConstantMapping.apply_pre_ground_term terms) ⋯ ⋯ ⋯ ⋯ (List.map g forbidden_constants)).snd