Verified Commit 9155496c authored by Tej Chajed's avatar Tej Chajed
Browse files

Add Countable instance for vec

parent 268507ec
......@@ -13,6 +13,7 @@ API-breaking change is listed.
https://gitlab.mpi-sws.org/iris/stdpp/merge_requests/93
- Add type class `TopSet` for sets with a `⊤` element. Provide instances for
`boolset`, `propset`, and `coPset`.
- Add a `Countable` instance for `vec`.
## std++ 1.2.1 (released 2019-08-29)
......
......@@ -2,6 +2,7 @@
(* This file is distributed under the terms of the BSD license. *)
From Coq.QArith Require Import QArith_base Qcanon.
From stdpp Require Export list numbers.
From stdpp Require Import vector.
Set Default Proof Using "Type".
Local Open Scope positive.
......@@ -322,3 +323,28 @@ Next Obligation.
intros T ?? t.
by rewrite <-(right_id_L [] _ (gen_tree_to_list _)), gen_tree_of_to_list.
Qed.
(** ** Vectors *)
Fixpoint list_to_option_vec {A} (l: list A) n : option (vec A n) :=
match l, n with
| [], O => Some vnil
| _::_, O => None
| [], S _ => None
| x::l, S n =>
vcons x <$> list_to_option_vec l n
end.
Theorem vec_to_of_list_option {A n} (v: vec A n) :
list_to_option_vec (vec_to_list v) n = Some v.
Proof.
induction v; simpl; auto.
by rewrite IHv.
Qed.
Instance vec_countable `{Countable A} n : Countable (vec A n).
Proof.
apply (inj_countable (λ v, vec_to_list v)
(λ l, list_to_option_vec l n)).
intros v; by rewrite vec_to_of_list_option.
Qed.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment