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