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 decidbale equality ******)
  15
  16 record FinSet : Type[1] ≝
  17 { carr:> DeqSet;
  18   enum: list carr;
  19   enum_complete: ∀x.memb carr x enum = true;
  20   enum_unique: uniqueb carr enum = true
  21 }.
  22
  23 (*
  24 definition DeqBool ≝ mk_DeqSet bool beqb beqb_true.
  25
  26 unification hint  0 ≔ ;
  27     X ≟ mk_DeqSet bool beqb beqb_true
  28 (* ---------------------------------------- *) ⊢
  29     bool ≡ carr X.
  30
  31 unification hint  0 ≔ b1,b2:bool;
  32     X ≟ mk_DeqSet bool beqb beqb_true
  33 (* ---------------------------------------- *) ⊢
  34     beqb b1 b2 ≡ eqb X b1 b2.
  35
  36 example exhint: ∀b:bool. (b == false) = true → b = false.
  37 #b #H @(\P H).
  38 qed.
  39
  40 (* pairs *)
  41 definition eq_pairs ≝
  42   λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
  43
  44 lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
  45   eq_pairs A B p1 p2 = true ↔ p1 = p2.
  46 #A #B * #a1 #b1 * #a2 #b2 %
  47   [#H cases (andb_true …H) #eqa #eqb >(\P eqa) >(\P eqb) //
  48   |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
  49   ]
  50 qed.
  51
  52 definition DeqProd ≝ λA,B:DeqSet.
  53   mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
  54
  55 unification hint  0 ≔ C1,C2;
  56     T1 ≟ carr C1,
  57     T2 ≟ carr C2,
  58     X ≟ DeqProd C1 C2
  59 (* ---------------------------------------- *) ⊢
  60     T1×T2 ≡ carr X.
  61
  62 unification hint  0 ≔ T1,T2,p1,p2;
  63     X ≟ DeqProd T1 T2
  64 (* ---------------------------------------- *) ⊢
  65     eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
  66
  67 example hint2: ∀b1,b2.
  68   〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
  69 #b1 #b2 #H @(\P H).
  70 *)