commit by user andrea

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index 79b6bafff14a082f5ed40334cd1b60332c84b79c..21a7a6c0ef80bf29230209b9ca91986666b13f67 100644 (file)
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -69,19 +69,19 @@ definition cat : ∀S,l1,l2,w.Prop ≝
   λS.λl1,l2.λw:\ 5a href="cic:/matita/tutorial/chapter4/word.def(3)"\ 6word\ 5/a\ 6 S.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6w1,w2.w1 \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 w2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 w \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l1 w1 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l2 w2.
 interpretation "cat lang" 'concat a b = (cat ? a b).
 
-definition star ≝ λS.λl.λw:\ 5a href="cic:/matita/tutorial/chapter4/word.def(3)"\ 6word\ 5/a\ 6 S.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6lw. \ 5a href="cic:/matita/tutorial/chapter4/flatten.fix(0,1,4)"\ 6flatten\ 5/a\ 6 ? lw \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 w \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter4/conjunct.fix(0,1,4)"\ 6conjunct\ 5/a\ 6 ? lw l. 
-interpretation "star lang" 'kstar l = (star ? l).
+definition star_lang ≝ λS.λl.λw:\ 5a href="cic:/matita/tutorial/chapter4/word.def(3)"\ 6word\ 5/a\ 6 S.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6lw. \ 5a href="cic:/matita/tutorial/chapter4/flatten.fix(0,1,4)"\ 6flatten\ 5/a\ 6 ? lw \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 w \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter4/conjunct.fix(0,1,4)"\ 6conjunct\ 5/a\ 6 ? 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 : \ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6) (r : \ 5a href="cic:/matita/tutorial/chapter4/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S) on r : \ 5a href="cic:/matita/tutorial/chapter4/word.def(3)"\ 6word\ 5/a\ 6 S → Prop ≝ 
 match r with
  [ zero ⇒ \ 5a title="empty lang" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6 
  | epsilon ⇒ \ 5a title="sing lang" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6: \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] }
- |  char x ⇒ \ 5a title="sing lang" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6: x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] }
- | concat r1 r2 ⇒ ℓ r1 \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 ℓ r2 
- | or r1 r2 ⇒ ℓ r1 \ 5a title="union lang" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 ℓ r2 
- | star r1 ⇒ (ℓ r1)\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6* 
+ | char x ⇒ \ 5a title="sing lang" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6: x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] }
+ | concat r1 r2 ⇒ in_l ? r1 \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 in_l ? r2 
+ | or r1 r2 ⇒ in_l ? r1 \ 5a title="union lang" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 in_l ? r2 
+ | star r1 ⇒ (in_l ? r1)\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6* 
  ].
 
 notation "ℓ term 70 E" non associative with precedence 75 for @{'in_l $E}.
@@ -131,11 +131,65 @@ let rec forget (S: \ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alph
   | ppoint x ⇒ \ 5a href="cic:/matita/tutorial/chapter4/re.con(0,3,1)"\ 6char\ 5/a\ 6 ? x  
   | pconcat e1 e2 ⇒ │e1│ \ 5a title="cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 │e2│
   | por e1 e2 ⇒ │e1│  \ 5a title="or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 │e2│
-  | pstar e ⇒ │e│\ 5a title="star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6* 
+  | pstar e ⇒ │e│\ 5a title="star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*
   ].
 
-notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.
+notation "│ term 19 e │" non associative with precedence 70 for @{'forget $e}.
 interpretation "forget" 'forget a = (forget ? a).
 
-
 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}.
+
+let rec in_pl (S : \ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6) (r : \ 5a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S) on r : \ 5a href="cic:/matita/tutorial/chapter4/word.def(3)"\ 6word\ 5/a\ 6 S → Prop ≝ 
+match r with
+  [ pzero ⇒ \ 5a title="empty lang" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6 
+  | pepsilon ⇒ \ 5a title="empty lang" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
+  | pchar _ ⇒ \ 5a title="empty lang" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
+  | ppoint x ⇒ \ 5a title="sing lang" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6: x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] } 
+  | pconcat pe1 pe2 ⇒ in_pl ? pe1 \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6ℓ\ 5/a\ 6 │pe2│  \ 5a title="union lang" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 in_pl ? pe2 
+  | por pe1 pe2 ⇒ in_pl ? pe1 \ 5a title="union lang" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 in_pl ? pe2
+  | pstar pe ⇒ in_pl ? pe \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6ℓ\ 5/a\ 6 │pe│\ 5a title="star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*
+  ].
+
+interpretation "in_pl" 'in_l E = (in_pl ? E).
+interpretation "in_pl mem" 'mem w l = (in_pl ? l w).
+
+definition epsilon ≝ λS,b.if b then { ([ ] : word S) } else {}.
+
+interpretation "epsilon" 'epsilon = (epsilon ?).
+notation < "ϵ b" non associative with precedence 90 for @{'app_epsilon $b}.
+interpretation "epsilon lang" 'app_epsilon b = (epsilon ? b).
+
+ndefinition in_prl ≝ λS : Alpha.λp:pre S.  𝐋\p (\fst p) ∪ ϵ (\snd p).
+  
+interpretation "in_prl mem" 'mem w l = (in_prl ? l w).
+interpretation "in_prl" 'in_pl E = (in_prl ? E).
+
+nlemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = [ ] → w1 = [ ].
+#S w1; nelim w1; //. #x tl IH w2; nnormalize; #abs; ndestruct; nqed.
+
+(* lemma 12 *)
+nlemma epsilon_in_true : ∀S.∀e:pre S. [ ] ∈ e ↔ \snd e = true.
+#S r; ncases r; #e b; @; ##[##2: #H; nrewrite > H; @2; /2/; ##] ncases b;//; 
+nnormalize; *; ##[##2:*] nelim e;
+##[ ##1,2: *; ##| #c; *; ##| #c; nnormalize; #; ndestruct; ##| ##7: #p H;
+##| #r1 r2 H G; *; ##[##2: /3/ by or_intror]
+##| #r1 r2 H1 H2; *; /3/ by or_intror, or_introl; ##]
+*; #w1; *; #w2; *; *; #defw1; nrewrite > (append_eq_nil … w1 w2 …); /3/ by {};//;
+nqed.
+
+nlemma not_epsilon_lp : ∀S:Alpha.∀e:pitem S. ¬ ((𝐋\p e) [ ]).
+#S e; nelim e; nnormalize; /2/ by nmk;
+##[ #; @; #; ndestruct;
+##| #r1 r2 n1 n2; @; *; /2/; *; #w1; *; #w2; *; *; #H;
+    nrewrite > (append_eq_nil …H…); /2/;
+##| #r1 r2 n1 n2; @; *; /2/;
+##| #r n; @; *; #w1; *; #w2; *; *; #H;     
+    nrewrite > (append_eq_nil …H…); /2/;##]
+nqed.
+
+ndefinition lo ≝ λS:Alpha.λ
\ No newline at end of file