From 7ee248797524e139a116d699155f06cbc327f306 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 4 Jul 2018 00:12:07 +0200
Subject: [PATCH] make sbi_laterN compute and rely on that instead of
 MakeLaterN

With a pretty proof by Robbert
---
 tests/ipm_paper.ref                  |  6 ++++++
 tests/ipm_paper.v                    |  3 +++
 tests/proofmode.ref                  | 25 +++++++++++++++++++++++++
 tests/proofmode.v                    |  6 +++---
 theories/base_logic/bi.v             |  2 +-
 theories/base_logic/derived.v        |  6 ++++++
 theories/bi/derived_connectives.v    |  7 +++++--
 theories/heap_lang/proofmode.v       |  4 ++--
 theories/proofmode/frame_instances.v |  4 ----
 theories/proofmode/reduction.v       |  2 +-
 10 files changed, 52 insertions(+), 13 deletions(-)

diff --git a/tests/ipm_paper.ref b/tests/ipm_paper.ref
index 315580437..9bcb74f82 100644
--- a/tests/ipm_paper.ref
+++ b/tests/ipm_paper.ref
@@ -1,3 +1,5 @@
+"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
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index f423ed213..179183d14 100644
--- a/tests/ipm_paper.v
+++ b/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.
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 0cdf47241..d9611c679 100644
--- a/tests/proofmode.ref
+++ b/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
diff --git a/tests/proofmode.v b/tests/proofmode.v
index f558964ab..48d83b752 100644
--- a/tests/proofmode.v
+++ b/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.
diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index 1b7fdb09d..114d50904 100644
--- a/theories/base_logic/bi.v
+++ b/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.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 8ea72840f..004892b1c 100644
--- a/theories/base_logic/derived.v
+++ b/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.
 
diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index 024ad1291..b6128cb5a 100644
--- a/theories/bi/derived_connectives.v
+++ b/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.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 58b7feee3..15c2f92de 100644
--- a/theories/heap_lang/proofmode.v
+++ b/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 →
diff --git a/theories/proofmode/frame_instances.v b/theories/proofmode/frame_instances.v
index 9dc54746d..3dee777bf 100644
--- a/theories/proofmode/frame_instances.v
+++ b/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.
 
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index 3dd260e5a..79dde2343 100644
--- a/theories/proofmode/reduction.v
+++ b/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 :=
-- 
GitLab