Extensions to finset (sum) and auxiliary lemmas.

[helm.git] / matita / matita / lib / basics / finset.ma

diff --git a/matita/matita/lib/basics/finset.ma b/matita/matita/lib/basics/finset.ma
index 1b972ec06c7cdb8db859838572c93bef7813fcd6..0f41619973b1b09a6b150c440252fd9e223f6891 100644 (file)
--- a/matita/matita/lib/basics/finset.ma
+++ b/matita/matita/lib/basics/finset.ma
@@ -11,18 +11,64 @@
 
 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
 (* ---------------------------------------- *) ⊢ 
@@ -52,17 +98,6 @@ qed.
 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〉.