almost there

[helm.git] / matita / matita / lib / basics / lists / listb.ma

diff --git a/matita/matita/lib/basics/lists/listb.ma b/matita/matita/lib/basics/lists/listb.ma
index ac72b008bee54237a9360bb2830545ab5ec7b853..a95d8a05adb91bcb3eeb7054f200d4759cfe632c 100644 (file)
--- a/matita/matita/lib/basics/lists/listb.ma
+++ b/matita/matita/lib/basics/lists/listb.ma
@@ -103,6 +103,16 @@ lemma memb_compose: ∀S1,S2,S3,op,a1,a2,l1,l2.
   ]
 qed.
 
+lemma memb_reverse: ∀S:DeqSet.∀a:S.∀l.
+  memb ? a l = true → memb ? a (reverse ? l) = true.
+#S #a #l elim l [normalize //]
+#b #tl #Hind #memba change with ([b]@tl) in match (b::tl);
+>reverse_append cases (orb_true_l … memba) #Hcase
+  [@memb_append_l2 >(\P Hcase) whd in match (reverse ??); @memb_hd
+  |@memb_append_l1 /2/
+  ]
+qed.
+
 lemma mem_to_memb: ∀S:DeqSet.∀a,l. mem S a l → memb S a l = true.
 #S #a #l elim l normalize
   [@False_ind
@@ -112,6 +122,15 @@ lemma mem_to_memb: ∀S:DeqSet.∀a,l. mem S a l → memb S a l = true.
     ]
   ]
 qed.
+
+lemma memb_to_mem: ∀S:DeqSet.∀l,a. memb S a l =true → mem S a l.
+#S #l #a elim l 
+  [normalize #H destruct
+  |#b #tl #Hind #mema cases (orb_true_l … mema) 
+    [#eqab >(\P eqab) %1 % |#memtl %2 @Hind @memtl]
+  ]
+qed.
+
 (**************** unicity test *****************)
 
 let rec uniqueb (S:DeqSet) l on l : bool ≝