Port to Coq 8.7

snu-sf · Oct 19, 2017 · 5806c1a · 5806c1a
1 parent 4f5110d
commit 5806c1a
Show file tree

Hide file tree

Showing 6 changed files with 61 additions and 59 deletions.
diff --git a/.dir-locals.el b/.dir-locals.el
@@ -14,4 +14,5 @@
                                 (rec ,(pre "src/hahn") "cmem")
                                 (rec ,(pre "src/while") "cmem")
                                ))))
-              (coq-prog-args . ("-emacs-U")))))
+              ;; (coq-prog-args . ("-emacs-U"))
+              )))
diff --git a/.gitignore b/.gitignore
@@ -1,5 +1,6 @@
 _CoqProject
 Makefile.coq
+Makefile.coq.conf
 .build
 
 *.vo

diff --git a/README.md b/README.md
@@ -8,7 +8,7 @@ Please visit the [project website](http://sf.snu.ac.kr/promise-concurrency/) for
 
 ## Build
 
-- Requirement: [Coq 8.6](https://coq.inria.fr/download), Make, Rsync.
+- Requirement: [Coq 8.7](https://coq.inria.fr/download), Make, Rsync.
 
 - Initialization
 

diff --git a/src/lib/respectful5.v b/src/lib/respectful5.v
@@ -23,12 +23,12 @@ Section Respectful5.
   .
   Hint Constructors sound5.
 
-  Structure respectful5 (clo: rel -> rel) : Prop :=
-  | respectful5_intro
-      (MON: monotone5 clo)
-      (RESPECTFUL:
-         forall l r (LE: l <5= r) (GF: l <5= gf r),
-           clo l <5= gf (clo r)).
+  Structure respectful5 (clo: rel -> rel) : Prop := respectful5_intro {
+    MON: monotone5 clo;
+    RESPECTFUL:
+      forall l r (LE: l <5= r) (GF: l <5= gf r),
+        clo l <5= gf (clo r);
+  }.
   Hint Constructors respectful5.
 
   Inductive grespectful5 (r: rel) e1 e2 e3 e4 e5: Prop :=
@@ -69,7 +69,7 @@ Section Respectful5.
       unfold rr in *; des; eauto 10 using gf_mon. }
     induction n; i; [by s; eauto using gf_mon|].
     ss; des; [by eauto using gf_mon|].
-    eapply gf_mon; [eapply RESPECTFUL; [|apply IHn|]|]; inst; s; eauto.
+    eapply gf_mon; [eapply RESPECTFUL0; [|apply IHn|]|]; inst; s; eauto.
   Qed.
 
   Lemma respectful5_compose
@@ -80,10 +80,10 @@ Section Respectful5.
   Proof.
     i. destruct RES1, RES2.
     econs.
-    - ii. eapply MON; eauto.
-    - i. eapply RESPECTFUL; [| |apply PR].
-      + i. eapply MON0; eauto.
-      + i. eapply RESPECTFUL0; eauto.
+    - ii. eapply MON0; eauto.
+    - i. eapply RESPECTFUL0; [| |apply PR].
+      + i. eapply MON1; eauto.
+      + i. eapply RESPECTFUL1; eauto.
   Qed.
 
   Lemma grespectful5_respectful5: respectful5 grespectful5.
@@ -122,7 +122,7 @@ Section Respectful5.
   Proof.
     intro r; pcofix CIH; i; pfold.
     eapply gf_mon, grespectful5_compose, grespectful5_respectful5.
-    destruct grespectful5_respectful5; eapply RESPECTFUL, PR; i; [by apply grespectful5_incl; eauto|].
+    destruct grespectful5_respectful5; eapply RESPECTFUL0, PR; i; [by apply grespectful5_incl; eauto|].
     punfold PR0.
       by eapply gfgres5_mon; eauto; i; destruct PR1; eauto.
   Qed.
@@ -174,12 +174,12 @@ Section Respectful5.
     econs 2; eauto.
   Qed.
 
-  Structure weak_respectful5 (clo: rel -> rel) : Prop :=
-  | weak_respectful5_intro
-      (MON: monotone5 clo)
-      (RESPECTFUL:
-         forall l r (LE: l <5= r) (GF: l <5= gf r),
-           clo l <5= gf (rclo5 clo r)).
+  Structure weak_respectful5 (clo: rel -> rel) : Prop := weak_respectful5_intro {
+    WEAK_MON: monotone5 clo;
+    WEAK_RESPECTFUL:
+      forall l r (LE: l <5= r) (GF: l <5= gf r),
+        clo l <5= gf (rclo5 clo r);
+  }.
   Hint Constructors weak_respectful5.
 
   Lemma weak_respectful5_respectful5
@@ -190,7 +190,7 @@ Section Respectful5.
     induction PR; i.
     - eapply gf_mon; eauto. i.
       apply rclo5_incl. auto.
-    - exploit RESPECTFUL; [|apply H|apply CLOR'|].
+    - exploit WEAK_RESPECTFUL0; [|apply H|apply CLOR'|].
       + i. eapply rclo5_mon; eauto.
       + i. eapply gf_mon; eauto.
         apply rclo5_rclo5; auto.

diff --git a/src/lib/respectful7.v b/src/lib/respectful7.v
@@ -25,12 +25,12 @@ Section Respectful7.
   .
   Hint Constructors sound7.
 
-  Structure respectful7 (clo: rel -> rel) : Prop :=
-  | respectful7_intro
-      (MON: monotone7 clo)
-      (RESPECTFUL:
-         forall l r (LE: l <7= r) (GF: l <7= gf r),
-           clo l <7= gf (clo r)).
+  Structure respectful7 (clo: rel -> rel) : Prop := respectful7_intro {
+    MON: monotone7 clo;
+    RESPECTFUL:
+      forall l r (LE: l <7= r) (GF: l <7= gf r),
+        clo l <7= gf (clo r);
+  }.
   Hint Constructors respectful7.
 
   Inductive grespectful7 (r: rel) e1 e2 e3 e4 e5 e6 e7: Prop :=
@@ -71,7 +71,7 @@ Section Respectful7.
       unfold rr in *; des; eauto 10 using gf_mon. }
     induction n; i; [by s; eauto using gf_mon|].
     ss; des; [by eauto using gf_mon|].
-    eapply gf_mon; [eapply RESPECTFUL; [|apply IHn|]|]; inst; s; eauto.
+    eapply gf_mon; [eapply RESPECTFUL0; [|apply IHn|]|]; inst; s; eauto.
   Qed.
 
   Lemma respectful7_compose
@@ -82,10 +82,10 @@ Section Respectful7.
   Proof.
     i. destruct RES1, RES2.
     econs.
-    - ii. eapply MON; eauto.
-    - i. eapply RESPECTFUL; [| |apply PR].
-      + i. eapply MON0; eauto.
-      + i. eapply RESPECTFUL0; eauto.
+    - ii. eapply MON0; eauto.
+    - i. eapply RESPECTFUL0; [| |apply PR].
+      + i. eapply MON1; eauto.
+      + i. eapply RESPECTFUL1; eauto.
   Qed.
 
   Lemma grespectful7_respectful7: respectful7 grespectful7.
@@ -124,7 +124,7 @@ Section Respectful7.
   Proof.
     intro r; pcofix CIH; i; pfold.
     eapply gf_mon, grespectful7_compose, grespectful7_respectful7.
-    destruct grespectful7_respectful7; eapply RESPECTFUL, PR; i; [by apply grespectful7_incl; eauto|].
+    destruct grespectful7_respectful7; eapply RESPECTFUL0, PR; i; [by apply grespectful7_incl; eauto|].
     punfold PR0.
       by eapply gfgres7_mon; eauto; i; destruct PR1; eauto.
   Qed.
@@ -176,12 +176,12 @@ Section Respectful7.
     econs 2; eauto.
   Qed.
 
-  Structure weak_respectful7 (clo: rel -> rel) : Prop :=
-  | weak_respectful7_intro
-      (MON: monotone7 clo)
-      (RESPECTFUL:
-         forall l r (LE: l <7= r) (GF: l <7= gf r),
-           clo l <7= gf (rclo7 clo r)).
+  Structure weak_respectful7 (clo: rel -> rel) : Prop := weak_respectful7_intro {
+    WEAK_MON: monotone7 clo;
+    WEAK_RESPECTFUL:
+      forall l r (LE: l <7= r) (GF: l <7= gf r),
+        clo l <7= gf (rclo7 clo r);
+  }.
   Hint Constructors weak_respectful7.
 
   Lemma weak_respectful7_respectful7
@@ -192,7 +192,7 @@ Section Respectful7.
     induction PR; i.
     - eapply gf_mon; eauto. i.
       apply rclo7_incl. auto.
-    - exploit RESPECTFUL; [|apply H|apply CLOR'|].
+    - exploit WEAK_RESPECTFUL0; [|apply H|apply CLOR'|].
       + i. eapply rclo7_mon; eauto.
       + i. eapply gf_mon; eauto.
         apply rclo7_rclo7; auto.

diff --git a/src/lib/respectful9.v b/src/lib/respectful9.v
@@ -27,12 +27,12 @@ Section Respectful9.
   .
   Hint Constructors sound9.
 
-  Structure respectful9 (clo: rel -> rel) : Prop :=
-  | respectful9_intro
-      (MON: monotone9 clo)
-      (RESPECTFUL:
-         forall l r (LE: l <9= r) (GF: l <9= gf r),
-           clo l <9= gf (clo r)).
+  Structure respectful9 (clo: rel -> rel) : Prop := respectful9_intro {
+    MON: monotone9 clo;
+    RESPECTFUL:
+      forall l r (LE: l <9= r) (GF: l <9= gf r),
+        clo l <9= gf (clo r);
+  }.
   Hint Constructors respectful9.
 
   Inductive grespectful9 (r: rel) e1 e2 e3 e4 e5 e6 e7 e8 e9: Prop :=
@@ -73,7 +73,7 @@ Section Respectful9.
       unfold rr in *; des; eauto 10 using gf_mon. }
     induction n; i; [by s; eauto using gf_mon|].
     ss; des; [by eauto using gf_mon|].
-    eapply gf_mon; [eapply RESPECTFUL; [|apply IHn|]|]; inst; s; eauto.
+    eapply gf_mon; [eapply RESPECTFUL0; [|apply IHn|]|]; inst; s; eauto.
   Qed.
 
   Lemma respectful9_compose
@@ -84,10 +84,10 @@ Section Respectful9.
   Proof.
     i. destruct RES1, RES2.
     econs.
-    - ii. eapply MON; eauto.
-    - i. eapply RESPECTFUL; [| |apply PR].
-      + i. eapply MON0; eauto.
-      + i. eapply RESPECTFUL0; eauto.
+    - ii. eapply MON0; eauto.
+    - i. eapply RESPECTFUL0; [| |apply PR].
+      + i. eapply MON1; eauto.
+      + i. eapply RESPECTFUL1; eauto.
   Qed.
 
   Lemma grespectful9_respectful9: respectful9 grespectful9.
@@ -126,7 +126,7 @@ Section Respectful9.
   Proof.
     intro r; pcofix CIH; i; pfold.
     eapply gf_mon, grespectful9_compose, grespectful9_respectful9.
-    destruct grespectful9_respectful9; eapply RESPECTFUL, PR; i; [by apply grespectful9_incl; eauto|].
+    destruct grespectful9_respectful9; eapply RESPECTFUL0, PR; i; [by apply grespectful9_incl; eauto|].
     punfold PR0.
       by eapply gfgres9_mon; eauto; i; destruct PR1; eauto.
   Qed.
@@ -178,12 +178,12 @@ Section Respectful9.
     econs 2; eauto.
   Qed.
 
-  Structure weak_respectful9 (clo: rel -> rel) : Prop :=
-  | weak_respectful9_intro
-      (MON: monotone9 clo)
-      (RESPECTFUL:
-         forall l r (LE: l <9= r) (GF: l <9= gf r),
-           clo l <9= gf (rclo9 clo r)).
+  Structure weak_respectful9 (clo: rel -> rel) : Prop := weak_respectful9_intro {
+    WEAK_MON: monotone9 clo;
+    WEAK_RESPECTFUL:
+      forall l r (LE: l <9= r) (GF: l <9= gf r),
+        clo l <9= gf (rclo9 clo r);
+  }.
   Hint Constructors weak_respectful9.
 
   Lemma weak_respectful9_respectful9
@@ -194,7 +194,7 @@ Section Respectful9.
     induction PR; i.
     - eapply gf_mon; eauto. i.
       apply rclo9_incl. auto.
-    - exploit RESPECTFUL; [|apply H|apply CLOR'|].
+    - exploit WEAK_RESPECTFUL0; [|apply H|apply CLOR'|].
       + i. eapply rclo9_mon; eauto.
       + i. eapply gf_mon; eauto.
         apply rclo9_rclo9; auto.