Backtracking Facts for a GroundTerm

We mainly lift the machinery around PreGroundTerm.backtrackFacts to GroundTerm. We spare the doc comments on the individual definitions and theorems.

def GroundTerm.backtrackTrigger {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] (term : GroundTerm sig) (term_is_func : ∃ (func : SkolemFS sig), ∃ (ts : List (GroundTerm sig)), ∃ (arity_ok : ts.length = func.arity), term = GroundTerm.func func ts arity_ok) (forbidden_constants : List sig.C) : PreTrigger sig

Equations

• term.backtrackTrigger term_is_func forbidden_constants = term.val.backtrackTrigger ⋯ ⋯ forbidden_constants

def GroundTerm.backtrackFacts {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] (term : GroundTerm sig) (forbidden_constants : List sig.C) : List (Fact sig) × List sig.C

Equations

• term.backtrackFacts forbidden_constants = term.val.backtrackFacts ⋯ forbidden_constants

def GroundTerm.backtrackFacts_list {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] (terms : List (GroundTerm sig)) (forbidden_constants : List sig.C) : List (Fact sig) × List sig.C

Equations

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

theorem GroundTerm.backtrackFacts_list_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] {terms : List (GroundTerm sig)} {forbidden_constants : List sig.C} : backtrackFacts_list terms forbidden_constants = PreGroundTerm.backtrackFacts_list terms.unattach ⋯ forbidden_constants

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

theorem GroundTerm.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 (GroundTerm sig)} {forbidden_constants : List sig.C} (c : sig.C) : c ∈ (backtrackFacts_list terms forbidden_constants).snd → ¬c ∈ forbidden_constants

theorem GroundTerm.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 : GroundTerm sig} {forbidden_constants : List sig.C} (f : Fact sig) : f ∈ (term.backtrackFacts forbidden_constants).fst → ∀ (c : sig.C), c ∈ f.constants → c ∈ List.flatMap Rule.constants term.rules ∨ c ∈ term.constants ∨ c ∈ (term.backtrackFacts forbidden_constants).snd

theorem GroundTerm.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 (GroundTerm sig)} {forbidden_constants : List sig.C} (f : Fact sig) : f ∈ (backtrackFacts_list terms forbidden_constants).fst → ∀ (c : sig.C), c ∈ f.constants → c ∈ List.flatMap Rule.constants (List.flatMap rules terms) ∨ c ∈ List.flatMap constants terms ∨ c ∈ (backtrackFacts_list terms forbidden_constants).snd