From: matitaweb Date: Wed, 16 Nov 2011 08:57:06 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~2108 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0410fb0737da599395caf7fbb698d224d4c8c7a2;p=helm.git commit by user andrea --- diff --git a/weblib/basics/pts.ma b/weblib/basics/pts.ma index 1b87a2d0b..b7d9a5da9 100644 --- a/weblib/basics/pts.ma +++ b/weblib/basics/pts.ma @@ -19,23 +19,3 @@ universe constraint Type[1] < Type[2]. universe constraint Type[2] < Type[3]. universe constraint Type[3] < Type[4]. -(*inductive True : Prop ≝ I : True. - -(*lemma fa : ∀X:Prop.X → X. -#X #p // -qed. - -(* check fa*) - -lemma ggr ≝ fa.*) - -inductive False : Prop ≝ . - -inductive bool : Prop ≝ True : bool | false : bool. - -inductive eq (A:Type[1]) (x:A) : A → Prop ≝ - refl: eq A x x. - -lemma provable_True : True → eq Prop True True. -#H % -qed.*) \ No newline at end of file diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma index cf7f4aafc..6cb68782b 100644 --- a/weblib/tutorial/chapter4.ma +++ b/weblib/tutorial/chapter4.ma @@ -72,7 +72,7 @@ interpretation "cat lang" 'concat a b = (cat ? a b). definition star_lang ≝ λS.λl.λw:a href="cic:/matita/tutorial/chapter4/word.def(3)"word/a S.a title="exists" href="cic:/fakeuri.def(1)"∃/alw. a href="cic:/matita/tutorial/chapter4/flatten.fix(0,1,4)"flatten/a ? lw a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a w a title="logical and" href="cic:/fakeuri.def(1)"∧/a a href="cic:/matita/tutorial/chapter4/conjunct.fix(0,1,4)"conjunct/a ? lw l. interpretation "star lang" 'kstar l = (star_lang ? l). -(* notation "ℓ term 70 E" non associative with precedence 75 for @{in_l ? $E}. *) +(* notation "| term 70 E| " non associative with precedence 75 for @{in_l ? $E}. *) let rec in_l (S : a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"Alpha/a) (r : a href="cic:/matita/tutorial/chapter4/re.ind(1,0,1)"re/a S) on r : a href="cic:/matita/tutorial/chapter4/word.def(3)"word/a S → Prop ≝ match r with @@ -84,7 +84,7 @@ match r with | star r1 ⇒ (in_l ? r1)a title="star lang" href="cic:/fakeuri.def(1)"^/a* ]. -notation "ℓ term 70 E" non associative with precedence 75 for @{'in_l $E}. +notation "\sem{E}" non associative with precedence 75 for @{'in_l $E}. interpretation "in_l" 'in_l E = (in_l ? E). interpretation "in_l mem" 'mem w l = (in_l ? l w). @@ -121,69 +121,71 @@ interpretation "patom" 'pchar a = (pchar ? a). interpretation "pepsilon" 'epsilon = (pepsilon ?). interpretation "pempty" 'empty = (pzero ?). -notation "\boxv term 19 e \boxv" (* slash boxv *) non associative with precedence 70 for @{forget ? $e}. +notation "| e |" non associative with precedence 65 for @{forget ? $e}. let rec forget (S: a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"Alpha/a) (l : a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"pitem/a S) on l: a href="cic:/matita/tutorial/chapter4/re.ind(1,0,1)"re/a S ≝ match l with [ pzero ⇒ a title="empty" href="cic:/fakeuri.def(1)"∅/a | pepsilon ⇒ a title="epsilon" href="cic:/fakeuri.def(1)"ϵ/a | pchar x ⇒ a href="cic:/matita/tutorial/chapter4/re.con(0,3,1)"char/a ? x - | ppoint x ⇒ a href="cic:/matita/tutorial/chapter4/re.con(0,3,1)"char/a ? x - | pconcat e1 e2 ⇒ │e1│ a title="cat" href="cic:/fakeuri.def(1)"·/a │e2│ - | por e1 e2 ⇒ │e1│ a title="or" href="cic:/fakeuri.def(1)"+/a │e2│ - | pstar e ⇒ │e│a title="star" href="cic:/fakeuri.def(1)"^/a* + | ppoint x ⇒ a href="cic:/matita/tutorial/chapter4/re.con(0,3,1)"char/a ? x + | pconcat e1 e2 ⇒ |e1| a title="cat" href="cic:/fakeuri.def(1)"·/a |e2| + | por e1 e2 ⇒ |e1| a title="or" href="cic:/fakeuri.def(1)"+/a |e2| + | pstar e ⇒ |e|a title="star" href="cic:/fakeuri.def(1)"^/a* ]. -notation "│ term 19 e │" non associative with precedence 70 for @{'forget $e}. -interpretation "forget" 'forget a = (forget ? a). +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 "ℓ term 70 E" non associative with precedence 75 for @{in_pl ? $E}. +(* notation "\sem{E}" non associative with precedence 75 for @{in_pl ? $E}. *) -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 ≝ +let rec in_pl (S : Alpha) (r : pitem S) on r : word S → Prop ≝ match r with - [ 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)"ℓ/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)"ℓ/a │pe│a title="star" href="cic:/fakeuri.def(1)"^/a* + [ 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|}^* ]. interpretation "in_pl" 'in_l E = (in_pl ? E). interpretation "in_pl mem" 'mem w l = (in_pl ? l w). -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)" title="null"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. +definition eps: ∀S:Alpha.bool → word S → Prop + ≝ λS,b. if_then_else ? b {: [] } ∅. (* 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 : 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)"ℓ/a (a title="fst" 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="snd" href="cic:/fakeuri.def(1)"\snd/a p). +definition in_prl ≝ λS : Alpha.λp:pre S. ℓ (\fst p) ∪ ϵ_(\snd 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:a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"pitem/a S. a title="logical not" href="cic:/fakeuri.def(1)"¬/a ((a title="in_pl" href="cic:/fakeuri.def(1)"ℓ/a pi) a title="nil" href="cic:/fakeuri.def(1)"[/a]). -#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/ +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/ ] qed. -lemma if_true_epsilon: ∀S.∀e:a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S. a title="snd" 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="in_prl" href="cic:/fakeuri.def(1)"ℓ/a e) a title="nil" href="cic:/fakeuri.def(1)"[/a]). +lemma if_true_epsilon: ∀S.∀e:pre S. \snd e = true → ((ℓ e) []). #S #e #H %2 >H // qed. -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="snd" 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 /2/] cases b normalize // @False_ind +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 qed. definition lor ≝ λS:Alpha.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉.