base_logic.v 3.12 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 4
From iris.proofmode Require Import tactics.
From iris.algebra Require Import proofmode_classes.
5
Set Default Proof Using "Type".
6

7 8 9
(* 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 *)
10 11 12
Module Import uPred.
  Export upred.uPred.
  Export derived.uPred.
Robbert Krebbers's avatar
Robbert Krebbers committed
13
  Export bi.
14 15 16
End uPred.

(* Hint DB for the logic *)
17
Hint Resolve pure_intro : I.
18 19
Hint Resolve or_elim or_intro_l' or_intro_r' : I.
Hint Resolve and_intro and_elim_l' and_elim_r' : I.
20
Hint Resolve persistently_mono : I.
Robbert Krebbers's avatar
Robbert Krebbers committed
21
Hint Resolve sep_mono : I. (* sep_elim_l' sep_elim_r'  *)
22
Hint Immediate True_intro False_elim : I.
Robbert Krebbers's avatar
Robbert Krebbers committed
23
Hint Immediate iff_refl internal_eq_refl : I.
24 25 26 27 28 29 30 31 32 33

(* 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.

34 35
Global Instance from_pure_cmra_valid {A : cmraT} (a : A) :
  @FromPure (uPredI M) ( a) ( a).
36
Proof.
37
  rewrite /FromPure. eapply bi.pure_elim; [done|]=> ?.
38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83
  rewrite -cmra_valid_intro //. by apply pure_intro.
Qed.

(* FromOp *)
(* TODO: Worst case there could be a lot of backtracking on these instances,
try to refactor. *)
Global Instance is_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
  IsOp a b1 b2  IsOp a' b1' b2'  IsOp' (a,a') (b1,b1') (b2,b2').
Proof. by constructor. Qed.
Global Instance is_op_pair_core_id_l {A B : cmraT} (a : A) (a' b1' b2' : B) :
  CoreId  a  IsOp a' b1' b2'  IsOp' (a,a') (a,b1') (a,b2').
Proof. constructor=> //=. by rewrite -core_id_dup. Qed.
Global Instance is_op_pair_core_id_r {A B : cmraT} (a b1 b2 : A) (a' : B) :
  CoreId a'  IsOp a b1 b2  IsOp' (a,a') (b1,a') (b2,a').
Proof. constructor=> //=. by rewrite -core_id_dup. Qed.

Global Instance is_op_Some {A : cmraT} (a : A) b1 b2 :
  IsOp a b1 b2  IsOp' (Some a) (Some b1) (Some b2).
Proof. by constructor. Qed.
(* This one has a higher precendence than [is_op_op] so we get a [+] instead of
an [⋅]. *)
Global Instance is_op_plus (n1 n2 : nat) : IsOp (n1 + n2) n1 n2.
Proof. done. 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.
  intros. apply affinely_persistently_if_mono. by rewrite (is_op a) ownM_op sep_and.
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.