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

diff --git a/weblib/basics/lists/length.ma b/weblib/basics/lists/length.ma
new file mode 100644
index 000000000..a347b1066
--- /dev/null
+++ b/weblib/basics/lists/length.ma
@@ -0,0 +1,115 @@
+(**************************** length ******************************)
+
+include "basics/lists/iterators.ma".
+include "basics/lists/reverse.ma".
+include "arithmetics/nat.ma".
+
+img class="anchor" src="icons/tick.png" id="length"let rec length (A:Type[0]) (l:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A) on l ≝ 
+  match l with 
+    [ nil ⇒ a title="natural number" href="cic:/fakeuri.def(1)"0/a
+    | cons a tl ⇒ a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a (length A tl)].
+
+interpretation "list length" 'card l = (length ? l).
+
+img class="anchor" src="icons/tick.png" id="length_tail"lemma length_tail: ∀A,l. |a href="cic:/matita/basics/lists/lists/tail.def(1)"tail/a A la title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a (|la title="list length" href="cic:/fakeuri.def(1)"|/a).
+#A #l elim l // 
+qed.
+
+img class="anchor" src="icons/tick.png" id="length_tail1"lemma length_tail1 : ∀A,l.a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a |la title="list length" href="cic:/fakeuri.def(1)"|/a → |a href="cic:/matita/basics/lists/lists/tail.def(1)"tail/a A la title="list length" href="cic:/fakeuri.def(1)"|/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a |la title="list length" href="cic:/fakeuri.def(1)"|/a.
+#A * normalize //
+qed.
+
+img class="anchor" src="icons/tick.png" id="length_append"lemma length_append: ∀A.∀l1,l2:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A. 
+  |l1a title="append" href="cic:/fakeuri.def(1)"@/al2a title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |l1a title="list length" href="cic:/fakeuri.def(1)"|/aa title="natural plus" href="cic:/fakeuri.def(1)"+/a|l2a title="list length" href="cic:/fakeuri.def(1)"|/a.
+#A #l1 elim l1 // normalize /span class="autotactic"2span class="autotrace" trace /span/span/
+qed.
+
+img class="anchor" src="icons/tick.png" id="length_map"lemma length_map: ∀A,B,l.∀f:A→B. |a href="cic:/matita/basics/lists/iterators/map.fix(0,3,1)"map/a ?? f la title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |la title="list length" href="cic:/fakeuri.def(1)"|/a.
+#A #B #l #f elim l // #a #tl #Hind normalize //
+qed.
+
+img class="anchor" src="icons/tick.png" id="length_reverse"lemma length_reverse: ∀A.∀l:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A. 
+  |a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a A la title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |la title="list length" href="cic:/fakeuri.def(1)"|/a.
+#A #l elim l // #a #l0 #IH >a href="cic:/matita/basics/lists/reverse/reverse_cons.def(6)"reverse_cons/a >a href="cic:/matita/basics/lists/length/length_append.def(2)"length_append/a >IH normalize //
+qed.
+
+img class="anchor" src="icons/tick.png" id="lenght_to_nil"lemma lenght_to_nil: ∀A.∀l:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A.
+  |la title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="natural number" href="cic:/fakeuri.def(1)"0/a → l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a [ a title="nil" href="cic:/fakeuri.def(1)"]/a.
+#A * // #a #tl normalize #H destruct
+qed.
+ 
+img class="anchor" src="icons/tick.png" id="lists_length_split"lemma lists_length_split : ∀A.∀l1,l2:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A.a title="exists" href="cic:/fakeuri.def(1)"∃/ala,lba title="exists" href="cic:/fakeuri.def(1)"./a
+  (|laa title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |l1a title="list length" 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 laa title="append" href="cic:/fakeuri.def(1)"@/alb) a title="logical or" href="cic:/fakeuri.def(1)"∨/a (|laa title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |l2a title="list length" href="cic:/fakeuri.def(1)"|/a a title="logical and" href="cic:/fakeuri.def(1)"∧/a l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a laa title="append" href="cic:/fakeuri.def(1)"@/alb).
+#A #l1 elim l1
+[ #l2 %{[ a title="nil" href="cic:/fakeuri.def(1)"]/a} %{l2} % % %
+| #hd1 #tl1 #IH *
+  [ %{[ a title="nil" href="cic:/fakeuri.def(1)"]/a} %{(hd1:a title="cons" href="cic:/fakeuri.def(1)":/atl1)} %2 % %
+  | #hd2 #tl2 cases (IH tl2) #x * #y *
+    [ * #IH1 #IH2 %{(hd2:a title="cons" href="cic:/fakeuri.def(1)":/ax)} %{y} % normalize % //
+    | * #IH1 #IH2 %{(hd1:a title="cons" href="cic:/fakeuri.def(1)":/ax)} %{y} %2 normalize % // ]
+  ]
+]
+qed.
+
+(****************** traversing two lists in parallel *****************)
+img class="anchor" src="icons/tick.png" id="list_ind2"lemma list_ind2 : 
+  ∀T1,T2:Type[0].∀l1:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a T1.∀l2:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a T2.∀P:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a T1 → a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a T2 → Prop.
+  |l1a title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |l2a title="list length" href="cic:/fakeuri.def(1)"|/a →
+  (P [a title="nil" href="cic:/fakeuri.def(1)"]/a [a title="nil" href="cic:/fakeuri.def(1)"]/a) → 
+  (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1:a title="cons" href="cic:/fakeuri.def(1)":/atl1) (hd2:a title="cons" href="cic:/fakeuri.def(1)":/atl2)) → 
+  P l1 l2.
+#T1 #T2 #l1 #l2 #P #Hl #Pnil #Pcons
+generalize in match Hl; generalize in match l2;
+elim l1
+  [#l2 cases l2 // normalize #t2 #tl2 #H destruct
+  |#t1 #tl1 #IH #l2 cases l2
+    [normalize #H destruct
+    |#t2 #tl2 #H @Pcons @IH normalize in H; destruct // ]
+  ]
+qed.
+
+img class="anchor" src="icons/tick.png" id="list_cases2"lemma list_cases2 : 
+  ∀T1,T2:Type[0].∀l1:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a T1.∀l2:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a T2.∀P:Prop.
+  |l1a title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |l2a title="list length" 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 → l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a [a title="nil" href="cic:/fakeuri.def(1)"]/a → P) → 
+  (∀hd1,hd2,tl1,tl2.l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a hd1:a title="cons" href="cic:/fakeuri.def(1)":/atl1 → l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a hd2:a title="cons" href="cic:/fakeuri.def(1)":/atl2 → P) → P.
+#T1 #T2 #l1 #l2 #P #Hl @(a href="cic:/matita/basics/lists/length/list_ind2.def(3)"list_ind2/a … Hl)
+  [ #Pnil #Pcons @Pnil //
+  | #tl1 #tl2 #hd1 #hd2 #IH1 #IH2 #Hp @Hp // ]
+qed.
+
+(*********************** properties of append ***********************)
+img class="anchor" src="icons/tick.png" id="append_l1_injective"lemma append_l1_injective : 
+  ∀A.∀l1,l2,l3,l4:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A. |l1a title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |l2a title="list length" href="cic:/fakeuri.def(1)"|/a → l1a title="append" href="cic:/fakeuri.def(1)"@/al3 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l2a title="append" href="cic:/fakeuri.def(1)"@/al4 → l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l2.
+#a #l1 #l2 #l3 #l4 #Hlen @(a href="cic:/matita/basics/lists/length/list_ind2.def(3)"list_ind2/a … Hlen) //
+#tl1 #tl2 #hd1 #hd2 #IH normalize #Heq destruct @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a /span class="autotactic"2span class="autotrace" trace /span/span/
+qed.
+  
+img class="anchor" src="icons/tick.png" id="append_l2_injective"lemma append_l2_injective : 
+  ∀A.∀l1,l2,l3,l4:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A. |l1a title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |l2a title="list length" href="cic:/fakeuri.def(1)"|/a → l1a title="append" href="cic:/fakeuri.def(1)"@/al3 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l2a title="append" href="cic:/fakeuri.def(1)"@/al4 → l3 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l4.
+#a #l1 #l2 #l3 #l4 #Hlen @(a href="cic:/matita/basics/lists/length/list_ind2.def(3)"list_ind2/a … Hlen) normalize //
+#tl1 #tl2 #hd1 #hd2 #IH normalize #Heq destruct /span class="autotactic"2span class="autotrace" trace /span/span/
+qed.
+
+img class="anchor" src="icons/tick.png" id="append_l1_injective_r"lemma append_l1_injective_r :
+  ∀A.∀l1,l2,l3,l4:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A. |l3a title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |l4a title="list length" href="cic:/fakeuri.def(1)"|/a → l1a title="append" href="cic:/fakeuri.def(1)"@/al3 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l2a title="append" href="cic:/fakeuri.def(1)"@/al4 → l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l2.
+#a #l1 #l2 #l3 #l4 #Hlen #Heq lapply (a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a … (a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a ?) … Heq)
+>a href="cic:/matita/basics/lists/reverse/reverse_append.def(7)"reverse_append/a >a href="cic:/matita/basics/lists/reverse/reverse_append.def(7)"reverse_append/a #Heq1
+lapply (a href="cic:/matita/basics/lists/length/append_l2_injective.def(4)"append_l2_injective/a … Heq1) [ // ] #Heq2
+lapply (a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a … (a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a ?) … Heq2) //
+qed.
+  
+img class="anchor" src="icons/tick.png" id="append_l2_injective_r"lemma append_l2_injective_r : 
+  ∀A.∀l1,l2,l3,l4:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A. |l3a title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |l4a title="list length" href="cic:/fakeuri.def(1)"|/a → l1a title="append" href="cic:/fakeuri.def(1)"@/al3 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l2a title="append" href="cic:/fakeuri.def(1)"@/al4 → l3 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l4.
+#a #l1 #l2 #l3 #l4 #Hlen #Heq lapply (a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a … (a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a ?) … Heq)
+>a href="cic:/matita/basics/lists/reverse/reverse_append.def(7)"reverse_append/a >a href="cic:/matita/basics/lists/reverse/reverse_append.def(7)"reverse_append/a #Heq1
+lapply (a href="cic:/matita/basics/lists/length/append_l1_injective.def(4)"append_l1_injective/a … Heq1) [ // ] #Heq2
+lapply (a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a … (a href="cic:/matita/basics/lists/reverse/reverse.def(2)"reverse/a ?) … Heq2) //
+qed.
+
+img class="anchor" src="icons/tick.png" id="length_rev_append"lemma length_rev_append: ∀A.∀l,acc:a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"list/a A. 
+  |a href="cic:/matita/basics/lists/reverse/rev_append.fix(0,1,1)"rev_append/a ? l acca title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a |la title="list length" href="cic:/fakeuri.def(1)"|/aa title="natural plus" href="cic:/fakeuri.def(1)"+/a|acca title="list length" href="cic:/fakeuri.def(1)"|/a.
+#A #l elim l // #a #tl #Hind normalize 
+#acc >Hind normalize // 
+qed.
+ 
\ No newline at end of file