make sbi_laterN compute and rely on that instead of MakeLaterN

With a pretty proof by Robbert

tests/ipm_paper.ref

+"sep_exist"
+     : string
 1 subgoal
   
   M : ucmraT
@@ -44,6 +46,8 @@ P
   --------------------------------------∗
   P
   
+"sep_exist_short"
+     : string
 1 subgoal
   
   M : ucmraT
@@ -57,6 +61,8 @@ P
   --------------------------------------∗
   ∃ a : A, Ψ a ∗ P
   
+"read_spec"
+     : string
 1 subgoal
   
   Σ : gFunctors

tests/ipm_paper.v

@@ -25,6 +25,7 @@ Section demo.
   Qed.
 
   (* The version in IPM *)
+  Check "sep_exist".
   Lemma sep_exist A (P R: iProp) (Ψ: A → iProp) :
     P ∗ (∃ a, Ψ a) ∗ R ⊢ ∃ a, Ψ a ∗ P.
   Proof.
@@ -35,6 +36,7 @@ Section demo.
   Qed.
 
   (* The short version in IPM, as in the paper *)
+  Check "sep_exist_short".
   Lemma sep_exist_short A (P R: iProp) (Ψ: A → iProp) :
     P ∗ (∃ a, Ψ a) ∗ R ⊢ ∃ a, Ψ a ∗ P.
   Proof. iIntros "[HP [HΨ HR]]". Show. iFrame "HP". iAssumption. Qed.
@@ -235,6 +237,7 @@ Section counter_proof.
       wp_if. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
   Qed.
 
+  Check "read_spec".
   Lemma read_spec l n :
     {{ C l n }} read #l {{ v, ∃ m : nat, ⌜v = #m ∧ n ≤ m⌝ ∧ C l m }}.
   Proof.

tests/proofmode.ref

@@ -59,6 +59,31 @@ In nested Ltac calls to "iSpecialize (open_constr)",
 "iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
 failed.
 Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I with P.
+1 subgoal
+  
+  PROP : sbi
+  P, Q : PROP
+  n, m, k : nat
+  ============================
+  --------------------------------------∗
+  ▷^(S n + S m) emp
+  
+1 subgoal
+  
+  PROP : sbi
+  P, Q : PROP
+  ============================
+  --------------------------------------∗
+  ▷ emp
+  
+1 subgoal
+  
+  PROP : sbi
+  P, Q : PROP
+  ============================
+  --------------------------------------∗
+  ▷ emp
+  
 The command has indeed failed with message:
 In nested Ltac calls to "iFrame (constr)",
 "<iris.proofmode.ltac_tactics.iFrame_go>" and

tests/proofmode.v

@@ -367,7 +367,7 @@ Lemma test_iNext_plus_2 P n m : ▷^n ▷^m P -∗ ▷^(n+m) P.
 Proof. iIntros "H". iNext. done. Qed.
 Lemma test_iNext_plus_3 P Q n m k :
   ▷^m ▷^(2 + S n + k) P -∗ ▷^m ▷ ▷^(2 + S n) Q -∗ ▷^k ▷ ▷^(S (S n + S m)) (P ∗ Q).
-Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Qed.
+Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Show. iModIntro. done. Qed.
 
 Lemma test_iNext_unfold P Q n m (R := (▷^n P)%I) :
   R ⊢ ▷^m True.
@@ -409,10 +409,10 @@ Lemma test_iPureIntro_absorbing (φ : Prop) :
 Proof. intros ?. iPureIntro. done. Qed.
 
 Lemma test_iFrame_later_1 P Q : P ∗ ▷ Q -∗ ▷ (P ∗ ▷ Q).
-Proof. iIntros "H". iFrame "H". auto. Qed.
+Proof. iIntros "H". iFrame "H". Show. auto. Qed.
 
 Lemma test_iFrame_later_2 P Q : ▷ P ∗ ▷ Q -∗ ▷ (▷ P ∗ ▷ Q).
-Proof. iIntros "H". iFrame "H". auto. Qed.
+Proof. iIntros "H". iFrame "H". Show. auto. Qed.
 
 Lemma test_with_ident P Q R : P -∗ Q -∗ (P -∗ Q -∗ R) -∗ R.
 Proof.

theories/base_logic/bi.v

@@ -206,7 +206,7 @@ Lemma ofe_fun_validI `{B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i,
 Proof. exact: uPred_primitive.ofe_fun_validI. Qed.
 
 (** Consistency/soundness statement *)
-Lemma soundness φ n : (▷^n ⌜ φ ⌝ : uPred M)%I → φ.
+Lemma soundness_iter φ n : Nat.iter n sbi_later (⌜ φ ⌝ : uPred M)%I → φ.
 Proof. exact: uPred_primitive.soundness. Qed.
 
 End restate.

theories/base_logic/derived.v

@@ -91,8 +91,14 @@ Global Instance uPred_ownM_sep_homomorphism :
   MonoidHomomorphism op uPred_sep (≡) (@uPred_ownM M).
 Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
 
+(** Iterated later *)
+Lemma laterN_iter n P : (▷^n P)%I = Nat.iter n sbi_later P.
+Proof. induction n; f_equal/=; auto. Qed.
 
 (** Consistency/soundness statement *)
+Lemma soundness φ n : (▷^n ⌜ φ ⌝ : uPred M)%I → φ.
+Proof. rewrite laterN_iter. apply soundness_iter. Qed.
+
 Corollary consistency_modal n : ¬ (▷^n False : uPred M)%I.
 Proof. exact (soundness False n). Qed.
 

theories/bi/derived_connectives.v

@@ -88,8 +88,11 @@ Fixpoint bi_hforall {PROP : bi} {As} : himpl As PROP → PROP :=
   | tcons A As => λ Φ, ∀ x, bi_hforall (Φ x)
   end%I.
 
-Definition sbi_laterN {PROP : sbi} (n : nat) (P : PROP) : PROP :=
-  Nat.iter n sbi_later P.
+Fixpoint sbi_laterN {PROP : sbi} (n : nat) (P : PROP) : PROP :=
+  match n with
+  | O => P
+  | S n' => ▷ sbi_laterN n' P
+  end%I.
 Arguments sbi_laterN {_} !_%nat_scope _%I.
 Instance: Params (@sbi_laterN) 2.
 Notation "▷^ n P" := (sbi_laterN n P) : bi_scope.

theories/heap_lang/proofmode.v

@@ -27,8 +27,8 @@ Tactic Notation "wp_expr_eval" tactic(t) :=
   | _ => fail "wp_expr_eval: not a 'wp'"
   end.
 
-Ltac wp_expr_simpl := wp_expr_eval simpl.
-Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
+Ltac wp_expr_simpl := (wp_expr_eval simpl); pm_prettify.
+Ltac wp_expr_simpl_subst := (wp_expr_eval simpl_subst); pm_prettify.
 
 Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ Φ :
   PureExec φ e1 e2 →

theories/proofmode/frame_instances.v

@@ -287,10 +287,6 @@ Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_True. Qed.
 Global Instance make_laterN_emp `{!BiAffine PROP} n :
   @KnownMakeLaterN PROP n emp emp | 0.
 Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_emp. Qed.
-Global Instance make_laterN_0 P : MakeLaterN 0 P P | 0.
-Proof. by rewrite /MakeLaterN. Qed.
-Global Instance make_laterN_1 P : MakeLaterN 1 P (▷ P) | 2.
-Proof. by rewrite /MakeLaterN. Qed.
 Global Instance make_laterN_default P : MakeLaterN n P (▷^n P) | 100.
 Proof. by rewrite /MakeLaterN. Qed.
 

theories/proofmode/reduction.v

@@ -22,7 +22,7 @@ Declare Reduction pm_cbn := cbn [
   tele_fold tele_bind tele_app
   (* BI connectives *)
   bi_persistently_if bi_affinely_if bi_intuitionistically_if
-  bi_wandM big_opL
+  bi_wandM sbi_laterN big_opL
   bi_tforall bi_texist
 ].
 Ltac pm_eval t :=