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 BoolFS ≝ mk_FinSet DeqBool [true;false] bool_enum_unique.
  27
  28 unification hint  0 ≔ ;
  29     X ≟ BoolFS
  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 (* sum *)
  62 definition enum_sum ≝ λA,B:DeqSet.λl1.λl2.
  63   (map ?? (inl A B) l1) @ (map ?? (inr A B) l2).
  64
  65 lemma enumAB_def : ∀A,B:FinSet.∀l1,l2. enum_sum A B l1 l2 =
  66   (map ?? (inl A B) l1) @ (map ?? (inr A B) l2).
  67 // qed.
  68
  69 lemma enumAB_unique: ∀A,B:DeqSet.∀l1,l2.
  70   uniqueb A l1 = true → uniqueb B l2 = true →
  71     uniqueb ? (enum_sum A B l1 l2) = true.
  72 #A #B #l1 #l2 elim l1
  73   [#_ #ul2 @unique_map_inj // #b1 #b2 #Hinr destruct //
  74   |#a #tl #Hind #uA #uB @true_to_andb_true
  75     [@sym_eq @noteq_to_eqnot % #H
  76      cases (memb_append … (sym_eq … H))
  77       [#H1 @(absurd (memb ? a tl = true))
  78         [@(memb_map_inj …H1) #a1 #a2 #Hinl destruct //
  79         |<(andb_true_l … uA) @eqnot_to_noteq //
  80         ]
  81       |elim l2
  82         [normalize #H destruct
  83         |#b #tlB #Hind #membH cases (orb_true_l … membH)
  84           [#H lapply (\P H) #H1 destruct |@Hind]
  85         ]
  86       ]
  87     |@Hind // @(andb_true_r … uA)
  88     ]
  89   ]
  90 qed.
  91
  92 definition FinSum ≝ λA,B:FinSet.
  93   mk_FinSet (DeqSum A B)
  94    (enum_sum A B (enum A) (enum B))
  95    (enumAB_unique … (enum_unique A) (enum_unique B)).
  96
  97 unification hint  0 ≔ C1,C2;
  98     T1 ≟ FinSetcarr C1,
  99     T2 ≟ FinSetcarr C2,
 100     X ≟ FinSum C1 C2
 101 (* ---------------------------------------- *) ⊢
 102     T1+T2 ≡ FinSetcarr X.
 103
 104
 105 (*
 106 unification hint  0 ≔ ;
 107     X ≟ mk_DeqSet bool beqb beqb_true
 108 (* ---------------------------------------- *) ⊢
 109     bool ≡ carr X.
 110
 111 unification hint  0 ≔ b1,b2:bool;
 112     X ≟ mk_DeqSet bool beqb beqb_true
 113 (* ---------------------------------------- *) ⊢
 114     beqb b1 b2 ≡ eqb X b1 b2.
 115
 116 example exhint: ∀b:bool. (b == false) = true → b = false.
 117 #b #H @(\P H).
 118 qed.
 119
 120 (* pairs *)
 121 definition eq_pairs ≝
 122   λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
 123
 124 lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
 125   eq_pairs A B p1 p2 = true ↔ p1 = p2.
 126 #A #B * #a1 #b1 * #a2 #b2 %
 127   [#H cases (andb_true …H) #eqa #eqb >(\P eqa) >(\P eqb) //
 128   |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
 129   ]
 130 qed.
 131
 132 definition DeqProd ≝ λA,B:DeqSet.
 133   mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
 134
 135
 136 example hint2: ∀b1,b2.
 137   〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
 138 #b1 #b2 #H @(\P H).
 139 *)