X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Flist.ma;h=d6c0661208c15e31c7b10684657a3f98bbd0060c;hb=6ebf3e5a09012b3349c6020fe692c3b22020684a;hp=245a9fd3b4789818833887095b8db4cb1e04a1cf;hpb=a5c551d0b7399f00e8eef3dfb06e2a0895eac3d4;p=helm.git

diff --git a/weblib/basics/list.ma b/weblib/basics/list.ma
index 245a9fd3b..d6c066120 100644
--- a/weblib/basics/list.ma
+++ b/weblib/basics/list.ma
@@ -104,7 +104,7 @@ definition filter ≝
   a href="cic:/matita/basics/list/foldr.fix(0,4,1)"foldr/a T (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a T) (λx,l0.if (p x) then (xa title="cons" href="cic:/fakeuri.def(1)":/a:l0) else l0) (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a T).
 
 definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
-    a href="cic:/matita/basics/list/foldr.fix(0,4,1)"foldr/a ?? (λi,acc.(a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a ?? (f i) l2)a title="append" href="cic:/fakeuri.def(1)"@/aacc) a title="nil" href="cic:/fakeuri.def(1)"[/a ] l1.
+    a href="cic:/matita/basics/list/foldr.fix(0,4,1)"foldr/a ?? (λi,acc.(a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a ?? (f i) l2)a title="append" href="cic:/fakeuri.def(1)"@/aacc) a title="nil" href="cic:/fakeuri.def(1)"[/a ] l1. 
 
 lemma filter_true : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → 
   a href="cic:/matita/basics/list/filter.def(2)"filter/a A p (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a a title="cons" href="cic:/fakeuri.def(1)":/a: a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l.
@@ -124,6 +124,46 @@ match l1 with
   | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g
   ]. *)
 
+(**************************** reverse *****************************)
+let rec rev_append S (l1,l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a S) on l1 ≝
+  match l1 with 
+  [ nil ⇒ l2
+  | cons a tl ⇒ rev_append S tl (aa title="cons" href="cic:/fakeuri.def(1)":/a:l2)
+  ]
+.
+
+definition reverse ≝λS.λl.a href="cic:/matita/basics/list/rev_append.fix(0,1,1)"rev_append/a S l a title="nil" href="cic:/fakeuri.def(1)"[/a].
+
+lemma reverse_single : ∀S,a. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]). 
+// qed.
+
+lemma rev_append_def : ∀S,l1,l2. 
+  a href="cic:/matita/basics/list/rev_append.fix(0,1,1)"rev_append/a S l1 l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l1) a title="append" href="cic:/fakeuri.def(1)"@/a l2 .
+#S #l1 elim l1 normalize // 
+qed.
+
+lemma reverse_cons : ∀S,a,l. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l)a title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]).
+#S #a #l whd in ⊢ (??%?); // 
+qed.
+
+lemma reverse_append: ∀S,l1,l2. 
+  a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (l1 a title="append" href="cic:/fakeuri.def(1)"@/a l2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l2)a title="append" href="cic:/fakeuri.def(1)"@/a(a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l1).
+#S #l1 elim l1 [normalize // | #a #tl #Hind #l2 >a href="cic:/matita/basics/list/reverse_cons.def(7)"reverse_cons/a
+>a href="cic:/matita/basics/list/reverse_cons.def(7)"reverse_cons/a // qed.
+
+lemma reverse_reverse : ∀S,l. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l.
+#S #l elim l // #a #tl #Hind >a href="cic:/matita/basics/list/reverse_cons.def(7)"reverse_cons/a >a href="cic:/matita/basics/list/reverse_append.def(8)"reverse_append/a 
+normalize // qed.
+
+(* an elimination principle for lists working on the tail;
+useful for strings *)
+lemma list_elim_left: ∀S.∀P:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a S → Prop. P (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a S) →
+(∀a.∀tl.P tl → P (tla title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]))) → ∀l. P l.span class="error" title="Parse error: SYMBOL ':' or RPAREN expected after [term] (in [term])"/span
+#S #P #Pnil #Pstep #l <(a href="cic:/matita/basics/list/reverse_reverse.def(9)"reverse_reverse/a … l) 
+generalize in match (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l); #l elim l //
+#a #tl #H >a href="cic:/matita/basics/list/reverse_cons.def(7)"reverse_cons/a @Pstep //
+qed.
+
 (**************************** length *******************************)
 
 let rec length (A:Type[0]) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l ≝ 
@@ -197,4 +237,4 @@ theorem fold_sum: ∀A,B. ∀I,J:a href="cic:/matita/basics/list/list.ind(1,0,1
     a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈(Ia title="append" href="cic:/fakeuri.def(1)"@/aJ)} (f i).
 #A #B #I #J #nil #op #f (elim I) normalize 
   [>a href="cic:/matita/basics/list/nill.fix(0,2,2)"nill/a //|#a #tl #Hind <a href="cic:/matita/basics/list/assoc.fix(0,2,2)"assoc/a //]
-qed.
\ No newline at end of file
+qed.