X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Flist%2Flist.ma;h=077e1af6c443682939461692d20bdfc20f60be22;hb=7c4bb1d1baed259e4301d4cf0ecca7a0e3885d92;hp=a180cbabc8b5d4dfcd7a6d0aea16440adde1ef97;hpb=bfb7fbf61e86114e49cb3671503e8307a4582342;p=helm.git

diff --git a/helm/software/matita/library/list/list.ma b/helm/software/matita/library/list/list.ma
index a180cbabc..077e1af6c 100644
--- a/helm/software/matita/library/list/list.ma
+++ b/helm/software/matita/library/list/list.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/list/".
 include "logic/equality.ma".
 include "datatypes/bool.ma".
 include "higher_order_defs/functions.ma".
@@ -24,7 +23,7 @@ inductive list (A:Type) : Type :=
   | cons: A -> list A -> list A.
 
 notation "hvbox(hd break :: tl)"
-  right associative with precedence 46
+  right associative with precedence 47
   for @{'cons $hd $tl}.
 
 notation "[ list0 x sep ; ]"
@@ -35,15 +34,13 @@ notation "hvbox(l1 break @ l2)"
   right associative with precedence 47
   for @{'append $l1 $l2 }.
 
-interpretation "nil" 'nil = (cic:/matita/list/list/list.ind#xpointer(1/1/1) _).
-interpretation "cons" 'cons hd tl =
-  (cic:/matita/list/list/list.ind#xpointer(1/1/2) _ hd tl).
+interpretation "nil" 'nil = (nil ?).
+interpretation "cons" 'cons hd tl = (cons ? hd tl).
 
 (* theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: []. *)
 
 theorem nil_cons:
-  \forall A:Type.\forall l:list A.\forall a:A.
-    a::l <> [].
+  \forall A:Type.\forall l:list A.\forall a:A. a::l ≠ [].
   intros;
   unfold Not;
   intros;
@@ -65,7 +62,7 @@ definition tail := \lambda A:Type. \lambda l: list A.
   [ nil => []
   | (cons hd tl) => tl].
 
-interpretation "append" 'append l1 l2 = (cic:/matita/list/list/append.con _ l1 l2).
+interpretation "append" 'append l1 l2 = (append ? l1 l2).
 
 theorem append_nil: \forall A:Type.\forall l:list A.l @ [] = l.
   intros;
@@ -112,8 +109,8 @@ with permut1 : list A -> list A -> Prop \def
   | step : \forall l1,l2:list A. \forall x,y:A. 
       permut1 ? (l1 @ (x :: y :: l2)) (l1 @ (y :: x :: l2)).
 
-include "nat/nat.ma".  
-   
+(*
+
 definition x1 \def S O.
 definition x2 \def S x1.
 definition x3 \def S x2.
@@ -124,15 +121,9 @@ theorem tmp : permutation nat (x1 :: x2 :: x3 :: []) (x1 :: x3 :: x2 :: []).
   apply (step ? (x1::[]) [] x2 x3).
   qed. 
 
-
-(*
 theorem nil_append_nil_both:
   \forall A:Type.\forall l1,l2:list A.
     l1 @ l2 = [] \to l1 = [] \land l2 = [].
-*)
-
-(*
-include "nat/nat.ma".
 
 theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: []. 
 reflexivity.
@@ -142,23 +133,32 @@ theorem test_append: [O;O;O;O;O;O] = [O;O;O] @ [O;O] @ [O].
 simplify.
 reflexivity.
 qed.
+
 *)
 
-let rec nth (A:Type) l d n on n ≝
- match n with
-  [ O ⇒
-     match l with
-      [ nil ⇒ d
-      | cons (x : A) _ ⇒ x
-      ]
-  | S n' ⇒ nth A (tail ? l) d n'
-  ].
+definition nth ≝
+  λA:Type.
+    let rec nth l d n on n ≝
+      match n with
+      [ O ⇒
+         match l with
+         [ nil ⇒ d
+         | cons (x : A) _ ⇒ x
+         ]
+      | S n' ⇒ nth (tail ? l) d n']
+    in nth.
   
-let rec map (A,B:Type) (f: A → B) (l : list A) on l : list B ≝
-  match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
+definition map ≝
+  λA,B:Type.λf:A→B.
+  let rec map (l : list A) on l : list B ≝
+    match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map tl)]
+  in map.
   
-let rec foldr (A,B:Type) (f : A → B → B) (b : B) (l : list A) on l : B := 
-  match l with [ nil ⇒ b | (cons a l) ⇒ f a (foldr ? ? f b l)].
+definition foldr ≝
+  λA,B:Type.λf:A→B→B.λb:B.
+  let rec foldr (l : list A) on l : B := 
+    match l with [ nil ⇒ b | (cons a l) ⇒ f a (foldr l)]
+  in foldr.
    
 definition length ≝ λT:Type.λl:list T.foldr T nat (λx,c.S c) O l.
 
@@ -178,21 +178,26 @@ lemma list_ind2 :
   (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) → 
   P l1 l2.
 intros (T1 T2 l1 l2 P Hl Pnil Pcons);
-generalize in match Hl; clear Hl; generalize in match l2; clear l2;
-elim l1 1 (l2 x1); [ cases l2; intros (Hl); [assumption| simplify in Hl; destruct Hl]]
+elim l1 in Hl l2 ⊢ % 1 (l2 x1); [ cases l2; intros (Hl); [assumption| simplify in Hl; destruct Hl]]
 intros 3 (tl1 IH l2); cases l2; [1: simplify; intros 1 (Hl); destruct Hl] 
 intros 1 (Hl); apply Pcons; apply IH; simplify in Hl; destruct Hl; assumption;
 qed.
 
 lemma eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
 intros (A B f g l Efg); elim l; simplify; [1: reflexivity ];
-rewrite > (Efg t); rewrite > H; reflexivity;  
+rewrite > (Efg a); rewrite > H; reflexivity;  
 qed.
 
 lemma le_length_filter : \forall A,l,p.length A (filter A l p) \leq length A l.
 intros;elim l
   [simplify;apply le_n
-  |simplify;apply (bool_elim ? (p t));intro
+  |simplify;apply (bool_elim ? (p a));intro
      [simplify;apply le_S_S;assumption
      |simplify;apply le_S;assumption]]
-qed.
\ No newline at end of file
+qed.
+
+lemma length_append : ∀A,l,m.length A (l@m) = length A l + length A m.
+intros;elim l
+[reflexivity
+|simplify;rewrite < H;reflexivity]
+qed.