derived_connectives.v 4.6 KB
 Jacques-Henri Jourdan committed Dec 04, 2017 1 2 3 4 5 6 7 8 9 10 11 12 13 ``````From iris.bi Require Export interface. From iris.algebra Require Import monoid. From stdpp Require Import hlist. Definition bi_iff {PROP : bi} (P Q : PROP) : PROP := ((P → Q) ∧ (Q → P))%I. Arguments bi_iff {_} _%I _%I : simpl never. Instance: Params (@bi_iff) 1. Infix "↔" := bi_iff : bi_scope. Definition bi_wand_iff {PROP : bi} (P Q : PROP) : PROP := ((P -∗ Q) ∧ (Q -∗ P))%I. Arguments bi_wand_iff {_} _%I _%I : simpl never. Instance: Params (@bi_wand_iff) 1. `````` 14 ``````Infix "∗-∗" := bi_wand_iff : bi_scope. `````` Jacques-Henri Jourdan committed Dec 04, 2017 15 `````` `````` Robbert Krebbers committed Mar 04, 2018 16 ``````Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ P. `````` Jacques-Henri Jourdan committed Dec 04, 2017 17 18 19 20 21 22 23 24 25 ``````Arguments Persistent {_} _%I : simpl never. Arguments persistent {_} _%I {_}. Hint Mode Persistent + ! : typeclass_instances. Instance: Params (@Persistent) 1. Definition bi_affinely {PROP : bi} (P : PROP) : PROP := (emp ∧ P)%I. Arguments bi_affinely {_} _%I : simpl never. Instance: Params (@bi_affinely) 1. Typeclasses Opaque bi_affinely. `````` 26 ``````Notation "'' P" := (bi_affinely P) : bi_scope. `````` Robbert Krebbers committed Mar 04, 2018 27 `````` `````` Jacques-Henri Jourdan committed Dec 04, 2017 28 29 30 31 32 33 ``````Class Affine {PROP : bi} (Q : PROP) := affine : Q ⊢ emp. Arguments Affine {_} _%I : simpl never. Arguments affine {_} _%I {_}. Hint Mode Affine + ! : typeclass_instances. Class BiAffine (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q. `````` Jacques-Henri Jourdan committed Mar 04, 2018 34 ``````Hint Mode BiAffine ! : typeclass_instances. `````` Jacques-Henri Jourdan committed Dec 04, 2017 35 36 37 ``````Existing Instance absorbing_bi | 0. Class BiPositive (PROP : bi) := `````` Robbert Krebbers committed Mar 04, 2018 38 `````` bi_positive (P Q : PROP) : (P ∗ Q) ⊢ P ∗ Q. `````` Jacques-Henri Jourdan committed Mar 04, 2018 39 ``````Hint Mode BiPositive ! : typeclass_instances. `````` Jacques-Henri Jourdan committed Dec 04, 2017 40 41 42 43 44 `````` Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True ∗ P)%I. Arguments bi_absorbingly {_} _%I : simpl never. Instance: Params (@bi_absorbingly) 1. Typeclasses Opaque bi_absorbingly. `````` 45 ``````Notation "'' P" := (bi_absorbingly P) : bi_scope. `````` Jacques-Henri Jourdan committed Dec 04, 2017 46 `````` `````` Robbert Krebbers committed Mar 04, 2018 47 ``````Class Absorbing {PROP : bi} (P : PROP) := absorbing : P ⊢ P. `````` Jacques-Henri Jourdan committed Dec 04, 2017 48 49 ``````Arguments Absorbing {_} _%I : simpl never. Arguments absorbing {_} _%I. `````` Jacques-Henri Jourdan committed Mar 04, 2018 50 ``````Hint Mode Absorbing + ! : typeclass_instances. `````` Jacques-Henri Jourdan committed Dec 04, 2017 51 52 `````` Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP := `````` Robbert Krebbers committed Mar 04, 2018 53 `````` (if p then P else P)%I. `````` Jacques-Henri Jourdan committed Dec 04, 2017 54 55 56 ``````Arguments bi_persistently_if {_} !_ _%I /. Instance: Params (@bi_persistently_if) 2. Typeclasses Opaque bi_persistently_if. `````` 57 ``````Notation "'?' p P" := (bi_persistently_if p P) : bi_scope. `````` Jacques-Henri Jourdan committed Dec 04, 2017 58 59 `````` Definition bi_affinely_if {PROP : bi} (p : bool) (P : PROP) : PROP := `````` Robbert Krebbers committed Mar 04, 2018 60 `````` (if p then P else P)%I. `````` Jacques-Henri Jourdan committed Dec 04, 2017 61 62 63 ``````Arguments bi_affinely_if {_} !_ _%I /. Instance: Params (@bi_affinely_if) 2. Typeclasses Opaque bi_affinely_if. `````` 64 ``````Notation "'?' p P" := (bi_affinely_if p P) : bi_scope. `````` Robbert Krebbers committed Mar 04, 2018 65 `````` `````` 66 67 68 69 70 ``````Definition bi_intuitionistically {PROP : bi} (P : PROP) : PROP := ( P)%I. Arguments bi_intuitionistically {_} _%I : simpl never. Instance: Params (@bi_intuitionistically) 1. Typeclasses Opaque bi_intuitionistically. `````` 71 ``````Notation "□ P" := (bi_intuitionistically P) : bi_scope. `````` 72 73 74 75 76 77 `````` Definition bi_intuitionistically_if {PROP : bi} (p : bool) (P : PROP) : PROP := (if p then □ P else P)%I. Arguments bi_intuitionistically_if {_} !_ _%I /. Instance: Params (@bi_intuitionistically_if) 2. Typeclasses Opaque bi_intuitionistically_if. `````` 78 ``````Notation "'□?' p P" := (bi_intuitionistically_if p P) : bi_scope. `````` Jacques-Henri Jourdan committed Dec 04, 2017 79 80 81 82 83 84 85 86 87 88 89 90 `````` Fixpoint bi_hexist {PROP : bi} {As} : himpl As PROP → PROP := match As return himpl As PROP → PROP with | tnil => id | tcons A As => λ Φ, ∃ x, bi_hexist (Φ x) end%I. Fixpoint bi_hforall {PROP : bi} {As} : himpl As PROP → PROP := match As return himpl As PROP → PROP with | tnil => id | tcons A As => λ Φ, ∀ x, bi_hforall (Φ x) end%I. `````` Ralf Jung committed Jul 04, 2018 91 92 93 94 95 ``````Fixpoint sbi_laterN {PROP : sbi} (n : nat) (P : PROP) : PROP := match n with | O => P | S n' => ▷ sbi_laterN n' P end%I. `````` Jacques-Henri Jourdan committed Dec 04, 2017 96 97 ``````Arguments sbi_laterN {_} !_%nat_scope _%I. Instance: Params (@sbi_laterN) 2. `````` 98 99 ``````Notation "▷^ n P" := (sbi_laterN n P) : bi_scope. Notation "▷? p P" := (sbi_laterN (Nat.b2n p) P) : bi_scope. `````` Jacques-Henri Jourdan committed Dec 04, 2017 100 `````` `````` Jacques-Henri Jourdan committed Dec 04, 2017 101 102 ``````Definition sbi_except_0 {PROP : sbi} (P : PROP) : PROP := (▷ False ∨ P)%I. Arguments sbi_except_0 {_} _%I : simpl never. `````` 103 ``````Notation "◇ P" := (sbi_except_0 P) : bi_scope. `````` Jacques-Henri Jourdan committed Dec 04, 2017 104 105 ``````Instance: Params (@sbi_except_0) 1. Typeclasses Opaque sbi_except_0. `````` Jacques-Henri Jourdan committed Dec 04, 2017 106 107 108 109 110 111 `````` Class Timeless {PROP : sbi} (P : PROP) := timeless : ▷ P ⊢ ◇ P. Arguments Timeless {_} _%I : simpl never. Arguments timeless {_} _%I {_}. Hint Mode Timeless + ! : typeclass_instances. Instance: Params (@Timeless) 1. `````` Ralf Jung committed Jul 02, 2018 112 113 114 115 116 117 118 119 120 121 122 123 `````` (** An optional precondition [mP] to [Q]. TODO: We may actually consider generalizing this to a list of preconditions, and e.g. also using it for texan triples. *) Definition bi_wandM {PROP : bi} (mP : option PROP) (Q : PROP) : PROP := match mP with | None => Q | Some P => (P -∗ Q)%I end. Arguments bi_wandM {_} !_%I _%I /. Notation "mP -∗? Q" := (bi_wandM mP Q) (at level 99, Q at level 200, right associativity) : bi_scope.``````