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] [CustomBasicDatastructures.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 done using the GetFreshInhabitant typeclass.

Equations

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

@[simp]

theorem Rule.length_fresh_consts_for_pure_body_vars {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [CustomBasicDatastructures.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] [CustomBasicDatastructures.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] [CustomBasicDatastructures.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.