Backtracking Facts for a PreGroundTerm

The main outcome of this file is PreGroundTerm.backtrackFacts, which returns facts necessarily involved in the derivation of a given functional term.

def PreGroundTerm.backtrackTrigger {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] (term : PreGroundTerm sig) (term_is_func : ∃ (func : SkolemFS sig), ∃ (ts : List (FiniteTree (SkolemFS sig) sig.C)), term = FiniteTree.inner func ts) (term_arity_ok : arity_ok term = true) (forbidden_constants : List sig.C) : PreTrigger sig

For a functional PreGroundTerm, we can find a PreTrigger that introduces it (while putting fresh constants for body variables).

Equations

• One or more equations did not get rendered due to their size.
• PreGroundTerm.backtrackTrigger (FiniteTree.leaf c) term_is_func_2 term_arity_ok_2 forbidden_constants = ⋯.elim

def PreGroundTerm.backtrackFacts {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] (term : PreGroundTerm sig) (term_arity_ok : arity_ok term = true) (forbidden_constants : List sig.C) : List (Fact sig) × List sig.C

For a PreGroundTerm, we can find the facts necessary to introduce this term. These are all facts in the body and head of the backtrackTrigger for the term as well as all backtrackFacts for the subterms (i.e. the children) or the term. Because we need to know which "fresh" constants have already been used, we also return those. Note that we also take a list of constants that are already forbidden.

Equations

• One or more equations did not get rendered due to their size.
• PreGroundTerm.backtrackFacts (FiniteTree.leaf c) term_arity_ok_2 forbidden_constants = ([], [])

def PreGroundTerm.backtrackFacts_list {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [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) : List (Fact sig) × List sig.C

Equations

• One or more equations did not get rendered due to their size.
• PreGroundTerm.backtrackFacts_list [] terms_arity_ok_2 forbidden_constants = ([], [])

theorem PreGroundTerm.backtrackFacts_list_nil {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] {forbidden_constants : List sig.C} : backtrackFacts_list [] ⋯ forbidden_constants = ([], [])

theorem PreGroundTerm.backtrackFacts_list_cons {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] {term : PreGroundTerm sig} {terms : List (PreGroundTerm sig)} {terms_arity_ok : ∀ (t : PreGroundTerm sig), t ∈ term :: terms → arity_ok t = true} {forbidden_constants : List sig.C} : backtrackFacts_list (term :: terms) terms_arity_ok forbidden_constants = have res_t := term.backtrackFacts ⋯ forbidden_constants; have res_ts := backtrackFacts_list terms ⋯ (forbidden_constants ++ res_t.snd); (res_t.fst ++ res_ts.fst, res_t.snd ++ res_ts.snd)

theorem PreGroundTerm.backtrackFacts_fresh_constants_not_forbidden {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] {term : PreGroundTerm sig} {term_arity_ok : arity_ok term = true} {forbidden_constants : List sig.C} (c : sig.C) : c ∈ (term.backtrackFacts term_arity_ok forbidden_constants).snd → ¬c ∈ forbidden_constants

The fresh constants are indeed not forbidden.

theorem PreGroundTerm.backtrackFacts_list_fresh_constants_not_forbidden {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [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} (c : sig.C) : c ∈ (backtrackFacts_list terms terms_arity_ok forbidden_constants).snd → ¬c ∈ forbidden_constants

theorem PreGroundTerm.backtrackFacts_constants_in_rules_or_term_or_fresh {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] {term : PreGroundTerm sig} {term_arity_ok : arity_ok term = true} {forbidden_constants : List sig.C} (f : Fact sig) : f ∈ (term.backtrackFacts term_arity_ok forbidden_constants).fst → ∀ (c : sig.C), c ∈ f.constants → c ∈ List.flatMap (Rule.constants ∘ SkolemFS.rule) (FiniteTree.innerLabels term) ∨ c ∈ FiniteTree.leaves term ∨ c ∈ (term.backtrackFacts term_arity_ok forbidden_constants).snd

Each constant in PreGroundTerm.backtrackFacts is in the rule set, a leaf in the term, or a fresh constant.

theorem PreGroundTerm.backtrackFacts_list_constants_in_rules_or_term_or_fresh {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [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} (f : Fact sig) : f ∈ (backtrackFacts_list terms terms_arity_ok forbidden_constants).fst → ∀ (c : sig.C), c ∈ f.constants → c ∈ List.flatMap (Rule.constants ∘ SkolemFS.rule) (List.flatMap FiniteTree.innerLabels terms) ∨ c ∈ List.flatMap FiniteTree.leaves terms ∨ c ∈ (backtrackFacts_list terms terms_arity_ok forbidden_constants).snd