include "basics/lists/listb.ma".
-(****** DeqSet: a set with a decidbale equality ******)
+(****** DeqSet: a set with a decidable equality ******)
record FinSet : Type[1] ≝
-{ carr:> DeqSet;
- enum: list carr;
- enum_complete: ∀x.memb carr x enum = true;
- enum_unique: uniqueb carr enum = true
+{ FinSetcarr:> DeqSet;
+ enum: list FinSetcarr;
+ enum_unique: uniqueb FinSetcarr enum = true
}.
-(*
-definition DeqBool ≝ mk_DeqSet bool beqb beqb_true.
+definition enum_sum ≝ λA,B:DeqSet.λl1.λl2.
+ (map ?? (inl A B) l1) @ (map ?? (inr A B) l2).
+
+lemma enumAB_def : ∀A,B:FinSet.∀l1,l2. enum_sum A B l1 l2 =
+ (map ?? (inl A B) l1) @ (map ?? (inr A B) l2).
+// qed.
+
+axiom unique_map_inj: ∀A,B:DeqSet.∀f:A→B.∀l. injective A B f →
+ uniqueb A l = true → uniqueb B (map ?? f l) = true .
+axiom memb_map_inj: ∀A,B:DeqSet.∀f:A→B.∀l,a. injective A B f →
+ memb ? (f a) (map ?? f l) = true → memb ? a l = true.
+
+lemma enumAB_unique: ∀A,B:DeqSet.∀l1,l2.
+ uniqueb A l1 = true → uniqueb B l2 = true →
+ uniqueb ? (enum_sum A B l1 l2) = true.
+#A #B #l1 #l2 elim l1
+ [#_ #ul2 @unique_map_inj // #b1 #b2 #Hinr destruct //
+ |#a #tl #Hind #uA #uB @true_to_andb_true
+ [@sym_eq @noteq_to_eqnot % #H
+ cases (memb_append … (sym_eq … H))
+ [#H1 @(absurd (memb ? a tl = true))
+ [@(memb_map_inj …H1) #a1 #a2 #Hinl destruct //
+ |<(andb_true_l … uA) @eqnot_to_noteq //
+ ]
+ |elim l2
+ [normalize #H destruct
+ |#b #tlB #Hind #membH cases (orb_true_l … membH)
+ [#H lapply (\P H) #H1 destruct |@Hind]
+ ]
+ ]
+ |@Hind // @(andb_true_r … uA)
+ ]
+ ]
+qed.
+
+definition FinSum ≝ λA,B:FinSet.
+ mk_FinSet (DeqSum A B)
+ (enum_sum A B (enum A) (enum B))
+ (enumAB_unique … (enum_unique A) (enum_unique B)).
+
+unification hint 0 ≔ C1,C2;
+ T1 ≟ FinSetcarr C1,
+ T2 ≟ FinSetcarr C2,
+ X ≟ FinSum C1 C2
+(* ---------------------------------------- *) ⊢
+ T1+T2 ≡ FinSetcarr X.
+
+
+(*
unification hint 0 ≔ ;
X ≟ mk_DeqSet bool beqb beqb_true
(* ---------------------------------------- *) ⊢
definition DeqProd ≝ λA,B:DeqSet.
mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
-unification hint 0 ≔ C1,C2;
- T1 ≟ carr C1,
- T2 ≟ carr C2,
- X ≟ DeqProd C1 C2
-(* ---------------------------------------- *) ⊢
- T1×T2 ≡ carr X.
-
-unification hint 0 ≔ T1,T2,p1,p2;
- X ≟ DeqProd T1 T2
-(* ---------------------------------------- *) ⊢
- eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
example hint2: ∀b1,b2.
〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.