commit by user andrea

[helm.git] / weblib / basics / lists / reverse.ma

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