excl.v 7.35 KB
 Robbert Krebbers committed Feb 04, 2016 1 ``````Require Export algebra.cmra. `````` Robbert Krebbers committed Feb 11, 2016 2 ``````Require Import algebra.functor. `````` Robbert Krebbers committed Nov 22, 2015 3 4 ``````Local Arguments validN _ _ _ !_ /. Local Arguments valid _ _ !_ /. `````` Robbert Krebbers committed Nov 11, 2015 5 6 7 `````` Inductive excl (A : Type) := | Excl : A → excl A `````` Robbert Krebbers committed Nov 22, 2015 8 `````` | ExclUnit : excl A `````` Robbert Krebbers committed Nov 11, 2015 9 10 11 12 `````` | ExclBot : excl A. Arguments Excl {_} _. Arguments ExclUnit {_}. Arguments ExclBot {_}. `````` Robbert Krebbers committed Nov 22, 2015 13 14 ``````Instance maybe_Excl {A} : Maybe (@Excl A) := λ x, match x with Excl a => Some a | _ => None end. `````` Robbert Krebbers committed Nov 11, 2015 15 `````` `````` Robbert Krebbers committed Jan 14, 2016 16 17 18 ``````Section excl. Context {A : cofeT}. `````` Robbert Krebbers committed Nov 22, 2015 19 ``````(* Cofe *) `````` Robbert Krebbers committed Jan 14, 2016 20 ``````Inductive excl_equiv : Equiv (excl A) := `````` Robbert Krebbers committed Nov 11, 2015 21 `````` | Excl_equiv (x y : A) : x ≡ y → Excl x ≡ Excl y `````` Robbert Krebbers committed Nov 22, 2015 22 `````` | ExclUnit_equiv : ExclUnit ≡ ExclUnit `````` Robbert Krebbers committed Nov 11, 2015 23 24 `````` | ExclBot_equiv : ExclBot ≡ ExclBot. Existing Instance excl_equiv. `````` Robbert Krebbers committed Nov 22, 2015 25 ``````Inductive excl_dist `{Dist A} : Dist (excl A) := `````` Ralf Jung committed Feb 10, 2016 26 27 28 `````` | Excl_dist (x y : A) n : x ≡{n}≡ y → Excl x ≡{n}≡ Excl y | ExclUnit_dist n : ExclUnit ≡{n}≡ ExclUnit | ExclBot_dist n : ExclBot ≡{n}≡ ExclBot. `````` Robbert Krebbers committed Nov 22, 2015 29 ``````Existing Instance excl_dist. `````` Robbert Krebbers committed Feb 02, 2016 30 31 32 33 34 35 36 37 ``````Global Instance Excl_ne : Proper (dist n ==> dist n) (@Excl A). Proof. by constructor. Qed. Global Instance Excl_proper : Proper ((≡) ==> (≡)) (@Excl A). Proof. by constructor. Qed. Global Instance Excl_inj : Injective (≡) (≡) (@Excl A). Proof. by inversion_clear 1. Qed. Global Instance Excl_dist_inj n : Injective (dist n) (dist n) (@Excl A). Proof. by inversion_clear 1. Qed. `````` Robbert Krebbers committed Jan 14, 2016 38 ``````Program Definition excl_chain `````` Robbert Krebbers committed Nov 22, 2015 39 40 41 `````` (c : chain (excl A)) (x : A) (H : maybe Excl (c 1) = Some x) : chain A := {| chain_car n := match c n return _ with Excl y => y | _ => x end |}. Next Obligation. `````` Robbert Krebbers committed Feb 10, 2016 42 43 44 `````` intros c x ? n [|i] ?; [omega|]; simpl. destruct (c 1) eqn:?; simplify_equality'. by feed inversion (chain_cauchy c n (S i)). `````` Robbert Krebbers committed Nov 22, 2015 45 ``````Qed. `````` Robbert Krebbers committed Jan 14, 2016 46 ``````Instance excl_compl : Compl (excl A) := λ c, `````` Robbert Krebbers committed Nov 22, 2015 47 48 49 `````` match Some_dec (maybe Excl (c 1)) with | inleft (exist x H) => Excl (compl (excl_chain c x H)) | inright _ => c 1 end. `````` Robbert Krebbers committed Jan 14, 2016 50 ``````Definition excl_cofe_mixin : CofeMixin (excl A). `````` Robbert Krebbers committed Nov 22, 2015 51 52 53 54 55 56 57 58 59 60 61 62 63 ``````Proof. split. * intros mx my; split; [by destruct 1; constructor; apply equiv_dist|]. intros Hxy; feed inversion (Hxy 1); subst; constructor; apply equiv_dist. by intros n; feed inversion (Hxy n). * intros n; split. + by intros [x| |]; constructor. + by destruct 1; constructor. + destruct 1; inversion_clear 1; constructor; etransitivity; eauto. * by inversion_clear 1; constructor; apply dist_S. * intros c n; unfold compl, excl_compl. destruct (Some_dec (maybe Excl (c 1))) as [[x Hx]|]. { assert (c 1 = Excl x) by (by destruct (c 1); simplify_equality'). `````` Robbert Krebbers committed Feb 10, 2016 64 65 `````` assert (∃ y, c (S n) = Excl y) as [y Hy]. { feed inversion (chain_cauchy c 0 (S n)); eauto with lia congruence. } `````` Robbert Krebbers committed Nov 22, 2015 66 `````` rewrite Hy; constructor. `````` Robbert Krebbers committed Feb 10, 2016 67 68 69 `````` by rewrite (conv_compl (excl_chain c x Hx) n) /= Hy. } feed inversion (chain_cauchy c 0 (S n)); first lia; constructor; destruct (c 1); simplify_equality'. `````` Robbert Krebbers committed Nov 22, 2015 70 ``````Qed. `````` Robbert Krebbers committed Jan 14, 2016 71 72 73 ``````Canonical Structure exclC : cofeT := CofeT excl_cofe_mixin. Global Instance Excl_timeless (x : A) : Timeless x → Timeless (Excl x). `````` Robbert Krebbers committed Dec 11, 2015 74 ``````Proof. by inversion_clear 2; constructor; apply (timeless _). Qed. `````` Robbert Krebbers committed Jan 14, 2016 75 ``````Global Instance ExclUnit_timeless : Timeless (@ExclUnit A). `````` Robbert Krebbers committed Dec 11, 2015 76 ``````Proof. by inversion_clear 1; constructor. Qed. `````` Robbert Krebbers committed Jan 14, 2016 77 ``````Global Instance ExclBot_timeless : Timeless (@ExclBot A). `````` Robbert Krebbers committed Dec 11, 2015 78 ``````Proof. by inversion_clear 1; constructor. Qed. `````` Robbert Krebbers committed Jan 14, 2016 79 ``````Global Instance excl_timeless : `````` Robbert Krebbers committed Jan 13, 2016 80 81 `````` (∀ x : A, Timeless x) → ∀ x : excl A, Timeless x. Proof. intros ? []; apply _. Qed. `````` Robbert Krebbers committed Jan 16, 2016 82 83 ``````Global Instance excl_leibniz : LeibnizEquiv A → LeibnizEquiv (excl A). Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed. `````` Robbert Krebbers committed Nov 22, 2015 84 85 `````` (* CMRA *) `````` Robbert Krebbers committed Jan 14, 2016 86 ``````Instance excl_validN : ValidN (excl A) := λ n x, `````` Robbert Krebbers committed Feb 10, 2016 87 `````` match x with Excl _ | ExclUnit => True | ExclBot => False end. `````` Robbert Krebbers committed Jan 14, 2016 88 89 90 ``````Global Instance excl_empty : Empty (excl A) := ExclUnit. Instance excl_unit : Unit (excl A) := λ _, ∅. Instance excl_op : Op (excl A) := λ x y, `````` Robbert Krebbers committed Nov 11, 2015 91 92 93 94 95 `````` match x, y with | Excl x, ExclUnit | ExclUnit, Excl x => Excl x | ExclUnit, ExclUnit => ExclUnit | _, _=> ExclBot end. `````` Robbert Krebbers committed Jan 14, 2016 96 ``````Instance excl_minus : Minus (excl A) := λ x y, `````` Robbert Krebbers committed Nov 11, 2015 97 98 99 100 101 `````` match x, y with | _, ExclUnit => x | Excl _, Excl _ => ExclUnit | _, _ => ExclBot end. `````` Robbert Krebbers committed Jan 14, 2016 102 ``````Definition excl_cmra_mixin : CMRAMixin (excl A). `````` Robbert Krebbers committed Nov 11, 2015 103 104 ``````Proof. split. `````` Robbert Krebbers committed Nov 22, 2015 105 `````` * by intros n []; destruct 1; constructor. `````` Robbert Krebbers committed Nov 11, 2015 106 `````` * constructor. `````` Robbert Krebbers committed Feb 10, 2016 107 `````` * by destruct 1; intros ?. `````` Robbert Krebbers committed Nov 22, 2015 108 109 `````` * by destruct 1; inversion_clear 1; constructor. * intros n [?| |]; simpl; auto with lia. `````` Robbert Krebbers committed Nov 11, 2015 110 111 112 113 `````` * by intros [?| |] [?| |] [?| |]; constructor. * by intros [?| |] [?| |]; constructor. * by intros [?| |]; constructor. * constructor. `````` Robbert Krebbers committed Nov 22, 2015 114 115 116 `````` * by intros n [?| |] [?| |]; exists ∅. * by intros n [?| |] [?| |]. * by intros n [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor. `````` Robbert Krebbers committed Nov 11, 2015 117 ``````Qed. `````` Robbert Krebbers committed Jan 14, 2016 118 ``````Definition excl_cmra_extend_mixin : CMRAExtendMixin (excl A). `````` Robbert Krebbers committed Nov 22, 2015 119 ``````Proof. `````` Robbert Krebbers committed Feb 10, 2016 120 `````` intros n x y1 y2 ? Hx. `````` Robbert Krebbers committed Nov 22, 2015 121 122 123 124 125 126 `````` by exists match y1, y2 with | Excl a1, Excl a2 => (Excl a1, Excl a2) | ExclBot, _ => (ExclBot, y2) | _, ExclBot => (y1, ExclBot) | ExclUnit, _ => (ExclUnit, x) | _, ExclUnit => (x, ExclUnit) end; destruct y1, y2; inversion_clear Hx; repeat constructor. Qed. `````` Robbert Krebbers committed Jan 14, 2016 127 128 ``````Canonical Structure exclRA : cmraT := CMRAT excl_cofe_mixin excl_cmra_mixin excl_cmra_extend_mixin. `````` Robbert Krebbers committed Feb 01, 2016 129 130 ``````Global Instance excl_cmra_identity : CMRAIdentity exclRA. Proof. split. done. by intros []. apply _. Qed. `````` Robbert Krebbers committed Feb 10, 2016 131 ``````Lemma excl_validN_inv_l n x y : ✓{n} (Excl x ⋅ y) → y = ∅. `````` Robbert Krebbers committed Jan 16, 2016 132 ``````Proof. by destruct y. Qed. `````` Robbert Krebbers committed Feb 10, 2016 133 ``````Lemma excl_validN_inv_r n x y : ✓{n} (x ⋅ Excl y) → x = ∅. `````` Robbert Krebbers committed Jan 16, 2016 134 ``````Proof. by destruct x. Qed. `````` Ralf Jung committed Feb 10, 2016 135 ``````Lemma Excl_includedN n x y : ✓{n} y → Excl x ≼{n} y ↔ y ≡{n}≡ Excl x. `````` Robbert Krebbers committed Jan 18, 2016 136 ``````Proof. `````` Robbert Krebbers committed Feb 10, 2016 137 `````` intros Hvalid; split; [|by intros ->]. `````` Robbert Krebbers committed Jan 18, 2016 138 139 `````` by intros [z ?]; cofe_subst; rewrite (excl_validN_inv_l n x z). Qed. `````` Robbert Krebbers committed Nov 22, 2015 140 `````` `````` Robbert Krebbers committed Feb 11, 2016 141 142 143 144 145 146 ``````(** ** Local updates *) Global Instance excl_local_update b : LocalUpdate (λ a, if a is Excl _ then True else False) (λ _, Excl b). Proof. split. by intros n y1 y2 Hy. by intros n [a| |] [b'| |]. Qed. (** Updates *) `````` Ralf Jung committed Feb 03, 2016 147 ``````Lemma excl_update (x : A) y : ✓ y → Excl x ~~> y. `````` Robbert Krebbers committed Nov 11, 2015 148 ``````Proof. by destruct y; intros ? [?| |]. Qed. `````` Ralf Jung committed Feb 03, 2016 149 ``````Lemma excl_updateP (P : excl A → Prop) x y : ✓ y → P y → Excl x ~~>: P. `````` Robbert Krebbers committed Feb 02, 2016 150 ``````Proof. intros ?? z n ?; exists y. by destruct y, z as [?| |]. Qed. `````` Robbert Krebbers committed Jan 14, 2016 151 152 153 154 ``````End excl. Arguments exclC : clear implicits. Arguments exclRA : clear implicits. `````` Robbert Krebbers committed Nov 11, 2015 155 `````` `````` Robbert Krebbers committed Nov 22, 2015 156 ``````(* Functor *) `````` Robbert Krebbers committed Feb 04, 2016 157 ``````Definition excl_map {A B} (f : A → B) (x : excl A) : excl B := `````` Robbert Krebbers committed Nov 22, 2015 158 159 160 `````` match x with | Excl a => Excl (f a) | ExclUnit => ExclUnit | ExclBot => ExclBot end. `````` Robbert Krebbers committed Feb 04, 2016 161 ``````Lemma excl_map_id {A} (x : excl A) : excl_map id x = x. `````` Robbert Krebbers committed Jan 19, 2016 162 ``````Proof. by destruct x. Qed. `````` Robbert Krebbers committed Feb 04, 2016 163 164 ``````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 165 ``````Proof. by destruct x. Qed. `````` Robbert Krebbers committed Feb 04, 2016 166 167 168 169 170 ``````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. Instance excl_map_cmra_ne {A B : cofeT} n : Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@excl_map A B). `````` Robbert Krebbers committed Nov 22, 2015 171 ``````Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed. `````` Robbert Krebbers committed Feb 04, 2016 172 173 ``````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 174 175 ``````Proof. split. `````` Robbert Krebbers committed Feb 04, 2016 176 `````` * intros n x y [z Hy]; exists (excl_map f z); rewrite Hy. `````` Robbert Krebbers committed Nov 22, 2015 177 178 179 `````` by destruct x, z; constructor. * by intros n [a| |]. Qed. `````` Robbert Krebbers committed Feb 04, 2016 180 ``````Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B := `````` Robbert Krebbers committed Feb 04, 2016 181 `````` CofeMor (excl_map f). `````` Robbert Krebbers committed Feb 04, 2016 182 ``````Instance exclC_map_ne A B n : Proper (dist n ==> dist n) (@exclC_map A B). `````` Robbert Krebbers committed Nov 22, 2015 183 ``````Proof. by intros f f' Hf []; constructor; apply Hf. Qed. `````` Ralf Jung committed Feb 05, 2016 184 185 186 187 188 `````` Program Definition exclF : iFunctor := {| ifunctor_car := exclRA; ifunctor_map := @exclC_map |}. Next Obligation. by intros A x; rewrite /= excl_map_id. Qed. Next Obligation. by intros A B C f g x; rewrite /= excl_map_compose. Qed.``````