From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Fri, 16 Sep 2011 12:17:47 +0000 (+0000)
Subject: mah...
X-Git-Tag: make_still_working~2279
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cf367920b94b3a95c5c068c2f0672b97bf579731;p=helm.git

mah...
---

diff --git a/weblib/basics/list.ma b/weblib/basics/list.ma
index 798f57629..14f7aaaa7 100644
--- a/weblib/basics/list.ma
+++ b/weblib/basics/list.ma
@@ -9,8 +9,8 @@
      \ /   GNU General Public License Version 2   
       V_______________________________________________________________ *)
 
-include "basics/types.ma".
-include "arithmetics/nat.ma".
+include "basics/bool.ma".
+(* include "arithmetics/nat.ma". *)
 
 inductive list (A:Type[0]) : Type[0] :=
   | nil: list A
@@ -31,12 +31,12 @@ notation "hvbox(l1 break @ l2)"
 interpretation "nil" 'nil = (nil ?).
 interpretation "cons" 'cons hd tl = (cons ? hd tl).
 
-definition not_nil: ∀A:Type[0].list A → Prop ≝
- λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ].
+definition not_nil: ∀A:Type[0].a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A → Prop ≝
+ λA.λl.match l with [ nil ⇒ a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a | cons hd tl ⇒ a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a ].
 
 theorem nil_cons:
-  ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
-  #A #l #a @nmk #Heq (change with (not_nil ? (a::l))) >Heq //
+  ∀A:Type[0].∀l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀a:A. aa title="cons" href="cic:/fakeuri.def(1)":/a:l a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a title="nil" href="cic:/fakeuri.def(1)"[/a].
+  #A #l #a @a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a #Heq (change with (a href="cic:/matita/basics/list/not_nil.def(1)"not_nil/a ? (aa title="cons" href="cic:/fakeuri.def(1)":/a:l))) >Heq //
 qed.
 
 (*
@@ -45,24 +45,24 @@ let rec id_list A (l: list A) on l :=
   [ nil => []
   | (cons hd tl) => hd :: id_list A tl ]. *)
 
-let rec append A (l1: list A) l2 on l1 ≝ 
+let rec append A (l1: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) l2 on l1 ≝ 
   match l1 with
   [ nil ⇒  l2
-  | cons hd tl ⇒  hd :: append A tl l2 ].
+  | cons hd tl ⇒  hd a title="cons" href="cic:/fakeuri.def(1)":/a: append A tl l2 ].
 
-definition hd ≝ λA.λl: list A.λd:A.
+definition hd ≝ λA.λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.λd:A.
   match l with [ nil ⇒ d | cons a _ ⇒ a].
 
-definition tail ≝  λA.λl: list A.
-  match l with [ nil ⇒  [] | cons hd tl ⇒  tl].
+definition tail ≝  λA.λl: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.
+  match l with [ nil ⇒  a title="nil" href="cic:/fakeuri.def(1)"[/a] | cons hd tl ⇒  tl].
 
 interpretation "append" 'append l1 l2 = (append ? l1 l2).
 
-theorem append_nil: ∀A.∀l:list A.l @ [] = l.
+theorem append_nil: ∀A.∀l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.l a title="append" href="cic:/fakeuri.def(1)"@/a a title="nil" href="cic:/fakeuri.def(1)"[/a] a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l.
 #A #l (elim l) normalize // qed.
 
 theorem associative_append: 
- ∀A.associative (list A) (append A).
+ ∀A.a href="cic:/matita/basics/relations/associative.def(1)"associative/a (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) (a href="cic:/matita/basics/list/append.fix(0,1,1)"append/a A).
 #A #l1 #l2 #l3 (elim l1) normalize // qed.
 
 (* deleterio per auto 
@@ -71,50 +71,51 @@ ntheorem cons_append_commute:
     a :: (l1 @ l2) = (a :: l1) @ l2.
 //; nqed. *)
 
-theorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
+theorem append_cons:∀A.∀a:A.∀l,l1.la title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:l1)a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a(la title="append" href="cic:/fakeuri.def(1)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/aa])a title="append" href="cic:/fakeuri.def(1)"@/al1.
 /2/ qed.
 
-theorem nil_append_elim: ∀A.∀l1,l2: list A.∀P:?→?→Prop. 
-  l1@l2=[] → P (nil A) (nil A) → P l1 l2.
+theorem nil_append_elim: ∀A.∀l1,l2: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀P:?→?→Prop. 
+  l1a title="append" href="cic:/fakeuri.def(1)"@/al2a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa title="nil" href="cic:/fakeuri.def(1)"[/a] → P (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a A) (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a A) → P l1 l2.
 #A #l1 #l2 #P (cases l1) normalize //
 #a #l3 #heq destruct
 qed.
 
-theorem nil_to_nil:  ∀A.∀l1,l2:list A.
-  l1@l2 = [] → l1 = [] ∧ l2 = [].
-#A #l1 #l2 #isnil @(nil_append_elim A l1 l2) /2/
+theorem nil_to_nil:  ∀A.∀l1,l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.
+  l1a title="append" href="cic:/fakeuri.def(1)"@/al2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/a] → l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/a] a title="logical and" href="cic:/fakeuri.def(1)"∧/a l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="nil" href="cic:/fakeuri.def(1)"[/a].
+#A #l1 #l2 #isnil @(a href="cic:/matita/basics/list/nil_append_elim.def(3)"nil_append_elim/a A l1 l2) /2/
 qed.
 
 (* iterators *)
 
-let rec map (A,B:Type[0]) (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)].
+let rec map (A,B:Type[0]) (f: A → B) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l: a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a B ≝
+ match l with [ nil ⇒ a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a ? | cons x tl ⇒ f x a title="cons" href="cic:/fakeuri.def(1)":/a: (map A B f tl)].
   
-let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝  
+let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l :B ≝  
  match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
  
 definition filter ≝ 
-  λT.λp:T → bool.
-  foldr T (list T) (λx,l0.if_then_else ? (p x) (x::l0) l0) (nil T).
+  λT.λp:T → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a.
+  a href="cic:/matita/basics/list/foldr.fix(0,4,1)"foldr/a T (a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a T) (λx,l0.a href="cic:/matita/basics/bool/if_then_else.def(1)"if_then_else/a ? (p x) (xa title="cons" href="cic:/fakeuri.def(1)":/a:l0) l0) (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a T).
 
-lemma filter_true : ∀A,l,a,p. p a = true → 
-  filter A p (a::l) = a :: filter A p l.
+lemma filter_true : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → 
+  a href="cic:/matita/basics/list/filter.def(2)"filter/a A p (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a a title="cons" href="cic:/fakeuri.def(1)":/a: a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l.
 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
 
-lemma filter_false : ∀A,l,a,p. p a = false → 
-  filter A p (a::l) = filter A p l.
+lemma filter_false : ∀A,l,a,p. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → 
+  a href="cic:/matita/basics/list/filter.def(2)"filter/a A p (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/filter.def(2)"filter/a A p l.
 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
 
-theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
+theorem eq_map : ∀A,B,f,g,l. (∀x.f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g x) → a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B f l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/list/map.fix(0,3,1)"map/a A B g l.
 #A #B #f #g #l #eqfg (elim l) normalize // qed.
 
+(*
 let rec dprodl (A:Type[0]) (f:A→Type[0]) (l1:list A) (g:(∀a:A.list (f a))) on l1 ≝
 match l1 with
-  [ nil ⇒ nil ?
+  [ nil ⇒ nil ?  
   | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g
-  ].
+  ]. *)
 
-(**************************** length ******************************)
+(**************************** length ******************************
 
 let rec length (A:Type[0]) (l:list A) on l ≝ 
   match l with 
@@ -129,12 +130,12 @@ let rec nth n (A:Type[0]) (l:list A) (d:A)  ≝
     [O ⇒ hd A l d
     |S m ⇒ nth m A (tail A l) d].
 
-(**************************** fold *******************************)
+**************************** fold *******************************)
 
-let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→bool) (f:A→B) (l:list A) on l :B ≝  
+let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a) (f:A→B) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l :B ≝  
  match l with 
   [ nil ⇒ b 
-  | cons a l ⇒ if_then_else ? (p a) (op (f a) (fold A B op b p f l))
+  | cons a l ⇒ a href="cic:/matita/basics/bool/if_then_else.def(1)"if_then_else/a ? (p a) (op (f a) (fold A B op b p f l))
       (fold A B op b p f l)].
       
 notation "\fold  [ op , nil ]_{ ident i ∈ l | p} f"
@@ -148,38 +149,38 @@ for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}.
 interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
 
 theorem fold_true: 
-∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a = true → 
-  \fold[op,nil]_{i ∈ a::l| p i} (f i) = 
-    op (f a) \fold[op,nil]_{i ∈ l| p i} (f i). 
+∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → 
+  a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ aa title="cons" href="cic:/fakeuri.def(1)":/a:l| p i} (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+    op (f a) a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p i} (f i). 
 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
 
 theorem fold_false: 
 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
-p a = false → \fold[op,nil]_{i ∈ a::l| p i} (f i) = 
-  \fold[op,nil]_{i ∈ l| p i} (f i).
+p a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a → a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ aa title="cons" href="cic:/fakeuri.def(1)":/a:l| p i} (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+  a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p i} (f i).
 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
 
 theorem fold_filter: 
 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
-  \fold[op,nil]_{i ∈ l| p i} (f i) = 
-    \fold[op,nil]_{i ∈ (filter A p l)} (f i).
+  a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ l| p i} (f i) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 
+    a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i ∈ (a href="cic:/matita/basics/list/filter.def(2)"filter/a A p l)} (f i).
 #A #B #a #l #p #op #nil #f elim l //  
-#a #tl #Hind cases(true_or_false (p a)) #pa 
-  [ >filter_true // > fold_true // >fold_true //
-  | >filter_false // >fold_false // ]
+#a #tl #Hind cases(a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (p a)) #pa 
+  [ >a href="cic:/matita/basics/list/filter_true.def(3)"filter_true/a // > a href="cic:/matita/basics/list/fold_true.def(3)"fold_true/a // >a href="cic:/matita/basics/list/fold_true.def(3)"fold_true/a //
+  | >a href="cic:/matita/basics/list/filter_false.def(3)"filter_false/a // >a href="cic:/matita/basics/list/fold_false.def(3)"fold_false/a // ]
 qed.
 
 record Aop (A:Type[0]) (nil:A) : Type[0] ≝
   {op :2> A → A → A; 
-   nill:∀a. op nil a = a; 
-   nilr:∀a. op a nil = a;
-   assoc: ∀a,b,c.op a (op b c) = op (op a b) c
+   nill:∀a. op nil a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a; 
+   nilr:∀a. op a nil a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a;
+   assoc: ∀a,b,c.op a (op b c) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a op (op a b) c
   }.
 
-theorem fold_sum: ∀A,B. ∀I,J:list A.∀nil.∀op:Aop B nil.∀f.
-  op (\fold[op,nil]_{i∈I} (f i)) (\fold[op,nil]_{i∈J} (f i)) =
-    \fold[op,nil]_{i∈(I@J)} (f i).
+theorem fold_sum: ∀A,B. ∀I,J:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A.∀nil.∀op:a href="cic:/matita/basics/list/Aop.ind(1,0,2)"Aop/a B nil.∀f.
+  op (a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈I} (f i)) (a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈J} (f i)) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a
+    a title="\fold" href="cic:/fakeuri.def(1)"\fold/a[op,nil]_{i∈(Ia title="append" href="cic:/fakeuri.def(1)"@/aJ)} (f i).
 #A #B #I #J #nil #op #f (elim I) normalize 
-  [>nill //|#a #tl #Hind <assoc //]
+  [>a href="cic:/matita/basics/list/nill.fix(0,2,2)"nill/a //|#a #tl #Hind <a href="cic:/matita/basics/list/assoc.fix(0,2,2)"assoc/a //]
 qed.
 
diff --git a/weblib/basics/types.ma b/weblib/basics/types.ma
index c14cc60b4..494177cfc 100644
--- a/weblib/basics/types.ma
+++ b/weblib/basics/types.ma
@@ -25,10 +25,10 @@ interpretation "Pair construction" 'pair x y = (pair ? ? x y).
 
 interpretation "Product" 'product x y = (Prod x y).
 
-definition fst ≝ λA,B.λp:A × B.
+definition fst ≝ λA,B.λp:A a title="Product" href="cic:/fakeuri.def(1)"×/a B.
   match p with [pair a b ⇒ a]. 
 
-definition snd ≝ λA,B.λp:A × B.
+definition snd ≝ λA,B.λp:A a title="Product" href="cic:/fakeuri.def(1)"×/a B.
   match p with [pair a b ⇒ b].
 
 interpretation "pair pi1" 'pi1 = (fst ? ?).
@@ -38,8 +38,8 @@ interpretation "pair pi2" 'pi2a x = (snd ? ? x).
 interpretation "pair pi1" 'pi1b x y = (fst ? ? x y).
 interpretation "pair pi2" 'pi2b x y = (snd ? ? x y).
 
-theorem eq_pair_fst_snd: ∀A,B.∀p:A × B.
-  p = 〈 \fst p, \snd p 〉.
+theorem eq_pair_fst_snd: ∀A,B.∀p:A a title="Product" href="cic:/fakeuri.def(1)"×/a B.
+  p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a p, a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a p 〉.
 #A #B #p (cases p) // qed.
 
 (* sum *)