From 6756545478920d6eca9445a3aeede39bfe11cb83 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 17 May 2012 07:20:23 +0000
Subject: [PATCH] filtering on a list without repetitions

---
 matita/matita/lib/basics/lists/listb.ma | 28 ++++++++++++++++++-------
 1 file changed, 21 insertions(+), 7 deletions(-)

diff --git a/matita/matita/lib/basics/lists/listb.ma b/matita/matita/lib/basics/lists/listb.ma
index 7951f2997..640f1391c 100644
--- a/matita/matita/lib/basics/lists/listb.ma
+++ b/matita/matita/lib/basics/lists/listb.ma
@@ -225,6 +225,27 @@ qed.
 
 (********************* filtering *****************)
 
+lemma memb_filter_memb: ∀S,f,a,l. 
+  memb S a (filter S f l) = true → memb S a l = true.
+#S #f #a #l elim l [normalize //]
+#b #tl #Hind normalize (cases (f b)) normalize 
+cases (a==b) normalize // @Hind
+qed.
+  
+lemma uniqueb_filter : ∀S,l,f.
+ uniqueb S l = true → uniqueb S (filter S f l) = true.
+#S #l #f elim l //
+#a #tl #Hind #Hunique cases (andb_true … Hunique)
+#memba #uniquetl cases (true_or_false … (f a)) #Hfa
+  [>filter_true // @true_to_andb_true
+    [@sym_eq @noteq_to_eqnot @(not_to_not … (eqnot_to_noteq … (sym_eq … memba)))
+     #H @sym_eq @(memb_filter_memb … f) <H // 
+    |/2/
+    ]
+  |>filter_false /2/
+  ]
+qed.
+  
 lemma filter_true: ∀S,f,a,l. 
   memb S a (filter S f l) = true → f a = true.
 #S #f #a #l elim l [normalize #H @False_ind /2/]
@@ -234,13 +255,6 @@ cases (true_or_false (a==b)) #eqab
   [#_ >(\P eqab) // | >eqab normalize @Hind]
 qed. 
   
-lemma memb_filter_memb: ∀S,f,a,l. 
-  memb S a (filter S f l) = true → memb S a l = true.
-#S #f #a #l elim l [normalize //]
-#b #tl #Hind normalize (cases (f b)) normalize 
-cases (a==b) normalize // @Hind
-qed.
-  
 lemma memb_filter: ∀S,f,l,x. memb S x (filter ? f l) = true → 
 memb S x l = true ∧ (f x = true).
 /3/ qed.
-- 
2.39.2