From 0872908ef7c03762bbdac4bdbbd96bb07b300834 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 26 Jul 2021 15:03:06 +0200
Subject: [PATCH] import options in tests

---
 tests/algebra.v           |  1 +
 tests/atomic.v            |  2 +-
 tests/heap_lang.v         |  5 +++--
 tests/heap_lang2.v        |  2 +-
 tests/heap_lang_proph.v   | 12 +++++++++---
 tests/heapprop.v          |  1 +
 tests/ipm_paper.ref       |  9 +--------
 tests/ipm_paper.v         | 12 ++++++++----
 tests/list_reverse.v      |  2 +-
 tests/mosel_paper.v       |  1 +
 tests/one_shot.v          | 10 +++++++---
 tests/one_shot_once.v     | 10 +++++++---
 tests/proofmode.v         | 34 +++++++++++++++++++++++-----------
 tests/proofmode_ascii.v   |  4 ++--
 tests/proofmode_iris.v    |  3 ++-
 tests/proofmode_monpred.v |  1 +
 tests/proofmode_siprop.v  |  1 +
 tests/string_ident.v      |  2 +-
 tests/telescopes.v        |  2 +-
 tests/tree_sum.v          |  2 +-
 20 files changed, 73 insertions(+), 43 deletions(-)

diff --git a/tests/algebra.v b/tests/algebra.v
index e62e613f8..68cc8177c 100644
--- a/tests/algebra.v
+++ b/tests/algebra.v
@@ -1,5 +1,6 @@
 From iris.algebra Require Import auth excl lib.gmap_view.
 From iris.base_logic.lib Require Import invariants.
+From iris.prelude Require Import options.
 
 Section test_dist_equiv_mode.
   (* check that the mode for [Dist] does not trigger https://github.com/coq/coq/issues/14441.
diff --git a/tests/atomic.v b/tests/atomic.v
index b36f9b636..fc69d02d0 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -1,7 +1,7 @@
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export atomic.
 From iris.heap_lang Require Import proofmode notation atomic_heap.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index dfabf4c10..da4831eb2 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -3,7 +3,7 @@ From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.heap_lang Require Import lang adequacy proofmode notation.
 (* Import lang *again*. This used to break notation. *)
 From iris.heap_lang Require Import lang.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
@@ -196,7 +196,7 @@ Section tests.
     val_is_unboxed v â†’
     l â†¦ v -âˆ— WP CmpXchg #l v v {{ _, True }}.
   Proof.
-    iIntros (?) "?". wp_cmpxchg as ? | ?. done. done.
+    iIntros (?) "?". wp_cmpxchg as ? | ?; done.
   Qed.
 
   Lemma wp_xchg l (vâ‚ vâ‚‚ : val) :
@@ -478,5 +478,6 @@ Section error_tests.
   Abort.
 End error_tests.
 
+(* Test a closed proof *)
 Lemma heap_e_adequate Ïƒ : adequate NotStuck heap_e Ïƒ (Î» v _, v = #2).
 Proof. eapply (heap_adequacy heapÎ£)=> ?. iIntros "_". by iApply heap_e_spec. Qed.
diff --git a/tests/heap_lang2.v b/tests/heap_lang2.v
index 8d72a987c..a4b12e368 100644
--- a/tests/heap_lang2.v
+++ b/tests/heap_lang2.v
@@ -3,7 +3,7 @@ printing *)
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Export primitive_laws notation.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
diff --git a/tests/heap_lang_proph.v b/tests/heap_lang_proph.v
index 4d8e5f234..cb9db7b85 100644
--- a/tests/heap_lang_proph.v
+++ b/tests/heap_lang_proph.v
@@ -1,7 +1,6 @@
 From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.heap_lang Require Import lang adequacy proofmode notation.
-From iris.heap_lang Require Import lang.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Section tests.
   Context `{!heapGS Î£}.
@@ -16,7 +15,14 @@ Section tests.
   Proof.
     iIntros "Hl Hp". wp_pures. wp_apply (wp_resolve with "Hp"); first done.
     wp_cmpxchg_suc. iIntros "!>" (ws ->) "Hp". eauto with iFrame.
-  Restart.
+  Qed.
+
+  Lemma test_resolve1' E (l : loc) (n : Z) (p : proph_id) (vs : list (val * val)) (v : val) :
+    l â†¦ #n -âˆ—
+    proph p vs -âˆ—
+    WP Resolve (CmpXchg #l #n (#n + #1)) #p v @ E
+      {{ v, âŒœv = (#n, #true)%VâŒ âˆ— âˆƒvs, proph p vs âˆ— l â†¦ #(n+1) }}.
+  Proof.
     iIntros "Hl Hp". wp_pures. wp_apply (wp_resolve_cmpxchg_suc with "[$Hp $Hl]"); first by left.
     iIntros "Hpost". iDestruct "Hpost" as (ws ->) "Hp". eauto with iFrame.
   Qed.
diff --git a/tests/heapprop.v b/tests/heapprop.v
index 9f2b36e04..de2eaa478 100644
--- a/tests/heapprop.v
+++ b/tests/heapprop.v
@@ -1,6 +1,7 @@
 From stdpp Require Import gmap.
 From iris.bi Require Import interface.
 From iris.proofmode Require Import tactics.
+From iris.prelude Require Import options.
 
 (** This file constructs a simple non step-indexed linear separation logic as
 predicates over heaps (modeled as maps from integer locations to integer values).
diff --git a/tests/ipm_paper.ref b/tests/ipm_paper.ref
index d7ba9448a..ffb9ec740 100644
--- a/tests/ipm_paper.ref
+++ b/tests/ipm_paper.ref
@@ -14,7 +14,7 @@
   --------------------------------------âˆ—
   Î¨ x âˆ— P
   
-2 goals
+1 goal
   
   M : ucmra
   A : Type
@@ -26,13 +26,6 @@
   --------------------------------------âˆ—
   Î¨ x
   
-
-goal 2 is:
- "HP" : P
-"HR" : R
---------------------------------------âˆ—
-P
-
 1 goal
   
   M : ucmra
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 24abfeda8..3bc0914b3 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -7,7 +7,7 @@ From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import base_logic.
 From iris.deprecated.program_logic Require Import hoare.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
@@ -23,7 +23,9 @@ Section demo.
     intros [HP [HÎ¨ HR]].
     destruct HÎ¨ as [x HÎ¨].
     exists x.
-    split. assumption. assumption.
+    split.
+    -  assumption.
+    -  assumption.
   Qed.
 
   (* The version in IPM *)
@@ -34,7 +36,9 @@ Section demo.
     iIntros "[HP [HÎ¨ HR]]".
     iDestruct "HÎ¨" as (x) "HÎ¨".
     iExists x. Show.
-    iSplitL "HÎ¨". Show. iAssumption. Show. iAssumption.
+    iSplitL "HÎ¨".
+    - Show. iAssumption.
+    - Show. iAssumption.
   Qed.
 
   (* The short version in IPM, as in the paper *)
@@ -174,7 +178,7 @@ Section M.
   Global Instance frag_core_id n : CoreId (Frag n).
   Proof. by constructor. Qed.
   Lemma auth_frag_valid j n : âœ“ (Auth n â‹… Frag j) â†’ j â‰¤ n.
-  Proof. simpl. case_decide. done. by intros []. Qed.
+  Proof. simpl. case_decide; first done. by intros []. Qed.
   Lemma auth_frag_op (j n : nat) : j â‰¤ n â†’ Auth n = Auth n â‹… Frag j.
   Proof. intros. by rewrite /= decide_True. Qed.
 
diff --git a/tests/list_reverse.v b/tests/list_reverse.v
index 04d426610..4f98fa490 100644
--- a/tests/list_reverse.v
+++ b/tests/list_reverse.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Export tactics.
 From iris.program_logic Require Export total_weakestpre weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
diff --git a/tests/mosel_paper.v b/tests/mosel_paper.v
index 00a84f31f..ed19935dd 100644
--- a/tests/mosel_paper.v
+++ b/tests/mosel_paper.v
@@ -7,6 +7,7 @@ Jan-Oliver Kaiser, Amin Timany, Arthur CharguÃ©raud, Derek Dreyer
 ICFP 2018 *)
 From iris.bi Require Import monpred.
 From iris.proofmode Require Import tactics monpred.
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 12ac80df3..c5ca6dbb9 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -5,7 +5,7 @@ From iris.deprecated.program_logic Require Import hoare.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import assert proofmode notation adequacy.
 From iris.heap_lang.lib Require Import par.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 (** This is the introductory example from the "Iris from the Ground Up" journal
 paper. *)
@@ -76,8 +76,12 @@ Proof.
     iAssert (one_shot_inv Î³ l âˆ— (âŒœv = NONEVâŒ âˆ¨ âˆƒ n : Z,
       âŒœv = SOMEV #nâŒ âˆ— own Î³ (Shot n)))%I with "[Hl Hv]" as "[Hinv #Hv]".
     { iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as (m) "[% ?]"; subst.
-      + Show. iSplit. iLeft; by iSplitL "Hl". eauto.
-      + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
+      + Show. iSplit.
+        * iLeft; by iSplitL "Hl".
+        * eauto.
+      + iSplit.
+        * iRight; iExists m; by iSplitL "Hl".
+        * eauto. }
     iSplitL "Hinv"; first by eauto.
     iModIntro. wp_pures. iIntros "!> !>". wp_lam.
     iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% HÎ³']";
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index 5a23af9f5..7df7a2384 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -5,7 +5,7 @@ From iris.deprecated.program_logic Require Import hoare.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import assert proofmode notation adequacy.
 From iris.heap_lang.lib Require Import par.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 (** This is the introductory example from Ralf's PhD thesis.
 The difference to [one_shot] is that [set] asserts to be called only once. *)
@@ -92,8 +92,12 @@ Proof.
     iAssert (one_shot_inv Î³ l âˆ— (âŒœv = NONEVâŒ âˆ¨ âˆƒ n : Z,
       âŒœv = SOMEV #nâŒ âˆ— own Î³ (Shot n)))%I with "[Hl Hv]" as "[Hinv #Hv]".
     { iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as (m) "[% ?]"; subst.
-      + Show. iSplit. iLeft; by iSplitL "Hl". eauto.
-      + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
+      + Show. iSplit.
+        * iLeft; by iSplitL "Hl".
+        * eauto.
+      + iSplit.
+        * iRight; iExists m; by iSplitL "Hl".
+        * eauto. }
     iSplitL "Hinv"; first by eauto.
     iModIntro. wp_pures. iIntros "!> !>". wp_lam. wp_bind (! _)%E.
     iInv N as "Hinv".
diff --git a/tests/proofmode.v b/tests/proofmode.v
index afcfd89f2..03b44f242 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,6 +1,6 @@
 From iris.bi Require Import laterable.
 From iris.proofmode Require Import tactics intro_patterns.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
@@ -28,7 +28,7 @@ Proof.
   (* should remove the disjunction "H" *)
   iDestruct "H" as "[#?|#?]"; last by iLeft. Show.
   (* should keep the disjunction "H" because it is instantiated *)
-  iDestruct ("H2" $! 10) as "[%|%]". done. done.
+  iDestruct ("H2" $! 10) as "[%|%]"; done.
 Qed.
 
 Lemma demo_2 P1 P2 P3 P4 Q (P5 : nat â†’ PROP) `{!Affine P4, !Absorbing P2} :
@@ -46,7 +46,7 @@ Proof.
   (* split takes a list of hypotheses just for the LHS *)
   iSplitL "H3".
   - iFrame "H3". iRight. auto.
-  - iSplitL "HQ". iAssumption. by iSplitL "H1".
+  - iSplitL "HQ"; first iAssumption. by iSplitL "H1".
 Qed.
 
 Lemma demo_3 P1 P2 P3 :
@@ -719,7 +719,11 @@ Proof. iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ". Qed.
 
 Lemma test_iAlways P Q R :
   â–¡ P -âˆ— <pers> Q â†’ R -âˆ— <pers> <affine> <affine> P âˆ— â–¡ Q.
-Proof. iIntros "#HP #HQ HR". iSplitL. iModIntro. done. iModIntro. done. Qed.
+Proof.
+  iIntros "#HP #HQ HR". iSplitL.
+  - iModIntro. done.
+  - iModIntro. done.
+Qed.
 
 (* A bunch of test cases from #127 to establish that tactics behave the same on
 `âŒœ Ï† âŒ â†’ P` and `âˆ€ _ : Ï†, P` *)
@@ -731,7 +735,7 @@ Lemma test_forall_nondep_2 (Ï† : Prop) :
 Proof. iIntros (HÏ†) "HÏ†". iSpecialize ("HÏ†" with "[% //]"). done. Qed.
 Lemma test_forall_nondep_3 (Ï† : Prop) :
   Ï† â†’ (âˆ€ _ : Ï†, False : PROP) -âˆ— False.
-Proof. iIntros (HÏ†) "HÏ†". unshelve iSpecialize ("HÏ†" $! _). done. done. Qed.
+Proof. iIntros (HÏ†) "HÏ†". unshelve iSpecialize ("HÏ†" $! _); done. Qed.
 Lemma test_forall_nondep_4 (Ï† : Prop) :
   Ï† â†’ (âˆ€ _ : Ï†, False : PROP) -âˆ— False.
 Proof. iIntros (HÏ†) "HÏ†". iSpecialize ("HÏ†" $! HÏ†); done. Qed.
@@ -744,7 +748,7 @@ Lemma test_pure_impl_2 (Ï† : Prop) :
 Proof. iIntros (HÏ†) "HÏ†". iSpecialize ("HÏ†" with "[% //]"). done. Qed.
 Lemma test_pure_impl_3 (Ï† : Prop) :
   Ï† â†’ (âŒœÏ†âŒ â†’ False : PROP) -âˆ— False.
-Proof. iIntros (HÏ†) "HÏ†". unshelve iSpecialize ("HÏ†" $! _). done. done. Qed.
+Proof. iIntros (HÏ†) "HÏ†". unshelve iSpecialize ("HÏ†" $! _); done. Qed.
 Lemma test_pure_impl_4 (Ï† : Prop) :
   Ï† â†’ (âŒœÏ†âŒ â†’ False : PROP) -âˆ— False.
 Proof. iIntros (HÏ†) "HÏ†". iSpecialize ("HÏ†" $! HÏ†). done. Qed.
@@ -901,24 +905,32 @@ Qed.
 Lemma iFrame_with_evar_r P Q :
   âˆƒ R, (P -âˆ— Q -âˆ— P âˆ— R) âˆ§ R = Q.
 Proof.
-  eexists. split. iIntros "HP HQ". iFrame. iApply "HQ". done.
+  eexists. split.
+  - iIntros "HP HQ". iFrame. iApply "HQ".
+  - done.
 Qed.
 Lemma iFrame_with_evar_l P Q :
   âˆƒ R, (P -âˆ— Q -âˆ— R âˆ— P) âˆ§ R = Q.
 Proof.
-  eexists. split. iIntros "HP HQ". Fail iFrame "HQ".
-  iSplitR "HP"; iAssumption. done.
+  eexists. split.
+  - iIntros "HP HQ". Fail iFrame "HQ".
+    iSplitR "HP"; iAssumption.
+  - done.
 Qed.
 Lemma iFrame_with_evar_persistent P Q :
   âˆƒ R, (P -âˆ— â–¡ Q -âˆ— P âˆ— R âˆ— Q) âˆ§ R = emp%I.
 Proof.
-  eexists. split. iIntros "HP #HQ". iFrame "HQ HP". iEmpIntro. done.
+  eexists. split.
+  - iIntros "HP #HQ". iFrame "HQ HP". iEmpIntro.
+  - done.
 Qed.
 
 Lemma test_iAccu P Q R S :
   âˆƒ PP, (â–¡P -âˆ— Q -âˆ— R -âˆ— S -âˆ— PP) âˆ§ PP = (Q âˆ— R âˆ— S)%I.
 Proof.
-  eexists. split. iIntros "#? ? ? ?". iAccu. done.
+  eexists. split.
+  - iIntros "#? ? ? ?". iAccu.
+  - done.
 Qed.
 
 Lemma test_iAssumption_evar P : âˆƒ R, (R âŠ¢ P) âˆ§ R = P.
diff --git a/tests/proofmode_ascii.v b/tests/proofmode_ascii.v
index fa04cc2a5..f7f4d6021 100644
--- a/tests/proofmode_ascii.v
+++ b/tests/proofmode_ascii.v
@@ -1,10 +1,10 @@
 From iris.proofmode Require Import tactics monpred.
 From iris.base_logic Require Import base_logic.
 From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.
+From iris.prelude Require Import options.
 
 From iris.bi Require Import ascii.
 
-Set Default Proof Using "Type".
 Unset Mangle Names.
 
 (* Remove this and the [Set Printing Raw Literals.] below once we require Coq
@@ -36,7 +36,7 @@ Section base_logic_tests.
     iExists (S j + z1), z2.
     iNext.
     iApply ("H3" $! _ 0 with "[$]").
-    - iSplit. done. iApply "H2". iLeft. iApply "H2". by iRight.
+    - iSplit; first done. iApply "H2". iLeft. iApply "H2". by iRight.
     - done.
   Qed.
 
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 955fb532c..5bfe65ba2 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -2,6 +2,7 @@ From iris.algebra Require Import frac.
 From iris.proofmode Require Import tactics monpred.
 From iris.base_logic Require Import base_logic.
 From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
@@ -30,7 +31,7 @@ Section base_logic_tests.
     iExists (S j + z1), z2.
     iNext.
     iApply ("H3" $! _ 0 with "[$]").
-    - iSplit. done. iApply "H2". iLeft. iApply "H2". by iRight.
+    - iSplit; first done. iApply "H2". iLeft. iApply "H2". by iRight.
     - done.
   Qed.
 
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 990f81f2a..66d9f61aa 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -1,5 +1,6 @@
 From iris.proofmode Require Import tactics monpred.
 From iris.base_logic.lib Require Import invariants.
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
diff --git a/tests/proofmode_siprop.v b/tests/proofmode_siprop.v
index 57e9a7332..3e3efcc04 100644
--- a/tests/proofmode_siprop.v
+++ b/tests/proofmode_siprop.v
@@ -1,5 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.si_logic Require Import bi.
+From iris.prelude Require Import options.
 
 Section si_logic_tests.
   Implicit Types P Q R : siProp.
diff --git a/tests/string_ident.v b/tests/string_ident.v
index 6de14c131..dc22df6de 100644
--- a/tests/string_ident.v
+++ b/tests/string_ident.v
@@ -1,7 +1,7 @@
 From iris.proofmode Require Import string_ident.
 From Coq Require Import Strings.String.
 From stdpp Require Import base.
-Open Scope string.
+Local Open Scope string.
 
 Lemma test_basic_ident : âˆ€ (n:nat), n = n.
 Proof.
diff --git a/tests/telescopes.v b/tests/telescopes.v
index ce3a0290b..1e7fcc3e5 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -1,6 +1,6 @@
 From stdpp Require Import coPset namespaces.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
diff --git a/tests/tree_sum.v b/tests/tree_sum.v
index 7f830cba2..b5683256d 100644
--- a/tests/tree_sum.v
+++ b/tests/tree_sum.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Export tactics.
 From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+From iris.prelude Require Import options.
 
 Inductive tree :=
   | leaf : Z â†’ tree
-- 
GitLab