From: matitaweb Date: Tue, 6 Mar 2012 18:09:27 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~1891 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=44ef2738ac6d7544c22950602eecf1eb61a80729;p=helm.git commit by user andrea --- diff --git a/weblib/basics/list.ma b/weblib/basics/list.ma index e699b626a..39fdb1bd5 100644 --- a/weblib/basics/list.ma +++ b/weblib/basics/list.ma @@ -9,7 +9,7 @@ \ / GNU General Public License Version 2 V_______________________________________________________________ *) -include "arithmetics/nat.ma". +include "arithmetics/nat.ma".span class="error" title="disambiguation error"/span inductive list (A:Type[0]) : Type[0] := | nil: list A @@ -124,6 +124,46 @@ match l1 with | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g ]. *) +(**************************** reverse *****************************) +let rec rev_append S (l1,l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a S) on l1 ≝ + match l1 with + [ nil ⇒ l2 + | cons a tl ⇒ rev_append S tl (aa title="cons" href="cic:/fakeuri.def(1)":/a:l2) + ] +. + +definition reverse ≝λS.λl.a href="cic:/matita/basics/list/rev_append.fix(0,1,1)"rev_append/a S l a title="nil" href="cic:/fakeuri.def(1)"[/a]. + +lemma reverse_single : ∀S,a. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S a title="cons" href="cic:/fakeuri.def(1)"[/aa] a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="cons" href="cic:/fakeuri.def(1)"[/aa]. +// qed. + +lemma rev_append_def : ∀S,l1,l2. + a href="cic:/matita/basics/list/rev_append.fix(0,1,1)"rev_append/a S l1 l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l1) a title="append" href="cic:/fakeuri.def(1)"@/a l2 . +#S #l1 elim l1 normalize // +qed. + +lemma reverse_cons : ∀S,a,l. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (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/reverse.def(2)"reverse/a S l)a title="append" href="cic:/fakeuri.def(1)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/aa]. +#S #a #l whd in ⊢ (??%?); // +qed. + +lemma reverse_append: ∀S,l1,l2. + a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (l1 a title="append" href="cic:/fakeuri.def(1)"@/a l2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l2)a title="append" href="cic:/fakeuri.def(1)"@/a(a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l1). +#S #l1 elim l1 [normalize // | #a #tl #Hind #l2 >a href="cic:/matita/basics/list/reverse_cons.def(7)"reverse_cons/a +>a href="cic:/matita/basics/list/reverse_cons.def(7)"reverse_cons/a // qed. + +lemma reverse_reverse : ∀S,l. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a l. +#S #l elim l // #a #tl #Hind >a href="cic:/matita/basics/list/reverse_cons.def(7)"reverse_cons/a >a href="cic:/matita/basics/list/reverse_append.def(8)"reverse_append/a +normalize // qed. + +(* an elimination principle for lists working on the tail; +useful for strings *) +lemma list_elim_left: ∀S.∀P:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a S → Prop. P (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a S) → +(∀a.∀tl.P tl → P (tla title="append" href="cic:/fakeuri.def(1)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/aa])) → ∀l. P l. +#S #P #Pnil #Pstep #l <(a href="cic:/matita/basics/list/reverse_reverse.def(9)"reverse_reverse/a … l) +generalize in match (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l); #l elim l // +#a #tl #H >a href="cic:/matita/basics/list/reverse_cons.def(7)"reverse_cons/a @Pstep // +qed. + (**************************** length *******************************) let rec length (A:Type[0]) (l:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a A) on l ≝