From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Tue, 6 Mar 2012 18:09:27 +0000 (+0000)
Subject: commit by user andrea
X-Git-Tag: make_still_working~1891
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=44ef2738ac6d7544c22950602eecf1eb61a80729;p=helm.git

commit by user andrea
---

diff --git a/weblib/basics/list.ma b/weblib/basics/list.ma
index e699b626a..39fdb1bd5 100644
--- a/weblib/basics/list.ma
+++ b/weblib/basics/list.ma
@@ -9,7 +9,7 @@
      \ /   GNU General Public License Version 2   
       V_______________________________________________________________ *)
 
-include "arithmetics/nat.ma".
+include "arithmetics/nat.ma".span class="error" title="disambiguation error"/span
 
 inductive list (A:Type[0]) : Type[0] :=
   | nil: list A
@@ -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 a title="cons" href="cic:/fakeuri.def(1)"[/aa] a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="cons" href="cic:/fakeuri.def(1)"[/aa]. 
+// 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)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/aa].
+#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)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/aa])) → ∀l. P l.
+#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 ≝