Backtracking Facts for a Trigger

For DMFA/RMFA-like conditions, we need to be able to backtrack which facts are necessarily present when a trigger is loaded. This file starts with very basic auxiliary definitions for this endeavor.

def Rule.fresh_consts_for_pure_body_vars {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] (r : Rule sig) (forbidden_constants : List sig.C) : { l' : List sig.C // l'.length = r.pure_body_vars.length ∧ l'.Nodup ∧ ∀ (e : sig.C), e ∈ l' → ¬e ∈ forbidden_constants }

For a rule, we need to be able to obtain a fresh constant for each variable that only occurs in the body. This is doen using the GetFreshInhabitant typeclass.

Equations

• r.fresh_consts_for_pure_body_vars forbidden_constants = GetFreshInhabitant.fresh_n forbidden_constants r.pure_body_vars.length

theorem Rule.length_fresh_consts_for_pure_body_vars {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] {r : Rule sig} {forbidden_constants : List sig.C} : (r.fresh_consts_for_pure_body_vars forbidden_constants).val.length = r.pure_body_vars.length

The number of fresh constants obtained matches the number of variables.

theorem Rule.fresh_consts_for_pure_body_vars_idx_retained {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] {r : Rule sig} {forbidden_constants : List sig.C} {v : sig.V} {v_mem : v ∈ r.pure_body_vars} : List.idxOf (r.fresh_consts_for_pure_body_vars forbidden_constants).val[List.idxOf v r.pure_body_vars] (r.fresh_consts_for_pure_body_vars forbidden_constants).val = List.idxOf v r.pure_body_vars

For each variable, the index of the fresh constant introduced for this variable matches the index of the variable.

theorem Rule.fresh_consts_pure_body_vars_roundtrip {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [GetFreshInhabitant sig.C] {r : Rule sig} {forbidden_constants : List sig.C} {v : sig.V} {v_mem : v ∈ r.pure_body_vars} : r.pure_body_vars[List.idxOf (r.fresh_consts_for_pure_body_vars forbidden_constants).val[List.idxOf v r.pure_body_vars] (r.fresh_consts_for_pure_body_vars forbidden_constants).val] = v

Getting the variable at the index of the corresponding fresh constant returns the original variable.

def SkolemFS.ruleId_valid {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (sfs : SkolemFS sig) (rl : RuleList sig) : Prop

The rule id of a SkolemFS (Skolem Function Symbol) is valid if there is a rule with this id.

Equations

• sfs.ruleId_valid rl = ∃ (r : Rule sig), r ∈ rl.rules ∧ r.id = sfs.ruleId

def SkolemFS.disjunctIndex_valid {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (sfs : SkolemFS sig) (rl : RuleList sig) (ruleId_valid : sfs.ruleId_valid rl) : Prop

The disjunct index of a SkolemFS (Skolem Function Symbol) if the rule corresponding the its rule id indeed has enough head disjuncts.

Equations

• sfs.disjunctIndex_valid rl ruleId_valid = (sfs.disjunctIndex < (rl.get_by_id sfs.ruleId ruleId_valid).head.length)

def SkolemFS.arity_valid {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (sfs : SkolemFS sig) (rl : RuleList sig) (ruleId_valid : sfs.ruleId_valid rl) : Prop

The arity of a SkolemFS (Skolem Function Symbol) is valid if it matches the frontier length of the rule corresponding to its rule id.

Equations

• sfs.arity_valid rl ruleId_valid = (sfs.arity = (rl.get_by_id sfs.ruleId ruleId_valid).frontier.length)