1 files changed, 74 insertions, 75 deletions

diff --git a/kvx/abstractbb/Parallelizability.v b/kvx/abstractbb/Parallelizability.v
index feebeee5..e5d21434 100644
--- a/kvx/abstractbb/Parallelizability.v
+++ b/kvx/abstractbb/Parallelizability.v
@@ -26,7 +26,7 @@ Require Import Sorting.Permutation.
 Require Import Bool.
 Local Open Scope lazy_bool_scope.
 
-
+(** * Definition of the parallel semantics *)
 Module ParallelSemantics (L: SeqLanguage).
 
 Export L.
@@ -50,8 +50,8 @@ Fixpoint inst_prun (i: inst) (m tmp old: mem): option mem :=
 Lemma inst_run_prun i: forall m old,
   inst_run ge i m old = inst_prun i m m old.
 Proof.
-  induction i as [|[y e] i']; simpl; auto.
-  intros m old; destruct (exp_eval ge e m old); simpl; auto.
+  induction i as [|[y e] i']; cbn; auto.
+  intros m old; destruct (exp_eval ge e m old); cbn; auto.
 Qed.
 
 
@@ -76,8 +76,8 @@ Lemma inst_prun_equiv i old: forall m1 m2 tmp,
   (forall x, m1 x = m2 x) ->
   res_eq (inst_prun i m1 tmp old) (inst_prun i m2 tmp old).
 Proof.
-  induction i as [|[x e] i']; simpl; eauto.
-  intros m1 m2 tmp H; destruct (exp_eval ge e tmp old); simpl; auto.
+  induction i as [|[x e] i']; cbn; eauto.
+  intros m1 m2 tmp H; destruct (exp_eval ge e tmp old); cbn; auto.
   eapply IHi'; unfold assign. intros; destruct (R.eq_dec x x0); auto.
 Qed.
 
@@ -85,12 +85,12 @@ Lemma prun_iw_equiv p: forall m1 m2 old,
   (forall x, m1 x = m2 x) ->
   res_eq (prun_iw p m1 old) (prun_iw p m2 old).
 Proof.
-  induction p as [|i p']; simpl; eauto.
+  induction p as [|i p']; cbn; eauto.
   - intros m1 m2 old H.
     generalize (inst_prun_equiv i old m1 m2 old H);
-    destruct (inst_prun i m1 old old); simpl.
-    + intros (m3 & H3 & H4); rewrite H3; simpl; eauto.
-    + intros H1; rewrite H1; simpl; auto.
+    destruct (inst_prun i m1 old old); cbn.
+    + intros (m3 & H3 & H4); rewrite H3; cbn; eauto.
+    + intros H1; rewrite H1; cbn; auto.
 Qed.
 
 
@@ -101,8 +101,8 @@ Lemma prun_iw_app p1: forall m1 old p2,
      | None => None
      end.
 Proof.
-   induction p1; simpl; try congruence.
-   intros; destruct (inst_prun _ _ _); simpl; auto.
+   induction p1; cbn; try congruence.
+   intros; destruct (inst_prun _ _ _); cbn; auto.
 Qed.
 
 Lemma prun_iw_app_None p1: forall m1 old p2,
@@ -132,12 +132,12 @@ Fixpoint notIn {A} (x: A) (l:list A): Prop :=
 
 Lemma notIn_iff A (x:A) l: (~List.In x l) <-> notIn x l.
 Proof.
-  induction l; simpl; intuition.
+  induction l; cbn; intuition.
 Qed.
 
 Lemma notIn_app A (x:A) l1: forall l2, notIn x (l1++l2) <-> (notIn x l1 /\ notIn x l2).
 Proof.
-  induction l1; simpl.
+  induction l1; cbn.
   - intuition.
   - intros; rewrite IHl1. intuition.
 Qed.
@@ -145,7 +145,7 @@ Qed.
 
 Lemma In_Permutation A (l1 l2: list A): Permutation l1 l2 -> forall x, In x l1 -> In x l2.
 Proof.
-  induction 1; simpl; intuition.
+  induction 1; cbn; intuition.
 Qed.
 
 Lemma Permutation_incl A (l1 l2: list A): Permutation l1 l2 -> incl l1 l2.
@@ -174,7 +174,7 @@ Qed.
 
 Lemma disjoint_cons_l A (x:A) (l1 l2: list A): disjoint (x::l1) l2 <-> (notIn x l2) /\ (disjoint l1 l2).
 Proof.
-  unfold disjoint. simpl; intuition subst; auto. 
+  unfold disjoint. cbn; intuition subst; auto. 
 Qed.
 
 Lemma disjoint_cons_r A (x:A) (l1 l2: list A): disjoint l1 (x::l2) <-> (notIn x l1) /\ (disjoint l1 l2).
@@ -230,13 +230,13 @@ Fixpoint frame_assign m1 (f: list R.t) m2 :=
 Lemma frame_assign_def f: forall m1 m2 x,
    frame_assign m1 f m2 x = if notIn_dec x f then m1 x else m2 x.
 Proof.
-  induction f as [|y f] ; simpl; auto.
-  - intros; destruct (notIn_dec x []); simpl in *; tauto.
-  - intros; rewrite IHf; destruct (notIn_dec x (y::f)); simpl in *.
-    + destruct (notIn_dec x f); simpl in *; intuition.
+  induction f as [|y f] ; cbn; auto.
+  - intros; destruct (notIn_dec x []); cbn in *; tauto.
+  - intros; rewrite IHf; destruct (notIn_dec x (y::f)); cbn in *.
+    + destruct (notIn_dec x f); cbn in *; intuition.
       rewrite assign_diff; auto.
       rewrite <- notIn_iff in *; intuition.
-    + destruct (notIn_dec x f); simpl in *; intuition subst.
+    + destruct (notIn_dec x f); cbn in *; intuition subst.
       rewrite assign_eq; auto.
       rewrite <- notIn_iff in *; intuition.
 Qed.
@@ -266,7 +266,7 @@ Lemma frame_eq_list_split f1 (f2: R.t -> Prop) om1 om2:
  (forall m1 m2 x, om1 = Some m1 -> om2 = Some m2 -> f2 x -> notIn x f1 -> m1 x = m2 x) ->
  frame_eq f2 om1 om2.
 Proof.
-  unfold frame_eq; destruct om1 as [ m1 | ]; simpl; auto.
+  unfold frame_eq; destruct om1 as [ m1 | ]; cbn; auto.
   intros (m2 & H0 & H1); subst.
   intros H.
   eexists; intuition eauto.
@@ -280,7 +280,7 @@ Lemma frame_eq_res_eq f om1 om2:
  res_eq om1 om2.
 Proof.
   intros H H0; lapply (frame_eq_list_split f (fun _ => True) om1 om2 H); eauto.
-  clear H H0; unfold frame_eq, res_eq. destruct om1; simpl; firstorder.
+  clear H H0; unfold frame_eq, res_eq. destruct om1; cbn; firstorder.
 Qed.
 *)
 
@@ -296,9 +296,9 @@ Lemma inst_wframe_correct i m' old: forall m tmp,
   inst_prun ge i m tmp old = Some m' -> 
   forall x, notIn x (inst_wframe i) -> m' x  = m x.
 Proof.
-  induction i as [|[y e] i']; simpl.
+  induction i as [|[y e] i']; cbn.
   - intros m tmp H x H0; inversion_clear H; auto.
-  - intros m tmp H x (H1 & H2); destruct (exp_eval ge e tmp old); simpl; try congruence.
+  - intros m tmp H x (H1 & H2); destruct (exp_eval ge e tmp old); cbn; try congruence.
     cutrewrite (m x = assign m y v x); eauto.
     rewrite assign_diff; auto.
 Qed.
@@ -306,9 +306,9 @@ Qed.
 Lemma inst_prun_fequiv i old: forall m1 m2 tmp, 
   frame_eq (fun x => In x (inst_wframe i)) (inst_prun ge i m1 tmp old) (inst_prun ge i m2 tmp old).
 Proof.
-  induction i as [|[y e] i']; simpl.
+  induction i as [|[y e] i']; cbn.
   - intros m1 m2 tmp; eexists; intuition eauto.
-  - intros m1 m2 tmp. destruct (exp_eval ge e tmp old); simpl; auto.
+  - intros m1 m2 tmp. destruct (exp_eval ge e tmp old); cbn; auto.
     eapply frame_eq_list_split; eauto. clear IHi'.
     intros m1' m2' x H1 H2.
     lapply (inst_wframe_correct i' m1' old (assign m1 y v) (assign tmp y v)); eauto.
@@ -323,7 +323,7 @@ Lemma inst_prun_None i m1 m2 tmp old:
   inst_prun ge i m2 tmp old = None.
 Proof.
   intros H; generalize (inst_prun_fequiv i old m1 m2 tmp).
-  rewrite H; simpl; auto.
+  rewrite H; cbn; auto.
 Qed.
 
 Lemma inst_prun_Some i m1 m2 tmp old m1': 
@@ -331,7 +331,7 @@ Lemma inst_prun_Some i m1 m2 tmp old m1':
   res_eq (Some (frame_assign m2 (inst_wframe i) m1')) (inst_prun ge i m2 tmp old).
 Proof.
   intros H; generalize (inst_prun_fequiv i old m1 m2 tmp).
-  rewrite H; simpl.
+  rewrite H; cbn.
   intros (m2' & H1 & H2).
   eexists; intuition eauto.
   rewrite frame_assign_def.
@@ -351,7 +351,7 @@ Local Hint Resolve Permutation_app_head Permutation_app_tail Permutation_app_com
 Lemma bblock_wframe_Permutation p p': 
  Permutation p p' -> Permutation (bblock_wframe p)  (bblock_wframe p').
 Proof.
-  induction 1 as [|i p p'|i1 i2 p|p1 p2 p3]; simpl; auto.
+  induction 1 as [|i p p'|i1 i2 p|p1 p2 p3]; cbn; auto.
   - rewrite! app_assoc; auto.
   - eapply Permutation_trans; eauto.
 Qed.
@@ -361,11 +361,11 @@ Lemma bblock_wframe_correct p m' old: forall m,
   prun_iw p m old = Some m' -> 
   forall x, notIn x (bblock_wframe p) -> m' x = m x.
 Proof.
-  induction p as [|i p']; simpl.
+  induction p as [|i p']; cbn.
   - intros m H; inversion_clear H; auto.
   - intros m H x; rewrite notIn_app; intros (H1 & H2). 
     remember (inst_prun i m old old) as om.
-    destruct om as [m1|]; simpl.
+    destruct om as [m1|]; cbn.
     + eapply eq_trans.
       eapply IHp'; eauto.
       eapply inst_wframe_correct; eauto.
@@ -375,12 +375,12 @@ Qed.
 Lemma prun_iw_fequiv p old: forall m1 m2, 
   frame_eq (fun x => In x (bblock_wframe p)) (prun_iw p m1 old) (prun_iw p m2 old).
 Proof.
-  induction p as [|i p']; simpl.
+  induction p as [|i p']; cbn.
   - intros m1 m2; eexists; intuition eauto.
   - intros m1 m2; generalize (inst_prun_fequiv i old m1 m2 old).
     remember (inst_prun i m1 old old) as om.
-    destruct om as [m1'|]; simpl.
-    + intros (m2' & H1 & H2). rewrite H1; simpl.
+    destruct om as [m1'|]; cbn.
+    + intros (m2' & H1 & H2). rewrite H1; cbn.
     eapply frame_eq_list_split; eauto. clear IHp'.
     intros m1'' m2'' x H3 H4. rewrite in_app_iff.
     intros X X2. assert (X1: In x (inst_wframe i)). { destruct X; auto. rewrite <- notIn_iff in X2; tauto. }
@@ -389,7 +389,7 @@ Proof.
     lapply (bblock_wframe_correct p' m2'' old m2'); eauto.
     intros Xm2' Xm1'. 
     rewrite Xm1', Xm2'; auto.
-    + intro H; rewrite H; simpl; auto.
+    + intro H; rewrite H; cbn; auto.
 Qed.
 
 Lemma prun_iw_equiv p m1 m2 old: 
@@ -418,7 +418,7 @@ Fixpoint is_det (p: bblock): Prop :=
 Lemma is_det_Permutation p p': 
  Permutation p p' -> is_det p -> is_det p'.
 Proof.
-  induction 1; simpl; auto.
+  induction 1; cbn; auto.
   - intros; intuition. eapply disjoint_incl_r. 2: eauto.
     eapply Permutation_incl. eapply Permutation_sym. 
     eapply bblock_wframe_Permutation; auto.
@@ -431,20 +431,20 @@ Theorem is_det_correct p p':
   is_det p -> 
   forall m old, res_eq (prun_iw ge p m old) (prun_iw ge p' m old).
 Proof.
-  induction 1 as [ | i p p' | i1 i2 p | p1 p2 p3 ]; simpl; eauto.
+  induction 1 as [ | i p p' | i1 i2 p | p1 p2 p3 ]; cbn; eauto.
   - intros [H0 H1] m old.
     remember (inst_prun ge i m old old) as om0.
-    destruct om0 as [ m0 | ]; simpl; auto.
+    destruct om0 as [ m0 | ]; cbn; auto.
   - rewrite disjoint_app_r.
     intros ([Z1 Z2] & Z3 & Z4) m old.
     remember (inst_prun ge i2 m old old) as om2.
-    destruct om2 as [ m2 | ]; simpl; auto.
+    destruct om2 as [ m2 | ]; cbn; auto.
     + remember (inst_prun ge i1 m old old) as om1.
-      destruct om1 as [ m1 | ]; simpl; auto.
-      * lapply (inst_prun_Some i2 m m1 old old m2); simpl; auto.
-        lapply (inst_prun_Some i1 m m2 old old m1); simpl; auto.
+      destruct om1 as [ m1 | ]; cbn; auto.
+      * lapply (inst_prun_Some i2 m m1 old old m2); cbn; auto.
+        lapply (inst_prun_Some i1 m m2 old old m1); cbn; auto.
         intros (m1' & Hm1' & Xm1') (m2' & Hm2' & Xm2').
-        rewrite Hm1', Hm2'; simpl.
+        rewrite Hm1', Hm2'; cbn.
         eapply prun_iw_equiv.
         intros x; rewrite <- Xm1', <- Xm2'. clear Xm2' Xm1' Hm1' Hm2' m1' m2'.
         rewrite frame_assign_def.
@@ -455,9 +455,9 @@ Proof.
           erewrite (inst_wframe_correct i1 m1 old m old); eauto.
         }
         rewrite frame_assign_notIn; auto.
-     * erewrite inst_prun_None; eauto. simpl; auto.
+     * erewrite inst_prun_None; eauto. cbn; auto.
    + remember (inst_prun ge i1 m old old) as om1.
-     destruct om1 as [ m1 | ]; simpl; auto.
+     destruct om1 as [ m1 | ]; cbn; auto.
      erewrite inst_prun_None; eauto.
   - intros; eapply res_eq_trans.
     eapply IHPermutation1; eauto.
@@ -486,7 +486,7 @@ Lemma exp_frame_correct e old1 old2:
    (exp_eval ge e m1 old1)=(exp_eval ge e m2 old2).
 Proof.
   induction e using exp_mut with (P0:=fun l => (forall x, In x (list_exp_frame l) -> old1 x = old2 x) -> forall m1 m2, (forall x, In x (list_exp_frame l) -> m1 x = m2 x) ->
-   (list_exp_eval ge l m1 old1)=(list_exp_eval ge l m2 old2)); simpl; auto.
+   (list_exp_eval ge l m1 old1)=(list_exp_eval ge l m2 old2)); cbn; auto.
   - intros H1 m1 m2 H2; rewrite H2; auto.
   - intros H1 m1 m2 H2; erewrite IHe; eauto.
   - intros H1 m1 m2 H2; erewrite IHe, IHe0; eauto; 
@@ -501,7 +501,7 @@ Fixpoint inst_frame (i: inst): list R.t :=
 
 Lemma inst_wframe_frame i x: In x (inst_wframe i) -> In x (inst_frame i).
 Proof.
-  induction i as [ | [y e] i']; simpl; intuition.
+  induction i as [ | [y e] i']; cbn; intuition.
 Qed.
 
 
@@ -511,13 +511,13 @@ Lemma inst_frame_correct i wframe old1 old2: forall m tmp1 tmp2,
   (forall x, notIn x wframe -> tmp1 x = tmp2 x) ->
   inst_prun ge i m tmp1 old1 = inst_prun ge i m tmp2 old2.
 Proof.
-  induction i as [|[x e] i']; simpl; auto.
+  induction i as [|[x e] i']; cbn; auto.
   intros m tmp1 tmp2; rewrite disjoint_cons_l, disjoint_app_l.
   intros (H1 & H2 & H3) H6 H7.
   cutrewrite (exp_eval ge e tmp1 old1 = exp_eval ge e tmp2 old2).
   - destruct (exp_eval ge e tmp2 old2); auto.
     eapply IHi'; eauto. 
-    simpl; intros x0 H0; unfold assign. destruct (R.eq_dec x x0); simpl; auto. 
+    cbn; intros x0 H0; unfold assign. destruct (R.eq_dec x x0); cbn; auto. 
   - unfold disjoint in H2; apply exp_frame_correct.
     intros;apply H6; auto.
     intros;apply H7; auto.
@@ -535,8 +535,8 @@ Fixpoint pararec (p: bblock) (wframe: list R.t): Prop :=
 
 Lemma pararec_disjoint (p: bblock): forall wframe, pararec p wframe -> disjoint (bblock_wframe p) wframe.
 Proof.
-  induction p as [|i p']; simpl.
-  - unfold disjoint; simpl; intuition.
+  induction p as [|i p']; cbn.
+  - unfold disjoint; cbn; intuition.
   - intros wframe [H0 H1]; rewrite disjoint_app_l. 
     generalize (IHp' _ H1).
     rewrite disjoint_app_r. intuition. 
@@ -546,7 +546,7 @@ Qed.
 
 Lemma pararec_det p: forall wframe, pararec p wframe -> is_det p.
 Proof.
-  induction p as [|i p']; simpl; auto.
+  induction p as [|i p']; cbn; auto.
   intros wframe [H0 H1]. generalize (pararec_disjoint _ _ H1). rewrite disjoint_app_r.
   intuition. 
   - apply disjoint_sym; auto.
@@ -558,7 +558,7 @@ Lemma pararec_correct p old: forall wframe m,
   (forall x, notIn x wframe -> m x = old x) ->
   run ge p m = prun_iw ge p m old.
 Proof.
-  elim p; clear p; simpl; auto.
+  elim p; clear p; cbn; auto.
   intros i p' X wframe m [H H0] H1.
   erewrite inst_run_prun, inst_frame_correct; eauto.
   remember (inst_prun ge i m old old) as om0.
@@ -590,17 +590,17 @@ End PARALLELI.
 End ParallelizablityChecking.
 
 
-Module Type PseudoRegSet.
-
-Declare Module R: PseudoRegisters.
-
-(** We assume a datatype [t] refining (list R.t)
+(** * We assume a datatype [PseudoRegSet.t] refining [list R.t] *)
 
+(** 
 This data-refinement is given by an abstract "invariant" match_frame below, 
 preserved by the following operations.
-
 *)
 
+Module Type PseudoRegSet.
+
+Declare Module R: PseudoRegisters.
+
 Parameter t: Type.
 Parameter match_frame: t -> (list R.t) -> Prop.
 
@@ -646,7 +646,7 @@ Fixpoint inst_wsframe(i:inst): S.t :=
 
 Lemma inst_wsframe_correct i: S.match_frame (inst_wsframe i) (inst_wframe i).
 Proof.
-  induction i; simpl; auto.
+  induction i; cbn; auto.
 Qed.
 
 Fixpoint exp_sframe (e: exp): S.t :=
@@ -664,7 +664,7 @@ with list_exp_sframe (le: list_exp): S.t :=
 
 Lemma exp_sframe_correct e: S.match_frame (exp_sframe e) (exp_frame e).
 Proof.
-  induction e using exp_mut with (P0:=fun l => S.match_frame (list_exp_sframe l) (list_exp_frame l)); simpl; auto.
+  induction e using exp_mut with (P0:=fun l => S.match_frame (list_exp_sframe l) (list_exp_frame l)); cbn; auto.
 Qed.
 
 Fixpoint inst_sframe (i: inst): S.t :=
@@ -677,7 +677,7 @@ Local Hint Resolve exp_sframe_correct: core.
 
 Lemma inst_sframe_correct i: S.match_frame (inst_sframe i) (inst_frame i).
 Proof.
-  induction i as [|[y e] i']; simpl; auto.
+  induction i as [|[y e] i']; cbn; auto.
 Qed.
 
 Local Hint Resolve inst_wsframe_correct inst_sframe_correct: core.
@@ -692,7 +692,7 @@ Fixpoint is_pararec (p: bblock) (wsframe: S.t): bool :=
 
 Lemma is_pararec_correct (p: bblock): forall s l, S.match_frame s l -> (is_pararec p s)=true -> (pararec p l).
 Proof.
-  induction p; simpl; auto.
+  induction p; cbn; auto.
   intros s l H1 H2; rewrite lazy_andb_bool_true in H2. destruct H2 as [H2 H3].
   constructor 1; eauto.
 Qed.
@@ -716,6 +716,11 @@ End ParallelChecks.
 
 
 
+(** * Implementing the datatype [PosPseudoRegSet.t] refining [list R.t] *)
+
+(* This data-refinement is given by an abstract "invariant" match_frame below, 
+preserved by the following operations.
+*)
 
 Require Import PArith.
 Require Import MSets.MSetPositive.
@@ -724,12 +729,6 @@ Module PosPseudoRegSet <: PseudoRegSet with Module R:=Pos.
 
 Module R:=Pos.
 
-(** We assume a datatype [t] refining (list R.t)
-
-This data-refinement is given by an abstract "invariant" match_frame below, 
-preserved by the following operations.
-
-*)
 
 Definition t:=PositiveSet.t.
 
@@ -740,14 +739,14 @@ Definition empty:=PositiveSet.empty.
 
 Lemma empty_match_frame: match_frame empty nil.
 Proof.
-  unfold match_frame, empty, PositiveSet.In; simpl; intuition.
+  unfold match_frame, empty, PositiveSet.In; cbn; intuition.
 Qed.
 
 Definition add: R.t -> t -> t := PositiveSet.add.
 
 Lemma add_match_frame: forall s x l, match_frame s l -> match_frame (add x s) (x::l).
 Proof.
-  unfold match_frame, add; simpl. 
+  unfold match_frame, add; cbn. 
   intros s x l H y. rewrite PositiveSet.add_spec, H.
   intuition. 
 Qed.
@@ -773,13 +772,13 @@ Fixpoint is_disjoint (s s': PositiveSet.t) : bool :=
 
 Lemma is_disjoint_spec_true s: forall s', is_disjoint s s' = true -> forall x, PositiveSet.In x s -> PositiveSet.In x s' -> False.
 Proof.
-  unfold PositiveSet.In; induction s as [ |l IHl o r IHr]; simpl; try discriminate.
-  destruct s' as [|l' o' r']; simpl; try discriminate.
+  unfold PositiveSet.In; induction s as [ |l IHl o r IHr]; cbn; try discriminate.
+  destruct s' as [|l' o' r']; cbn; try discriminate.
   intros X.
   assert (H: ~(o = true /\ o'=true) /\ is_disjoint l l' = true /\ is_disjoint r r'=true).
-  { destruct o, o', (is_disjoint l l'), (is_disjoint r r'); simpl in X; intuition. }
+  { destruct o, o', (is_disjoint l l'), (is_disjoint r r'); cbn in X; intuition. }
   clear X; destruct H as (H & H1 & H2).
-  destruct x as [i|i|]; simpl; eauto.
+  destruct x as [i|i|]; cbn; eauto.
 Qed.
 
 Lemma is_disjoint_match_frame: forall s1 s2 l1 l2, match_frame s1 l1 -> match_frame s2 l2 -> (is_disjoint s1 s2)=true -> disjoint l1 l2.