From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 27 Apr 2012 11:46:07 +0000 (+0000)
Subject: Extensions to finset (sum) and auxiliary lemmas.
X-Git-Tag: make_still_working~1798
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a87c9d012b588c381dc82c53fd0652762a9e50c9;p=helm.git

Extensions to finset (sum) and auxiliary lemmas.
---

diff --git a/matita/matita/lib/basics/bool.ma b/matita/matita/lib/basics/bool.ma
index fb0106f12..587ab9ed6 100644
--- a/matita/matita/lib/basics/bool.ma
+++ b/matita/matita/lib/basics/bool.ma
@@ -54,6 +54,10 @@ theorem andb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
 match b1 with [ true ⇒ P b2 | false ⇒ P false] → P (b1 ∧ b2).
 #b1 #b2 #P (elim b1) normalize // qed.
 
+theorem true_to_andb_true: ∀b1,b2. b1 = true → b2 = true → (b1 ∧ b2) = true.
+#b1 cases b1 normalize //
+qed.
+
 theorem andb_true_l: ∀ b1,b2. (b1 ∧ b2) = true → b1 = true.
 #b1 (cases b1) normalize // qed.
 
diff --git a/matita/matita/lib/basics/deqsets.ma b/matita/matita/lib/basics/deqsets.ma
index 4d86c9f6c..2d6434f65 100644
--- a/matita/matita/lib/basics/deqsets.ma
+++ b/matita/matita/lib/basics/deqsets.ma
@@ -100,4 +100,47 @@ unification hint  0 ≔ T1,T2,p1,p2;
 
 example hint2: ∀b1,b2. 
   〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
-#b1 #b2 #H @(\P H).
\ No newline at end of file
+#b1 #b2 #H @(\P H)
+qed.
+
+(* sum *)
+definition eq_sum ≝
+  λA,B:DeqSet.λp1,p2:A+B.
+  match p1 with
+  [ inl a1 ⇒ match p2 with
+    [ inl a2 ⇒ a1 == a2 | inr b2 ⇒ false ]
+  | inr b1 ⇒ match p2 with 
+    [ inl a2 ⇒ false | inr b2 ⇒ b1 == b2 ]
+  ].
+
+lemma eq_sum_true: ∀A,B:DeqSet.∀p1,p2:A+B.
+  eq_sum A B p1 p2 = true ↔ p1 = p2.
+#A #B * 
+  [#a1 * 
+    [#a2 normalize % 
+      [#eqa >(\P eqa) // | #H destruct @(\b ?) //]
+    |#b2 normalize % #H destruct 
+    ]
+  |#b1 *
+    [#a2 normalize % #H destruct
+    |#b2 normalize %
+      [#eqb >(\P eqb) // | #H destruct @(\b ?) //]
+    ]
+  ]
+qed.
+
+definition DeqSum ≝ λA,B:DeqSet.
+  mk_DeqSet (A+B) (eq_sum A B) (eq_sum_true A B).
+  
+unification hint  0 ≔ C1,C2; 
+    T1 ≟ carr C1,
+    T2 ≟ carr C2,
+    X ≟ DeqSum C1 C2
+(* ---------------------------------------- *) ⊢ 
+    T1+T2 ≡ carr X.
+
+unification hint  0 ≔ T1,T2,p1,p2; 
+    X ≟ DeqSum T1 T2
+(* ---------------------------------------- *) ⊢ 
+    eq_sum T1 T2 p1 p2 ≡ eqb X p1 p2.
+
diff --git a/matita/matita/lib/basics/finset.ma b/matita/matita/lib/basics/finset.ma
index 1b972ec06..0f4161997 100644
--- 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〉.
diff --git a/matita/matita/lib/basics/lists/listb.ma b/matita/matita/lib/basics/lists/listb.ma
index b6d5864f8..e46f45f07 100644
--- a/matita/matita/lib/basics/lists/listb.ma
+++ b/matita/matita/lib/basics/lists/listb.ma
@@ -145,6 +145,30 @@ cases (true_or_false … (memb S a (unique_append S tl l2)))
 #H >H normalize [@Hind //] >H normalize @Hind //
 qed.
 
+lemma 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.
+#A #B #f #l #a #injf elim l
+  [normalize //
+  |#a1 #tl #Hind #Ha cases (orb_true_l … Ha)
+    [#eqf @orb_true_r1 @(\b ?)  >(injf … (\P eqf)) //
+    |#membtl @orb_true_r2 /2/
+    ]
+  ]
+qed.
+
+lemma unique_map_inj: ∀A,B:DeqSet.∀f:A→B.∀l. injective A B f → 
+  uniqueb A l = true → uniqueb B (map ?? f l) = true .
+#A #B #f #l #injf elim l 
+  [normalize //
+  |#a #tl #Hind #Htl @true_to_andb_true
+    [@sym_eq @noteq_to_eqnot @sym_not_eq 
+     @(not_to_not ?? (memb_map_inj … injf …) )
+     <(andb_true_l ?? Htl) /2/
+    |@Hind @(andb_true_r ?? Htl)
+    ]
+  ]
+qed.
+
 (******************* sublist *******************)
 definition sublist ≝ 
   λS,l1,l2.∀a. memb S a l1 = true → memb S a l2 = true.
diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma
index 8f981d469..70e743e99 100644
--- a/matita/matita/lib/basics/logic.ma
+++ b/matita/matita/lib/basics/logic.ma
@@ -263,10 +263,10 @@ definition eqProp ≝ λA:Prop.eq A.
 
 (* Example to avoid indexing and the consequential creation of ill typed
    terms during paramodulation *)
-example lemmaK : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x).
+lemma lemmaK : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x).
 #A #x #h @(refl ? h: eqProp ? ? ?).
-qed.
+qed-.
 
 theorem streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[3].P (refl ? t) → ∀p.P p.
  #T #t #P #H #p >(lemmaK T t p) @H
-qed.
+qed-.