From a65c5b3337075672736b1583b8519ff14bb16976 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 3 Jan 2012 15:58:23 +0000
Subject: [PATCH] reverse

---
 matita/matita/lib/basics/lists/list.ma | 46 ++++++++++++++++++++++----
 1 file changed, 40 insertions(+), 6 deletions(-)

diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma
index 40839b28f..021e9d400 100644
--- a/matita/matita/lib/basics/lists/list.ma
+++ b/matita/matita/lib/basics/lists/list.ma
@@ -65,12 +65,6 @@ theorem associative_append:
  ∀A.associative (list A) (append A).
 #A #l1 #l2 #l3 (elim l1) normalize // qed.
 
-(* deleterio per auto 
-ntheorem cons_append_commute:
-  ∀A:Type.∀l1,l2:list A.∀a:A.
-    a :: (l1 @ l2) = (a :: l1) @ l2.
-//; nqed. *)
-
 theorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
 #A #a #l #l1 >associative_append // qed.
 
@@ -121,6 +115,46 @@ lemma filter_false : ∀A,l,a,p. p a = false →
 theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
 #A #B #f #g #l #eqfg (elim l) normalize // qed.
 
+(**************************** reverse *****************************)
+let rec rev_append S (l1,l2:list S) on l1 ≝
+  match l1 with 
+  [ nil ⇒ l2
+  | cons a tl ⇒ rev_append S tl (a::l2)
+  ]
+.
+
+definition reverse ≝λS.λl.rev_append S l [].
+
+lemma reverse_single : ∀S,a. reverse S [a] = [a]. 
+// qed.
+
+lemma rev_append_def : ∀S,l1,l2. 
+  rev_append S l1 l2 = (reverse S l1) @ l2 .
+#S #l1 elim l1 normalize // 
+qed.
+
+lemma reverse_cons : ∀S,a,l. reverse S (a::l) = (reverse S l)@[a].
+#S #a #l whd in ⊢ (??%?); // 
+qed.
+
+lemma reverse_append: ∀S,l1,l2. 
+  reverse S (l1 @ l2) = (reverse S l2)@(reverse S l1).
+#S #l1 elim l1 [normalize // | #a #tl #Hind #l2 >reverse_cons
+>reverse_cons // qed.
+
+lemma reverse_reverse : ∀S,l. reverse S (reverse S l) = l.
+#S #l elim l // #a #tl #Hind >reverse_cons >reverse_append 
+normalize // qed.
+
+(* an elimination principle for lists working on the tail;
+useful for strings *)
+lemma list_elim_left: ∀S.∀P:list S → Prop. P (nil S) →
+(∀a.∀tl.P tl → P (tl@[a])) → ∀l. P l.
+#S #P #Pnil #Pstep #l <(reverse_reverse … l) 
+generalize in match (reverse S l); #l elim l //
+#a #tl #H >reverse_cons @Pstep //
+qed.
+
 (**************************** length ******************************)
 
 let rec length (A:Type[0]) (l:list A) on l ≝ 
-- 
2.39.2