From: matitaweb Date: Thu, 8 Mar 2012 07:55:11 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~1870 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=7c14b7c4725bfca4aa69098ad3cb704c68cb1aa8 commit by user andrea --- diff --git a/weblib/tutorial/chapter5.ma b/weblib/tutorial/chapter5.ma index 5e60831d0..e5d226c32 100644 --- a/weblib/tutorial/chapter5.ma +++ b/weblib/tutorial/chapter5.ma @@ -127,10 +127,18 @@ let rec unique_append (S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0 if a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a r then r else aa title="cons" href="cic:/fakeuri.def(1)":/a:r ]. +lemma memb_unique_append: ∀S,a,l1,l2. + a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a S l1 l2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l1a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="logical or" href="cic:/fakeuri.def(1)"∨/a a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. +#S #a #l1 elim l1 normalize [#l2 #H %2 //] +#b #tl #Hind #l2 cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a … (aa title="eqb" href="cic:/fakeuri.def(1)"=/a=b)) #Hab >Hab normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/bool/orb_true_l.def(2)"orb_true_l/a/span/span/ +cases (a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S b (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a S tl l2)) normalize + [@Hind | >Hab normalize @Hind] +qed. + lemma unique_append_elim: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀P: S → Prop.∀l1,l2. -(∀x. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aspan class="error" title="Parse error: NUMBER '1' or [term] or [sym=] expected after [sym=] (in [term])"/span a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → P x) → (∀x. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → P x) → -∀x. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a S l1 l2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → P x. -#S #P #l1 #l2 #Hl1 #Hl2 #x #membx cases (memb_unique_append … membx) /2/ + (∀x. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x l1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aspan class="error" title="Parse error: NUMBER '1' or [term] or [sym=] expected after [sym=] (in [term])"/span a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → P x) → (∀x. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → P x) → + ∀x. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x (a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"unique_append/a S l1 l2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → P x. +#S #P #l1 #l2 #Hl1 #Hl2 #x #membx cases (a href="cic:/matita/tutorial/chapter5/memb_unique_append.def(6)"memb_unique_append/aspan class="error" title="No choices for ID memb_unique_append"/span … membx) /span class="autotactic"2span class="autotrace" trace /span/span/ qed. lemma unique_append_unique: ∀S,l1,l2. a href="cic:/matita/tutorial/chapter5/uniqueb.fix(0,1,5)"uniqueb/a S l2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → @@ -199,7 +207,7 @@ qed. (*h2 class="section"Filtering/h2*) -lemma filter_true: ∀S,f,a,l. +lemma memb_filter_true: ∀S,f,a,l. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S a (a href="cic:/matita/basics/list/filter.def(2)"filter/a S f l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → f a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a. #S #f #a #l elim l [normalize #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/] #b #tl #Hind cases (a href="cic:/matita/basics/bool/true_or_false.def(1)"true_or_false/a (f b)) #H @@ -217,7 +225,7 @@ qed. lemma memb_filter: ∀S,f,l,x. a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x (a href="cic:/matita/basics/list/filter.def(2)"filter/a ? f l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="logical and" href="cic:/fakeuri.def(1)"∧/a (f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a). -/span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a, a href="cic:/matita/tutorial/chapter5/memb_filter_memb.def(5)"memb_filter_memb/a, a href="cic:/matita/tutorial/chapter5/filter_true.def(5)"filter_true/a/span/span/ qed. +/span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a, a href="cic:/matita/tutorial/chapter5/memb_filter_memb.def(5)"memb_filter_memb/a, a href="cic:/matita/tutorial/chapter5/memb_filter_true.def(5)"memb_filter_true/a/span/span/ qed. lemma memb_filter_l: ∀S,f,x,l. (f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) → a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x l a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"memb/a S x (a href="cic:/matita/basics/list/filter.def(2)"filter/a ? f l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.