From 26534645a1750d6ceb50f80901af7969cfd2a0c4 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Thu, 14 Jun 2018 10:14:52 +0200 Subject: [PATCH] monpred wand/impl framing: don't require indices to match syntactically --- theories/proofmode/monpred.v | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v index da749dc6f..68920fb9a 100644 --- a/theories/proofmode/monpred.v +++ b/theories/proofmode/monpred.v @@ -370,18 +370,22 @@ Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_and. Qed. Global Instance frame_monPred_at_or p P Q ð“¡ ð“ i : Frame p ð“¡ (P i ∨ Q i) ð“ → FrameMonPredAt p i ð“¡ (P ∨ Q) ð“ . Proof. rewrite /Frame /FrameMonPredAt=> ->. by rewrite monPred_at_or. Qed. -Global Instance frame_monPred_at_wand p P R Q1 Q2 i : - Frame p R Q1 Q2 → FrameMonPredAt p i (R i) (P -∗ Q1) ((P -∗ Q2) i). +Global Instance frame_monPred_at_wand p P R Q1 Q2 i j : + IsBiIndexRel i j → + Frame p R Q1 Q2 → + FrameMonPredAt p j (R i) (P -∗ Q1) ((P -∗ Q2) i). Proof. - rewrite /Frame /FrameMonPredAt=>Hframe. + rewrite /Frame /FrameMonPredAt=>-> Hframe. rewrite -monPred_at_intuitionistically_if -monPred_at_sep. apply monPred_in_entails. change ((â–¡?p R ∗ (P -∗ Q2)) -∗ P -∗ Q1). apply bi.wand_intro_r. rewrite -assoc bi.wand_elim_l. done. Qed. -Global Instance frame_monPred_at_impl P R Q1 Q2 i : - Frame true R Q1 Q2 → FrameMonPredAt true i (R i) (P → Q1) ((P → Q2) i). +Global Instance frame_monPred_at_impl P R Q1 Q2 i j : + IsBiIndexRel i j → + Frame true R Q1 Q2 → + FrameMonPredAt true j (R i) (P → Q1) ((P → Q2) i). Proof. - rewrite /Frame /FrameMonPredAt=>Hframe. + rewrite /Frame /FrameMonPredAt=>-> Hframe. rewrite -monPred_at_intuitionistically_if -monPred_at_sep. apply monPred_in_entails. change ((â–¡ R ∗ (P → Q2)) -∗ P → Q1). rewrite -bi.persistently_and_intuitionistically_sep_l. apply bi.impl_intro_r. -- GitLab