1 files changed, 609 insertions, 0 deletions

diff --git a/matching.v b/matching.v
new file mode 100644
index 0000000..494bb92
--- /dev/null
+++ b/matching.v
@@ -0,0 +1,609 @@
+Require Import Coq.Strings.Ascii.
+Require Import Coq.Strings.String.
+Require Import Coq.NArith.BinNat.
+From stdpp Require Import fin_sets gmap option.
+From mininix Require Import expr maptools.
+
+Open Scope string_scope.
+Open Scope N_scope.
+Open Scope Z_scope.
+Open Scope nat_scope.
+
+Reserved Notation "bs '~' m '~>' brs" (at level 55).
+
+Inductive matches_r : gmap string expr → matcher → gmap string b_rhs -> Prop :=
+  | E_MatchEmpty strict : ∅ ~ M_Matcher ∅ strict ~> ∅
+  | E_MatchAny bs : bs ~ M_Matcher ∅ false ~> ∅
+  | E_MatchMandatory bs x e m bs' strict :
+      bs !! x = None →
+      m !! x = None →
+      delete x bs ~ M_Matcher m strict ~> bs' →
+      <[x := e]>bs ~ M_Matcher (<[x := M_Mandatory]>m) strict
+        ~> <[x := B_Nonrec e]>bs'
+  | E_MatchOptAvail bs x d e m bs' strict :
+      bs !! x = None →
+      m !! x = None →
+      delete x bs ~ M_Matcher m strict ~> bs' →
+      <[x := d]>bs ~ M_Matcher (<[x := M_Optional e]>m) strict
+        ~> <[x := B_Nonrec d]>bs'
+  | E_MatchOptDefault bs x e m bs' strict :
+      bs !! x = None →
+      m !! x = None →
+      bs ~ M_Matcher m strict ~> bs' →
+      bs ~ M_Matcher (<[x := M_Optional e]>m) strict ~> <[x := B_Rec e]>bs'
+where "bs ~ m ~> brs" := (matches_r bs m brs).
+
+Definition map_foldM `{Countable K} `{FinMap K M} `{MBind F} `{MRet F} {A B}
+  (f : K → A → B → F B) (init : B) (m : M A) : F B :=
+    map_fold (λ i x acc, acc ≫= f i x) (mret init) m.
+
+Definition matches_aux_f (x : string) (rhs : m_rhs)
+  (acc : option (gmap string expr * gmap string b_rhs)) :=
+    acc ← acc;
+    let (bs, brs) := (acc : gmap string expr * gmap string b_rhs) in
+    match rhs with
+    | M_Mandatory  =>
+        e ← bs !! x;
+        Some (bs, <[x := B_Nonrec e]>brs)
+    | M_Optional e =>
+        match bs !! x with
+        | Some e' => Some (bs, <[x := B_Nonrec e']>brs)
+        | None => Some (bs, <[x := B_Rec e]>brs)
+        end
+    end.
+
+Definition matches_aux (ms : gmap string m_rhs) (bs : gmap string expr) :
+  option (gmap string expr * gmap string b_rhs) :=
+    map_fold matches_aux_f (Some (bs, ∅)) ms.
+
+Definition matches (m : matcher) (bs : gmap string expr) :
+  option (gmap string b_rhs) :=
+    match m with
+    | M_Matcher ms strict =>
+        guard (strict → dom bs ⊆ matcher_keys m);;
+        snd <$> matches_aux ms bs
+    end.
+
+(* Copied from stdpp and changed so that the value types
+   of m1 and m2 are decoupled *)
+Lemma dom_subseteq_size' `{FinMapDom K M D} {A B} (m1 : M A) (m2 : M B) :
+  dom m2 ⊆ dom m1 → size m2 ≤ size m1.
+Proof.
+  revert m1. induction m2 as [|i x m2 ? IH] using map_ind; intros m1 Hdom.
+  { rewrite map_size_empty. lia. }
+  rewrite dom_insert in Hdom.
+  assert (i ∉ dom m2) by (by apply not_elem_of_dom).
+  assert (i ∈ dom m1) as [x' Hx']%elem_of_dom by set_solver.
+  rewrite <-(insert_delete m1 i x') by done.
+  rewrite !map_size_insert_None, <-Nat.succ_le_mono
+  by (by rewrite ?lookup_delete).
+  apply IH. rewrite dom_delete. set_solver.
+Qed.
+
+Lemma dom_empty_subset `{Countable K} `{FinMapDom K M D} {A B} (m : M A) :
+  dom m ⊆ dom (∅ : M B) → m = ∅.
+Proof.
+  intros Hdom.
+  apply dom_subseteq_size' in Hdom.
+  rewrite map_size_empty in Hdom.
+  inv Hdom.
+  by apply map_size_empty_inv.
+Qed.
+
+Lemma matches_aux_empty bs : matches_aux ∅ bs = Some (bs, ∅).
+Proof. done. Qed.
+
+Lemma matches_aux_f_comm (x : string) (rhs : m_rhs) (m : gmap string m_rhs)
+  (y z : string) (rhs1 rhs2 : m_rhs)
+  (acc : option (gmap string expr * gmap string b_rhs)) :
+    m !! x = None → y ≠ z →
+    <[x:=rhs]> m !! y = Some rhs1 →
+    <[x:=rhs]> m !! z = Some rhs2 →
+    matches_aux_f y rhs1 (matches_aux_f z rhs2 acc) =
+    matches_aux_f z rhs2 (matches_aux_f y rhs1 acc).
+Proof.
+  intros Hxm Hyz Hym Hzm.
+  unfold matches_aux_f.
+  destruct acc.
+  repeat (simplify_option_eq || done ||
+          destruct (g !! y) eqn:Egy || destruct (g !! z) eqn:Egz ||
+          case_match || rewrite insert_commute). done.
+Qed.
+
+Lemma matches_aux_insert m bs x rhs :
+  m !! x = None →
+  matches_aux (<[x := rhs]>m) bs = matches_aux_f x rhs (matches_aux m bs).
+Proof.
+  intros Hnotin. unfold matches_aux.
+  rewrite map_fold_insert_L; try done.
+  clear bs.
+  intros y z rhs1 rhs2 acc Hyz Hym Hzm.
+  by eapply matches_aux_f_comm.
+Qed.
+
+Lemma matches_aux_bs m bs bs' brs :
+  matches_aux m bs = Some (bs', brs) → bs = bs'.
+Proof.
+  revert bs bs' brs.
+  induction m using map_ind; intros bs bs' brs Hmatches.
+  - rewrite matches_aux_empty in Hmatches. congruence.
+  - rewrite matches_aux_insert in Hmatches; try done.
+    unfold matches_aux_f in Hmatches.
+    simplify_option_eq.
+    destruct H0.
+    case_match; try case_match;
+      simplify_option_eq; by apply IHm with (brs := g0).
+Qed.
+
+Lemma matches_aux_impl m bs brs x e :
+  m !! x = None →
+  bs !! x = None →
+  matches_aux m (<[x := e]>bs) = Some (<[x := e]>bs, brs) →
+  matches_aux m bs = Some (bs, brs).
+Proof.
+  intros Hxm Hxbs Hmatches.
+  revert bs brs Hxm Hxbs Hmatches.
+  induction m using map_ind; intros bs brs Hxm Hxbs Hmatches.
+  - rewrite matches_aux_empty.
+    rewrite matches_aux_empty in Hmatches.
+    by simplify_option_eq.
+  - rewrite matches_aux_insert in Hmatches by done.
+    rewrite matches_aux_insert by done.
+    apply lookup_insert_None in Hxm as [Hxm1 Hxm2].
+    unfold matches_aux_f in Hmatches. simplify_option_eq.
+    destruct H0. case_match.
+    + simplify_option_eq.
+      rewrite lookup_insert_ne in Heqo0 by done.
+      pose proof (IHm bs g0 Hxm1 Hxbs Heqo).
+      rewrite H1. by simplify_option_eq.
+    + case_match; simplify_option_eq;
+        rewrite lookup_insert_ne in H1 by done;
+        pose proof (IHm bs g0 Hxm1 Hxbs Heqo);
+        rewrite H0; by simplify_option_eq.
+Qed.
+
+Lemma matches_aux_impl_2 m bs brs x e :
+  m !! x = None →
+  bs !! x = None →
+  matches_aux m bs = Some (bs, brs) →
+  matches_aux m (<[x := e]>bs) = Some (<[x := e]>bs, brs).
+Proof.
+  intros Hxm Hxbs Hmatches.
+  revert bs brs Hxm Hxbs Hmatches.
+  induction m using map_ind; intros bs brs Hxm Hxbs Hmatches.
+  - rewrite matches_aux_empty.
+    rewrite matches_aux_empty in Hmatches.
+    by simplify_option_eq.
+  - rewrite matches_aux_insert in Hmatches by done.
+    rewrite matches_aux_insert by done.
+    apply lookup_insert_None in Hxm as [Hxm1 Hxm2].
+    unfold matches_aux_f in Hmatches. simplify_option_eq.
+    destruct H0. case_match.
+    + simplify_option_eq.
+      rewrite <-lookup_insert_ne with (i := x) (x := e) in Heqo0 by done.
+      pose proof (IHm bs g0 Hxm1 Hxbs Heqo).
+      rewrite H1. by simplify_option_eq.
+    + case_match; simplify_option_eq;
+        rewrite <-lookup_insert_ne with (i := x) (x := e) in H1 by done;
+        pose proof (IHm bs g0 Hxm1 Hxbs Heqo);
+        rewrite H0; by simplify_option_eq.
+Qed.
+
+Lemma matches_aux_dom m bs brs :
+  matches_aux m bs = Some (bs, brs) → dom m = dom brs.
+Proof.
+  revert bs brs.
+  induction m using map_ind; intros bs brs Hmatches.
+  - rewrite matches_aux_empty in Hmatches. by simplify_eq.
+  - rewrite matches_aux_insert in Hmatches by done.
+    unfold matches_aux_f in Hmatches. simplify_option_eq. destruct H0.
+    case_match; try case_match;
+      simplify_option_eq; apply IHm in Heqo; set_solver.
+Qed.
+
+Lemma matches_aux_inv m bs brs x e :
+  m !! x = None → bs !! x = None → brs !! x = None →
+  matches_aux (<[x := M_Mandatory]>m) (<[x := e]>bs) =
+    Some (<[x := e]>bs, <[x := B_Nonrec e]>brs) →
+  matches_aux m bs = Some (bs, brs).
+Proof.
+  intros Hxm Hxbs Hxbrs Hmatches.
+  rewrite matches_aux_insert in Hmatches by done.
+  unfold matches_aux_f in Hmatches. simplify_option_eq.
+  destruct H. simplify_option_eq.
+  rewrite lookup_insert in Heqo0. simplify_option_eq.
+  apply matches_aux_impl in Heqo; try done.
+  simplify_option_eq.
+  apply matches_aux_dom in Heqo as Hdom.
+  rewrite Heqo. do 2 f_equal.
+  assert (g0 !! x = None).
+    { apply not_elem_of_dom in Hxm.
+      rewrite Hdom in Hxm.
+      by apply not_elem_of_dom. }
+  replace g0 with (delete x (<[x:=B_Nonrec H]> g0));
+    try by rewrite delete_insert.
+  replace brs with (delete x (<[x:=B_Nonrec H]> brs));
+    try by rewrite delete_insert.
+  by rewrite H1.
+Qed.
+
+Lemma disjoint_union_subseteq_l `{FinSet A C} `{!LeibnizEquiv C} (X Y Z : C) :
+  X ## Y → X ## Z → X ∪ Y ⊆ X ∪ Z → Y ⊆ Z.
+Proof.
+  revert Y Z.
+  induction X using set_ind_L; intros Y Z Hdisj1 Hdisj2 Hsubs.
+  - by do 2 rewrite union_empty_l_L in Hsubs.
+  - do 2 rewrite <-union_assoc_L in Hsubs.
+    apply IHX; set_solver.
+Qed.
+
+Lemma singleton_notin_union_disjoint `{FinMapDom K M D} {A} (m : M A) (i : K) :
+  m !! i = None →
+  {[i]} ## dom m.
+Proof.
+  intros Hlookup. apply disjoint_singleton_l.
+  by apply not_elem_of_dom in Hlookup.
+Qed.
+
+Lemma matches_step bs brs m strict x :
+  matches (M_Matcher (<[x := M_Mandatory]>m) strict) bs = Some brs →
+  ∃ e, bs !! x = Some e ∧ brs !! x = Some (B_Nonrec e).
+Proof.
+  intros Hmatches.
+  destruct (decide (is_Some (bs !! x))).
+  - destruct i. exists x0. split; [done|].
+    unfold matches in Hmatches.
+    destruct strict; simplify_option_eq.
+    + replace (<[x := M_Mandatory]>m) with (<[x := M_Mandatory]>(delete x m))
+      in Heqo0; try by rewrite insert_delete_insert.
+      rewrite matches_aux_insert in Heqo0 by apply lookup_delete.
+      unfold matches_aux_f in Heqo0. simplify_option_eq.
+      destruct H3. simplify_option_eq.
+      apply matches_aux_bs in Heqo as Hdom. simplify_option_eq.
+      apply lookup_insert.
+    + replace (<[x := M_Mandatory]>m) with (<[x := M_Mandatory]>(delete x m))
+      in Heqo; try by rewrite insert_delete_insert.
+      rewrite matches_aux_insert in Heqo by apply lookup_delete.
+      unfold matches_aux_f in Heqo. simplify_option_eq.
+      destruct H1. simplify_option_eq.
+      apply matches_aux_bs in Heqo0 as Hdom. simplify_option_eq.
+      apply lookup_insert.
+  - unfold matches in Hmatches.
+    destruct strict; simplify_option_eq.
+    + replace (<[x := M_Mandatory]>m) with (<[x := M_Mandatory]>(delete x m))
+      in Heqo0; try by rewrite insert_delete_insert.
+      rewrite matches_aux_insert in Heqo0 by apply lookup_delete.
+      unfold matches_aux_f in Heqo0. simplify_option_eq.
+      destruct H2. simplify_option_eq.
+      apply matches_aux_bs in Heqo as Hdom. simplify_option_eq.
+      rewrite Heqo1 in n.
+      exfalso. by apply n.
+    + replace (<[x := M_Mandatory]>m) with (<[x := M_Mandatory]>(delete x m))
+      in Heqo; try by rewrite insert_delete_insert.
+      rewrite matches_aux_insert in Heqo by apply lookup_delete.
+      unfold matches_aux_f in Heqo. simplify_option_eq.
+      destruct H0. simplify_option_eq.
+      apply matches_aux_bs in Heqo0 as Hdom. simplify_option_eq.
+      rewrite Heqo1 in n.
+      exfalso. by apply n.
+Qed.
+
+Lemma matches_step' bs brs m strict x :
+  matches (M_Matcher (<[x := M_Mandatory]>m) strict) bs = Some brs →
+  ∃ e bs' brs',
+    bs' !! x = None ∧ bs = <[x := e]>bs' ∧
+    brs' !! x = None ∧ brs = <[x := B_Nonrec e]>brs'.
+Proof.
+  intros Hmatches.
+  apply matches_step in Hmatches as He.
+  destruct He as [e [He1 He2]].
+  exists e, (delete x bs), (delete x brs).
+  split_and!; by apply lookup_delete || rewrite insert_delete.
+Qed.
+
+Lemma matches_opt_step bs brs m strict x d :
+  matches (M_Matcher (<[x := M_Optional d]>m) strict) bs = Some brs →
+  (∃ e, bs !! x = Some e ∧ brs !! x = Some (B_Nonrec e)) ∨
+  bs !! x = None ∧ brs !! x = Some (B_Rec d).
+Proof.
+  intros Hmatches.
+  destruct (decide (is_Some (bs !! x))).
+  - destruct i. left. exists x0. split; [done|].
+    unfold matches in Hmatches.
+    destruct strict; simplify_option_eq.
+    + replace (<[x := M_Optional d]>m) with (<[x := M_Optional d]>(delete x m))
+      in Heqo0; try by rewrite insert_delete_insert.
+      rewrite matches_aux_insert in Heqo0 by apply lookup_delete.
+      unfold matches_aux_f in Heqo0. simplify_option_eq.
+      destruct H3. simplify_option_eq.
+      apply matches_aux_bs in Heqo as Hdom. simplify_option_eq.
+      apply lookup_insert.
+    + replace (<[x := M_Optional d]>m) with (<[x := M_Optional d]>(delete x m))
+      in Heqo; try by rewrite insert_delete_insert.
+      rewrite matches_aux_insert in Heqo by apply lookup_delete.
+      unfold matches_aux_f in Heqo. simplify_option_eq.
+      destruct H1. simplify_option_eq.
+      apply matches_aux_bs in Heqo0 as Hdom. simplify_option_eq.
+      apply lookup_insert.
+  - unfold matches in Hmatches.
+    destruct strict; simplify_option_eq.
+    + right. apply eq_None_not_Some in n. split; [done|].
+      destruct H0. simplify_option_eq.
+      apply matches_aux_bs in Heqo0 as Hbs. subst.
+      replace (<[x := M_Optional d]>m) with (<[x := M_Optional d]>(delete x m))
+      in Heqo0; try by rewrite insert_delete_insert.
+      rewrite matches_aux_insert in Heqo0 by apply lookup_delete.
+      unfold matches_aux_f in Heqo0. simplify_option_eq.
+      destruct H0. simplify_option_eq.
+      apply matches_aux_bs in Heqo as Hdom. simplify_option_eq.
+      apply lookup_insert.
+    + right. apply eq_None_not_Some in n. split; [done|].
+      destruct H. simplify_option_eq.
+      apply matches_aux_bs in Heqo as Hbs. subst.
+      replace (<[x := M_Optional d]>m) with (<[x := M_Optional d]>(delete x m))
+      in Heqo; try by rewrite insert_delete_insert.
+      rewrite matches_aux_insert in Heqo by apply lookup_delete.
+      unfold matches_aux_f in Heqo. simplify_option_eq.
+      destruct H. simplify_option_eq.
+      apply matches_aux_bs in Heqo0 as Hdom. simplify_option_eq.
+      apply lookup_insert.
+Qed.
+
+Lemma matches_opt_step' bs brs m strict x d :
+  matches (M_Matcher (<[x := M_Optional d]>m) strict) bs = Some brs →
+  (∃ e bs' brs',
+     bs' !! x = None ∧ bs = <[x := e]>bs' ∧
+     brs' !! x = None ∧ brs = <[x := B_Nonrec e]>brs') ∨
+  (∃ brs',
+     bs !! x = None ∧ brs' !! x = None ∧
+     brs = <[x := B_Rec d]>brs').
+Proof.
+  intros Hmatches.
+  apply matches_opt_step in Hmatches as He.
+  destruct He as [He|He].
+  - destruct He as [e [He1 He2]]. left.
+    exists e, (delete x bs), (delete x brs).
+    split; try split; try split.
+    + apply lookup_delete.
+    + by rewrite insert_delete.
+    + apply lookup_delete.
+    + by rewrite insert_delete.
+  - destruct He as [He1 He2]. right.
+    exists (delete x brs). split; try split; try done.
+    + apply lookup_delete.
+    + by rewrite insert_delete.
+Qed.
+
+Lemma matches_inv m bs brs strict x e :
+  m !! x = None → bs !! x = None → brs !! x = None →
+  matches (M_Matcher (<[x := M_Mandatory]>m) strict) (<[x := e]>bs) =
+    Some (<[x := B_Nonrec e]>brs) →
+  matches (M_Matcher m strict) bs = Some brs.
+Proof.
+  intros Hxm Hxbs Hxbrs Hmatch.
+  destruct strict.
+  - simplify_option_eq.
+    + destruct H0. apply matches_aux_bs in Heqo0 as Hbs.
+      simplify_option_eq. by erewrite matches_aux_inv.
+    + exfalso. apply H2.
+      repeat rewrite dom_insert in H1.
+      assert ({[x]} ## dom bs). { by apply singleton_notin_union_disjoint. }
+      assert ({[x]} ## dom m). { by apply singleton_notin_union_disjoint. }
+      by apply disjoint_union_subseteq_l with (X := {[x]}).
+  - simplify_option_eq.
+    destruct H. apply matches_aux_bs in Heqo as Hbs.
+    simplify_option_eq. by erewrite matches_aux_inv.
+Qed.
+
+Lemma matches_aux_avail_inv m bs brs x d e :
+  m !! x = None → bs !! x = None → brs !! x = None →
+  matches_aux (<[x := M_Optional d]>m) (<[x := e]>bs) =
+    Some (<[x := e]>bs, <[x := B_Nonrec e]>brs) →
+  matches_aux m bs = Some (bs, brs).
+Proof.
+  intros Hxm Hxbs Hxbrs Hmatches.
+  rewrite matches_aux_insert in Hmatches by done.
+  unfold matches_aux_f in Hmatches. simplify_option_eq.
+  destruct H. simplify_option_eq.
+  apply matches_aux_bs in Heqo as Hbs. subst.
+  rewrite lookup_insert in Hmatches. simplify_option_eq.
+  apply matches_aux_impl in Heqo; try done.
+  simplify_option_eq.
+  apply matches_aux_dom in Heqo as Hdom.
+  rewrite Heqo. do 2 f_equal.
+  assert (g0 !! x = None).
+    { apply not_elem_of_dom in Hxm.
+      rewrite Hdom in Hxm.
+      by apply not_elem_of_dom. }
+  replace g0 with (delete x (<[x:=B_Nonrec e]> g0));
+    try by rewrite delete_insert.
+  replace brs with (delete x (<[x:=B_Nonrec e]> brs));
+    try by rewrite delete_insert.
+  by rewrite Hmatches.
+Qed.
+
+Lemma matches_avail_inv m bs brs strict x d e :
+  m !! x = None → bs !! x = None → brs !! x = None →
+  matches (M_Matcher (<[x := M_Optional d]>m) strict) (<[x := e]>bs) =
+    Some (<[x := B_Nonrec e]>brs) →
+  matches (M_Matcher m strict) bs = Some brs.
+Proof.
+  intros Hxm Hxbs Hxbrs Hmatch.
+  destruct strict.
+  - simplify_option_eq.
+    + destruct H0. apply matches_aux_bs in Heqo0 as Hbs.
+      simplify_option_eq. by erewrite matches_aux_avail_inv.
+    + exfalso. apply H2.
+      repeat rewrite dom_insert in H1.
+      assert ({[x]} ## dom bs). { by apply singleton_notin_union_disjoint. }
+      assert ({[x]} ## dom m). { by apply singleton_notin_union_disjoint. }
+      by apply disjoint_union_subseteq_l with (X := {[x]}).
+  - simplify_option_eq.
+    destruct H. apply matches_aux_bs in Heqo as Hbs.
+    simplify_option_eq. by erewrite matches_aux_avail_inv.
+Qed.
+
+Lemma matches_aux_default_inv m bs brs x e :
+  m !! x = None → bs !! x = None → brs !! x = None →
+  matches_aux (<[x := M_Optional e]>m) bs =
+    Some (bs, <[x := B_Rec e]>brs) →
+  matches_aux m bs = Some (bs, brs).
+Proof.
+  intros Hxm Hxbs Hxbrs Hmatches.
+  rewrite matches_aux_insert in Hmatches by done.
+  unfold matches_aux_f in Hmatches. simplify_option_eq.
+  destruct H. simplify_option_eq.
+  apply matches_aux_bs in Heqo as Hbs. subst.
+  rewrite Hxbs in Hmatches. simplify_option_eq.
+  apply matches_aux_dom in Heqo as Hdom.
+  do 2 f_equal.
+  assert (g0 !! x = None).
+    { apply not_elem_of_dom in Hxm.
+      rewrite Hdom in Hxm.
+      by apply not_elem_of_dom. }
+  replace g0 with (delete x (<[x:=B_Rec e]> g0));
+    try by rewrite delete_insert.
+  replace brs with (delete x (<[x:=B_Rec e]> brs));
+    try by rewrite delete_insert.
+  by rewrite Hmatches.
+Qed.
+
+Lemma matches_default_inv m bs brs strict x e :
+  m !! x = None → bs !! x = None → brs !! x = None →
+  matches (M_Matcher (<[x := M_Optional e]>m) strict) bs =
+    Some (<[x := B_Rec e]>brs) →
+  matches (M_Matcher m strict) bs = Some brs.
+Proof.
+  intros Hxm Hxbs Hxbrs Hmatch.
+  destruct strict.
+  - simplify_option_eq.
+    + destruct H0. apply matches_aux_bs in Heqo0 as Hbs.
+      simplify_option_eq. by erewrite matches_aux_default_inv.
+    + exfalso. apply H2.
+      rewrite dom_insert in H1.
+      assert ({[x]} ## dom bs). { by apply singleton_notin_union_disjoint. }
+      assert ({[x]} ## dom m). { by apply singleton_notin_union_disjoint. }
+      apply disjoint_union_subseteq_l with (X := {[x]}); set_solver.
+  - simplify_option_eq.
+    destruct H. apply matches_aux_bs in Heqo as Hbs.
+    simplify_option_eq. by erewrite matches_aux_default_inv.
+Qed.
+
+Theorem matches_sound m bs brs : matches m bs = Some brs → bs ~ m ~> brs.
+Proof.
+  intros Hmatches.
+  destruct m.
+  revert strict bs brs Hmatches.
+  induction ms using map_ind; intros strict bs brs Hmatches.
+  - destruct strict; simplify_option_eq.
+    + apply dom_empty_subset in H0. simplify_eq.
+      constructor.
+    + constructor.
+  - destruct x.
+    + apply matches_step' in Hmatches as He.
+      destruct He as [e [bs' [brs' [Hbs'1 [Hbs'2 [Hbrs'1 Hbrs'2]]]]]].
+      subst. constructor; try done.
+      rewrite delete_notin by done.
+      apply IHms.
+      by apply matches_inv in Hmatches.
+    + apply matches_opt_step' in Hmatches as He. destruct He as [He|He].
+      * destruct He as [d [bs' [brs' [Hibs' [Hbs' [Hibrs' Hbrs']]]]]].
+        subst. constructor; try done.
+        rewrite delete_notin by done.
+        apply IHms.
+        by apply matches_avail_inv in Hmatches.
+      * destruct He as [brs' [Hibs [Hibrs' Hbrs']]].
+        subst. constructor; try done.
+        apply IHms.
+        by apply matches_default_inv in Hmatches.
+Qed.
+
+Theorem matches_complete m bs brs : bs ~ m ~> brs → matches m bs = Some brs.
+Proof.
+  intros Hbs.
+  induction Hbs.
+  - unfold matches. by simplify_option_eq.
+  - unfold matches. by simplify_option_eq.
+  - unfold matches in *. destruct strict.
+    + simplify_option_eq.
+      * simplify_option_eq. destruct H2. simplify_option_eq.
+        apply fmap_Some. exists (<[x := e]>bs, <[x := B_Nonrec e]>g0).
+        split; [|done].
+        rewrite matches_aux_insert by done.
+        apply matches_aux_bs in Heqo0 as Hbs'. simplify_option_eq.
+        apply matches_aux_impl_2 with (x := x) (e := e) in Heqo0;
+          [| done | apply lookup_delete].
+        replace bs with (delete x bs); try by apply delete_notin.
+        unfold matches_aux_f.
+        simplify_option_eq. apply bind_Some. exists e.
+        split; [apply lookup_insert | done].
+      * exfalso. apply H4.
+        replace bs with (delete x bs); try by apply delete_notin.
+        apply map_dom_delete_insert_subseteq_L.
+        set_solver.
+    + simplify_option_eq. destruct H1. simplify_option_eq.
+      apply fmap_Some. exists (<[x := e]>bs, <[x := B_Nonrec e]>g0).
+      split; [|done].
+      rewrite matches_aux_insert by done.
+      apply matches_aux_bs in Heqo as Hbs'. simplify_option_eq.
+      apply matches_aux_impl_2 with (x := x) (e := e) in Heqo;
+        [| done | apply lookup_delete].
+      replace bs with (delete x bs); try by apply delete_notin.
+      unfold matches_aux_f.
+      simplify_option_eq. apply bind_Some. exists e.
+      split; [apply lookup_insert | done].
+  - unfold matches in *. destruct strict.
+    + simplify_option_eq.
+      * simplify_option_eq. destruct H2. simplify_option_eq.
+        apply fmap_Some. exists (<[x := d]>bs, <[x := B_Nonrec d]>g0).
+        split; [|done].
+        rewrite matches_aux_insert by done.
+        apply matches_aux_bs in Heqo0 as Hbs'. simplify_option_eq.
+        apply matches_aux_impl_2 with (x := x) (e := d) in Heqo0;
+          [| done | apply lookup_delete].
+        replace bs with (delete x bs); try by apply delete_notin.
+        unfold matches_aux_f.
+        simplify_option_eq. case_match.
+        -- rewrite lookup_insert in H2. congruence.
+        -- by rewrite lookup_insert in H2.
+      * exfalso. apply H4.
+        replace bs with (delete x bs); try by apply delete_notin.
+        apply map_dom_delete_insert_subseteq_L.
+        set_solver.
+    + simplify_option_eq. destruct H1. simplify_option_eq.
+      apply fmap_Some. exists (<[x := d]>bs, <[x := B_Nonrec d]>g0).
+      split; [|done].
+      rewrite matches_aux_insert by done.
+      apply matches_aux_bs in Heqo as Hbs'. simplify_option_eq.
+      apply matches_aux_impl_2 with (x := x) (e := d) in Heqo;
+        [| done | apply lookup_delete].
+      replace bs with (delete x bs); try by apply delete_notin.
+      unfold matches_aux_f.
+      simplify_option_eq. case_match.
+      * rewrite lookup_insert in H1. congruence.
+      * by rewrite lookup_insert in H1.
+  - unfold matches in *. destruct strict.
+    + simplify_option_eq.
+      * simplify_option_eq. destruct H2. simplify_option_eq.
+        apply fmap_Some. exists (bs, <[x := B_Rec e]>g0).
+        split; [|done].
+        rewrite matches_aux_insert by done.
+        apply matches_aux_bs in Heqo0 as Hbs'. simplify_option_eq.
+        unfold matches_aux_f.
+        by simplify_option_eq.
+      * exfalso. apply H4. set_solver.
+    + simplify_option_eq. destruct H1. simplify_option_eq.
+      apply fmap_Some. exists (bs, <[x := B_Rec e]>g0).
+      split; [|done].
+      rewrite matches_aux_insert by done.
+      apply matches_aux_bs in Heqo as Hbs'. simplify_option_eq.
+      unfold matches_aux_f.
+      by simplify_option_eq.
+Qed.
+
+Theorem matches_correct m bs brs : matches m bs = Some brs ↔ bs ~ m ~> brs.
+Proof. split; [apply matches_sound | apply matches_complete]. Qed.
+
+Theorem matches_deterministic m bs brs1 brs2 :
+  bs ~ m ~> brs1 → bs ~ m ~> brs2 → brs1 = brs2.
+Proof. intros H1 H2. apply matches_correct in H1, H2. congruence. Qed.