X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Flists%2Freverse.ma;fp=weblib%2Fbasics%2Flists%2Freverse.ma;h=20a0110d16c2e3d8b9f95d93699d42e4544ad660;hb=d13c122f5238597ef543eb213eb5ce788c0e9fd9;hp=0000000000000000000000000000000000000000;hpb=adfe42bbd5aaa4130a4133f345930e79444f0f3e;p=helm.git

diff --git a/weblib/basics/lists/reverse.ma b/weblib/basics/lists/reverse.ma
new file mode 100644
index 000000000..20a0110d1
--- /dev/null
+++ b/weblib/basics/lists/reverse.ma
@@ -0,0 +1,43 @@
+(**************************** reverse *****************************)
+
+include "basics/lists/iterators.ma".
+
+img class="anchor" src="icons/tick.png" id="rev_append"let rec rev_append S (l1,l2:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a S) on l1 ≝
+  match l1 with 
+  [ nil ⇒ l2
+  | cons a tl ⇒ rev_append S tl (a:a title="cons" href="cic:/fakeuri.def(1)":/al2)
+  ]
+.
+
+img class="anchor" src="icons/tick.png" id="reverse"definition reverse ≝λS.λl.a href="cic:/matita/basics/lists/reverse/rev_append.fix(0,1,1)"rev_append/a S l [a title="nil" href="cic:/fakeuri.def(1)"]/a.
+
+img class="anchor" src="icons/tick.png" id="reverse_single"lemma reverse_single : ∀S,a. a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a S a title="cons" href="cic:/fakeuri.def(1)"[/aaa title="nil" href="cic:/fakeuri.def(1)"]/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="cons" href="cic:/fakeuri.def(1)"[/aaa title="nil" href="cic:/fakeuri.def(1)"]/a. 
+// qed.
+
+img class="anchor" src="icons/tick.png" id="rev_append_def"lemma rev_append_def : ∀S,l1,l2. 
+  a href="cic:/matita/basics/lists/reverse/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/lists/reverse/reverse.def(2)"reverse/a S l1) a title="append" href="cic:/fakeuri.def(1)"@/a l2 .
+#S #l1 elim l1 normalize 
+  [// | #a #tl #Hind #l2 >Hind >(Hind a title="cons" href="cic:/fakeuri.def(1)"[/aaa title="nil" href="cic:/fakeuri.def(1)"]/a) >a href="cic:/matita/basics/lists/append/associative_append.def(4)"associative_append/a @a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a]
+qed.
+
+img class="anchor" src="icons/tick.png" id="reverse_cons"lemma reverse_cons : ∀S,a,l. a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a S (a:a title="cons" href="cic:/fakeuri.def(1)":/al) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a S l)a title="append" href="cic:/fakeuri.def(1)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/aaa title="nil" href="cic:/fakeuri.def(1)"]/a.
+#S #a #l whd in ⊢ (??%?); // 
+qed.
+
+img class="anchor" src="icons/tick.png" id="reverse_append"lemma reverse_append: ∀S,l1,l2. 
+  a href="cic:/matita/basics/lists/reverse/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/lists/reverse/reverse.def(2)"reverse/a S l2)a title="append" href="cic:/fakeuri.def(1)"@/a(a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a S l1).
+#S #l1 elim l1 [normalize // | #a #tl #Hind #l2 >a href="cic:/matita/basics/lists/reverse/reverse_cons.def(6)"reverse_cons/a
+>a href="cic:/matita/basics/lists/reverse/reverse_cons.def(6)"reverse_cons/a >Hind // qed.
+
+img class="anchor" src="icons/tick.png" id="reverse_reverse"lemma reverse_reverse : ∀S,l. a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a S (a href="cic:/matita/basics/lists/reverse/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/lists/reverse/reverse_cons.def(6)"reverse_cons/a >a href="cic:/matita/basics/lists/reverse/reverse_append.def(7)"reverse_append/a >Hind %
+qed.
+
+(* an elimination principle for lists working on the tail;
+useful for strings *)
+img class="anchor" src="icons/tick.png" id="list_elim_left"lemma list_elim_left: ∀S.∀P:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a S → Prop. P (a href="cic:/matita/basics/lists/lists/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)"[/aaa title="nil" href="cic:/fakeuri.def(1)"]/a)) → ∀l. P l.
+#S #P #Pnil #Pstep #l <(a href="cic:/matita/basics/lists/reverse/reverse_reverse.def(8)"reverse_reverse/a … l) 
+generalize in match (a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a S l); #l elim l //
+#a #tl #H >a href="cic:/matita/basics/lists/reverse/reverse_cons.def(6)"reverse_cons/a @Pstep //
+qed.