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