Merge pull request #4 from snu-sf/coq8.6

Migrate to Coq 8.6
snu-sf · Feb 15, 2017 · 9936c5a · 9936c5a
2 parents c6c0e68 + 99bd7e1
commit 9936c5a
Show file tree

Hide file tree

Showing 9 changed files with 26 additions and 27 deletions.
diff --git a/lib/hahn b/lib/hahn
diff --git a/src/axiomatic/GsimM.v b/src/axiomatic/GsimM.v
@@ -1054,7 +1054,7 @@ red; splits; try done.
        red; splits; eauto.
        eby eapply no_rmw_from_init.
        eby eapply rmw_acta.
-    + unfold singl_rel, sb_ext, eqv_rel, seq in *; desf; eauto; subst z0 z b a; left.
+    + unfold singl_rel, sb_ext, eqv_rel, seq in *; desf; eauto; left.
        eapply SB_AT_END; eauto.
        by left; congr.
        eby destruct SB3; subst.

diff --git a/src/axiomatic/Gstep.v b/src/axiomatic/Gstep.v
@@ -393,17 +393,14 @@ Section GstepLemmas.
     cdes WF'; cdes WF_SB0.
     specialize (SB_TID0 x y H).
     desf; try by exploit SB_INIT; eauto.
-    exploit sb_actb; eauto.
-    exploit sb_acta; eauto.
-    ins; desf; try subst x; try subst y.
-    by exfalso; auto.
-    by exfalso; auto.
+    forward eapply SB_ACTa0; eauto.
+    ins; desf; try subst x.
+    by exfalso; eapply SB_IRR0; eapply SB_T0; eauto.
+    assert (sb x y \/ sb y x).
+      eapply SB_TOT; eauto.
+      by intro; subst x; eauto.
+    desf; auto.
     by exfalso; eapply SB_IRR0; eapply SB_T0; eauto.
-    exploit SB_TOT; eauto.
-    ins; desf; eauto.
-    intro; subst x; eauto.
-    intro; desf; eauto.
-    exfalso; eauto.
   Qed.
 
   Lemma gstep_rmw_a : gstep_a rmw rmw'.
@@ -525,7 +522,8 @@ Proof.
   desf; ins.
   cdes WF_RF; cdes WF_MO; cdes INC.
   exploit (RF_TOT a). by left; eauto. eauto with acts.
-  intros; desc. exploit rf_lv; try edone; intro; desc.
+  intros; desc. 
+  forward eapply rf_lv with (rf:=rf'); try edone; intro; desc.
   eexists; splits; eauto.
   apply RF_ACTa in x0; destruct x0; eauto.
   exfalso; subst; destruct (lab a0); ins.
@@ -631,9 +629,10 @@ Proof.
   exists y; splits; eauto.
   desf.
   - left; splits. congruence. 
-  - right; splits; try done. eapply init_events_wf2; eauto.
-    intro. eapply init_proper_thread; eauto.
+  - right; splits; try done.
   - right; splits; eauto.
+    eapply init_events_wf2; eauto.
+    intro. eapply init_proper_thread; eauto.
   - exfalso. eapply init_not_proper with (a:=z0); eauto.
 Qed.
 

diff --git a/src/axiomatic/GstepWrite.v b/src/axiomatic/GstepWrite.v
@@ -399,10 +399,10 @@ Proof.
   rewrite gstep_urr_write; try edone; relsimp.
   rewrite gstep_sb_ext_helper_w2; ins.
   split; repeat apply inclusion_union_l; eauto 12 with rel.
-    red; unfold seq, eqv_rel; ins; desf; try (by destruct a as [??[]]);
+  red; unfold seq, eqv_rel; ins; desf; try (by destruct y as [??[]]);
     by right; eauto.
-  rewrite <- inclusion_union_r2, !eqv_join; unfold eqv_rel; red; ins; desf. 
-  subst y; splits; ins; tauto.
+  rewrite <- inclusion_union_r2, !eqv_join; unfold eqv_rel; red; 
+  ins; desf; splits; auto.
 Qed.
 
 Lemma gstep_c_rel_rwr_write l l' :
@@ -416,10 +416,10 @@ Proof.
   rewrite gstep_rwr_write; try edone; relsimp.
   rewrite gstep_sb_ext_helper_w2; ins.
   split; repeat apply inclusion_union_l; eauto 12 with rel.
-    red; unfold seq, eqv_rel; ins; desf; try (by destruct a as [??[]]);
+    red; unfold seq, eqv_rel; ins; desf; try (by destruct y as [??[]]);
     by right; eauto.
   rewrite <- inclusion_union_r2, !eqv_join; unfold eqv_rel; red; ins; desf. 
-  subst y; splits; ins; tauto.
+  splits; auto.
 Qed.
 
 Lemma gstep_t_rel_urr_write l' l x :

diff --git a/src/axiomatic/MsimG.v b/src/axiomatic/MsimG.v
@@ -341,7 +341,7 @@ Proof.
   intros K K'; cdes GSTEP; desf; ins; desf.
   by cdes WF'; exfalso; eapply WF_MO; eauto.
   assert (P: is_proper y).
-    by eapply no_mo_to_init; eauto.
+    by eapply no_mo_to_init with (mo:=mo0); eauto.
   destruct (classic (exists x : event, (rf;; rmw) x y)) as [C|]; desc; eauto.
   assert (INx: In x acts).
     by eapply seq_doma in C; [|eapply rf_acta]; eauto. 

diff --git a/src/drf/PIStep.v b/src/drf/PIStep.v
@@ -685,7 +685,7 @@ Proof.
   { inv WF. auto. }
   { ii. destruct (ThreadEvent.is_promising e0) eqn:E0; [by destruct e0|].
     ii; hexploit pi_wf_small_step_is_reading; try exact WF2; eauto.
-    i. hexploit pi_wf_small_step_is_promising; eauto.
+    i. hexploit pi_wf_small_step_is_promising; try exact STEPT; eauto.
   }
   { apply rtcn_rtc in A23. inv A12.
     exploit pi_step_except_small_step; eauto. i. destruct cST3. ss.
@@ -698,7 +698,7 @@ Proof.
   }
   i. destruct cST3. subst. des.
   { destruct (ThreadEvent.is_promising e0) eqn:E0; subst.
-    - exploit IH; try exact A23; eauto.
+    - exploit IH; try exact A23; try exact WF; eauto.
       { econs; econs; eauto; ii; by des; destruct e2', e0. }
       i. des. esplits; try exact STEPS; eauto.
     - assert (EQ: e2' = e0). 
@@ -749,7 +749,7 @@ Proof.
   }
 
   exploit IH; try exact STEP2'; eauto.
-  { eapply pi_step_future; eauto. }
+  { eapply pi_step_future; try exact WF; eauto. }
   i. des. esplits; [|econs; try exact STEPS0|]; eauto; omega.
 Qed.
 

diff --git a/src/invariant/Invariant.v b/src/invariant/Invariant.v
@@ -172,7 +172,7 @@ Section Invariant.
       { i. des. inv SEM. congr. }
       condtac; ss.
       { guardH o. i. des. inv SEM.
-        exploit Memory.split_get0; eauto. i. des.
+        exploit Memory.split_get0; try exact MEM; eauto. i. des.
         esplits; eauto.
       }
       i. esplits; eauto.

diff --git a/src/lang/MemoryFacts.v b/src/lang/MemoryFacts.v
@@ -75,7 +75,7 @@ Module MemoryFacts.
     - erewrite Memory.split_o; eauto. repeat condtac; ss.
       + des. subst. congr.
       + guardH o. des. subst. i. inv GET.
-        exploit Memory.split_get0; eauto. i. des. esplits; eauto.
+        exploit Memory.split_get0; try exact MEM; eauto. i. des. esplits; eauto.
       + i. esplits; eauto.
     - erewrite Memory.lower_o; eauto. condtac; ss.
       + des. subst. congr.

diff --git a/src/opt/Merge.v b/src/opt/Merge.v
@@ -300,7 +300,7 @@ Proof.
         { auto. }
       * econs 2. econs 2. econs; [|econs 4]; eauto.
         { econs. econs. s. rewrite ? Const.add_0_r. eauto. }
-        { eapply merge_write_read1; try apply STEP_SRC; eauto. }
+        { eapply merge_write_read1; try apply STEP2; eauto. }
       * auto.
       * etrans; eauto.
       * etrans; eauto.
+1 −1		Hahn.v
+4 −4		HahnBase.v
+21 −0		HahnDom.v
+324 −78		HahnPath.v
+176 −115		HahnRelationsBasic.v
+168 −0		HahnRewrite.v
+0 −2		HahnTotalExt.v
+1 −1		HahnTotalList.v
+1 −0		Makefile
+2 −1		README.md