vector.v 4.36 KB
 Jacques-Henri Jourdan committed Dec 26, 2016 1 2 3 ``````From iris.prelude Require Export vector. From iris.algebra Require Export ofe. From iris.algebra Require Import list. `````` Ralf Jung committed Jan 05, 2017 4 ``````Set Default Proof Using "Type". `````` Jacques-Henri Jourdan committed Dec 26, 2016 5 6 7 8 9 10 11 12 13 14 `````` Section ofe. Context {A : ofeT}. Instance vec_equiv m : Equiv (vec A m) := equiv (A:=list A). Instance vec_dist m : Dist (vec A m) := dist (A:=list A). Definition vec_ofe_mixin m : OfeMixin (vec A m). Proof. split. `````` Robbert Krebbers committed Jan 22, 2017 15 `````` - intros v w. apply (equiv_dist (A:=listC A)). `````` Jacques-Henri Jourdan committed Dec 26, 2016 16 17 `````` - unfold dist, vec_dist. split. by intros ?. by intros ??. by intros ?????; etrans. `````` Robbert Krebbers committed Jan 22, 2017 18 `````` - intros n v w. by apply (dist_S (A:=listC A)). `````` Jacques-Henri Jourdan committed Dec 26, 2016 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 `````` Qed. Canonical Structure vecC m : ofeT := OfeT (vec A m) (vec_ofe_mixin m). Global Instance vnil_timeless : Timeless (@vnil A). Proof. intros v _. by inv_vec v. Qed. Global Instance vcons_timeless n x (v : vec A n) : Timeless x → Timeless v → Timeless (x ::: v). Proof. intros ?? v' ?. inv_vec v'=>x' v'. inversion_clear 1. constructor. by apply timeless. change (v ≡ v'). by apply timeless. Qed. Global Instance vec_discrete_cofe m : Discrete A → Discrete (vecC m). Proof. intros ? v. induction v; apply _. Qed. End ofe. Arguments vecC : clear implicits. Typeclasses Opaque vec_dist. Section proper. Context {A : ofeT}. Global Instance vcons_ne n : Proper (dist n ==> forall_relation (λ _, dist n ==> dist n)) (@vcons A). Proof. by constructor. Qed. Global Instance vcons_proper : Proper (equiv ==> forall_relation (λ _, equiv ==> equiv)) (@vcons A). Proof. by constructor. Qed. Global Instance vlookup_ne n m : Proper (dist n ==> eq ==> dist n) (@Vector.nth A m). Proof. intros v. induction v as [|x m v IH]; intros v'; inv_vec v'. `````` Robbert Krebbers committed Jan 22, 2017 51 52 `````` - intros _ x. inv_fin x. - intros x' v' EQ i ? <-. inversion_clear EQ. inv_fin i=> // i. by apply IH. `````` Jacques-Henri Jourdan committed Dec 26, 2016 53 54 55 56 `````` Qed. Global Instance vlookup_proper m : Proper (equiv ==> eq ==> equiv) (@Vector.nth A m). Proof. `````` Robbert Krebbers committed Jan 22, 2017 57 `````` intros v v' ? x x' ->. apply equiv_dist=> n. f_equiv. by apply equiv_dist. `````` Jacques-Henri Jourdan committed Dec 26, 2016 58 59 60 61 `````` Qed. Global Instance vec_to_list_ne n m : Proper (dist n ==> dist n) (@vec_to_list A m). `````` Robbert Krebbers committed Jan 22, 2017 62 `````` Proof. by intros v v'. Qed. `````` Jacques-Henri Jourdan committed Dec 26, 2016 63 64 `````` Global Instance vec_to_list_proper m : Proper (equiv ==> equiv) (@vec_to_list A m). `````` Robbert Krebbers committed Jan 22, 2017 65 `````` Proof. by intros v v'. Qed. `````` Jacques-Henri Jourdan committed Dec 26, 2016 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 ``````End proper. Section cofe. Context `{Cofe A}. Global Program Instance list_cofe m : Cofe (vecC A m) := {| compl c := eq_rect _ (vec A) (list_to_vec (compl (chain_map vec_to_list c))) _ _ |}. Next Obligation. intros. by rewrite (conv_compl 0) vec_to_list_length. Qed. Next Obligation. simpl. intros m n c. unfold dist, ofe_dist, vecC, vec_dist. destruct (list_cofe_obligation_1 m c). by rewrite /= vec_to_list_of_list conv_compl. Qed. End cofe. (** Functor *) Definition vec_map {A B : ofeT} m (f : A → B) : vecC A m → vecC B m := @vmap A B f m. Lemma vec_map_ext_ne {A B : ofeT} m (f g : A → B) (v : vec A m) n : (∀ x, f x ≡{n}≡ g x) → vec_map m f v ≡{n}≡ vec_map m g v. Proof. intros Hf. eapply (list_fmap_ext_ne f g v) in Hf. by rewrite -!vec_to_list_map in Hf. Qed. Instance vec_map_ne {A B : ofeT} m f n : Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (@vec_map A B m f). Proof. `````` Robbert Krebbers committed Jan 22, 2017 97 `````` intros ? v v' H. eapply list_fmap_ne in H; last done. `````` Jacques-Henri Jourdan committed Dec 26, 2016 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 `````` by rewrite -!vec_to_list_map in H. Qed. Definition vecC_map {A B : ofeT} m (f : A -n> B) : vecC A m -n> vecC B m := CofeMor (vec_map m f). Instance vecC_map_ne {A A'} m n : Proper (dist n ==> dist n) (@vecC_map A A' m). Proof. intros f g ? v. by apply vec_map_ext_ne. Qed. Program Definition vecCF (F : cFunctor) m : cFunctor := {| cFunctor_car A B := vecC (cFunctor_car F A B) m; cFunctor_map A1 A2 B1 B2 fg := vecC_map m (cFunctor_map F fg) |}. Next Obligation. intros F A1 A2 B1 B2 n m f g Hfg. by apply vecC_map_ne, cFunctor_ne. Qed. Next Obligation. intros F m A B l. change (vec_to_list (vec_map m (cFunctor_map F (cid, cid)) l) ≡ l). rewrite vec_to_list_map. apply listCF. Qed. Next Obligation. intros F m A1 A2 A3 B1 B2 B3 f g f' g' l. change (vec_to_list (vec_map m (cFunctor_map F (f ◎ g, g' ◎ f')) l) ≡ vec_map m (cFunctor_map F (g, g')) (vec_map m (cFunctor_map F (f, f')) l)). rewrite !vec_to_list_map. by apply (cFunctor_compose (listCF F) f g f' g'). Qed. Instance vecCF_contractive F m : cFunctorContractive F → cFunctorContractive (vecCF F m). Proof. by intros ?? A1 A2 B1 B2 n ???; apply vecC_map_ne; first apply cFunctor_contractive. Qed.``````