From 10f67f78439c203b9fa05308bf398b39c9c2d3b0 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 22 Jan 2018 18:21:17 +0100
Subject: [PATCH] Bump Iris. Fix proofs in tstack which used induction.

---
 opam                       |  2 +-
 theories/examples/tstack.v | 16 ++++++----------
 theories/weakestpre.v      |  5 ++---
 3 files changed, 9 insertions(+), 14 deletions(-)

diff --git a/opam b/opam
index dab2693c..3819c7f8 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/igps" ]
 depends: [
-  "coq-iris" { (= "branch.gen_proofmode.2018-01-18.2") | (= "dev") }
+  "coq-iris" { (= "branch.gen_proofmode.2018-01-22.3") | (= "dev") }
 ]
diff --git a/theories/examples/tstack.v b/theories/examples/tstack.v
index a8c01fb6..5271171f 100644
--- a/theories/examples/tstack.v
+++ b/theories/examples/tstack.v
@@ -100,7 +100,7 @@ Section TreiberStack.
       iIntros "Head".
       iDestruct "Head" as (A) "Head".
       rewrite /ReachableD (fixpoint_unfold (ReachableD') _ _).
-      revert n. induction A as [|n' A'] => n.
+      iInduction A as [|n' A'] "IH" forall (n).
       - iDestruct "Head" as % ->.
         iSplitL; iExists []; by rewrite /ReachableD (fixpoint_unfold (ReachableD') _ _).
       - iDestruct "Head" as "(% & Head)".
@@ -108,9 +108,7 @@ Section TreiberStack.
         iAssert (▷ ((Head P false l s n') ∗ (Head P false l s n')))%I
           with "[Head]" as "(Hn1 & Hn2)".
         { iNext. rewrite (fixpoint_unfold (ReachableD') _ _).
-          (* iApply (IHA' n' with "[Head]"). *)
-          admit.
-        }
+          iApply ("IH" with "Head"). }
         iDestruct (na_frac_split_2 with "next") as "[NA1 NA2]".
         iSplitL "Hn1 NA1";
           [iDestruct "Hn1" as (A1) "Hn1"; iExists (n' :: A1)
@@ -119,7 +117,7 @@ Section TreiberStack.
            (iSplitL ""; first done); iExists (q/2)%Qp;
            [iFrame "NA1"| iFrame "NA2"];
            iNext; by rewrite (fixpoint_unfold (ReachableD') _ _).
-    Admitted.
+    Qed.
 
     Lemma Head_dup_main P l s n:
       Head P true l s n -∗ Head P true l s n ∗ Head P false l s n.
@@ -127,7 +125,7 @@ Section TreiberStack.
       iIntros "Head".
       iDestruct "Head" as (A) "Head".
       rewrite /Reachable (fixpoint_unfold (Reachable' P) _ _).
-      revert n. induction A as [|n' A'] => n.
+      iInduction A as [|n' A'] "IH" forall (n).
       - iDestruct "Head" as "#Head".
         iSplitL; iExists [].
         + by rewrite /Reachable' /Reachable (fixpoint_unfold (Reachable' P) _ _).
@@ -137,9 +135,7 @@ Section TreiberStack.
         iAssert (▷ ((Head P true l s h') ∗ (Head P false l s h')))%I
           with "[Head]" as "(Hn1 & Hn2)".
         { iNext. rewrite (fixpoint_unfold (Reachable' P) _ _).
-          (* by iApply (IHA' h' with "[Head]"). *)
-          admit.
-        }
+          iApply ("IH" with "Head"). }
         iDestruct (na_frac_split_2 with "next") as "[NA1 NA2]".
         iSplitL "Hn1 NA1 od P".
         + iDestruct "Hn1" as (A1) "Hn1"; iExists (n' :: A1).
@@ -152,7 +148,7 @@ Section TreiberStack.
           iSplitL ""; first done.
           iExists _. iFrame "NA2".
           iNext; by rewrite (fixpoint_unfold (ReachableD') _ _).
-    Admitted.
+    Qed.
   End Interpretation.
 
   Section proof.
diff --git a/theories/weakestpre.v b/theories/weakestpre.v
index ee1cab81..fdb70023 100644
--- a/theories/weakestpre.v
+++ b/theories/weakestpre.v
@@ -187,8 +187,7 @@ Proof.
   intros Hatomic. iStartProof (uPred _). iIntros (?) "H".
   rewrite wp_eq /wp_def /=. iIntros (?? π) "S".
   iApply (weakestpre.wp_atomic _ E1 E2) => //. iMod "H". iModIntro.
-  iApply (weakestpre.wp_strong_mono _ E2); first done.
-  iDestruct ("H" with "[%] S") as "$"; first done.
+  iApply (weakestpre.wp_strong_mono _ _ E2 with "[-]"); [done..|by iApply "H"|].
   iIntros (?) "H". case_match. iModIntro.
   by iDestruct "H" as "[$ H]".
 Qed.
@@ -242,7 +241,7 @@ Proof.
   iIntros "H" (V_1 ??) "S".
   iApply (wp_bind_iris).
   iSpecialize ("H" with "[%] S"); first done.
-  iApply (weakestpre.wp_strong_mono with "[$H]"); first done.
+  iApply (weakestpre.wp_strong_mono with "[$H]"); [done..|].
   iIntros ([v V_2]) "[S H]".
   by iApply ("H").
 Qed.
-- 
GitLab