clean up admits in mask core

theories/mask_core/calculus.v

@@ -94,6 +94,17 @@ Definition recognize (σ : signature) (r : range) : option (fin σ.(sig_length))
   | f :: _ => Some f
   end.
 
+Lemma recognize_spec σ r f :
+  recognize σ r = Some f → sig_ranges σ !!! f = r.
+Proof.
+  rewrite /recognize. move => Hr.
+  case_match => //.
+  have ? : t = f by naive_solver. subst.
+  have : f ∈ filter (λ f, sig_ranges σ !!! f = r) (enum (fin (sig_length σ))).
+  { rewrite Heql. apply elem_of_cons. by left. }
+  rewrite elem_of_list_filter. naive_solver.
+Qed.
+
 Lemma sig_disjoint σ f1 f2 :
   f1 ≠ f2 →
   (sig_ranges σ !!! f1 ≺ sig_ranges σ !!! f2) ∨
@@ -253,6 +264,17 @@ Inductive has_ty : tm → ty → Prop :=
 
 Reserved Notation "t →ᵣ t'" (at level 40).
 
+Lemma subsume_mv_bv t σ :
+  ⊢ t : mv σ →
+  ⊢ t : bv σ.
+Proof.
+  induction t; inversion 1; subst.
+  - constructor.
+  - econstructor; eauto. econstructor; eauto.
+    unfold field_width. erewrite recognize_spec; eauto.
+  - econstructor; eauto.
+Qed.
+
 (* Representing rewriting instances as a relation over the raw terms. *)
 Inductive step : relation tm :=
   (* val, proj, nil : no reduction *)

theories/mask_core/safety.v

 From stdpp Require Import prelude finite.
 From Coq Require Import ssreflect.
-From refinedc.mask_core Require Import calculus wn total_merge.
+From refinedc.mask_core Require Import calculus wn total_merge sorted.
 
 Local Open Scope bf_scope.
 Local Open Scope Z_scope.
 
 (* helper lemmas for automation *)
 
-Lemma recognize_spec σ r f :
-  recognize σ r = Some f → sig_ranges σ !!! f = r.
-Proof.
-  rewrite /recognize. move => Hr.
-  case_match => //.
-  have ? : t = f by naive_solver. subst.
-  have : f ∈ filter (λ f, sig_ranges σ !!! f = r) (enum (fin (sig_length σ))).
-  { rewrite Heql. apply elem_of_cons. by left. }
-  rewrite elem_of_list_filter. naive_solver.
-Qed.
-
-Lemma sig_range_disjoint {σ r1 r2 f1 f2} :
-  recognize σ r1 = Some f1 →
-  recognize σ r2 = Some f2 →
-  r1 ≠ r2 → r1 ≺ r2 ∨ r2 ≺ r1.
-Proof.
-  move => /recognize_spec <- /recognize_spec <- Hne.
-  apply sig_disjoint. naive_solver.
-Qed.
-
 Lemma sig_range_comparable {σ r1 r2 f1 f2} :
   recognize σ r1 = Some f1 →
   recognize σ r2 = Some f2 →
@@ -178,19 +158,19 @@ Proof.
   | [ H1 : ?r1 ≺ ?r2, H2 : ?r2 ≺ ?r1 |- _ ] =>
     unfold range_lt in H1, H2; lia
   end.
-  * auto_inv. eapply val_ranges_empty; eauto.
-  * by rewrite /merge total_merge_cons_r.
-Qed.
-
-Lemma subsume_mv_bv t σ :
-  ⊢ t : mv σ →
-  ⊢ t : bv σ.
-Proof.
-  induction t; inversion 1; subst.
-  - constructor.
-  - auto_inv. econstructor; eauto.
-    constructor. unfold field_width. erewrite recognize_spec; eauto.
-  - econstructor; eauto.
+  + auto_inv. eapply val_ranges_empty; eauto.
+  + auto_inv. unfold merge.
+    erewrite total_merge_cons_r_singleton => //.
+    * unfold range_lt. move => x Hx. simpl in Hx. lia.
+    * unfold range_lt. move => x Hx. lia.
+    * apply range_lt_trans.
+    * move => r1 r2 Hr1 Hr2 Hne.
+      eapply ranges_signature in Hr1 as [? ?]; eauto.
+      apply elem_of_cons in Hr2 as [?|Hr2].
+      1: subst.
+      2: eapply ranges_signature in Hr2 as [? ?]; eauto; last apply subsume_mv_bv; eauto.
+      all: eapply sig_range_disjoint; eauto.
+    * by apply range_lt_head_HdRel.
 Qed.
 
 Lemma disjoint_cons_l {A} x (l l' : list A) :

theories/mask_core/sorted.v

 From stdpp Require Import prelude sorting.
 From Coq Require Import ssreflect.
-From refinedc.mask_core Require Import calculus safety total_merge.
+From refinedc.mask_core Require Import calculus total_merge.
 
 Local Open Scope bf_scope.
 Local Open Scope Z_scope.
@@ -19,6 +19,17 @@ Proof.
   by rewrite elem_of_total_merge.
 Qed.
 
+(* sig ranges *)
+
+Lemma sig_range_disjoint {σ r1 r2 f1 f2} :
+  recognize σ r1 = Some f1 →
+  recognize σ r2 = Some f2 →
+  r1 ≠ r2 → r1 ≺ r2 ∨ r2 ≺ r1.
+Proof.
+  move => /recognize_spec <- /recognize_spec <- Hne.
+  apply sig_disjoint. naive_solver.
+Qed.
+
 (* sorted *)
 
 Lemma ranges_signature t σ r :
@@ -43,7 +54,7 @@ Theorem ranges_sorted t τ :
 Proof.
   induction t => Hty //.
   all: try by simpl.
-  all: invert Hty.
+  all: inversion Hty; subst; clear Hty.
   1,2: simpl; constructor; eauto; by apply range_lt_head_HdRel.
   all: try by (simpl; eapply IHt2; apply subsume_mv_bv; naive_solver).
   all: apply total_merge_sorted; eauto.

theories/mask_core/total_merge.v

@@ -79,10 +79,6 @@ Section total_merge.
       else x2 :: total_merge (x1 :: l1) l2.
   Proof. done. Qed.
 
-  Lemma total_merge_cons_r x l l' :
-    total_merge l (x :: l') = total_merge [x] (total_merge l l').
-  Admitted.
-
   Lemma HdRel_total_merge x l1 l2 :
     HdRel R x l1 → HdRel R x l2 → HdRel R x (total_merge l1 l2).
   Proof.
@@ -145,4 +141,68 @@ Section total_merge.
     - rewrite !elem_of_cons IH2 elem_of_cons. naive_solver.
   Qed.
 
+  (* total merge result lemmas *)
+
+  Lemma total_merge_cons_l_HdRel `{!Irreflexive R} x l1 l2 :
+    HdRel R x l2 →
+    total_merge (x :: l1) l2 = x :: total_merge l1 l2.
+  Proof.
+    inversion 1; subst.
+    - by rewrite !total_merge_nil_r.
+    - rewrite total_merge_cons.
+      repeat case_bool_decide => //.
+      subst. have ? : ¬ R b b by apply irreflexive_eq. contradiction.
+  Qed.
+
+  Lemma total_merge_cons_r_HdRel `{!Irreflexive R} `{!Asymmetric R} x l1 l2 :
+    HdRel R x l1 →
+    total_merge l1 (x :: l2) = x :: total_merge l1 l2.
+  Proof.
+    inversion 1; subst.
+    - by rewrite !total_merge_nil_l.
+    - rewrite total_merge_cons.
+      repeat case_bool_decide => //.
+      * subst. exfalso. naive_solver.
+      * exfalso. naive_solver.
+  Qed.
+
+  Lemma HdRel_trans `{!Transitive R} x y l :
+    R x y → HdRel R y l → HdRel R x l.
+  Proof.
+    intros HR. induction 1 => //.
+    apply HdRel_cons. etrans; eauto.
+  Qed.
+
+  Lemma total_merge_cons_r_singleton `{!Irreflexive R} `{!Asymmetric R} `{!Transitive R} x l1 l2 :
+    (∀ a b, a ∈ l1 → b ∈ x :: l2 → a ≠ b → R a b ∨ R b a) →
+    HdRel R x l2 →
+    total_merge l1 (x :: l2) = total_merge [x] (total_merge l1 l2).
+  Proof.
+    (* induction on l2 but remember l2 = ? *)
+    remember l1 as l; generalize dependent l;
+      induction l1 as [|x1 l1' IH1] => l1 Heq1 HR Hx.
+    all: rewrite Heq1; rewrite Heq1 in HR.
+    - rewrite !total_merge_nil_l.
+      erewrite total_merge_cons_l_HdRel => //.
+      by rewrite total_merge_nil_l.
+    - rewrite total_merge_cons. repeat case_bool_decide.
+      + subst.
+        have -> : total_merge (x :: l1') l2 = x :: total_merge l1' l2.
+        { erewrite total_merge_cons_l_HdRel => //. }
+        rewrite total_merge_cons. repeat case_bool_decide => //.
+        by rewrite total_merge_nil_l.
+      + have -> : total_merge (x1 :: l1') l2 = x1 :: total_merge l1' l2.
+        { erewrite total_merge_cons_l_HdRel => //. eapply HdRel_trans; eauto. }
+        symmetry. erewrite total_merge_cons_r_HdRel. 2: by apply HdRel_cons.
+        symmetry. rewrite IH1 // => e1 e2 ? ? ?.
+        apply HR => //. apply elem_of_cons. by right.
+      + have ? : R x x1.
+        { have ? : R x1 x ∨ R x x1.
+          { apply HR => //. all: apply elem_of_cons; by left. }
+          naive_solver. }
+        symmetry. erewrite total_merge_cons_l_HdRel.
+        2: { apply HdRel_total_merge => //. by apply HdRel_cons. }
+        by rewrite total_merge_nil_l.
+  Qed.
+
 End total_merge.