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 definition enum_sum ≝ λA,B:DeqSet.λl1.λl2.
  23   (map ?? (inl A B) l1) @ (map ?? (inr A B) l2).
  24
  25 lemma enumAB_def : ∀A,B:FinSet.∀l1,l2. enum_sum A B l1 l2 =
  26   (map ?? (inl A B) l1) @ (map ?? (inr A B) l2).
  27 // qed.
  28
  29 axiom unique_map_inj: ∀A,B:DeqSet.∀f:A→B.∀l. injective A B f →
  30   uniqueb A l = true → uniqueb B (map ?? f l) = true .
  31
  32 axiom memb_map_inj: ∀A,B:DeqSet.∀f:A→B.∀l,a. injective A B f →
  33   memb ? (f a) (map ?? f l) = true → memb ? a l = true.
  34
  35 lemma enumAB_unique: ∀A,B:DeqSet.∀l1,l2.
  36   uniqueb A l1 = true → uniqueb B l2 = true →
  37     uniqueb ? (enum_sum A B l1 l2) = true.
  38 #A #B #l1 #l2 elim l1
  39   [#_ #ul2 @unique_map_inj // #b1 #b2 #Hinr destruct //
  40   |#a #tl #Hind #uA #uB @true_to_andb_true
  41     [@sym_eq @noteq_to_eqnot % #H
  42      cases (memb_append … (sym_eq … H))
  43       [#H1 @(absurd (memb ? a tl = true))
  44         [@(memb_map_inj …H1) #a1 #a2 #Hinl destruct //
  45         |<(andb_true_l … uA) @eqnot_to_noteq //
  46         ]
  47       |elim l2
  48         [normalize #H destruct
  49         |#b #tlB #Hind #membH cases (orb_true_l … membH)
  50           [#H lapply (\P H) #H1 destruct |@Hind]
  51         ]
  52       ]
  53     |@Hind // @(andb_true_r … uA)
  54     ]
  55   ]
  56 qed.
  57
  58 definition FinSum ≝ λA,B:FinSet.
  59   mk_FinSet (DeqSum A B)
  60    (enum_sum A B (enum A) (enum B))
  61    (enumAB_unique … (enum_unique A) (enum_unique B)).
  62
  63 unification hint  0 ≔ C1,C2;
  64     T1 ≟ FinSetcarr C1,
  65     T2 ≟ FinSetcarr C2,
  66     X ≟ FinSum C1 C2
  67 (* ---------------------------------------- *) ⊢
  68     T1+T2 ≡ FinSetcarr X.
  69
  70
  71 (*
  72 unification hint  0 ≔ ;
  73     X ≟ mk_DeqSet bool beqb beqb_true
  74 (* ---------------------------------------- *) ⊢
  75     bool ≡ carr X.
  76
  77 unification hint  0 ≔ b1,b2:bool;
  78     X ≟ mk_DeqSet bool beqb beqb_true
  79 (* ---------------------------------------- *) ⊢
  80     beqb b1 b2 ≡ eqb X b1 b2.
  81
  82 example exhint: ∀b:bool. (b == false) = true → b = false.
  83 #b #H @(\P H).
  84 qed.
  85
  86 (* pairs *)
  87 definition eq_pairs ≝
  88   λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
  89
  90 lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
  91   eq_pairs A B p1 p2 = true ↔ p1 = p2.
  92 #A #B * #a1 #b1 * #a2 #b2 %
  93   [#H cases (andb_true …H) #eqa #eqb >(\P eqa) >(\P eqb) //
  94   |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
  95   ]
  96 qed.
  97
  98 definition DeqProd ≝ λA,B:DeqSet.
  99   mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
 100
 101
 102 example hint2: ∀b1,b2.
 103   〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
 104 #b1 #b2 #H @(\P H).
 105 *)