From d59fa2f7ea322672cbff03760d19c011b0f962c5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 23 Jun 2016 23:09:37 +0200
Subject: [PATCH] Use type classes instead of option hack to remove Trues while
 framing.

---
 proofmode/coq_tactics.v | 114 ++++++++++++++++++++++------------------
 proofmode/pviewshifts.v |   5 +-
 proofmode/weakestpre.v  |   6 +--
 3 files changed, 67 insertions(+), 58 deletions(-)

diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index b64ef1f0f..9349e964f 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -796,65 +796,77 @@ Proof.
 Qed.
 
 (** * Framing *)
-(** The [option] is to account for formulas that can be framed entirely, so
-we do not end up with [True]s everywhere. *)
-Class Frame (R P : uPred M) (mQ : option (uPred M)) :=
-  frame : R ★ from_option id True mQ ⊢ P.
+Class Frame (R P Q : uPred M) := frame : R ★ Q ⊢ P.
 Arguments frame : clear implicits.
 
-Global Instance frame_here R : Frame R R None.
+Global Instance frame_here R : Frame R R True.
 Proof. by rewrite /Frame right_id. Qed.
-Global Instance frame_sep_l R P1 P2 mQ :
-  Frame R P1 mQ →
-  Frame R (P1 ★ P2) (Some $ if mQ is Some Q then Q ★ P2 else P2)%I | 9.
-Proof. rewrite /Frame => <-. destruct mQ; simpl; solve_sep_entails. Qed.
-Global Instance frame_sep_r R P1 P2 mQ :
-  Frame R P2 mQ →
-  Frame R (P1 ★ P2) (Some $ if mQ is Some Q then P1 ★ Q else P1)%I | 10.
-Proof. rewrite /Frame => <-. destruct mQ; simpl; solve_sep_entails. Qed.
-Global Instance frame_and_l R P1 P2 mQ :
-  Frame R P1 mQ →
-  Frame R (P1 ∧ P2) (Some $ if mQ is Some Q then Q ∧ P2 else P2)%I | 9.
-Proof. rewrite /Frame => <-. destruct mQ; simpl; eauto 10 with I. Qed.
-Global Instance frame_and_r R P1 P2 mQ :
-  Frame R P2 mQ →
-  Frame R (P1 ∧ P2) (Some $ if mQ is Some Q then P1 ∧ Q else P1)%I | 10.
-Proof. rewrite /Frame => <-. destruct mQ; simpl; eauto 10 with I. Qed.
-Global Instance frame_or R P1 P2 mQ1 mQ2 :
-  Frame R P1 mQ1 → Frame R P2 mQ2 →
-  Frame R (P1 ∨ P2) (match mQ1, mQ2 with
-                     | Some Q1, Some Q2 => Some (Q1 ∨ Q2)%I | _, _ => None
-                     end).
-Proof.
-  rewrite /Frame=> <- <-.
-  destruct mQ1 as [Q1|], mQ2 as [Q2|]; simpl; auto with I.
-  by rewrite -sep_or_l.
-Qed.
-Global Instance frame_later R P mQ :
-  Frame R P mQ → Frame R (▷ P) (if mQ is Some Q then Some (▷ Q) else None)%I.
-Proof.
-  rewrite /Frame=><-.
-  by destruct mQ; rewrite /= later_sep -(later_intro R) ?later_True.
-Qed.
-Global Instance frame_exist {A} R (Φ : A → uPred M) mΨ :
-  (∀ a, Frame R (Φ a) (mΨ a)) →
-  Frame R (∃ x, Φ x) (Some (∃ x, if mΨ x is Some Q then Q else True))%I.
+
+Class MakeSep (P Q PQ : uPred M) := make_sep : P ★ Q ⊣⊢ PQ.
+Global Instance make_sep_true_l P : MakeSep True P P.
+Proof. by rewrite /MakeSep left_id. Qed.
+Global Instance make_sep_true_r P : MakeSep P True P.
+Proof. by rewrite /MakeSep right_id. Qed.
+Global Instance make_sep_fallthrough P Q : MakeSep P Q (P ★ Q) | 100.
+Proof. done. Qed.
+Global Instance frame_sep_l R P1 P2 Q Q' :
+  Frame R P1 Q → MakeSep Q P2 Q' → Frame R (P1 ★ P2) Q' | 9.
+Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
+Global Instance frame_sep_r R P1 P2 Q Q' :
+  Frame R P2 Q → MakeSep P1 Q Q' → Frame R (P1 ★ P2) Q' | 10.
+Proof. rewrite /Frame /MakeSep => <- <-. solve_sep_entails. Qed.
+
+Class MakeAnd (P Q PQ : uPred M) := make_and : P ∧ Q ⊣⊢ PQ.
+Global Instance make_and_true_l P : MakeAnd True P P.
+Proof. by rewrite /MakeAnd left_id. Qed.
+Global Instance make_and_true_r P : MakeAnd P True P.
+Proof. by rewrite /MakeAnd right_id. Qed.
+Global Instance make_and_fallthrough P Q : MakeSep P Q (P ★ Q) | 100.
+Proof. done. Qed.
+Global Instance frame_and_l R P1 P2 Q Q' :
+  Frame R P1 Q → MakeAnd Q P2 Q' → Frame R (P1 ∧ P2) Q' | 9.
+Proof. rewrite /Frame /MakeAnd => <- <-; eauto 10 with I. Qed.
+Global Instance frame_and_r R P1 P2 Q Q' :
+  Frame R P2 Q → MakeAnd P1 Q Q' → Frame R (P1 ∧ P2) Q' | 10.
+Proof. rewrite /Frame /MakeAnd => <- <-; eauto 10 with I. Qed.
+
+Class MakeOr (P Q PQ : uPred M) := make_or : P ∨ Q ⊣⊢ PQ.
+Global Instance make_or_true_l P : MakeOr True P True.
+Proof. by rewrite /MakeOr left_absorb. Qed.
+Global Instance make_or_true_r P : MakeOr P True True.
+Proof. by rewrite /MakeOr right_absorb. Qed.
+Global Instance make_or_fallthrough P Q : MakeOr P Q (P ∨ Q) | 100.
+Proof. done. Qed.
+Global Instance frame_or R P1 P2 Q1 Q2 Q :
+  Frame R P1 Q1 → Frame R P2 Q2 → MakeOr Q1 Q2 Q → Frame R (P1 ∨ P2) Q.
+Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.
+
+Class MakeLater (P lP : uPred M) := make_later : ▷ P ⊣⊢ lP.
+Global Instance make_later_true : MakeLater True True.
+Proof. by rewrite /MakeLater later_True. Qed.
+Global Instance make_later_fallthrough P : MakeLater P (â–· P) | 100.
+Proof. done. Qed.
+
+Global Instance frame_later R P Q Q' :
+  Frame R P Q → MakeLater Q Q' → Frame R (▷ P) Q'.
+Proof.
+  rewrite /Frame /MakeLater=><- <-. by rewrite later_sep -(later_intro R).
+Qed.
+
+Global Instance frame_exist {A} R (Φ Ψ : A → uPred M) :
+  (∀ a, Frame R (Φ a) (Ψ a)) → Frame R (∃ x, Φ x) (∃ x, Ψ x).
 Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
-Global Instance frame_forall {A} R (Φ : A → uPred M) mΨ :
-  (∀ a, Frame R (Φ a) (mΨ a)) →
-  Frame R (∀ x, Φ x) (Some (∀ x, if mΨ x is Some Q then Q else True))%I.
+Global Instance frame_forall {A} R (Φ Ψ : A → uPred M) :
+  (∀ a, Frame R (Φ a) (Ψ a)) → Frame R (∀ x, Φ x) (∀ x, Ψ x).
 Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
 
-Lemma tac_frame Δ Δ' i p R P mQ :
-  envs_lookup_delete i Δ = Some (p, R, Δ') → Frame R P mQ →
-  (if mQ is Some Q then (if p then Δ else Δ') ⊢ Q else True) →
-  Δ ⊢ P.
+Lemma tac_frame Δ Δ' i p R P Q :
+  envs_lookup_delete i Δ = Some (p, R, Δ') → Frame R P Q →
+  ((if p then Δ else Δ') ⊢ Q) → Δ ⊢ P.
 Proof.
   intros [? ->]%envs_lookup_delete_Some ? HQ. destruct p.
-  - rewrite envs_lookup_persistent_sound // always_elim.
-    rewrite -(frame R P). destruct mQ as [Q|]; rewrite ?HQ /=; auto with I.
-  - rewrite envs_lookup_sound //; simpl.
-    rewrite -(frame R P). destruct mQ as [Q|]; rewrite ?HQ /=; auto with I.
+  - by rewrite envs_lookup_persistent_sound // always_elim -(frame R P) HQ.
+  - rewrite envs_lookup_sound //; simpl. by rewrite -(frame R P) HQ.
 Qed.
 
 (** * Disjunction *)
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index f49d3f7a2..5085e6c50 100644
--- a/proofmode/pviewshifts.v
+++ b/proofmode/pviewshifts.v
@@ -21,9 +21,8 @@ Global Instance exists_split_pvs {A} E1 E2 P (Φ : A → iProp Λ Σ) :
 Proof.
   rewrite /ExistSplit=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
 Qed.
-Global Instance frame_pvs E1 E2 R P mQ :
-  Frame R P mQ →
-  Frame R (|={E1,E2}=> P) (Some (|={E1,E2}=> if mQ is Some Q then Q else True))%I.
+Global Instance frame_pvs E1 E2 R P Q :
+  Frame R P Q → Frame R (|={E1,E2}=> P) (|={E1,E2}=> Q).
 Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.
 Global Instance to_wand_pvs E1 E2 R P Q :
   ToWand R P Q → ToWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
diff --git a/proofmode/weakestpre.v b/proofmode/weakestpre.v
index ab3d1f0ea..2e60cd40e 100644
--- a/proofmode/weakestpre.v
+++ b/proofmode/weakestpre.v
@@ -8,10 +8,8 @@ Context {Λ : language} {Σ : iFunctor}.
 Implicit Types P Q : iProp Λ Σ.
 Implicit Types Φ : val Λ → iProp Λ Σ.
 
-Global Instance frame_wp E e R Φ mΨ :
-  (∀ v, Frame R (Φ v) (mΨ v)) →
-  Frame R (WP e @ E {{ Φ }})
-          (Some (WP e @ E {{ v, if mΨ v is Some Q then Q else True }}))%I.
+Global Instance frame_wp E e R Φ Ψ :
+  (∀ v, Frame R (Φ v) (Ψ v)) → Frame R (WP e @ E {{ Φ }}) (WP e @ E {{ Ψ }}).
 Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
 Global Instance fsa_split_wp E e Φ :
   FSASplit (WP e @ E {{ Φ }})%I E (wp_fsa e) (language.atomic e) Φ.
-- 
GitLab