Theory Extraction_Certificates

section ‹Candidate-set extraction certificates›

theory Extraction_Certificates
  imports EGraph_Explanations
begin

text ‹
  This lightweight interchange checker validates an explicitly enumerated
  candidate set: the chosen term is convertible to the source and has minimum
  cost among the supplied candidates.  The stronger acyclic-e-graph development
  builds and verifies a dynamic-programming extractor over every term
  represented by a finite e-class DAG.
›

fun term_cost :: "('f ⇒ nat) ⇒ ('f, 'v) term ⇒ nat" where
  "term_cost w (Var x) = 1"
| "term_cost w (Fun f ts) = w f + sum_list (map (term_cost w) ts)"

record ('f, 'v) extraction =
  ex_source :: "('f, 'v) term"
  ex_chosen :: "('f, 'v) term"
  ex_candidates ::
    "(('f, 'v) term × ('f, 'v) certificate_step list) list"

definition check_extraction ::
  "('f ⇒ nat) ⇒ ('f, 'v) rule list ⇒
    ('f, 'v) rule list ⇒ ('f, 'v) extraction ⇒ bool" where
  "check_extraction w R Γ E ⟷
     (∀p ∈ set (ex_candidates E).
        check_explanation R Γ (snd p) (ex_source E) (fst p)) ∧
     ex_chosen E ∈ set (map fst (ex_candidates E)) ∧
     (∀v ∈ set (map fst (ex_candidates E)).
        term_cost w (ex_chosen E) ≤ term_cost w v)"

lemma check_extraction_candidate_sound:
  assumes merges: "∀ab ∈ set Γ.
      (fst ab, snd ab) ∈ (rstep (set R))⇧↔⇧*"
    and check: "check_extraction w R Γ E"
    and candidate: "v ∈ set (map fst (ex_candidates E))"
  shows "(ex_source E, v) ∈ (rstep (set R))⇧↔⇧*"
proof -
  from candidate obtain p where
    p: "p ∈ set (ex_candidates E)" and v: "fst p = v"
    by force
  from check p have
    "check_explanation R Γ (snd p) (ex_source E) (fst p)"
    unfolding check_extraction_def by blast
  from check_explanation_sound[OF merges this] v show ?thesis by simp
qed

lemma check_extraction_chosen_sound:
  assumes "∀ab ∈ set Γ.
      (fst ab, snd ab) ∈ (rstep (set R))⇧↔⇧*"
    and "check_extraction w R Γ E"
  shows "(ex_source E, ex_chosen E) ∈ (rstep (set R))⇧↔⇧*"
proof -
  from assms(2) have
    "ex_chosen E ∈ set (map fst (ex_candidates E))"
    unfolding check_extraction_def by simp
  from check_extraction_candidate_sound[OF assms this] show ?thesis .
qed

lemma check_extraction_minimal:
  assumes "check_extraction w R Γ E"
    and "v ∈ set (map fst (ex_candidates E))"
  shows "term_cost w (ex_chosen E) ≤ term_cost w v"
  using assms unfolding check_extraction_def by blast

theorem extraction_over_checked_log_correct:
  assumes log: "check_merge_log R mlog"
    and extraction:
      "check_extraction w R (recorded_merges mlog) E"
  shows "(ex_source E, ex_chosen E)
           ∈ (rstep (set R))⇧↔⇧*"
    and "∀v ∈ set (map fst (ex_candidates E)).
           term_cost w (ex_chosen E) ≤ term_cost w v"
proof -
  have merges: "∀ab ∈ set (recorded_merges mlog).
      (fst ab, snd ab) ∈ (rstep (set R))⇧↔⇧*"
    using checked_merge_log_sound[OF log] by blast
  show "(ex_source E, ex_chosen E)
      ∈ (rstep (set R))⇧↔⇧*"
    by (rule check_extraction_chosen_sound[OF merges extraction])
  show "∀v ∈ set (map fst (ex_candidates E)).
      term_cost w (ex_chosen E) ≤ term_cost w v"
    using extraction unfolding check_extraction_def by blast
qed

end