matita/matita/lib/basics/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/lists/listb.ma".
  13
  14 (****** DeqSet: a set with a decidable equality ******)
  15
  16 record FinSet : Type[1] ≝
  17 { FinSetcarr:> DeqSet;
  18   enum: list FinSetcarr;
  19   enum_unique: uniqueb FinSetcarr enum = true
  20 }.
  21
  22 (* bool *)
  23 lemma bool_enum_unique: uniqueb ? [true;false] = true.
  24 // qed.
  25
  26 definition FinBool ≝ mk_FinSet DeqBool [true;false] bool_enum_unique.
  27
  28 unification hint  0 ≔ ;
  29     X ≟ FinBool
  30 (* ---------------------------------------- *) ⊢
  31     bool ≡ FinSetcarr X.
  32
  33 (* nat segment *)
  34
  35 lemma eqbnat_true : ∀n,m. eqb n m = true ↔ n = m.
  36 #n #m % [@eqb_true_to_eq | @eq_to_eqb_true]
  37 qed.
  38
  39 definition DeqNat ≝ mk_DeqSet nat eqb eqbnat_true.
  40
  41 let rec enumn n ≝
  42   match n with [ O ⇒ [ ] | S p ⇒ p::enumn p ].
  43
  44 lemma memb_enumn: ∀m,n. n ≤ m →  (¬ (memb DeqNat m (enumn n))) = true.
  45 #m #n elim n // #n1 #Hind #ltm  @sym_eq @noteq_to_eqnot @sym_not_eq
  46 % #H cases (orb_true_l … H)
  47   [#H1 @(absurd … (\P H1)) @sym_not_eq /2/
  48   |<(notb_notb (memb …)) >Hind normalize /2/
  49   ]
  50 qed.
  51
  52 lemma enumn_unique: ∀n. uniqueb DeqNat (enumn n) = true.
  53 #n elim n // #m #Hind @true_to_andb_true /2/
  54 qed.
  55
  56 definition initN ≝ λn.mk_FinSet DeqNat (enumn n) (enumn_unique n).
  57
  58 example tipa: ∀n.∃x: initN (S n). x = n.
  59 #n @(ex_intro … n) // qed.
  60
  61 example inject : ∃f: initN 2 → initN 4. injective ?? f.
  62 @(ex_intro … S) //
  63 qed.
  64
  65 (* sum *)
  66 definition enum_sum ≝ λA,B:DeqSet.λl1.λl2.
  67   (map ?? (inl A B) l1) @ (map ?? (inr A B) l2).
  68
  69 lemma enumAB_def : ∀A,B:FinSet.∀l1,l2. enum_sum A B l1 l2 =
  70   (map ?? (inl A B) l1) @ (map ?? (inr A B) l2).
  71 // qed.
  72
  73 lemma enumAB_unique: ∀A,B:DeqSet.∀l1,l2.
  74   uniqueb A l1 = true → uniqueb B l2 = true →
  75     uniqueb ? (enum_sum A B l1 l2) = true.
  76 #A #B #l1 #l2 elim l1
  77   [#_ #ul2 @unique_map_inj // #b1 #b2 #Hinr destruct //
  78   |#a #tl #Hind #uA #uB @true_to_andb_true
  79     [@sym_eq @noteq_to_eqnot % #H
  80      cases (memb_append … (sym_eq … H))
  81       [#H1 @(absurd (memb ? a tl = true))
  82         [@(memb_map_inj …H1) #a1 #a2 #Hinl destruct //
  83         |<(andb_true_l … uA) @eqnot_to_noteq //
  84         ]
  85       |elim l2
  86         [normalize #H destruct
  87         |#b #tlB #Hind #membH cases (orb_true_l … membH)
  88           [#H lapply (\P H) #H1 destruct |@Hind]
  89         ]
  90       ]
  91     |@Hind // @(andb_true_r … uA)
  92     ]
  93   ]
  94 qed.
  95
  96 definition FinSum ≝ λA,B:FinSet.
  97   mk_FinSet (DeqSum A B)
  98    (enum_sum A B (enum A) (enum B))
  99    (enumAB_unique … (enum_unique A) (enum_unique B)).
 100
 101 unification hint  0 ≔ C1,C2;
 102     T1 ≟ FinSetcarr C1,
 103     T2 ≟ FinSetcarr C2,
 104     X ≟ FinSum C1 C2
 105 (* ---------------------------------------- *) ⊢
 106     T1+T2 ≡ FinSetcarr X.
 107
 108 (* prod *)
 109
 110 definition enum_prod ≝ λA,B:DeqSet.λl1.λl2.
 111   compose ??? (mk_Prod A B) l1 l2.
 112
 113 axiom enum_prod_unique: ∀A,B,l1,l2.
 114   uniqueb A l1 = true → uniqueb B l2 = true →
 115   uniqueb ? (enum_prod A B l1 l2) = true.
 116
 117 definition FinProd ≝
 118 λA,B:FinSet.mk_FinSet (DeqProd A B)
 119   (enum_prod A B (enum A) (enum B))
 120   (enum_prod_unique A B (enum A) (enum B) (enum_unique A) (enum_unique B) ).
 121
 122 unification hint  0 ≔ C1,C2;
 123     T1 ≟ FinSetcarr C1,
 124     T2 ≟ FinSetcarr C2,
 125     X ≟ FinProd C1 C2
 126 (* ---------------------------------------- *) ⊢
 127     T1×T2 ≡ FinSetcarr X.
 128