base_logic.v 1.79 KB
Newer Older
1
From iris.base_logic Require Export derived.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From iris.bi Require Export bi.
3
From iris.algebra Require Import proofmode_classes.
4
Set Default Proof Using "Type".
5

6
7
8
(* The trick of having multiple [uPred] modules, which are all exported in
another [uPred] module is by Jason Gross and described in:
https://sympa.inria.fr/sympa/arc/coq-club/2016-12/msg00069.html *)
9
Module Import uPred.
10
  Export base_logic.bi.uPred.
11
  Export derived.uPred.
12
  Export bi.bi.
13
14
End uPred.

15
16
17
18
19
20
21
22
23
(* Setup of the proof mode *)
Section class_instances.
Context {M : ucmraT}.
Implicit Types P Q R : uPred M.

Global Instance into_pure_cmra_valid `{CmraDiscrete A} (a : A) :
  @IntoPure (uPredI M) ( a) ( a).
Proof. by rewrite /IntoPure discrete_valid. Qed.

24
25
Global Instance from_pure_cmra_valid {A : cmraT} af (a : A) :
  @FromPure (uPredI M) af ( a) ( a).
26
Proof.
27
  rewrite /FromPure. eapply bi.pure_elim; [by apply affinely_if_elim|]=> ?.
28
  rewrite -cmra_valid_intro //.
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
Qed.

Global Instance from_sep_ownM (a b1 b2 : M) :
  IsOp a b1 b2 
  FromSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof. intros. by rewrite /FromSep -ownM_op -is_op. Qed.
Global Instance from_sep_ownM_core_id (a b1 b2 : M) :
  IsOp a b1 b2  TCOr (CoreId b1) (CoreId b2) 
  FromAnd (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof.
  intros ? H. rewrite /FromAnd (is_op a) ownM_op.
  destruct H; by rewrite persistent_and_sep.
Qed.

Global Instance into_and_ownM p (a b1 b2 : M) :
  IsOp a b1 b2  IntoAnd p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof.
46
  intros. apply intuitionistically_if_mono. by rewrite (is_op a) ownM_op sep_and.
47
48
49
50
51
52
Qed.

Global Instance into_sep_ownM (a b1 b2 : M) :
  IsOp a b1 b2  IntoSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof. intros. by rewrite /IntoSep (is_op a) ownM_op. Qed.
End class_instances.