Generalize proofmode.

_CoqProject

@@ -24,17 +24,21 @@ theories/algebra/local_updates.v
 theories/algebra/gset.v
 theories/algebra/coPset.v
 theories/algebra/deprecated.v
+theories/bi/interface.v
+theories/bi/derived.v
+theories/bi/big_op.v
+theories/bi/bi.v
+theories/bi/tactics.v
+theories/bi/fractional.v
 theories/base_logic/upred.v
-theories/base_logic/primitive.v
 theories/base_logic/derived.v
 theories/base_logic/base_logic.v
-theories/base_logic/tactics.v
-theories/base_logic/big_op.v
-theories/base_logic/hlist.v
 theories/base_logic/soundness.v
 theories/base_logic/double_negation.v
 theories/base_logic/deprecated.v
 theories/base_logic/fixpoint.v
+theories/base_logic/proofmode.v
+theories/base_logic/proofmode_classes.v
 theories/base_logic/lib/iprop.v
 theories/base_logic/lib/own.v
 theories/base_logic/lib/saved_prop.v
@@ -49,7 +53,6 @@ theories/base_logic/lib/boxes.v
 theories/base_logic/lib/na_invariants.v
 theories/base_logic/lib/cancelable_invariants.v
 theories/base_logic/lib/counter_examples.v
-theories/base_logic/lib/fractional.v
 theories/base_logic/lib/gen_heap.v
 theories/base_logic/lib/core.v
 theories/base_logic/lib/fancy_updates_from_vs.v
@@ -89,6 +92,7 @@ theories/proofmode/class_instances.v
 theories/tests/heap_lang.v
 theories/tests/one_shot.v
 theories/tests/proofmode.v
+theories/tests/proofmode_iris.v
 theories/tests/list_reverse.v
 theories/tests/tree_sum.v
 theories/tests/ipm_paper.v

theories/algebra/auth.v

 From iris.algebra Require Export excl local_updates.
-From iris.base_logic Require Import base_logic.
-From iris.proofmode Require Import classes.
+From iris.base_logic Require Import base_logic proofmode_classes.
 Set Default Proof Using "Type".
 
 Record auth (A : Type) := Auth { authoritative : excl' A; auth_own : A }.

theories/algebra/frac.v

 From Coq.QArith Require Import Qcanon.
 From iris.algebra Require Export cmra.
-From iris.proofmode Require Import classes.
+From iris.base_logic Require Import proofmode_classes.
 Set Default Proof Using "Type".
 
 Notation frac := Qp (only parsing).

theories/algebra/frac_auth.v

 From iris.algebra Require Export frac auth.
 From iris.algebra Require Export updates local_updates.
-From iris.proofmode Require Import classes.
+From iris.base_logic Require Import proofmode_classes.
 
 Definition frac_authR (A : cmraT) : cmraT :=
   authR (optionUR (prodR fracR A)).

theories/base_logic/base_logic.v

 From iris.base_logic Require Export derived.
+From iris.bi Require Export bi.
 Set Default Proof Using "Type".
 
 Module Import uPred.
   Export upred.uPred.
-  Export primitive.uPred.
   Export derived.uPred.
+  Export bi.
 End uPred.
 
 (* Hint DB for the logic *)
@@ -12,6 +13,6 @@ Hint Resolve pure_intro.
 Hint Resolve or_elim or_intro_l' or_intro_r' : I.
 Hint Resolve and_intro and_elim_l' and_elim_r' : I.
 Hint Resolve persistently_mono : I.
-Hint Resolve sep_elim_l' sep_elim_r' sep_mono : I.
+Hint Resolve sep_mono : I. (* sep_elim_l' sep_elim_r'  *)
 Hint Immediate True_intro False_elim : I.
-Hint Immediate iff_refl internal_eq_refl' : I.
+Hint Immediate iff_refl internal_eq_refl : I.

theories/base_logic/deprecated.v

+(*
+FIXME
+
 From iris.base_logic Require Import primitive.
 Set Default Proof Using "Type".
 
@@ -10,3 +13,4 @@ Notation "x = y" := (uPred_pure (x%C%type = y%C%type)) (only parsing) : uPred_sc
 
 (* Deprecated 2016-11-22. Use ⌜x ⊥ y ⌝ instead. *)
 Notation "x ⊥ y" := (uPred_pure (x%C%type ⊥ y%C%type)) (only parsing) : uPred_scope.
+*)

theories/base_logic/double_negation.v

@@ -7,11 +7,11 @@ Definition uPred_nnupd {M} (P: uPred M) : uPred M :=
   ∀ n, (P -∗ ▷^n False) -∗ ▷^n False.
 
 Notation "|=n=> Q" := (uPred_nnupd Q)
-  (at level 99, Q at level 200, format "|=n=>  Q") : uPred_scope.
+  (at level 99, Q at level 200, format "|=n=>  Q") : bi_scope.
 Notation "P =n=> Q" := (P ⊢ |=n=> Q)
   (at level 99, Q at level 200, only parsing) : C_scope.
 Notation "P =n=∗ Q" := (P -∗ |=n=> Q)%I
-  (at level 99, Q at level 200, format "P  =n=∗  Q") : uPred_scope.
+  (at level 99, Q at level 200, format "P  =n=∗  Q") : bi_scope.
 
 (* Our goal is to prove that:
   (1) |=n=> has (nearly) all the properties of the |==> modality that are used in Iris
@@ -27,7 +27,7 @@ Implicit Types x : M.
 Import uPred.
 
 (* Helper lemmas about iterated later modalities *)
-Lemma laterN_big n a x φ: ✓{n} x →  a ≤ n → (▷^a ⌜φ⌝)%I n x → φ.
+Lemma laterN_big n a x φ: ✓{n} x →  a ≤ n → (▷^a ⌜φ⌝ : uPred M)%I n x → φ.
 Proof.
   induction 2 as [| ?? IHle].
   - induction a; repeat (rewrite //= || uPred.unseal). 
@@ -37,7 +37,7 @@ Proof.
     eapply uPred_closed; eauto using cmra_validN_S.
 Qed.
 
-Lemma laterN_small n a x φ: ✓{n} x →  n < a → (▷^a ⌜φ⌝)%I n x.
+Lemma laterN_small n a x φ: ✓{n} x →  n < a → (▷^a ⌜φ⌝ : uPred M)%I n x.
 Proof.
   induction 2.
   - induction n as [| n IHn]; [| move: IHn];
@@ -132,7 +132,7 @@ Fixpoint uPred_nnupd_k {M} k (P: uPred M) : uPred M :=
   end.
 
 Notation "|=n=>_ k Q" := (uPred_nnupd_k k Q)
-  (at level 99, k at level 9, Q at level 200, format "|=n=>_ k  Q") : uPred_scope.
+  (at level 99, k at level 9, Q at level 200, format "|=n=>_ k  Q") : bi_scope.
 
 
 (* One direction of the limiting process is easy -- nnupd implies nnupd_k for each k *)
@@ -183,13 +183,14 @@ Lemma nnupd_nnupd_k_dist k P: (|=n=> P)%I ≡{k}≡ (|=n=>_k P)%I.
          specialize (HPF n'' x''). exfalso.
          eapply laterN_big; last (unseal; eauto).
          eauto. omega.
-    * inversion Hle; subst.
+    * inversion Hle; simpl; subst.
       ** unseal. intros (HnnP&HnnP_IH) n k' x' ?? HPF.
          case (decide (k' < n)).
          *** move: laterN_small; uPred.unseal; naive_solver.
          *** intros. exfalso. assert (n ≤ k'). omega.
              assert (n = S k ∨ n < S k) as [->|] by omega.
-             **** eapply laterN_big; eauto; unseal. eapply HnnP; eauto.
+             **** eapply laterN_big; eauto; unseal.
+                  eapply HnnP; eauto. move: HPF; by unseal.
              **** move:nnupd_k_elim. unseal. intros Hnnupdk. 
                   eapply laterN_big; eauto. unseal.
                   eapply (Hnnupdk n k); first omega; eauto.
@@ -326,7 +327,6 @@ Proof.
     specialize (Hf3 (S k) (S k) ε). rewrite right_id in Hf3 *. unseal.
     intros Hf3. eapply Hf3; eauto.
     intros ??? Hx'. rewrite left_id in Hx' *=> Hx'.
-    unseal. 
     assert (n' < S k ∨ n' = S k) as [|] by omega.
     * intros. move:(laterN_small n' (S k) x' False). rewrite //=. unseal. intros Hsmall. 
       eapply Hsmall; eauto.
@@ -353,7 +353,7 @@ Lemma adequacy φ n : Nat.iter n (λ P, |=n=> ▷ P)%I ⌜φ⌝%I → ¬¬ φ.
 Proof.
   cut (∀ x, ✓{S n} x → Nat.iter n (λ P, |=n=> ▷ P)%I ⌜φ⌝%I (S n) x → ¬¬φ).
   { intros help H. eapply (help ∅); eauto using ucmra_unit_validN.
-    eapply H; try unseal; eauto using ucmra_unit_validN. red; rewrite //=. }
+    eapply H; eauto using ucmra_unit_validN. by unseal. }
   destruct n.
   - rewrite //=; unseal; auto.
   - intros ??? Hfal.

theories/base_logic/hlist.v

-From stdpp Require Export hlist.
-From iris.base_logic Require Export base_logic.
-Set Default Proof Using "Type".
-Import uPred.
-
-Fixpoint uPred_hexist {M As} : himpl As (uPred M) → uPred M :=
-  match As return himpl As (uPred M) → uPred M with
-  | tnil => id
-  | tcons A As => λ Φ, ∃ x, uPred_hexist (Φ x)
-  end%I.
-Fixpoint uPred_hforall {M As} : himpl As (uPred M) → uPred M :=
-  match As return himpl As (uPred M) → uPred M with
-  | tnil => id
-  | tcons A As => λ Φ, ∀ x, uPred_hforall (Φ x)
-  end%I.
-
-Section hlist.
-Context {M : ucmraT}.
-
-Lemma hexist_exist {As B} (f : himpl As B) (Φ : B → uPred M) :
-  uPred_hexist (hcompose Φ f) ⊣⊢ ∃ xs : hlist As, Φ (f xs).
-Proof.
-  apply (anti_symm _).
-  - induction As as [|A As IH]; simpl.
-    + by rewrite -(exist_intro hnil) .
-    + apply exist_elim=> x; rewrite IH; apply exist_elim=> xs.
-      by rewrite -(exist_intro (hcons x xs)).
-  - apply exist_elim=> xs; induction xs as [|A As x xs IH]; simpl; auto.
-    by rewrite -(exist_intro x) IH.
-Qed.
-
-Lemma hforall_forall {As B} (f : himpl As B) (Φ : B → uPred M) :
-  uPred_hforall (hcompose Φ f) ⊣⊢ ∀ xs : hlist As, Φ (f xs).
-Proof.
-  apply (anti_symm _).
-  - apply forall_intro=> xs; induction xs as [|A As x xs IH]; simpl; auto.
-    by rewrite (forall_elim x) IH.
-  - induction As as [|A As IH]; simpl.
-    + by rewrite (forall_elim hnil) .
-    + apply forall_intro=> x; rewrite -IH; apply forall_intro=> xs.
-      by rewrite (forall_elim (hcons x xs)).
-Qed.
-End hlist.

theories/base_logic/lib/auth.v

 From iris.base_logic.lib Require Export invariants.
 From iris.algebra Require Export auth.
 From iris.algebra Require Import gmap.
-From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 Import uPred.
@@ -73,6 +72,7 @@ Section auth.
   Lemma auth_own_op γ a b : auth_own γ (a ⋅ b) ⊣⊢ auth_own γ a ∗ auth_own γ b.
   Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
 
+(*
   Global Instance from_and_auth_own γ a b1 b2 :
     IsOp a b1 b2 →
     FromAnd false (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 90.
@@ -89,6 +89,7 @@ Section auth.
     IsOp a b1 b2 →
     IntoAnd p (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 90.
   Proof. intros. apply mk_into_and_sep. by rewrite (is_op a) auth_own_op. Qed.
+*)
 
   Lemma auth_own_mono γ a b : a ≼ b → auth_own γ b ⊢ auth_own γ a.
   Proof. intros [? ->]. by rewrite auth_own_op sep_elim_l. Qed.

theories/base_logic/lib/boxes.v

 From iris.base_logic.lib Require Export invariants.
 From iris.algebra Require Import auth gmap agree.
-From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 Import uPred.
@@ -101,7 +100,7 @@ Qed.
 
 Lemma box_alloc : box N ∅ True%I.
 Proof.
-  iIntros; iExists (λ _, True)%I; iSplit; last done.
+  iIntros; iExists (λ _, True)%I; iSplit; last by auto.
   iNext. by rewrite big_opM_empty.
 Qed.
 
@@ -209,11 +208,11 @@ Lemma box_fill E f P :
 Proof.
   iIntros (?) "H HP"; iDestruct "H" as (Φ) "[#HeqP Hf]".
   iExists Φ; iSplitR; first by rewrite big_opM_fmap.
-  rewrite internal_eq_iff later_iff big_opM_commute.
+  rewrite internal_eq_iff later_iff big_sepM_later.
   iDestruct ("HeqP" with "HP") as "HP".
   iCombine "Hf" "HP" as "Hf".
   rewrite -big_opM_opM big_opM_fmap; iApply (fupd_big_sepM _ _ f).
-  iApply (@big_sepM_impl with "[$Hf]").
+  iApply (@big_sepM_impl with "Hf").
   iIntros "!#" (γ b' ?) "[(Hγ' & #$ & #$) HΦ]".
   iInv N as (b) "[>Hγ _]" "Hclose".
   iMod (box_own_auth_update γ with "[Hγ Hγ']") as "[Hγ $]"; first by iFrame.
@@ -238,7 +237,7 @@ Proof.
     iMod ("Hclose" with "[Hγ]"); first (iNext; iExists false; iFrame; eauto).
     iFrame "HγΦ Hinv". by iApply "HΦ". }
   iModIntro; iSplitL "HΦ".
-  - rewrite internal_eq_iff later_iff big_opM_commute. by iApply "HeqP".
+  - rewrite internal_eq_iff later_iff big_sepM_later. by iApply "HeqP".
   - iExists Φ; iSplit; by rewrite big_opM_fmap.
 Qed.
 
@@ -273,7 +272,7 @@ Proof.
     iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
     { by eapply lookup_insert_None. }
     { by apply (lookup_insert_None (delete γ f) γ1 γ2 true). }
-    iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
+    iNext. eapply internal_eq_rewrite_contractive'; [by apply _| |by eauto].
     iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
   - iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; try done.
     iMod (slice_insert_empty with "Hbox") as (γ1 ?) "[#Hslice1 Hbox]".
@@ -281,7 +280,7 @@ Proof.
     iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
     { by eapply lookup_insert_None. }
     { by apply (lookup_insert_None (delete γ f) γ1 γ2 false). }
-    iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
+    iNext. eapply internal_eq_rewrite_contractive'; [by apply _| |by eauto].
     iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
 Qed.
 
@@ -298,14 +297,14 @@ Proof.
     iMod (slice_insert_full _ _ _ _ (Q1 ∗ Q2)%I with "[$HQ1 $HQ2] Hbox")
       as (γ ?) "[#Hslice Hbox]"; first done.
     iExists γ. iIntros "{$% $#} !>". iNext.
-    eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
+    eapply internal_eq_rewrite_contractive'; [by apply _| |by eauto].
     iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
   - iMod (slice_delete_empty with "Hslice1 Hbox") as (P1) "(Heq1 & Hbox)"; try done.
     iMod (slice_delete_empty with "Hslice2 Hbox") as (P2) "(Heq2 & Hbox)"; first done.
     { by simplify_map_eq. }
     iMod (slice_insert_empty with "Hbox") as (γ ?) "[#Hslice Hbox]".
     iExists γ. iIntros "{$% $#} !>". iNext.
-    eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
+    eapply internal_eq_rewrite_contractive'; [by apply _| |by eauto].
     iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
 Qed.
 End box.

theories/base_logic/lib/cancelable_invariants.v

-From iris.base_logic.lib Require Export invariants fractional.
+From iris.base_logic.lib Require Export invariants.
+From iris.bi Require Import fractional.
 From iris.algebra Require Export frac.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".

theories/base_logic/lib/counter_examples.v

-From iris.base_logic Require Import base_logic soundness.
+From iris.base_logic Require Import base_logic soundness proofmode.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type*".
 
@@ -7,7 +7,7 @@ name-dependent allocation. *)
 Module savedprop. Section savedprop.
   Context (M : ucmraT).
   Notation iProp := (uPred M).
-  Notation "¬ P" := (□ (P → False))%I : uPred_scope.
+  Notation "¬ P" := (□ (P → False))%I : bi_scope.
   Implicit Types P : iProp.
 
   (** Saved Propositions and the update modality *)
@@ -41,7 +41,7 @@ Module savedprop. Section savedprop.
   Lemma contradiction : False.
   Proof using All.
     apply (@soundness M False 1); simpl.
-    iIntros "". iMod A_alloc as (i) "#H".
+    iMod A_alloc as (i) "#H".
     iPoseProof (saved_NA with "H") as "HN".
     iModIntro. iNext.
     iApply "HN". iApply saved_A. done.
@@ -108,25 +108,25 @@ Module inv. Section inv.
   Proof. intros P Q ?. by apply fupd_mono. Qed.
   Instance fupd_proper E : Proper ((⊣⊢) ==> (⊣⊢)) (fupd E).
   Proof.
-    intros P Q; rewrite !uPred.equiv_spec=> -[??]; split; by apply fupd_mono.
+    intros P Q; rewrite !bi.equiv_spec=> -[??]; split; by apply fupd_mono.
   Qed.
 
   Lemma fupd_frame_r E P Q : fupd E P ∗ Q ⊢ fupd E (P ∗ Q).
   Proof. by rewrite comm fupd_frame_l comm. Qed.
 
   Global Instance elim_fupd_fupd E P Q : ElimModal (fupd E P) P (fupd E Q) (fupd E Q).
-  Proof. by rewrite /ElimModal fupd_frame_r uPred.wand_elim_r fupd_fupd. Qed.
+  Proof. by rewrite /ElimModal fupd_frame_r bi.wand_elim_r fupd_fupd. Qed.
 
   Global Instance elim_fupd0_fupd1 P Q : ElimModal (fupd M0 P) P (fupd M1 Q) (fupd M1 Q).
   Proof.
-    by rewrite /ElimModal fupd_frame_r uPred.wand_elim_r fupd_mask_mono fupd_fupd.
+    by rewrite /ElimModal fupd_frame_r bi.wand_elim_r fupd_mask_mono fupd_fupd.
   Qed.
 
   Global Instance exists_split_fupd0 {A} E P (Φ : A → iProp) :
     FromExist P Φ → FromExist (fupd E P) (λ a, fupd E (Φ a)).
   Proof.
-    rewrite /FromExist=>HP. apply uPred.exist_elim=> a.
-    apply fupd_mono. by rewrite -HP -(uPred.exist_intro a).
+    rewrite /FromExist=>HP. apply bi.exist_elim=> a.
+    apply fupd_mono. by rewrite -HP -(bi.exist_intro a).
   Qed.
 
   (** Now to the actual counterexample. We start with a weird form of saved propositions. *)
@@ -163,7 +163,7 @@ Module inv. Section inv.
   Qed.
 
   (** And now we tie a bad knot. *)
-  Notation "¬ P" := (□ (P -∗ fupd M1 False))%I : uPred_scope.
+  Notation "¬ P" := (□ (P -∗ fupd M1 False))%I : bi_scope.
   Definition A i : iProp := ∃ P, ¬P ∗ saved i P.
   Global<