From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 13 Dec 2011 11:38:15 +0000 (+0000)
Subject: Splitted re into lang.ma nd re.ma
X-Git-Tag: make_still_working~2015
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5c71d6a1d1461007f941f73d2cc7975c7116fd0d;p=helm.git
Splitted re into lang.ma nd re.ma
---
diff --git a/matita/matita/lib/re/lang.ma b/matita/matita/lib/re/lang.ma
new file mode 100644
index 000000000..a0a5a938d
--- /dev/null
+++ b/matita/matita/lib/re/lang.ma
@@ -0,0 +1,126 @@
+
+
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "arithmetics/nat.ma".
+include "basics/lists/list.ma".
+include "basics/sets.ma".
+
+definition word â λS:DeqSet.list S.
+
+notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
+interpretation "epsilon" 'epsilon = (nil ?).
+
+(* concatenation *)
+definition cat : âS,l1,l2,w.Prop â
+ λS.λl1,l2.λw:word S.âw1,w2.w1 @ w2 = w ⧠l1 w1 ⧠l2 w2.
+notation "a · b" non associative with precedence 60 for @{ 'middot $a $b}.
+interpretation "cat lang" 'middot a b = (cat ? a b).
+
+let rec flatten (S : DeqSet) (l : list (word S)) on l : word S â
+match l with [ nil â [ ] | cons w tl â w @ flatten ? tl ].
+
+let rec conjunct (S : DeqSet) (l : list (word S)) (r : word S â Prop) on l: Prop â
+match l with [ nil â True | cons w tl â r w ⧠conjunct ? tl r ].
+
+(* kleene's star *)
+definition star â λS.λl.λw:word S.âlw.flatten ? lw = w ⧠conjunct ? lw l.
+notation "a ^ *" non associative with precedence 90 for @{ 'star $a}.
+interpretation "star lang" 'star l = (star ? l).
+
+lemma cat_ext_l: âS.âA,B,C:word S âProp.
+ A =1 C â A · B =1 C · B.
+#S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
+cases (H w1) /6/
+qed.
+
+lemma cat_ext_r: âS.âA,B,C:word S âProp.
+ B =1 C â A · B =1 A · C.
+#S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
+cases (H w2) /6/
+qed.
+
+lemma distr_cat_r: âS.âA,B,C:word S âProp.
+ (A ⪠B) · C =1 A · C ⪠B · C.
+#S #A #B #C #w %
+ [* #w1 * #w2 * * #eqw * /6/ |* * #w1 * #w2 * * /6/]
+qed.
+
+lemma espilon_in_star: âS.âA:word S â Prop.
+ A^* ϵ.
+#S #A @(ex_intro ⦠[ ]) normalize /2/
+qed.
+
+lemma cat_to_star:âS.âA:word S â Prop.
+ âw1,w2. A w1 â A^* w2 â A^* (w1@w2).
+#S #A #w1 #w2 #Aw * #l * #H #H1 @(ex_intro ⦠(w1::l))
+% normalize /2/
+qed.
+
+lemma fix_star: âS.âA:word S â Prop.
+ A^* =1 A · A^* ⪠{ϵ}.
+#S #A #w %
+ [* #l generalize in match w; -w cases l [normalize #w * /2/]
+ #w1 #tl #w * whd in ⢠((??%?)â?); #eqw whd in ⢠(%â?); *
+ #w1A #cw1 %1 @(ex_intro ⦠w1) @(ex_intro ⦠(flatten S tl))
+ % /2/ whd @(ex_intro ⦠tl) /2/
+ |* [2: whd in ⢠(%â?); #eqw <eqw //]
+ * #w1 * #w2 * * #eqw <eqw @cat_to_star
+ ]
+qed.
+
+lemma star_fix_eps : âS.âA:word S â Prop.
+ A^* =1 (A - {ϵ}) · A^* ⪠{ϵ}.
+#S #A #w %
+ [* #l elim l
+ [* whd in ⢠((??%?)â?); #eqw #_ %2 <eqw //
+ |* [#tl #Hind * #H * #_ #H2 @Hind % [@H | //]
+ |#a #w1 #tl #Hind * whd in ⢠((??%?)â?); #H1 * #H2 #H3 %1
+ @(ex_intro ⦠(a::w1)) @(ex_intro ⦠(flatten S tl)) %
+ [% [@H1 | normalize % /2/] |whd @(ex_intro ⦠tl) /2/]
+ ]
+ ]
+ |* [* #w1 * #w2 * * #eqw * #H1 #_ <eqw @cat_to_star //
+ | whd in ⢠(%â?); #H <H //
+ ]
+ ]
+qed.
+
+lemma star_epsilon: âS:DeqSet.âA:word S â Prop.
+ A^* ⪠{ϵ} =1 A^*.
+#S #A #w % /2/ * //
+qed.
+
+lemma epsilon_cat_r: âS.âA:word S âProp.
+ A · {ϵ} =1 A.
+#S #A #w %
+ [* #w1 * #w2 * * #eqw #inw1 normalize #eqw2 <eqw //
+ |#inA @(ex_intro ⦠w) @(ex_intro ⦠[ ]) /3/
+ ]
+qed.
+
+lemma epsilon_cat_l: âS.âA:word S âProp.
+ {ϵ} · A =1 A.
+#S #A #w %
+ [* #w1 * #w2 * * #eqw normalize #eqw2 <eqw <eqw2 //
+ |#inA @(ex_intro ⦠ϵ) @(ex_intro ⦠w) /3/
+ ]
+qed.
+
+lemma distr_cat_r_eps: âS.âA,C:word S âProp.
+ (A ⪠{ϵ}) · C =1 A · C ⪠C.
+#S #A #C @eqP_trans [|@distr_cat_r |@eqP_union_l @epsilon_cat_l]
+qed.
+
diff --git a/matita/matita/lib/re/moves.ma b/matita/matita/lib/re/moves.ma
index b7f094d86..4967bf059 100644
--- a/matita/matita/lib/re/moves.ma
+++ b/matita/matita/lib/re/moves.ma
@@ -304,6 +304,7 @@ lemma notb_eq_true_l: âb. notb b = true â b = false.
#b cases b normalize //
qed.
+(*
lemma notb_eq_true_r: âb. b = false â notb b = true.
#b cases b normalize //
qed.
@@ -314,7 +315,7 @@ qed.
lemma notb_eq_false_r:âb. b = true â notb b = false.
#b cases b normalize //
-qed.
+qed. *)
(* include "arithmetics/exp.ma". *)
diff --git a/matita/matita/lib/re/re.ma b/matita/matita/lib/re/re.ma
index 1695575f0..3f58c2c48 100644
--- a/matita/matita/lib/re/re.ma
+++ b/matita/matita/lib/re/re.ma
@@ -1,5 +1,3 @@
-
-
(**************************************************************************)
(* ___ *)
(* ||M|| *)
@@ -14,11 +12,7 @@
(* *)
(**************************************************************************)
-include "arithmetics/nat.ma".
-include "basics/lists/list.ma".
-include "basics/sets.ma".
-
-definition word â λS:DeqSet.list S.
+include "re/lang.ma".
inductive re (S: DeqSet) : Type[0] â
z: re S
@@ -27,59 +21,24 @@ inductive re (S: DeqSet) : Type[0] â
| c: re S â re S â re S
| o: re S â re S â re S
| k: re S â re S.
-
-(* notation < "a \sup â" non associative with precedence 90 for @{ 'pk $a}.*)
-notation "a ^ *" non associative with precedence 90 for @{ 'pk $a}.
-interpretation "star" 'pk a = (k ? a).
-interpretation "or" 'plus a b = (o ? a b).
-
-notation "a · b" non associative with precedence 60 for @{ 'pc $a $b}.
-interpretation "cat" 'pc a b = (c ? a b).
-
-(* to get rid of \middot
-ncoercion c : âS:DeqSet.âp:re S. re S â re S â c on _p : re ? to â_:?.?.
-*)
+
+interpretation "re epsilon" 'epsilon = (e ?).
+interpretation "re or" 'plus a b = (o ? a b).
+interpretation "re cat" 'middot a b = (c ? a b).
+interpretation "re star" 'star a = (k ? a).
notation < "a" non associative with precedence 90 for @{ 'ps $a}.
notation > "` term 90 a" non associative with precedence 90 for @{ 'ps $a}.
interpretation "atom" 'ps a = (s ? a).
-notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
-interpretation "epsilon" 'epsilon = (e ?).
-
notation "`â
" non associative with precedence 90 for @{ 'empty }.
interpretation "empty" 'empty = (z ?).
-let rec flatten (S : DeqSet) (l : list (word S)) on l : word S â
-match l with [ nil â [ ] | cons w tl â w @ flatten ? tl ].
-
-let rec conjunct (S : DeqSet) (l : list (word S)) (r : word S â Prop) on l: Prop â
-match l with [ nil â True | cons w tl â r w ⧠conjunct ? tl r ].
-
-(*
-definition empty_lang â λS.λw:word S.False.
-notation "{}" non associative with precedence 90 for @{'empty_lang}.
-interpretation "empty lang" 'empty_lang = (empty_lang ?).
-
-definition sing_lang â λS.λx,w:word S.x=w.
-(* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}.*)
-interpretation "sing lang" 'singl x = (sing_lang ? x).
-
-definition union : âS,l1,l2,w.Prop â λS.λl1,l2.λw:word S.l1 w ⨠l2 w.
-interpretation "union lang" 'union a b = (union ? a b). *)
-
-definition cat : âS,l1,l2,w.Prop â
- λS.λl1,l2.λw:word S.âw1,w2.w1 @ w2 = w ⧠l1 w1 ⧠l2 w2.
-interpretation "cat lang" 'pc a b = (cat ? a b).
-
-definition star â λS.λl.λw:word S.âlw.flatten ? lw = w ⧠conjunct ? lw l.
-interpretation "star lang" 'pk l = (star ? l).
-
let rec in_l (S : DeqSet) (r : re S) on r : word S â Prop â
match r with
[ z â â
-| e â { [ ] }
-| s x â { [x] }
+| e â {ϵ}
+| s x â {[x]}
| c r1 r2 â (in_l ? r1) · (in_l ? r2)
| o r1 r2 â (in_l ? r1) ⪠(in_l ? r2)
| k r1 â (in_l ? r1) ^*].
@@ -91,6 +50,8 @@ interpretation "in_l mem" 'mem w l = (in_l ? l w).
lemma rsem_star : âS.âr: re S. \sem{r^*} = \sem{r}^*.
// qed.
+
+(* pointed items *)
inductive pitem (S: DeqSet) : Type[0] â
pz: pitem S
| pe: pitem S
@@ -102,20 +63,15 @@ inductive pitem (S: DeqSet) : Type[0] â
definition pre â λS.pitem S à bool.
-interpretation "pstar" 'pk a = (pk ? a).
-interpretation "por" 'plus a b = (po ? a b).
-interpretation "pcat" 'pc a b = (pc ? a b).
+interpretation "pitem star" 'star a = (pk ? a).
+interpretation "pitem or" 'plus a b = (po ? a b).
+interpretation "pitem cat" 'middot a b = (pc ? a b).
notation < ".a" non associative with precedence 90 for @{ 'pp $a}.
notation > "`. term 90 a" non associative with precedence 90 for @{ 'pp $a}.
-interpretation "ppatom" 'pp a = (pp ? a).
-
-(* to get rid of \middot
-ncoercion pc : âS.âp:pitem S. pitem S â pitem S â pc on _p : pitem ? to â_:?.?.
-*)
-
-interpretation "patom" 'ps a = (ps ? a).
-interpretation "pepsilon" 'epsilon = (pe ?).
-interpretation "pempty" 'empty = (pz ?).
+interpretation "pitem pp" 'pp a = (pp ? a).
+interpretation "pitem ps" 'ps a = (ps ? a).
+interpretation "pitem epsilon" 'epsilon = (pe ?).
+interpretation "pitem empty" 'empty = (pz ?).
let rec forget (S: DeqSet) (l : pitem S) on l: re S â
match l with
@@ -143,22 +99,14 @@ match r with
interpretation "in_pl" 'in_l E = (in_pl ? E).
interpretation "in_pl mem" 'mem w l = (in_pl ? l w).
-(*
-definition epsilon : âS:DeqSet.bool â word S â Prop
-â λ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). *)
-
definition in_prl â λS : DeqSet.λp:pre S.
- if (\snd p) then \sem{\fst p} ⪠{ ([ ] : word S) } else \sem{\fst p}.
+ if (\snd p) then \sem{\fst p} ⪠{ϵ} else \sem{\fst p}.
interpretation "in_prl mem" 'mem w l = (in_prl ? l w).
interpretation "in_prl" 'in_l E = (in_prl ? E).
lemma sem_pre_true : âS.âi:pitem S.
- \sem{â©i,trueâª} = \sem{i} ⪠{ ([ ] : word S) }.
+ \sem{â©i,trueâª} = \sem{i} ⪠{ϵ}.
// qed.
lemma sem_pre_false : âS.âi:pitem S.
@@ -189,10 +137,10 @@ lemma sem_star_w : âS.âi:pitem S.âw.
\sem{i^*} w = (âw1,w2.w1 @ w2 = w ⧠\sem{i} w1 ⧠\sem{|i|}^* w2).
// qed.
-lemma append_eq_nil : âS.âw1,w2:word S. w1 @ w2 = [ ] â w1 = [ ].
+lemma append_eq_nil : âS.âw1,w2:word S. w1 @ w2 = ϵ â w1 = ϵ.
#S #w1 #w2 cases w1 // #a #tl normalize #H destruct qed.
-lemma not_epsilon_lp : âS:DeqSet.âe:pitem S. ¬ ([ ] â e).
+lemma not_epsilon_lp : âS:DeqSet.âe:pitem S. ¬ (ϵ â e).
#S #e elim e normalize /2/
[#r1 #r2 * #n1 #n2 % * /2/ * #w1 * #w2 * * #H
>(append_eq_nil â¦Hâ¦) /2/
@@ -202,11 +150,11 @@ lemma not_epsilon_lp : âS:DeqSet.âe:pitem S. ¬ ([ ] â e).
qed.
(* lemma 12 *)
-lemma epsilon_to_true : âS.âe:pre S. [ ] â e â \snd e = true.
+lemma epsilon_to_true : âS.âe:pre S. ϵ â e â \snd e = true.
#S * #i #b cases b // normalize #H @False_ind /2/
qed.
-lemma true_to_epsilon : âS.âe:pre S. \snd e = true â [ ] â e.
+lemma true_to_epsilon : âS.âe:pre S. \snd e = true â ϵ â e.
#S * #i #b #btrue normalize in btrue; >btrue %2 //
qed.
@@ -222,10 +170,6 @@ definition pre_concat_r â λS:DeqSet.λi:pitem S.λe:pre S.
notation "i â e" left associative with precedence 60 for @{'ltrif $i $e}.
interpretation "pre_concat_r" 'ltrif i e = (pre_concat_r ? i e).
-
-definition eq_f1 â λS.λa,b:word S â Prop.âw.a w â b w.
-notation "A =1 B" non associative with precedence 45 for @{'eq_f1 $A $B}.
-interpretation "eq f1" 'eq_f1 a b = (eq_f1 ? a b).
lemma eq_to_ex_eq: âS.âA,B:word S â Prop.
A = B â A =1 B.
@@ -233,7 +177,7 @@ lemma eq_to_ex_eq: âS.âA,B:word S â Prop.
lemma sem_pre_concat_r : âS,i.âe:pre S.
\sem{i â e} =1 \sem{i} · \sem{|\fst e|} ⪠\sem{e}.
-#S #i * #i1 #b1 cases b1 /2/
+#S #i * #i1 #b1 cases b1 [2: @eq_to_ex_eq //]
>sem_pre_true >sem_cat >sem_pre_true /2/
qed.
@@ -261,23 +205,6 @@ definition lk â λS:DeqSet.λbcast:âS:DeqSet.âE:pitem S.pre S.λe:pre S.
]
].
-(*
-lemma oplus_tt : âS: DeqSet.âi1,i2:pitem S.
- â©i1,true⪠â â©i2,true⪠= â©i1 + i2,trueâª.
-// qed.
-
-lemma oplus_tf : âS: DeqSet.âi1,i2:pitem S.
- â©i1,true⪠â â©i2,false⪠= â©i1 + i2,trueâª.
-// qed.
-
-lemma oplus_ft : âS: DeqSet.âi1,i2:pitem S.
- â©i1,false⪠â â©i2,true⪠= â©i1 + i2,trueâª.
-// qed.
-
-lemma oplus_ff : âS: DeqSet.âi1,i2:pitem S.
- â©i1,false⪠â â©i2,false⪠= â©i1 + i2,falseâª.
-// qed. *)
-
(* notation < "a \sup â" non associative with precedence 90 for @{'lk $op $a}.*)
interpretation "lk" 'lk op a = (lk ? op a).
notation "a^â" non associative with precedence 90 for @{'lk eclose $a}.
@@ -359,113 +286,11 @@ lemma erase_bull : âS.âi:pitem S. |\fst (â¢i)| = |i|.
| #i #IH >eclose_star >(erase_star ⦠i) <IH cases (â¢i) //
]
qed.
-
-lemma cat_ext_l: âS.âA,B,C:word S âProp.
- A =1 C â A · B =1 C · B.
-#S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
-cases (H w1) /6/
-qed.
-
-lemma cat_ext_r: âS.âA,B,C:word S âProp.
- B =1 C â A · B =1 A · C.
-#S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
-cases (H w2) /6/
-qed.
-
-lemma distr_cat_r: âS.âA,B,C:word S âProp.
- (A ⪠B) · C =1 A · C ⪠B · C.
-#S #A #B #C #w %
- [* #w1 * #w2 * * #eqw * /6/ |* * #w1 * #w2 * * /6/]
-qed.
-
-lemma espilon_in_star: âS.âA:word S â Prop.
- A^* [ ].
-#S #A @(ex_intro ⦠[ ]) normalize /2/
-qed.
-
-lemma cat_to_star:âS.âA:word S â Prop.
- âw1,w2. A w1 â A^* w2 â A^* (w1@w2).
-#S #A #w1 #w2 #Aw * #l * #H #H1 @(ex_intro ⦠(w1::l))
-% normalize /2/
-qed.
-
-lemma fix_star: âS.âA:word S â Prop.
- A^* =1 A · A^* ⪠{ [ ] }.
-#S #A #w %
- [* #l generalize in match w; -w cases l [normalize #w * /2/]
- #w1 #tl #w * whd in ⢠((??%?)â?); #eqw whd in ⢠(%â?); *
- #w1A #cw1 %1 @(ex_intro ⦠w1) @(ex_intro ⦠(flatten S tl))
- % /2/ whd @(ex_intro ⦠tl) /2/
- |* [2: whd in ⢠(%â?); #eqw <eqw //]
- * #w1 * #w2 * * #eqw <eqw @cat_to_star
- ]
-qed.
-
-lemma star_fix_eps : âS.âA:word S â Prop.
- A^* =1 (A - {[ ]}) · A^* ⪠{[ ]}.
-#S #A #w %
- [* #l elim l
- [* whd in ⢠((??%?)â?); #eqw #_ %2 <eqw //
- |* [#tl #Hind * #H * #_ #H2 @Hind % [@H | //]
- |#a #w1 #tl #Hind * whd in ⢠((??%?)â?); #H1 * #H2 #H3 %1
- @(ex_intro ⦠(a::w1)) @(ex_intro ⦠(flatten S tl)) %
- [% [@H1 | normalize % /2/] |whd @(ex_intro ⦠tl) /2/]
- ]
- ]
- |* [* #w1 * #w2 * * #eqw * #H1 #_ <eqw @cat_to_star //
- | whd in ⢠(%â?); #H <H //
- ]
- ]
-qed.
-
-lemma star_epsilon: âS:DeqSet.âA:word S â Prop.
- A^* ⪠{ [ ] } =1 A^*.
-#S #A #w % /2/ * //
-qed.
lemma sem_eclose_star: âS:DeqSet.âi:pitem S.
- \sem{â©i^*,trueâª} =1 \sem{â©i,falseâª}·\sem{|i|}^* ⪠{ [ ] }.
+ \sem{â©i^*,trueâª} =1 \sem{â©i,falseâª}·\sem{|i|}^* ⪠{ϵ}.
/2/ qed.
-(* this kind of results are pretty bad for automation;
- better not index them *)
-
-lemma epsilon_cat_r: âS.âA:word S âProp.
- A · { [ ] } =1 A.
-#S #A #w %
- [* #w1 * #w2 * * #eqw #inw1 normalize #eqw2 <eqw //
- |#inA @(ex_intro ⦠w) @(ex_intro ⦠[ ]) /3/
- ]
-qed.
-
-lemma epsilon_cat_l: âS.âA:word S âProp.
- { [ ] } · A =1 A.
-#S #A #w %
- [* #w1 * #w2 * * #eqw normalize #eqw2 <eqw <eqw2 //
- |#inA @(ex_intro ⦠[ ]) @(ex_intro ⦠w) /3/
- ]
-qed.
-
-lemma distr_cat_r_eps: âS.âA,C:word S âProp.
- (A ⪠{ [ ] }) · C =1 A · C ⪠C.
-#S #A #C @eqP_trans [|@distr_cat_r |@eqP_union_l @epsilon_cat_l]
-qed.
-
-(* axiom eplison_cut_l: âS.âA:word S âProp.
- { [ ] } · A =1 A.
-
- axiom eplison_cut_r: âS.âA:word S âProp.
- A · { [ ] } =1 A. *)
-
-(*
-lemma eta_lp : âS.âp:pre S.ð\p p = ð\p â©\fst p, \snd pâª.
-#S p; ncases p; //; nqed.
-
-nlemma epsilon_dot: âS.âp:word S â Prop. {[]} · p = p.
-#S e; napply extP; #w; nnormalize; @; ##[##2: #Hw; @[]; @w; /3/; ##]
-*; #w1; *; #w2; *; *; #defw defw1 Hw2; nrewrite < defw; nrewrite < defw1;
-napply Hw2; nqed.*)
-
(* theorem 16: 1 â 3 *)
lemma odot_dot_aux : âS.âe1:pre S.âi2:pitem S.
\sem{â¢i2} =1 \sem{i2} ⪠\sem{|i2|} â
@@ -610,58 +435,3 @@ theorem sem_ostar: âS.âe:pre S.
]
qed.
-(*
-nlet rec pre_of_re (S : DeqSet) (e : re S) on e : pitem S â
- match e with
- [ z â pz ?
- | e â pe ?
- | s x â ps ? x
- | c e1 e2 â pc ? (pre_of_re ? e1) (pre_of_re ? e2)
- | o e1 e2 â po ? (pre_of_re ? e1) (pre_of_re ? e2)
- | k e1 â pk ? (pre_of_re ? e1)].
-
-nlemma notFalse : ¬False. @; //; nqed.
-
-nlemma dot0 : âS.âA:word S â Prop. {} · A = {}.
-#S A; nnormalize; napply extP; #w; @; ##[##2: *]
-*; #w1; *; #w2; *; *; //; nqed.
-
-nlemma Lp_pre_of_re : âS.âe:re S. ð\p (pre_of_re ? e) = {}.
-#S e; nelim e; ##[##1,2,3: //]
-##[ #e1 e2 H1 H2; nchange in match (ð\p (pre_of_re S (e1 e2))) with (?âª?);
- nrewrite > H1; nrewrite > H2; nrewrite > (dot0â¦); nrewrite > (cupIDâ¦);//
-##| #e1 e2 H1 H2; nchange in match (ð\p (pre_of_re S (e1+e2))) with (?âª?);
- nrewrite > H1; nrewrite > H2; nrewrite > (cupIDâ¦); //
-##| #e1 H1; nchange in match (ð\p (pre_of_re S (e1^* ))) with (ð\p (pre_of_re ??) · ?);
- nrewrite > H1; napply dot0; ##]
-nqed.
-
-nlemma erase_pre_of_reK : âS.âe. ð |pre_of_re S e| = ð e.
-#S A; nelim A; //;
-##[ #e1 e2 H1 H2; nchange in match (ð (e1 · e2)) with (ð e1·?);
- nrewrite < H1; nrewrite < H2; //
-##| #e1 e2 H1 H2; nchange in match (ð (e1 + e2)) with (ð e1 ⪠?);
- nrewrite < H1; nrewrite < H2; //
-##| #e1 H1; nchange in match (ð (e1^* )) with ((ð e1)^* );
- nrewrite < H1; //]
-nqed.
-
-(* corollary 17 *)
-nlemma L_Lp_bull : âS.âe:re S.ð e = ð\p (â¢pre_of_re ? e).
-#S e; nrewrite > (bull_cupâ¦); nrewrite > (Lp_pre_of_reâ¦);
-nrewrite > (cupCâ¦); nrewrite > (cup0â¦); nrewrite > (erase_pre_of_reKâ¦); //;
-nqed.
-
-nlemma Pext : âS.âf,g:word S â Prop. f = g â âw.f w â g w.
-#S f g H; nrewrite > H; //; nqed.
-
-(* corollary 18 *)
-ntheorem bull_true_epsilon : âS.âe:pitem S. \snd (â¢e) = true â [ ] â |e|.
-#S e; @;
-##[ #defsnde; nlapply (bull_cup ? e); nchange in match (ð\p (â¢e)) with (?âª?);
- nrewrite > defsnde; #H;
- nlapply (Pext ??? H [ ] ?); ##[ @2; //] *; //;
-
-*)
-
-