matita/matita/lib/basics/vector_finset.ma

   1 (*
   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.
   5     ||I||
   6     ||T||
   7     ||A||
   8     \   /  This file is distributed under the terms of the
   9      \ /   GNU General Public License Version 2
  10       V_____________________________________________________________*)
  11
  12 include "basics/vectors.ma".
  13 include "basics/finset.ma".
  14
  15 (* DeqSet *)
  16 let rec eq_Vector (A:DeqSet) n on n ≝
  17   match n return (λn.∀v1,v2:Vector A n.bool) with
  18   [O ⇒ λv1,v2.true
  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)].
  21
  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)).
  26 // qed.
  27
  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).
  31
  32 (* uses proof irrelevance *)
  33 axiom eq_Vector_true: ∀A:DeqSet.∀n,v1,v2.
  34   eq_Vector A n v1 v2 = true ↔ v1 = v2.
  35 (*
  36 #A #n elim n
  37   [normalize #v1 #v2 % // #_ >(vector_nil … v1) >(vector_nil … v2) //
  38   |#m #Hind #v1 #v2
  39 *)
  40
  41 definition DeqVector ≝ λA:DeqSet.λn.
  42   mk_DeqSet (Vector A n) (eq_Vector A n) (eq_Vector_true A n).
  43
  44 unification hint  0 ≔ C,n;
  45     A ≟ carr C,
  46     X ≟ DeqVector C n
  47 (* ---------------------------------------- *) ⊢
  48     Vector A n ≡ carr X.
  49
  50 unification hint  0 ≔ A,n,v1,v2;
  51     X ≟ DeqVector A n
  52 (* ---------------------------------------- *) ⊢
  53     eq_Vector A n v1 v2 ≡ eqb X v1 v2.
  54
  55 (* finset structure *)
  56
  57 let rec enum_vector A l n on n ≝
  58   match n with
  59   [ O ⇒ [ ]
  60   | S n ⇒ foldr ?? (λi,acc.(map ?? (vec_cons A i n) (enum_vector A l n))@acc) [ ] l
  61   ].
  62
  63 axiom enum_vector_unique: ∀A,l,n.
  64   uniqueb A l = true → uniqueb (DeqVector A n) (enum_vector A l n) = true.
  65
  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.
  69
  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)).
  75
  76 unification hint  0 ≔ C,n;
  77     A ≟ FinSetcarr C,
  78     X ≟ FinVector C n
  79 (* ---------------------------------------- *) ⊢
  80     Vector A n ≡ FinSetcarr X.
  81