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.

@[irreducible]

def PreGroundTerm.skolem_ruleIds_valid {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rl : RuleList sig) : PreGroundTerm sig → Prop

SkolemFS.ruleId_valid lifted to PreGroundTerm.

Equations

• PreGroundTerm.skolem_ruleIds_valid rl (FiniteTree.leaf a) = True
• PreGroundTerm.skolem_ruleIds_valid rl (FiniteTree.inner func ts) = (func.ruleId_valid rl ∧ ∀ (t : FiniteTree (SkolemFS sig) sig.C), t ∈ ts → PreGroundTerm.skolem_ruleIds_valid rl t)

@[irreducible]

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

SkolemFS.disjunctIndex_valid lifted to PreGroundTerm.

Equations

• One or more equations did not get rendered due to their size.
• PreGroundTerm.skolem_disjIdx_valid rl (FiniteTree.leaf a) term_ruleIds_valid_2 = True

@[irreducible]

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

SkolemFS.arity_valid lifted to PreGroundTerm.

Equations

• One or more equations did not get rendered due to their size.
• PreGroundTerm.skolem_rule_arity_valid rl (FiniteTree.leaf a) term_ruleIds_valid_2 = True

def PreGroundTerm.backtrackTrigger {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] [Inhabited sig.C] (rl : RuleList sig) (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) (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

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 rl (FiniteTree.leaf c) term_is_func_2 term_arity_ok_2 term_ruleIds_valid_2 term_rule_arity_valid_2 forbidden_constants = ⋯.elim

def PreGroundTerm.backtrackFacts {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [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) : 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 rl (FiniteTree.leaf c) term_arity_ok_2 term_ruleIds_valid_2 term_disjIdx_valid_2 term_rule_arity_valid_2 forbidden_constants = ([], [])

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

Equations

• One or more equations did not get rendered due to their size.
• PreGroundTerm.backtrackFacts_list rl [] terms_arity_ok_2 terms_ruleIds_valid_2 terms_disjIdx_valid_2 terms_rule_arity_valid_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] {rl : RuleList sig} {forbidden_constants : List sig.C} : backtrackFacts_list rl [] ⋯ ⋯ ⋯ ⋯ forbidden_constants = ([], [])

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

@[irreducible]

theorem PreGroundTerm.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 : 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} (c : sig.C) : c ∈ (backtrackFacts rl term term_arity_ok term_ruleIds_valid term_disjIdx_valid term_rule_arity_valid forbidden_constants).snd → ¬c ∈ forbidden_constants

The fresh constants are indeed not forbidden.

@[irreducible]

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] {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} (c : sig.C) : c ∈ (backtrackFacts_list rl terms terms_arity_ok terms_ruleIds_valid terms_disjIdx_valid terms_rule_arity_valid forbidden_constants).snd → ¬c ∈ forbidden_constants

@[irreducible]

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] {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} (f : Fact sig) : f ∈ (backtrackFacts rl term term_arity_ok 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 ∈ FiniteTree.leaves term ∨ c ∈ (backtrackFacts rl term term_arity_ok term_ruleIds_valid term_disjIdx_valid term_rule_arity_valid forbidden_constants).snd

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

@[irreducible]

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] {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} (f : Fact sig) : f ∈ (backtrackFacts_list rl terms terms_arity_ok 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 FiniteTree.leaves terms ∨ c ∈ (backtrackFacts_list rl terms terms_arity_ok terms_ruleIds_valid terms_disjIdx_valid terms_rule_arity_valid forbidden_constants).snd