From: matitaweb Date: Wed, 7 Mar 2012 10:37:05 +0000 (+0000) Subject: commit by user utente2 X-Git-Tag: make_still_working~1883 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=111e641bb0772a542293b796c9d4a18fc9d58a00;p=helm.git commit by user utente2 --- diff --git a/weblib/basics/list.ma b/weblib/basics/list.ma index 39fdb1bd5..4e44ce298 100644 --- a/weblib/basics/list.ma +++ b/weblib/basics/list.ma @@ -134,7 +134,7 @@ let rec rev_append S (l1,l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"li 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]. +lemma reverse_single : ∀S,a. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]). // qed. lemma rev_append_def : ∀S,l1,l2. @@ -142,7 +142,7 @@ lemma rev_append_def : ∀S,l1,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]. +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)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]). #S #a #l whd in ⊢ (??%?); // qed. @@ -158,7 +158,7 @@ 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. +(∀a.∀tl.P tl → P (tla title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]))) → ∀l. P l.span class="error" title="Parse error: SYMBOL ':' or RPAREN expected after [term] (in [term])"/span #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 //