Theory Equality_Saturation_Checker

section ‹Equality-saturation explanation certificates›

theory Equality_Saturation_Checker
  imports
    First_Order_Rewriting.Trs
    First_Order_Terms.Term_Impl
begin

text ‹
  This development deliberately reuses the first-order terms, substitutions,
  positions, and contexts from the AFP session
  \<^session>‹First_Order_Terms›.  It uses the rewrite relation from
  \<^session>‹First_Order_Rewriting›.  In particular, the semantic target of
  the checker is the existing conversion relation
  \<^term>‹(rstep (set R))⇧↔⇧*›; no separate term language or
  equational calculus is introduced here.

  What is specific to equality saturation is the certificate boundary.  A
  certificate is a flat path whose steps either apply a numbered input rule at
  an AFP position, or reuse a numbered equality recorded by an earlier checked
  e-class merge.  Recorded merges are concrete term equalities, as in an
  e-graph, and therefore need no substitution when reused.
›

datatype direction = Forward | Backward

fun orient_pair :: "direction ⇒ 'a × 'a ⇒ 'a × 'a" where
  "orient_pair Forward ab = ab"
| "orient_pair Backward (a, b) = (b, a)"

datatype ('f, 'v) certificate_step =
    Rule_At pos nat direction "('f, 'v) subst"
  | Merge_At pos nat direction

fun apply_step ::
  "('f, 'v) rule list ⇒ ('f, 'v) rule list ⇒
    ('f, 'v) certificate_step ⇒ ('f, 'v) term ⇒
    ('f, 'v) term option" where
  "apply_step R Γ (Rule_At p i d σ) t =
     (if i < length R ∧ p ∈ poss t ∧
          t |_ p = fst (orient_pair d (R ! i)) ⋅ σ
      then Some (replace_at t p (snd (orient_pair d (R ! i)) ⋅ σ))
      else None)"
| "apply_step R Γ (Merge_At p i d) t =
     (if i < length Γ ∧ p ∈ poss t ∧
          t |_ p = fst (orient_pair d (Γ ! i))
      then Some (replace_at t p (snd (orient_pair d (Γ ! i))))
      else None)"

fun apply_steps ::
  "('f, 'v) rule list ⇒ ('f, 'v) rule list ⇒
    ('f, 'v) certificate_step list ⇒ ('f, 'v) term ⇒
    ('f, 'v) term option" where
  "apply_steps R Γ [] t = Some t"
| "apply_steps R Γ (st # sts) t =
     (case apply_step R Γ st t of
        None ⇒ None
      | Some u ⇒ apply_steps R Γ sts u)"

definition check_explanation ::
  "('f, 'v) rule list ⇒ ('f, 'v) rule list ⇒
    ('f, 'v) certificate_step list ⇒ ('f, 'v) term ⇒
    ('f, 'v) term ⇒ bool" where
  "check_explanation R Γ sts t u ⟷
     apply_steps R Γ sts t = Some u"

subsection ‹Soundness in the AFP rewrite relation›

lemma lift_conversion_at_position:
  assumes p: "p ∈ poss t"
    and sub: "t |_ p = s"
    and conv: "(s, u) ∈ (rstep R)⇧↔⇧*"
  shows "(t, replace_at t p u) ∈ (rstep R)⇧↔⇧*"
proof -
  have "((ctxt_of_pos_term p t)⟨s⟩,
         (ctxt_of_pos_term p t)⟨u⟩) ∈ (rstep R)⇧↔⇧*"
    by (rule conversion_ctxt_closed[OF conv])
  moreover have "(ctxt_of_pos_term p t)⟨s⟩ = t"
    using ctxt_supt_id[OF p] sub by simp
  ultimately show ?thesis by simp
qed

lemma oriented_rule_conversion:
  assumes i: "i < length R"
  shows "(fst (orient_pair d (R ! i)) ⋅ σ,
          snd (orient_pair d (R ! i)) ⋅ σ)
         ∈ (rstep (set R))⇧↔⇧*"
proof -
  obtain l r where lr: "R ! i = (l, r)" by (cases "R ! i")
  have "R ! i ∈ set R" by (rule nth_mem[OF i])
  then have mem: "(l, r) ∈ set R" using lr by simp
  have step: "(l ⋅ σ, r ⋅ σ) ∈ rstep (set R)"
    by (rule rstep_subst[OF rstep_rule[OF mem]])
  show ?thesis
  proof (cases d)
    case Forward
    with lr step show ?thesis
      unfolding conversion_def by auto
  next
    case Backward
    with lr step show ?thesis
      unfolding conversion_def by auto
  qed
qed

lemma apply_step_sound:
  assumes merges:
    "∀ab ∈ set Γ. (fst ab, snd ab) ∈ (rstep (set R))⇧↔⇧*"
    and step: "apply_step R Γ st t = Some u"
  shows "(t, u) ∈ (rstep (set R))⇧↔⇧*"
proof (cases st)
  case (Rule_At p i d σ)
  from step Rule_At have i: "i < length R" and p: "p ∈ poss t"
    and sub: "t |_ p = fst (orient_pair d (R ! i)) ⋅ σ"
    and u: "u = replace_at t p (snd (orient_pair d (R ! i)) ⋅ σ)"
    by (auto split: if_splits)
  have "(fst (orient_pair d (R ! i)) ⋅ σ,
         snd (orient_pair d (R ! i)) ⋅ σ)
        ∈ (rstep (set R))⇧↔⇧*"
    by (rule oriented_rule_conversion[OF i])
  from lift_conversion_at_position[OF p sub this] u show ?thesis by simp
next
  case (Merge_At p i d)
  from step Merge_At have i: "i < length Γ" and p: "p ∈ poss t"
    and sub: "t |_ p = fst (orient_pair d (Γ ! i))"
    and u: "u = replace_at t p (snd (orient_pair d (Γ ! i)))"
    by (auto split: if_splits)
  have mem: "Γ ! i ∈ set Γ" by (rule nth_mem[OF i])
  obtain a b where ab: "Γ ! i = (a, b)" by (cases "Γ ! i")
  have base:
    "(a, b) ∈ (rstep (set R))⇧↔⇧*"
    using merges mem ab by fastforce
  have oriented:
    "(fst (orient_pair d (Γ ! i)), snd (orient_pair d (Γ ! i)))
      ∈ (rstep (set R))⇧↔⇧*"
  proof (cases d)
    case Forward
    with base ab show ?thesis by simp
  next
    case Backward
    have "(b, a) ∈ (rstep (set R))⇧↔⇧*"
      using base
      by (rule conversion_sym[unfolded sym_def, rule_format])
    with Backward ab show ?thesis by simp
  qed
  from lift_conversion_at_position[OF p sub oriented] u show ?thesis by simp
qed

lemma apply_steps_sound:
  assumes merges:
    "∀ab ∈ set Γ. (fst ab, snd ab) ∈ (rstep (set R))⇧↔⇧*"
    and run: "apply_steps R Γ sts t = Some u"
  shows "(t, u) ∈ (rstep (set R))⇧↔⇧*"
  using run
proof (induction sts arbitrary: t)
  case Nil
  then show ?case by simp
next
  case (Cons st sts)
  from Cons.prems obtain v where
    first: "apply_step R Γ st t = Some v" and
    rest: "apply_steps R Γ sts v = Some u"
    by (auto split: option.splits)
  have tv: "(t, v) ∈ (rstep (set R))⇧↔⇧*"
    by (rule apply_step_sound[OF merges first])
  have vu: "(v, u) ∈ (rstep (set R))⇧↔⇧*"
    by (rule Cons.IH[OF rest])
  from tv vu show ?case
    unfolding conversion_def by (rule rtrancl_trans)
qed

theorem check_explanation_sound:
  assumes "∀ab ∈ set Γ.
      (fst ab, snd ab) ∈ (rstep (set R))⇧↔⇧*"
    and "check_explanation R Γ sts t u"
  shows "(t, u) ∈ (rstep (set R))⇧↔⇧*"
  using apply_steps_sound[OF assms(1) assms(2)[unfolded check_explanation_def]] .

corollary check_rule_explanation_sound:
  assumes "check_explanation R [] sts t u"
  shows "(t, u) ∈ (rstep (set R))⇧↔⇧*"
  by (rule check_explanation_sound[OF _ assms]) simp

end