From bbb3d322ec78bbcccb218bafc96824a1f9491520 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Wed, 16 Nov 2011 09:16:28 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter4.ma | 60 ++++++++++++++++--------------------- 1 file changed, 25 insertions(+), 35 deletions(-) diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma index 6cb68782b..272465561 100644 --- a/weblib/tutorial/chapter4.ma +++ b/weblib/tutorial/chapter4.ma @@ -84,8 +84,8 @@ match r with | star r1 ⇒ (in_l ? r1)a title="star lang" href="cic:/fakeuri.def(1)"^/a* ]. -notation "\sem{E}" non associative with precedence 75 for @{'in_l $E}. -interpretation "in_l" 'in_l E = (in_l ? E). +notation "\sem{E}" non associative with precedence 75 for @{'sem $E}. +interpretation "in_l" 'sem E = (in_l ? E). interpretation "in_l mem" 'mem w l = (in_l ? l w). notation "a ∨ b" left associative with precedence 30 for @{'orb $a $b}. @@ -137,55 +137,45 @@ let rec forget (S: a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"Alph notation "| e |" non associative with precedence 65 for @{'fmap $e}. interpretation "forget" 'fmap a = (forget ? a). -lemma foo:∀a. 'fst a = 0. - -notation "\fst term 90 x" non associative with precedence 90 for @{'fst $x}. -interpretation "fst" 'fst x = (fst ? ? x). -notation "\snd term 90 x" non associative with precedence 90 for @{'snd $x}. -interpretation "snd" 'snd x = (snd ? ? x). - -(* notation "\sem{E}" non associative with precedence 75 for @{in_pl ? $E}. *) - -let rec in_pl (S : Alpha) (r : pitem S) on r : word S → Prop ≝ +let rec in_pl (S : a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"Alpha/a) (r : a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"pitem/a S) on r : a href="cic:/matita/tutorial/chapter4/word.def(3)"word/a S → Prop ≝ match r with - [ pzero ⇒ ∅ - | pepsilon ⇒ ∅ - | pchar _ ⇒ ∅ - | ppoint x ⇒ {: x::[] } - | pconcat pe1 pe2 ⇒ in_pl ? pe1 · \sem{|pe2|} ∪ in_pl ? pe2 - | por pe1 pe2 ⇒ in_pl ? pe1 ∪ in_pl ? pe2 - | pstar pe ⇒ in_pl ? pe · \sem{|pe|}^* + [ pzero ⇒ a title="empty lang" href="cic:/fakeuri.def(1)"∅/a + | pepsilon ⇒ a title="empty lang" href="cic:/fakeuri.def(1)"∅/a + | pchar _ ⇒ a title="empty lang" href="cic:/fakeuri.def(1)"∅/a + | ppoint x ⇒ a title="sing lang" href="cic:/fakeuri.def(1)"{/a: xa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a] } + | pconcat pe1 pe2 ⇒ in_pl ? pe1 a title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{|pe2|} a title="union lang" href="cic:/fakeuri.def(1)"∪/a in_pl ? pe2 + | por pe1 pe2 ⇒ in_pl ? pe1 a title="union lang" href="cic:/fakeuri.def(1)"∪/a in_pl ? pe2 + | pstar pe ⇒ in_pl ? pe a title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{|pe|}a title="star lang" href="cic:/fakeuri.def(1)"^/a* ]. -interpretation "in_pl" 'in_l E = (in_pl ? E). +interpretation "in_pl" 'sem E = (in_pl ? E). interpretation "in_pl mem" 'mem w l = (in_pl ? l w). -definition eps: ∀S:Alpha.bool → word S → Prop - ≝ λS,b. if_then_else ? b {: [] } ∅. +definition eps: ∀S:a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"Alpha/a.a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → a href="cic:/matita/tutorial/chapter4/word.def(3)"word/a S → Prop + ≝ λS,b. a href="cic:/matita/basics/bool/if_then_else.def(1)"if_then_else/a ? b a title="sing lang" href="cic:/fakeuri.def(1)"{/a: a title="nil" href="cic:/fakeuri.def(1)"[/a] } a title="empty lang" href="cic:/fakeuri.def(1)"∅/a. -(* interpretation "epsilon" 'epsilon = (epsilon ?). *) notation "ϵ _ b" non associative with precedence 90 for @{'app_epsilon $b}. interpretation "epsilon lang" 'app_epsilon b = (eps ? b). -definition in_prl ≝ λS : Alpha.λp:pre S. ℓ (\fst p) ∪ ϵ_(\snd p). +definition in_prl ≝ λS : a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"Alpha/a.λp:a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S. a title="in_pl" href="cic:/fakeuri.def(1)"\sem/a{a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a p} a title="union lang" href="cic:/fakeuri.def(1)"∪/a a title="epsilon lang" href="cic:/fakeuri.def(1)"ϵ/a_(a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a p). interpretation "in_prl mem" 'mem w l = (in_prl ? l w). -interpretation "in_prl" 'in_l E = (in_prl ? E). - -lemma not_epsilon_lp :∀S.∀pi:pitem S. ¬ ((ℓ pi) []). -#S #pi (elim pi) normalize /span class="autotactic"2span class="autotrace" trace nmk/span/span/ - [#pi1 #pi2 #H1 #H2 % * /span class="autotactic"2span class="autotrace" trace absurd/span/span/ * #w1 * #w2 * * #appnil - cases (nil_to_nil … appnil) /span class="autotactic"2span class="autotrace" trace absurd/span/span/ - |#p11 #p12 #H1 #H2 % * /span class="autotactic"2span class="autotrace" trace absurd/span/span/ - |#pi #H % * #w1 * #w2 * * #appnil (cases (nil_to_nil … appnil)) /span class="autotactic"2span class="autotrace" trace absurd/span/span/ +interpretation "in_prl" 'sem E = (in_prl ? E). + +lemma not_epsilon_lp :∀S.∀pi:a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"pitem/a S.a title="logical not" href="cic:/fakeuri.def(1)"\neg/a(a title="nil" href="cic:/fakeuri.def(1)"[/a] a title="in_pl mem" href="cic:/fakeuri.def(1)"∈/a pi). +#S #pi (elim pi) normalize / span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a/span/span/ + [#pi1 #pi2 #H1 #H2 % * /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ * #w1 * #w2 * * #appnil + cases (a href="cic:/matita/tutorial/chapter3/nil_to_nil.def(5)"nil_to_nil/a … appnil) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ + |#p11 #p12 #H1 #H2 % * /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ + |#pi #H % * #w1 * #w2 * * #appnil (cases (a href="cic:/matita/tutorial/chapter3/nil_to_nil.def(5)"nil_to_nil/a … appnil)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ ] qed. -lemma if_true_epsilon: ∀S.∀e:pre S. \snd e = true → ((ℓ e) []). +lemma if_true_epsilon: ∀S.∀e:a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S. a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a e 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="nil" href="cic:/fakeuri.def(1)"[/a] a title="in_prl mem" href="cic:/fakeuri.def(1)"∈/a e). #S #e #H %2 >H // qed. -lemma if_epsilon_true : ∀S.∀e:pre S. [ ] ∈ e → \snd e = true. -#S * #pi #b * [normalize #abs @False_ind /2/] cases b normalize // @False_ind +lemma if_epsilon_true : ∀S.∀e:a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S. a title="nil" href="cic:/fakeuri.def(1)"[/a ] a title="in_prl mem" href="cic:/fakeuri.def(1)"∈/a e → a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a e 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 * #pi #b * [normalize #abs @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/] cases b normalize // @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a qed. definition lor ≝ λS:Alpha.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉. -- 2.39.2