excl.v 6.66 KB
Newer Older
 Robbert Krebbers committed Mar 10, 2016 1 2 ``````From iris.algebra Require Export cmra. From iris.algebra Require Import upred. `````` Robbert Krebbers committed Nov 22, 2015 3 4 ``````Local Arguments validN _ _ _ !_ /. Local Arguments valid _ _ !_ /. `````` Robbert Krebbers committed Nov 11, 2015 5 6 7 8 9 10 `````` Inductive excl (A : Type) := | Excl : A → excl A | ExclBot : excl A. Arguments Excl {_} _. Arguments ExclBot {_}. `````` Robbert Krebbers committed May 28, 2016 11 12 13 14 `````` Notation Excl' x := (Some (Excl x)). Notation ExclBot' := (Some ExclBot). `````` Robbert Krebbers committed Nov 22, 2015 15 16 ``````Instance maybe_Excl {A} : Maybe (@Excl A) := λ x, match x with Excl a => Some a | _ => None end. `````` Robbert Krebbers committed Nov 11, 2015 17 `````` `````` Robbert Krebbers committed Jan 14, 2016 18 19 ``````Section excl. Context {A : cofeT}. `````` Robbert Krebbers committed Feb 26, 2016 20 21 ``````Implicit Types a b : A. Implicit Types x y : excl A. `````` Robbert Krebbers committed Jan 14, 2016 22 `````` `````` Robbert Krebbers committed Nov 22, 2015 23 ``````(* Cofe *) `````` Robbert Krebbers committed Jan 14, 2016 24 ``````Inductive excl_equiv : Equiv (excl A) := `````` Robbert Krebbers committed Feb 26, 2016 25 `````` | Excl_equiv a b : a ≡ b → Excl a ≡ Excl b `````` Robbert Krebbers committed Nov 11, 2015 26 27 `````` | ExclBot_equiv : ExclBot ≡ ExclBot. Existing Instance excl_equiv. `````` Robbert Krebbers committed Feb 26, 2016 28 ``````Inductive excl_dist : Dist (excl A) := `````` Robbert Krebbers committed Feb 26, 2016 29 `````` | Excl_dist a b n : a ≡{n}≡ b → Excl a ≡{n}≡ Excl b `````` Ralf Jung committed Feb 10, 2016 30 `````` | ExclBot_dist n : ExclBot ≡{n}≡ ExclBot. `````` Robbert Krebbers committed Nov 22, 2015 31 ``````Existing Instance excl_dist. `````` Robbert Krebbers committed Feb 26, 2016 32 `````` `````` Robbert Krebbers committed Feb 18, 2016 33 ``````Global Instance Excl_ne n : Proper (dist n ==> dist n) (@Excl A). `````` Robbert Krebbers committed Feb 02, 2016 34 35 36 ``````Proof. by constructor. Qed. Global Instance Excl_proper : Proper ((≡) ==> (≡)) (@Excl A). Proof. by constructor. Qed. `````` Robbert Krebbers committed Feb 11, 2016 37 ``````Global Instance Excl_inj : Inj (≡) (≡) (@Excl A). `````` Robbert Krebbers committed Feb 02, 2016 38 ``````Proof. by inversion_clear 1. Qed. `````` Robbert Krebbers committed Feb 11, 2016 39 ``````Global Instance Excl_dist_inj n : Inj (dist n) (dist n) (@Excl A). `````` Robbert Krebbers committed Feb 02, 2016 40 ``````Proof. by inversion_clear 1. Qed. `````` Robbert Krebbers committed Feb 26, 2016 41 `````` `````` Robbert Krebbers committed Mar 19, 2016 42 ``````Program Definition excl_chain (c : chain (excl A)) (a : A) : chain A := `````` Robbert Krebbers committed Feb 26, 2016 43 `````` {| chain_car n := match c n return _ with Excl y => y | _ => a end |}. `````` Robbert Krebbers committed Mar 19, 2016 44 ``````Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed. `````` Robbert Krebbers committed Jan 14, 2016 45 ``````Instance excl_compl : Compl (excl A) := λ c, `````` Robbert Krebbers committed Mar 19, 2016 46 `````` match c 0 with Excl a => Excl (compl (excl_chain c a)) | x => x end. `````` Robbert Krebbers committed Jan 14, 2016 47 ``````Definition excl_cofe_mixin : CofeMixin (excl A). `````` Robbert Krebbers committed Nov 22, 2015 48 49 ``````Proof. split. `````` Robbert Krebbers committed Feb 26, 2016 50 `````` - intros x y; split; [by destruct 1; constructor; apply equiv_dist|]. `````` Robbert Krebbers committed Nov 22, 2015 51 52 `````` intros Hxy; feed inversion (Hxy 1); subst; constructor; apply equiv_dist. by intros n; feed inversion (Hxy n). `````` Robbert Krebbers committed Feb 17, 2016 53 `````` - intros n; split. `````` Robbert Krebbers committed Feb 26, 2016 54 `````` + by intros []; constructor. `````` Robbert Krebbers committed Nov 22, 2015 55 `````` + by destruct 1; constructor. `````` Ralf Jung committed Feb 20, 2016 56 `````` + destruct 1; inversion_clear 1; constructor; etrans; eauto. `````` Robbert Krebbers committed Feb 17, 2016 57 `````` - by inversion_clear 1; constructor; apply dist_S. `````` Robbert Krebbers committed Mar 19, 2016 58 59 60 `````` - intros n c; rewrite /compl /excl_compl. feed inversion (chain_cauchy c 0 n); first auto with lia; constructor. rewrite (conv_compl n (excl_chain c _)) /=. destruct (c n); naive_solver. `````` Robbert Krebbers committed Nov 22, 2015 61 ``````Qed. `````` Robbert Krebbers committed May 25, 2016 62 ``````Canonical Structure exclC : cofeT := CofeT (excl A) excl_cofe_mixin. `````` Robbert Krebbers committed Feb 24, 2016 63 64 65 66 ``````Global Instance excl_discrete : Discrete A → Discrete exclC. Proof. by inversion_clear 2; constructor; apply (timeless _). Qed. Global Instance excl_leibniz : LeibnizEquiv A → LeibnizEquiv (excl A). Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed. `````` Robbert Krebbers committed Jan 14, 2016 67 `````` `````` Robbert Krebbers committed Feb 26, 2016 68 ``````Global Instance Excl_timeless a : Timeless a → Timeless (Excl a). `````` Robbert Krebbers committed Dec 11, 2015 69 ``````Proof. by inversion_clear 2; constructor; apply (timeless _). Qed. `````` Robbert Krebbers committed Jan 14, 2016 70 ``````Global Instance ExclBot_timeless : Timeless (@ExclBot A). `````` Robbert Krebbers committed Dec 11, 2015 71 ``````Proof. by inversion_clear 1; constructor. Qed. `````` Robbert Krebbers committed Nov 22, 2015 72 73 `````` (* CMRA *) `````` Robbert Krebbers committed Feb 24, 2016 74 ``````Instance excl_valid : Valid (excl A) := λ x, `````` Robbert Krebbers committed May 28, 2016 75 `````` match x with Excl _ => True | ExclBot => False end. `````` Robbert Krebbers committed Jan 14, 2016 76 ``````Instance excl_validN : ValidN (excl A) := λ n x, `````` Robbert Krebbers committed May 28, 2016 77 78 79 `````` match x with Excl _ => True | ExclBot => False end. Instance excl_pcore : PCore (excl A) := λ _, None. Instance excl_op : Op (excl A) := λ x y, ExclBot. `````` Robbert Krebbers committed Mar 11, 2016 80 `````` `````` Robbert Krebbers committed May 27, 2016 81 ``````Lemma excl_cmra_mixin : CMRAMixin (excl A). `````` Robbert Krebbers committed Nov 11, 2015 82 ``````Proof. `````` Robbert Krebbers committed May 28, 2016 83 `````` split; try discriminate. `````` Robbert Krebbers committed Feb 17, 2016 84 85 `````` - by intros n []; destruct 1; constructor. - by destruct 1; intros ?. `````` Robbert Krebbers committed Feb 24, 2016 86 `````` - intros x; split. done. by move=> /(_ 0). `````` Robbert Krebbers committed May 28, 2016 87 88 89 90 `````` - intros n [?|]; simpl; auto with lia. - by intros [?|] [?|] [?|]; constructor. - by intros [?|] [?|]; constructor. - by intros n [?|] [?|]. `````` Robbert Krebbers committed Aug 14, 2016 91 `````` - intros n x [?|] [?|] ?; inversion_clear 1; eauto. `````` Robbert Krebbers committed Nov 11, 2015 92 ``````Qed. `````` Robbert Krebbers committed May 27, 2016 93 ``````Canonical Structure exclR := `````` Robbert Krebbers committed May 25, 2016 94 `````` CMRAT (excl A) excl_cofe_mixin excl_cmra_mixin. `````` Robbert Krebbers committed May 27, 2016 95 `````` `````` Robbert Krebbers committed Mar 01, 2016 96 ``````Global Instance excl_cmra_discrete : Discrete A → CMRADiscrete exclR. `````` Robbert Krebbers committed Feb 24, 2016 97 98 ``````Proof. split. apply _. by intros []. Qed. `````` Robbert Krebbers committed Feb 13, 2016 99 100 ``````(** Internalized properties *) Lemma excl_equivI {M} (x y : excl A) : `````` Robbert Krebbers committed May 31, 2016 101 102 103 104 105 `````` x ≡ y ⊣⊢ (match x, y with | Excl a, Excl b => a ≡ b | ExclBot, ExclBot => True | _, _ => False end : uPred M). `````` Robbert Krebbers committed Feb 25, 2016 106 107 108 ``````Proof. uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor. Qed. `````` Robbert Krebbers committed Feb 13, 2016 109 ``````Lemma excl_validI {M} (x : excl A) : `````` Robbert Krebbers committed May 28, 2016 110 `````` ✓ x ⊣⊢ (if x is ExclBot then False else True : uPred M). `````` Robbert Krebbers committed Feb 25, 2016 111 ``````Proof. uPred.unseal. by destruct x. Qed. `````` Robbert Krebbers committed Feb 13, 2016 112 `````` `````` Jacques-Henri Jourdan committed May 31, 2016 113 114 115 ``````(** Exclusive *) Global Instance excl_exclusive x : Exclusive x. Proof. by destruct x; intros n []. Qed. `````` Robbert Krebbers committed May 28, 2016 116 117 118 119 120 121 122 123 124 125 126 `````` (** Option excl *) Lemma excl_validN_inv_l n mx a : ✓{n} (Excl' a ⋅ mx) → mx = None. Proof. by destruct mx. Qed. Lemma excl_validN_inv_r n mx a : ✓{n} (mx ⋅ Excl' a) → mx = None. Proof. by destruct mx. Qed. Lemma Excl_includedN n a mx : ✓{n} mx → Excl' a ≼{n} mx ↔ mx ≡{n}≡ Excl' a. Proof. intros Hvalid; split; [|by intros ->]. intros [z ?]; cofe_subst. by rewrite (excl_validN_inv_l n z a). Qed. `````` Robbert Krebbers committed Jan 14, 2016 127 128 129 ``````End excl. Arguments exclC : clear implicits. `````` Robbert Krebbers committed Mar 01, 2016 130 ``````Arguments exclR : clear implicits. `````` Robbert Krebbers committed Nov 11, 2015 131 `````` `````` Robbert Krebbers committed Nov 22, 2015 132 ``````(* Functor *) `````` Robbert Krebbers committed Feb 04, 2016 133 ``````Definition excl_map {A B} (f : A → B) (x : excl A) : excl B := `````` Robbert Krebbers committed May 28, 2016 134 `````` match x with Excl a => Excl (f a) | ExclBot => ExclBot end. `````` Robbert Krebbers committed Feb 04, 2016 135 ``````Lemma excl_map_id {A} (x : excl A) : excl_map id x = x. `````` Robbert Krebbers committed Jan 19, 2016 136 ``````Proof. by destruct x. Qed. `````` Robbert Krebbers committed Feb 04, 2016 137 138 ``````Lemma excl_map_compose {A B C} (f : A → B) (g : B → C) (x : excl A) : excl_map (g ∘ f) x = excl_map g (excl_map f x). `````` Robbert Krebbers committed Jan 19, 2016 139 ``````Proof. by destruct x. Qed. `````` Robbert Krebbers committed Feb 04, 2016 140 141 142 ``````Lemma excl_map_ext {A B : cofeT} (f g : A → B) x : (∀ x, f x ≡ g x) → excl_map f x ≡ excl_map g x. Proof. by destruct x; constructor. Qed. `````` Robbert Krebbers committed May 28, 2016 143 ``````Instance excl_map_ne {A B : cofeT} n : `````` Robbert Krebbers committed Feb 04, 2016 144 `````` Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@excl_map A B). `````` Robbert Krebbers committed Nov 22, 2015 145 ``````Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed. `````` Robbert Krebbers committed Feb 04, 2016 146 147 ``````Instance excl_map_cmra_monotone {A B : cofeT} (f : A → B) : (∀ n, Proper (dist n ==> dist n) f) → CMRAMonotone (excl_map f). `````` Robbert Krebbers committed Nov 22, 2015 148 ``````Proof. `````` Robbert Krebbers committed Feb 26, 2016 149 `````` split; try apply _. `````` Robbert Krebbers committed May 28, 2016 150 `````` - by intros n [a|]. `````` Robbert Krebbers committed Feb 26, 2016 151 152 `````` - intros x y [z Hy]; exists (excl_map f z); apply equiv_dist=> n. move: Hy=> /equiv_dist /(_ n) ->; by destruct x, z. `````` Robbert Krebbers committed Nov 22, 2015 153 ``````Qed. `````` Robbert Krebbers committed Feb 04, 2016 154 ``````Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B := `````` Robbert Krebbers committed Feb 04, 2016 155 `````` CofeMor (excl_map f). `````` Robbert Krebbers committed Feb 04, 2016 156 ``````Instance exclC_map_ne A B n : Proper (dist n ==> dist n) (@exclC_map A B). `````` Robbert Krebbers committed Nov 22, 2015 157 ``````Proof. by intros f f' Hf []; constructor; apply Hf. Qed. `````` Ralf Jung committed Feb 05, 2016 158 `````` `````` Robbert Krebbers committed May 28, 2016 159 160 161 ``````Program Definition exclRF (F : cFunctor) : rFunctor := {| rFunctor_car A B := (exclR (cFunctor_car F A B)); rFunctor_map A1 A2 B1 B2 fg := exclC_map (cFunctor_map F fg) `````` Robbert Krebbers committed Mar 02, 2016 162 ``````|}. `````` Robbert Krebbers committed Mar 07, 2016 163 164 165 ``````Next Obligation. intros F A1 A2 B1 B2 n x1 x2 ??. by apply exclC_map_ne, cFunctor_ne. Qed. `````` Robbert Krebbers committed Mar 06, 2016 166 167 168 169 170 171 172 173 ``````Next Obligation. intros F A B x; simpl. rewrite -{2}(excl_map_id x). apply excl_map_ext=>y. by rewrite cFunctor_id. Qed. Next Obligation. intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -excl_map_compose. apply excl_map_ext=>y; apply cFunctor_compose. Qed. `````` Ralf Jung committed Mar 07, 2016 174 `````` `````` Robbert Krebbers committed May 28, 2016 175 176 ``````Instance exclRF_contractive F : cFunctorContractive F → rFunctorContractive (exclRF F). `````` Ralf Jung committed Mar 07, 2016 177 ``````Proof. `````` Robbert Krebbers committed Mar 07, 2016 178 `````` intros A1 A2 B1 B2 n x1 x2 ??. by apply exclC_map_ne, cFunctor_contractive. `````` Ralf Jung committed Mar 07, 2016 179 ``Qed.``