vector.v 4.01 KB
 Ralf Jung committed Feb 06, 2017 1 ``````From stdpp Require Export vector. `````` Jacques-Henri Jourdan committed Dec 26, 2016 2 3 ``````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 `````` 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). `````` Robbert Krebbers committed Feb 10, 2017 13 14 15 16 `````` Proof. by apply (iso_ofe_mixin vec_to_list). Qed. Canonical Structure vecC m : ofeT := OfeT (vec A m) (vec_ofe_mixin m). Global Instance list_cofe `{Cofe A} m : Cofe (vecC m). `````` Jacques-Henri Jourdan committed Dec 26, 2016 17 `````` Proof. `````` Robbert Krebbers committed Feb 16, 2017 18 `````` apply: (iso_cofe_subtype (λ l : list A, length l = m) `````` Robbert Krebbers committed Feb 10, 2017 19 20 `````` (λ l, eq_rect _ (vec A) (list_to_vec l) m) vec_to_list)=> //. - intros v []. by rewrite /= vec_to_list_of_list. `````` Robbert Krebbers committed Feb 16, 2017 21 `````` - intros c. by rewrite (conv_compl 0 (chain_map _ c)) /= vec_to_list_length. `````` Jacques-Henri Jourdan committed Dec 26, 2016 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 `````` Qed. 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 : `````` Ralf Jung committed Mar 21, 2017 43 `````` Proper (dist n ==> forall_relation (λ x, dist n ==> dist n)) (@vcons A). `````` Jacques-Henri Jourdan committed Dec 26, 2016 44 45 `````` Proof. by constructor. Qed. Global Instance vcons_proper : `````` Ralf Jung committed Mar 21, 2017 46 `````` Proper (equiv ==> forall_relation (λ x, equiv ==> equiv)) (@vcons A). `````` Jacques-Henri Jourdan committed Dec 26, 2016 47 48 49 50 51 52 `````` 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 53 54 `````` - 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 55 56 57 58 `````` Qed. Global Instance vlookup_proper m : Proper (equiv ==> eq ==> equiv) (@Vector.nth A m). Proof. `````` Robbert Krebbers committed Jan 22, 2017 59 `````` intros v v' ? x x' ->. apply equiv_dist=> n. f_equiv. by apply equiv_dist. `````` Jacques-Henri Jourdan committed Dec 26, 2016 60 61 `````` Qed. `````` Robbert Krebbers committed Feb 10, 2017 62 `````` Global Instance vec_to_list_ne m : NonExpansive (@vec_to_list A m). `````` Robbert Krebbers committed Jan 22, 2017 63 `````` Proof. by intros v v'. Qed. `````` Robbert Krebbers committed Feb 10, 2017 64 `````` Global Instance vec_to_list_proper m : Proper ((≡) ==> (≡)) (@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 ``````End proper. (** 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 81 `````` intros ? v v' H. eapply list_fmap_ne in H; last done. `````` Jacques-Henri Jourdan committed Dec 26, 2016 82 83 84 85 `````` 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). `````` Ralf Jung committed Jan 27, 2017 86 87 88 ``````Instance vecC_map_ne {A A'} m : NonExpansive (@vecC_map A A' m). Proof. intros n f g ? v. by apply vec_map_ext_ne. Qed. `````` Jacques-Henri Jourdan committed Dec 26, 2016 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 `````` 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.``````