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.skolem_ruleIds_valid {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rl : RuleList sig) (term : GroundTerm sig) : Prop

Equations

• GroundTerm.skolem_ruleIds_valid rl term = PreGroundTerm.skolem_ruleIds_valid rl term.val

def GroundTerm.skolem_disjIdx_valid {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rl : RuleList sig) (term : GroundTerm sig) (term_ruleIds_valid : skolem_ruleIds_valid rl term) : Prop

Equations

• GroundTerm.skolem_disjIdx_valid rl term term_ruleIds_valid = PreGroundTerm.skolem_disjIdx_valid rl term.val term_ruleIds_valid

def GroundTerm.skolem_rule_arity_valid {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rl : RuleList sig) (term : GroundTerm sig) (term_ruleIds_valid : skolem_ruleIds_valid rl term) : Prop

Equations

• GroundTerm.skolem_rule_arity_valid rl term term_ruleIds_valid = PreGroundTerm.skolem_rule_arity_valid rl term.val term_ruleIds_valid

theorem GroundTerm.skolem_ruleIds_valid_const {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rl : RuleList sig) (c : sig.C) : skolem_ruleIds_valid rl (const c)

theorem GroundTerm.skolem_disjIdx_valid_const {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rl : RuleList sig) (c : sig.C) : skolem_disjIdx_valid rl (const c) ⋯

theorem GroundTerm.skolem_rule_arity_valid_const {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rl : RuleList sig) (c : sig.C) : skolem_rule_arity_valid rl (const c) ⋯

def GroundTerm.backtrackTrigger {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] (rl : RuleList sig) (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) (term_ruleIds_valid : skolem_ruleIds_valid rl term) (term_rule_arity_valid : skolem_rule_arity_valid rl term term_ruleIds_valid) (forbidden_constants : List sig.C) : PreTrigger sig

Equations

• One or more equations did not get rendered due to their size.

def GroundTerm.backtrackFacts {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] (rl : RuleList sig) (term : GroundTerm sig) (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) : List (Fact sig) × List sig.C

Equations

• One or more equations did not get rendered due to their size.

def GroundTerm.backtrackFacts_list {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] (rl : RuleList sig) (terms : List (GroundTerm sig)) (terms_ruleIds_valid : ∀ (t : GroundTerm sig), t ∈ terms → skolem_ruleIds_valid rl t) (terms_disjIdx_valid : ∀ (t : GroundTerm sig) (mem : t ∈ terms), skolem_disjIdx_valid rl t ⋯) (terms_rule_arity_valid : ∀ (t : GroundTerm sig) (mem : t ∈ terms), skolem_rule_arity_valid rl t ⋯) (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 rl [] terms_ruleIds_valid_2 terms_disjIdx_valid_2 terms_rule_arity_valid_2 forbidden_constants = ([], [])

theorem GroundTerm.backtrackFacts_list_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] {rl : RuleList sig} {terms : List (GroundTerm sig)} {terms_ruleIds_valid : ∀ (t : GroundTerm sig), t ∈ terms → skolem_ruleIds_valid rl t} {terms_disjIdx_valid : ∀ (t : GroundTerm sig) (mem : t ∈ terms), skolem_disjIdx_valid rl t ⋯} {terms_rule_arity_valid : ∀ (t : GroundTerm sig) (mem : t ∈ terms), skolem_rule_arity_valid rl t ⋯} {forbidden_constants : List sig.C} : backtrackFacts_list rl terms terms_ruleIds_valid terms_disjIdx_valid terms_rule_arity_valid forbidden_constants = PreGroundTerm.backtrackFacts_list rl 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] {rl : RuleList sig} {term : GroundTerm sig} {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} (c : sig.C) : c ∈ (backtrackFacts rl term term_ruleIds_valid term_disjIdx_valid term_rule_arity_valid 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] {rl : RuleList sig} {terms : List (GroundTerm sig)} {terms_ruleIds_valid : ∀ (t : GroundTerm sig), t ∈ terms → skolem_ruleIds_valid rl t} {terms_disjIdx_valid : ∀ (t : GroundTerm sig) (mem : t ∈ terms), skolem_disjIdx_valid rl t ⋯} {terms_rule_arity_valid : ∀ (t : GroundTerm sig) (mem : t ∈ terms), skolem_rule_arity_valid rl t ⋯} {forbidden_constants : List sig.C} (c : sig.C) : c ∈ (backtrackFacts_list rl terms terms_ruleIds_valid terms_disjIdx_valid terms_rule_arity_valid 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] {rl : RuleList sig} {term : GroundTerm sig} {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} (f : Fact sig) : f ∈ (backtrackFacts rl term term_ruleIds_valid term_disjIdx_valid term_rule_arity_valid forbidden_constants).fst → ∀ (c : sig.C), c ∈ f.constants → c ∈ List.flatMap Rule.constants rl.rules ∨ c ∈ term.constants ∨ c ∈ (backtrackFacts rl term term_ruleIds_valid term_disjIdx_valid term_rule_arity_valid 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] {rl : RuleList sig} {terms : List (GroundTerm sig)} {terms_ruleIds_valid : ∀ (t : GroundTerm sig), t ∈ terms → skolem_ruleIds_valid rl t} {terms_disjIdx_valid : ∀ (t : GroundTerm sig) (mem : t ∈ terms), skolem_disjIdx_valid rl t ⋯} {terms_rule_arity_valid : ∀ (t : GroundTerm sig) (mem : t ∈ terms), skolem_rule_arity_valid rl t ⋯} {forbidden_constants : List sig.C} (f : Fact sig) : f ∈ (backtrackFacts_list rl terms terms_ruleIds_valid terms_disjIdx_valid terms_rule_arity_valid forbidden_constants).fst → ∀ (c : sig.C), c ∈ f.constants → c ∈ List.flatMap Rule.constants rl.rules ∨ c ∈ List.flatMap constants terms ∨ c ∈ (backtrackFacts_list rl terms terms_ruleIds_valid terms_disjIdx_valid terms_rule_arity_valid forbidden_constants).snd