2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
8 \ / This file is distributed under the terms of the
9 \ / GNU General Public License Version 2
10 V_____________________________________________________________*)
12 include "basics/vectors.ma".
13 include "basics/finset.ma".
16 let rec eq_Vector (A:DeqSet) n on n ≝
17 match n return (λn.∀v1,v2:Vector A n.bool) with
19 |S m ⇒ λv1,v2. vec_hd A m v1 == vec_hd A m v2 ∧
20 eq_Vector A m (vec_tail A (S m) v1) (vec_tail A (S m) v2)].
22 lemma eq_Vector_S : ∀A:DeqSet.∀n,v1,v2.
23 eq_Vector A (S n) v1 v2 =
24 (vec_hd A n v1 == vec_hd A n v2 ∧
25 eq_Vector A n (vec_tail A (S n) v1) (vec_tail A (S n) v2)).
28 axiom eq_Vector_S1 : ∀A:DeqSet.∀n,a1,a2,v1,v2.
29 eq_Vector A (S n) (vec_cons A a1 n v1) (vec_cons A a2 n v2) =
30 (a1 == a2 ∧ eq_Vector A n v1 v2).
32 (* uses proof irrelevance *)
33 axiom eq_Vector_true: ∀A:DeqSet.∀n,v1,v2.
34 eq_Vector A n v1 v2 = true ↔ v1 = v2.
37 [normalize #v1 #v2 % // #_ >(vector_nil … v1) >(vector_nil … v2) //
41 definition DeqVector ≝ λA:DeqSet.λn.
42 mk_DeqSet (Vector A n) (eq_Vector A n) (eq_Vector_true A n).
44 unification hint 0 ≔ C,n;
47 (* ---------------------------------------- *) ⊢
50 unification hint 0 ≔ A,n,v1,v2;
52 (* ---------------------------------------- *) ⊢
53 eq_Vector A n v1 v2 ≡ eqb X v1 v2.
55 (* finset structure *)
57 let rec enum_vector A l n on n ≝
60 | S n ⇒ foldr ?? (λi,acc.(map ?? (vec_cons A i n) (enum_vector A l n))@acc) [ ] l
63 axiom enum_vector_unique: ∀A,l,n.
64 uniqueb A l = true → uniqueb (DeqVector A n) (enum_vector A l n) = true.
66 axiom enum_vector_complete:∀A:DeqSet.∀l,n.
67 (∀a. memb A a l = true) →
68 ∀v. memb ? v (enum_vector A l n) = true.
70 definition FinVector ≝
71 λA:FinSet.λn.mk_FinSet (DeqVector A n)
72 (enum_vector A (enum A) n)
73 (enum_vector_unique A … (enum_unique A))
74 (enum_vector_complete A … (enum_complete A)).
76 unification hint 0 ≔ C,n;
79 (* ---------------------------------------- *) ⊢
80 Vector A n ≡ FinSetcarr X.