proof restructuring due to helper lemmas being generalized

mit-plv · Mar 10, 2024 · ad70a26 · ad70a26
1 parent 0b44c8e
commit ad70a26
Show file tree

Hide file tree

Showing 3 changed files with 70 additions and 94 deletions.
diff --git a/compiler/src/compiler/DeadCodeElim.v b/compiler/src/compiler/DeadCodeElim.v
@@ -22,39 +22,6 @@ Section WithArguments1.
   Context {mem: map.map word (Init.Byte.byte : Type) } {mem_ok : map.ok mem } .
   Context {locals: map.map string word } {locals_ok : map.ok locals }.
   Context {ext_spec : Semantics.ExtSpec } {ext_spec_ok: Semantics.ext_spec.ok ext_spec } .
-
-  Lemma subset_of_list_find_removeb:
-    forall a x l,
-      subset
-        (of_list
-           (if find (eqb a) (List.removeb eqb x l)
-            then List.removeb eqb x l
-            else a :: List.removeb eqb x l))
-        (of_list (if find (eqb a) l then l else a :: l)).
-  Proof.
-    unfold subset, of_list, elem_of in *; simpl; intros.
-    destr (find (eqb a) (List.removeb eqb x l)).
-    - destr (find (eqb a) l ).
-      + eapply List.In_removeb_weaken. eassumption.
-      + eapply in_cons. eapply List.In_removeb_weaken.
-        eassumption.
-    - eapply in_inv in H.
-      destr H.
-      + rewrite H in *.
-        destr (find (eqb x0)).
-        * inversion E.
-        * destr (find (eqb x0) l).
-          -- pose proof E1 as E1'.
-             eapply find_eqb in E1.
-             rewrite <- E1 in E1'.
-             eapply find_some.
-             eapply E1'.
-          -- eapply in_eq.
-      + destr (find (eqb a) l ).
-        * eapply List.In_removeb_weaken. eassumption.
-        * eapply in_cons. eapply List.In_removeb_weaken.
-          eassumption.
-  Qed.
 
   Lemma agree_on_put_existsb_false:
     forall used_after x (l: locals) lL,
@@ -64,16 +31,12 @@ Section WithArguments1.
   Proof.
     intros. eapply agree_on_put_not_in; try eassumption.
     eapply agree_on_subset.
-    4: { eapply H. }
-    - eapply String.eqb_spec.
-    - eassumption.
+    2: { eapply H. }
     - unfold subset, diff, singleton_set, elem_of.
       intros.
       propositional idtac.
-      unfold of_list in *.
-      eapply existsb_eqb_in in H1.
-      rewrite H0 in H1.
-      discriminate.
+      eapply existsb_of_list in H1. rewrite H1 in H0.
+      discriminate. 
   Qed.
 
    Ltac subset_union_solve :=
@@ -105,25 +68,22 @@ Section WithArguments1.
     | H: map.agree_on ?s ?x ?y |-
         map.agree_on _ ?x ?y =>
         eapply agree_on_subset with (ks := s);
-        [ eapply String.eqb_spec | eassumption | subset_union_solve | eapply H ]
+        [ idtac | eapply H ]; subset_union_solve
     | H: map.agree_on ?s ?x ?y |-
         map.agree_on _ ?y ?x =>
-        eapply agree_on_comm;
-        [ eapply String.eqb_spec | eassumption | agree_on_solve ]
+        eapply agree_on_comm; agree_on_solve 
     | H: map.agree_on ?s ?mH ?mL,
         H1: map.putmany_of_list_zip ?lk ?lv ?mH = Some ?mH',
           H2: map.putmany_of_list_zip ?lk ?lv ?mL = Some ?mL'
       |- map.agree_on _ ?mH' ?mL' =>
         eapply agree_on_subset;
-        [ eapply String.eqb_spec | eassumption
-        | idtac
+        [ idtac
         | eapply agree_on_putmany_of_list_zip;
-          [ eapply String.eqb_spec | eassumption
-          | eapply H | eapply H1 | eapply H2 ]
+          [ eapply H | eapply H1 | eapply H2 ]
         ]
     | H: map.agree_on (diff (of_list ?x) (singleton_set ?y)) ?l ?lL |-
         map.agree_on (of_list ?x) (map.put ?l ?y ?v) (map.put ?lL ?y ?v)
-      => eapply agree_on_diff_put; [ eapply String.eqb_spec | eassumption | eapply H ]
+      => eapply agree_on_diff_put; eapply H
     | _ => idtac
     end.
 
@@ -165,8 +125,8 @@ Section WithArguments1.
     - intros.
       eapply @exec.interact; try solve [eassumption].
       + erewrite agree_on_getmany.
-        1-3: eauto using String.eqb_spec.
-        repeat listset_to_set. agree_on_solve.
+        * eapply H1.
+        * repeat listset_to_set. agree_on_solve.
       + intros.
         eapply H3 in H5.
         fwd.
@@ -190,11 +150,10 @@ Section WithArguments1.
         2: { eapply H0. }
         fwd. eassumption.
       + erewrite agree_on_getmany.
-        1-3: eauto using String.eqb_spec.
-        listset_to_set. agree_on_solve.
+        * eapply H1.
+        * listset_to_set. agree_on_solve. 
       + eapply IHexec.
         eapply agree_on_refl.
-        assumption.
       + intros.
         unfold compile_post in *.
         fwd. eapply H4 in H6p1. fwd.
@@ -203,20 +162,18 @@ Section WithArguments1.
         eapply map.putmany_of_list_zip_sameLength,  map.sameLength_putmany_of_list in H6p1p1. fwd.
         exists retvs. eexists. repeat split.
         * erewrite agree_on_getmany.
-          1-3: eauto using String.eqb_spec.
-          listset_to_set. agree_on_solve.
-        * eassumption.
-        * exists l'. eexists.
-          split; [ | eassumption ].
+          -- eapply H6p1p0.
+          -- listset_to_set. agree_on_solve.
+        * eapply H6p1p1.
+        * do 2 eexists. split; [ | eassumption ].
           agree_on_solve.
           repeat listset_to_set.
           subset_union_solve.
     - intros.
-      eapply agree_on_find in H3; fwd; [ | eassumption ].
+      eapply agree_on_find in H3; fwd. 
       destr (existsb (eqb x) used_after); fwd.
       + eapply @exec.load.
-        * erewrite <- H3p0; [ eassumption | ].
-          unfold elem_of, of_list. eauto using in_eq.
+        * rewrite <- H3p1. eassumption. 
         * eauto.
         * unfold compile_post.
           exists (map.put l x v); eexists; split; [ | eassumption ].
@@ -227,8 +184,6 @@ Section WithArguments1.
           exists (map.put l x v); eexists; split; [ | eassumption ].
           repeat listset_to_set.
           agree_on_solve.
-
-
     - intros. repeat listset_to_set.
       eapply agree_on_union in H4; fwd.
       all: try solve [ eauto using String.eqb_spec ].
@@ -240,12 +195,11 @@ Section WithArguments1.
       + eassumption.
       + unfold compile_post. exists l; eexists; split; eassumption.
     - intros.
-      eapply agree_on_find in H4; fwd; [ | eassumption ].
+      eapply agree_on_find in H4; fwd.
       destr (existsb (eqb x) used_after); fwd.
       + eapply @exec.inlinetable; eauto.
-        * rewrite <- H4p0; eauto.
-          unfold elem_of, of_list. eapply in_eq.
-        * unfold compile_post; do 2 eexists; split; [ | eassumption ].
+        * rewrite <- H4p1. eassumption. 
+        * unfold compile_post; do 2 eexists; split ; [ | eassumption ].
           repeat listset_to_set; agree_on_solve.
       + eapply @exec.skip; eauto.
         unfold compile_post.
@@ -299,26 +253,24 @@ Section WithArguments1.
           do 2 eexists; split; [ | eassumption ].
           agree_on_solve.
       + intros.
-        eapply agree_on_find in H3; fwd; [ | eassumption ].
+        eapply agree_on_find in H3; fwd. 
         destr (existsb (eqb x) used_after).
         * eapply @exec.op.
-          -- rewrite <- H3p0; [ eassumption | ].
-             unfold elem_of; eapply in_eq.
+          -- rewrite <- H3p1. eassumption. 
           -- simpl. constructor.
           -- unfold compile_post. simpl in *. inversion H1. fwd.  do 2 eexists; split; [ | eassumption ].
              repeat listset_to_set.
              agree_on_solve.
         * eapply @exec.skip. unfold compile_post.
-          do 2 eexists; split; [ | eassumption ].
+          do 2 eexists; split ; [ | eassumption ].
           repeat listset_to_set.
           agree_on_solve.
     - intros.
-      eapply agree_on_find in H2; fwd; [ | eassumption ].
+      eapply agree_on_find in H2; fwd.
       repeat listset_to_set.
       destr (existsb (eqb x) used_after).
       { eapply @exec.set.
-        - rewrite  <- H2p0; [ eassumption | ].
-          unfold elem_of; eapply in_eq.
+        - rewrite <- H2p1; eassumption. 
         - unfold compile_post. do 2 eexists; split; [ | eassumption ].
           agree_on_solve.
       }
@@ -329,22 +281,18 @@ Section WithArguments1.
     - intros.
       repeat listset_to_set.
       eapply agree_on_union in H2; fwd.
-      2-3: eauto using String.eqb_spec.
       eapply agree_on_union in H2p0; fwd.
-      2-3: eauto using String.eqb_spec.
       eapply @exec.if_true.
       + erewrite agree_on_eval_bcond; [ eassumption | ].
-        eauto using agree_on_comm, String.eqb_spec.
+        eauto using agree_on_comm. 
       + eauto.
-    -  intros.
+    - intros.
       repeat listset_to_set.
       eapply agree_on_union in H2; fwd.
-      2-3: eauto using String.eqb_spec.
       eapply agree_on_union in H2p0; fwd.
-      2-3: eauto using String.eqb_spec.
       eapply @exec.if_false.
       + erewrite agree_on_eval_bcond; [ eassumption | ].
-        eauto using agree_on_comm, String.eqb_spec.
+        eauto using agree_on_comm. 
       + eauto.
     - intros.
       cbn - [live].
@@ -355,8 +303,6 @@ Section WithArguments1.
       eapply @exec.loop with (mid2 := compile_post (live (SLoop body1 cond body2) used_after) mid2).
       { eapply IH1.
         eapply agree_on_subset.
-        - eapply String.eqb_spec.
-        - eassumption.
         - let Heq := fresh in
           specialize (live_while body1 cond body2 used_after) as Heq; cbn zeta in Heq.
           eapply H4.
@@ -368,12 +314,10 @@ Section WithArguments1.
         eapply H1 in H6.
         erewrite agree_on_eval_bcond; [ eassumption | ].
         eapply agree_on_comm.
-        1-2: eauto using String.eqb_spec.
         repeat listset_to_set.
         eapply agree_on_union in H4.
-        2-3: eauto using String.eqb_spec.
         fwd.
-        eapply agree_on_subset; [ eapply String.eqb_spec | eassumption | | eapply H4p1 ].
+        eapply agree_on_subset; [ | eapply H4p1 ].
         subset_union_solve.
       }
       { intros.
@@ -384,12 +328,12 @@ Section WithArguments1.
           eexists.
           split.
           + repeat listset_to_set.
-            eapply agree_on_subset; [ eapply String.eqb_spec | eassumption | | eapply H4 ].
+            eapply agree_on_subset; [ | eapply H4 ].
             subset_union_solve.
           + eapply H8.
         - erewrite agree_on_eval_bcond; [ eassumption | ].
           repeat listset_to_set.
-          eapply agree_on_subset; [ eapply String.eqb_spec | eassumption | | eapply H4 ].
+          eapply agree_on_subset; [ | eapply H4 ].
           subset_union_solve.
       }
       {
@@ -400,10 +344,10 @@ Section WithArguments1.
         - eapply H8.
         - erewrite agree_on_eval_bcond; [ eassumption | ].
           repeat listset_to_set.
-          eapply agree_on_subset; [ eapply String.eqb_spec | eassumption | | eapply H4 ].
+          eapply agree_on_subset; [ | eapply H4 ].
           subset_union_solve.
         - repeat listset_to_set.
-          eapply agree_on_subset; [ eapply String.eqb_spec | eassumption | | eapply H4 ].
+          eapply agree_on_subset; [ | eapply H4 ].
           subset_union_solve.
       }
       {
@@ -413,7 +357,6 @@ Section WithArguments1.
         eapply IH12.
         - eapply H6.
         - eapply H4.
-
       }
     - intros.
       eapply @exec.seq.

diff --git a/compiler/src/compiler/DeadCodeElimDef.v b/compiler/src/compiler/DeadCodeElimDef.v
@@ -14,7 +14,6 @@ Require Import coqutil.Tactics.fwd.
 (*  below only for of_list_list_diff *)
 Require Import Coq.Logic.PropExtensionality.
 Require Import Coq.Logic.FunctionalExtensionality.
-Require Export compiler.DeadCodeElimHelper.
 
 Section WithArguments1.
   Context {width: Z}.
@@ -210,6 +209,40 @@ Section WithArguments1.
     eapply H.
   Qed.
 
+
+  Lemma subset_of_list_find_removeb:
+    forall a x l,
+      subset
+        (of_list
+           (if find (eqb a) (List.removeb eqb x l)
+            then List.removeb eqb x l
+            else a :: List.removeb eqb x l))
+        (of_list (if find (eqb a) l then l else a :: l)).
+  Proof.
+    unfold subset, of_list, elem_of in *; simpl; intros.
+    destr (find (eqb a) (List.removeb eqb x l)).
+    - destr (find (eqb a) l ).
+      + eapply List.In_removeb_weaken. eassumption.
+      + eapply in_cons. eapply List.In_removeb_weaken.
+        eassumption.
+    - eapply in_inv in H.
+      destr H.
+      + rewrite H in *.
+        destr (find (eqb x0)).
+        * inversion E.
+        * destr (find (eqb x0) l).
+          -- pose proof E1 as E1'.
+             eapply List.find_eqb in E1.
+             rewrite <- E1 in E1'.
+             eapply find_some.
+             eapply E1'.
+          -- eapply in_eq.
+      + destr (find (eqb a) l ).
+        * eapply List.In_removeb_weaken. eassumption.
+        * eapply in_cons. eapply List.In_removeb_weaken.
+          eassumption.
+  Qed.
+
   Fixpoint live(s: stmt var)(l: list var): list var :=
     match s with
     | SInteract resvars _ argvars  =>

diff --git a/compiler/src/compiler/Pipeline.v b/compiler/src/compiler/Pipeline.v
@@ -341,11 +341,11 @@ Section WithWordAndMem.
       intros.
       eapply @exec.weaken.
       - eapply dce_correct_aux; eauto.
-        eapply agree_on_refl. eauto.
+        eapply MapEauto.agree_on_refl. 
       - unfold compile_post. intros. fwd.
         exists retvals.
         split.
-        + erewrite agree_on_getmany; [ eassumption | eapply String.eqb_spec | eauto | eapply agree_on_comm; [ eapply String.eqb_spec | eauto | eassumption ] ].
+        + erewrite MapEauto.agree_on_getmany; [ eauto | eapply MapEauto.agree_on_comm; [ eassumption ] ].
         + eassumption.
        Unshelve. eauto.
     Qed.