Theory Bounded_Certificate_Search

section ‹A certificate-producing bounded search›

theory Bounded_Certificate_Search
  imports Equality_Saturation_Checker
begin

text ‹
  The trusted result in this theory is independent of matching and scheduling.
  An arbitrary generator proposes certificate steps; only proposals accepted by
  \<^const>‹apply_step› enter the frontier.  Consequently every path emitted by
  the bounded search is accepted by the independent checker.
›

definition step_children ::
  "('f, 'v) rule list ⇒ ('f, 'v) rule list ⇒
    (('f, 'v) term ⇒ ('f, 'v) certificate_step list) ⇒
    ('f, 'v) term ⇒ ('f, 'v) certificate_step list ⇒
    (('f, 'v) term × ('f, 'v) certificate_step list) list" where
  "step_children R Γ gen u sts =
     concat (map (λst. case apply_step R Γ st u of
                         None ⇒ []
                       | Some u' ⇒ [(u', sts @ [st])]) (gen u))"

definition expand ::
  "('f, 'v) rule list ⇒ ('f, 'v) rule list ⇒
    (('f, 'v) term ⇒ ('f, 'v) certificate_step list) ⇒
    (('f, 'v) term × ('f, 'v) certificate_step list) ⇒
    (('f, 'v) term × ('f, 'v) certificate_step list) list" where
  "expand R Γ gen p = step_children R Γ gen (fst p) (snd p)"

fun iterate_search ::
  "('f, 'v) rule list ⇒ ('f, 'v) rule list ⇒
    (('f, 'v) term ⇒ ('f, 'v) certificate_step list) ⇒ nat ⇒
    (('f, 'v) term × ('f, 'v) certificate_step list) list ⇒
    (('f, 'v) term × ('f, 'v) certificate_step list) list" where
  "iterate_search R Γ gen 0 F = F"
| "iterate_search R Γ gen (Suc n) F =
     iterate_search R Γ gen n
       (F @ concat (map (expand R Γ gen) F))"

definition run_bounded_search ::
  "('f, 'v) rule list ⇒ ('f, 'v) rule list ⇒
    (('f, 'v) term ⇒ ('f, 'v) certificate_step list) ⇒ nat ⇒
    ('f, 'v) term ⇒
    (('f, 'v) term × ('f, 'v) certificate_step list) list" where
  "run_bounded_search R Γ gen n t =
    iterate_search R Γ gen n [(t, [])]"

lemma apply_steps_append:
  "apply_steps R Γ (as @ bs) t =
     (case apply_steps R Γ as t of
        None ⇒ None
      | Some u ⇒ apply_steps R Γ bs u)"
  by (induction as arbitrary: t) (auto split: option.splits)

lemma apply_steps_snoc:
  assumes "apply_steps R Γ sts t = Some u"
    and "apply_step R Γ st u = Some u'"
  shows "apply_steps R Γ (sts @ [st]) t = Some u'"
  using assms by (auto simp: apply_steps_append)

lemma step_children_accepted:
  assumes "apply_steps R Γ sts t = Some u"
    and "(u', sts') ∈ set (step_children R Γ gen u sts)"
  shows "apply_steps R Γ sts' t = Some u'"
proof -
  from assms(2) obtain st where
    emit: "(u', sts') ∈
      set (case apply_step R Γ st u of
             None ⇒ []
           | Some v ⇒ [(v, sts @ [st])])"
    unfolding step_children_def by auto
  then obtain v where
    accepted: "apply_step R Γ st u = Some v" and
    pair: "(u', sts') = (v, sts @ [st])"
    by (auto split: option.splits)
  from apply_steps_snoc[OF assms(1) accepted] pair show ?thesis by simp
qed

lemma expand_accepted:
  assumes "apply_steps R Γ (snd p) t = Some (fst p)"
    and "q ∈ set (expand R Γ gen p)"
  shows "apply_steps R Γ (snd q) t = Some (fst q)"
proof -
  obtain u sts where q: "q = (u, sts)" by (cases q)
  from assms(2) q have
    "(u, sts) ∈ set (step_children R Γ gen (fst p) (snd p))"
    by (simp add: expand_def)
  from step_children_accepted[OF assms(1) this] q show ?thesis by simp
qed

lemma iterate_search_accepted:
  assumes "∀p ∈ set F.
      apply_steps R Γ (snd p) t = Some (fst p)"
  shows "∀p ∈ set (iterate_search R Γ gen n F).
      apply_steps R Γ (snd p) t = Some (fst p)"
  using assms
proof (induction n arbitrary: F)
  case 0
  then show ?case by simp
next
  case (Suc n)
  let ?F = "F @ concat (map (expand R Γ gen) F)"
  have "∀p ∈ set ?F.
      apply_steps R Γ (snd p) t = Some (fst p)"
  proof
    fix p
    assume "p ∈ set ?F"
    then consider "p ∈ set F"
      | "p ∈ set (concat (map (expand R Γ gen) F))"
      by auto
    then show "apply_steps R Γ (snd p) t = Some (fst p)"
    proof cases
      case 1
      then show ?thesis using Suc.prems by blast
    next
      case 2
      then obtain q where
        "q ∈ set F" and "p ∈ set (expand R Γ gen q)"
        by auto
      then show ?thesis using expand_accepted Suc.prems by blast
    qed
  qed
  from Suc.IH[OF this] show ?case by simp
qed

theorem run_bounded_search_accepted:
  assumes "(u, sts) ∈ set (run_bounded_search R Γ gen n t)"
  shows "check_explanation R Γ sts t u"
proof -
  have "∀p ∈ set [(t, [])].
      apply_steps R Γ (snd p) t = Some (fst p)"
    by simp
  from assms iterate_search_accepted[OF this]
  have "apply_steps R Γ sts t = Some u"
    by (fastforce simp: run_bounded_search_def)
  then show ?thesis by (simp add: check_explanation_def)
qed

corollary run_bounded_search_sound:
  assumes merges: "∀ab ∈ set Γ.
      (fst ab, snd ab) ∈ (rstep (set R))⇧↔⇧*"
    and result: "(u, sts) ∈ set (run_bounded_search R Γ gen n t)"
  shows "(t, u) ∈ (rstep (set R))⇧↔⇧*"
  by (rule check_explanation_sound[
        OF merges run_bounded_search_accepted[OF result]])

definition find_explanation ::
  "('f, 'v) rule list ⇒ ('f, 'v) rule list ⇒
    (('f, 'v) term ⇒ ('f, 'v) certificate_step list) ⇒ nat ⇒
    ('f, 'v) term ⇒ ('f, 'v) term ⇒
    ('f, 'v) certificate_step list option" where
  "find_explanation R Γ gen n t u =
     (case filter (λp. fst p = u)
       (run_bounded_search R Γ gen n t) of
        [] ⇒ None
      | p # _ ⇒ Some (snd p))"

theorem find_explanation_accepted:
  assumes "find_explanation R Γ gen n t u = Some sts"
  shows "check_explanation R Γ sts t u"
proof -
  from assms have
    "filter (λp. fst p = u)
      (run_bounded_search R Γ gen n t) ≠ []"
    unfolding find_explanation_def by (auto split: list.splits)
  then obtain p ps where
    filter: "filter (λp. fst p = u)
      (run_bounded_search R Γ gen n t) = p # ps"
    by (cases "filter (λp. fst p = u)
          (run_bounded_search R Γ gen n t)") auto
  from assms filter have snd_p: "snd p = sts"
    unfolding find_explanation_def by simp
  have in_filter:
    "p ∈ set (filter (λp. fst p = u)
      (run_bounded_search R Γ gen n t))"
    using filter by simp
  then have mem:
    "p ∈ set (run_bounded_search R Γ gen n t)" by simp
  from in_filter have fst_p: "fst p = u" by simp
  from fst_p snd_p have p: "p = (u, sts)" by (cases p) simp
  from mem p have
    "(u, sts) ∈ set (run_bounded_search R Γ gen n t)" by simp
  then show ?thesis by (rule run_bounded_search_accepted)
qed

corollary find_explanation_sound:
  assumes "∀ab ∈ set Γ.
      (fst ab, snd ab) ∈ (rstep (set R))⇧↔⇧*"
    and "find_explanation R Γ gen n t u = Some sts"
  shows "(t, u) ∈ (rstep (set R))⇧↔⇧*"
  by (rule check_explanation_sound[OF assms(1)
        find_explanation_accepted[OF assms(2)]])

end