1 (**************************** reverse *****************************)
3 include "basics/lists/iterators.ma".
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 ≝
8 | cons a tl ⇒ rev_append S tl (a:
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6l2)
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.
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.
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]
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 ⊢ (??%?); //
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.
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 %
36 (* an elimination principle for lists working on the tail;
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 //