weblib/basics/lists/reverse.ma

   1 (**************************** reverse *****************************)
   2
   3 include "basics/lists/iterators.ma".
   4
   5 \ 5img class="anchor" src="icons/tick.png" id="rev_append"\ 6let rec rev_append S (l1,l2:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 S) on l1 ≝
   6   match l1 with
   7   [ nil ⇒ l2
   8   | cons a tl ⇒ rev_append S tl (a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l2)
   9   ]
  10 .
  11
  12 \ 5img class="anchor" src="icons/tick.png" id="reverse"\ 6definition reverse ≝λS.λl.\ 5a href="cic:/matita/basics/lists/reverse/rev_append.fix(0,1,1)"\ 6rev_append\ 5/a\ 6 S l [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
  13
  14 \ 5img class="anchor" src="icons/tick.png" id="reverse_single"\ 6lemma reverse_single : ∀S,a. \ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 S \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6a\ 5a title="nil" 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="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6a\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
  15 // qed.
  16
  17 \ 5img class="anchor" src="icons/tick.png" id="rev_append_def"\ 6lemma rev_append_def : ∀S,l1,l2.
  18   \ 5a href="cic:/matita/basics/lists/reverse/rev_append.fix(0,1,1)"\ 6rev_append\ 5/a\ 6 S l1 l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l1) \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 l2 .
  19 #S #l1 elim l1 normalize
  20   [// | #a #tl #Hind #l2 >Hind >(Hind \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6a\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6) >\ 5a href="cic:/matita/basics/lists/append/associative_append.def(4)"\ 6associative_append\ 5/a\ 6 @\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6]
  21 qed.
  22
  23 \ 5img class="anchor" src="icons/tick.png" id="reverse_cons"\ 6lemma reverse_cons : ∀S,a,l. \ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 S (a:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l)\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6a\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
  24 #S #a #l whd in ⊢ (??%?); //
  25 qed.
  26
  27 \ 5img class="anchor" src="icons/tick.png" id="reverse_append"\ 6lemma reverse_append: ∀S,l1,l2.
  28   \ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 S (l1 \ 5a title="append" 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 href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l2)\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(\ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l1).
  29 #S #l1 elim l1 [normalize // | #a #tl #Hind #l2 >\ 5a href="cic:/matita/basics/lists/reverse/reverse_cons.def(6)"\ 6reverse_cons\ 5/a\ 6
  30 >\ 5a href="cic:/matita/basics/lists/reverse/reverse_cons.def(6)"\ 6reverse_cons\ 5/a\ 6 >Hind // qed.
  31
  32 \ 5img class="anchor" src="icons/tick.png" id="reverse_reverse"\ 6lemma reverse_reverse : ∀S,l. \ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 S (\ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l.
  33 #S #l elim l // #a #tl #Hind >\ 5a href="cic:/matita/basics/lists/reverse/reverse_cons.def(6)"\ 6reverse_cons\ 5/a\ 6 >\ 5a href="cic:/matita/basics/lists/reverse/reverse_append.def(7)"\ 6reverse_append\ 5/a\ 6 >Hind %
  34 qed.
  35
  36 (* an elimination principle for lists working on the tail;
  37 useful for strings *)
  38 \ 5img class="anchor" src="icons/tick.png" id="list_elim_left"\ 6lemma list_elim_left: ∀S.∀P:\ 5a href="cic:/matita/basics/lists/lists/list.ind(1,0,1)"\ 6list\ 5/a\ 6 S → Prop. P (\ 5a href="cic:/matita/basics/lists/lists/list.con(0,1,1)"\ 6nil\ 5/a\ 6 S) →
  39 (∀a.∀tl.P tl → P (tl\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6a\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6)) → ∀l. P l.
  40 #S #P #Pnil #Pstep #l <(\ 5a href="cic:/matita/basics/lists/reverse/reverse_reverse.def(8)"\ 6reverse_reverse\ 5/a\ 6 … l)
  41 generalize in match (\ 5a href="cic:/matita/basics/lists/reverse/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l); #l elim l //
  42 #a #tl #H >\ 5a href="cic:/matita/basics/lists/reverse/reverse_cons.def(6)"\ 6reverse_cons\ 5/a\ 6 @Pstep //
  43 qed.