-(* We shall apply all the previous machinery to the study of regular languages
+(*
+\ 5h1\ 6Regular Expressions \ 5/h1\ 6
+We shall apply all the previous machinery to the study of regular languages
and the constructions of the associated finite automata. *)
include "tutorial/chapter6.ma".
(* The type re of regular expressions over an alphabet $S$ is the smallest
collection of objects generated by the following constructors: *)
-inductive re (S: \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) : Type[0] ≝
+\ 5img class="anchor" src="icons/tick.png" id="re"\ 6inductive re (S: \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) : Type[0] ≝
z: re S (* empty: ∅ *)
| e: re S (* epsilon: ϵ *)
| s: S → re S (* symbol: a *)
(* The language sem{e} associated with the regular expression e is inductively
defined by the following function: *)
-let rec in_l (S : \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6\ 5span class="error" title="Parse error: RPAREN expected after [term] (in [arg])"\ 6\ 5/span\ 6) (r : \ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S) on r : \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6\ 5span class="error" title="Parse error: SYMBOL '≝' expected (in [let_defs])"\ 6\ 5/span\ 6 S → Prop ≝
+\ 5img class="anchor" src="icons/tick.png" id="in_l"\ 6let rec in_l (S : \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6\ 5span class="error" title="Parse error: RPAREN expected after [term] (in [arg])"\ 6\ 5/span\ 6) (r : \ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S) on r : \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6\ 5span class="error" title="Parse error: SYMBOL '≝' expected (in [let_defs])"\ 6\ 5/span\ 6 S → Prop ≝
match r with
-[ z ⇒ \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6\ 5span class="error" title="Parse error: SYMBOL '|' or SYMBOL ']' expected (in [term])"\ 6\ 5/span\ 6
-| e ⇒ \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6}
-| s x ⇒ \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5span class="error" title="Parse error: [ident] or [term level 19] expected after [sym{] (in [term])"\ 6\ 5/span\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5span class="error" title="Parse error: [term] expected after [sym[] (in [term])"\ 6\ 5/span\ 6x]}
+[ z ⇒ \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
+| e ⇒ \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6\ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6
+| s x ⇒ \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5span class="error" title="Parse error: [ident] or [term level 19] expected after [sym{] (in [term])"\ 6\ 5/span\ 6 (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6) \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6
| c r1 r2 ⇒ (in_l ? r1) \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 (in_l ? r2)
| o r1 r2 ⇒ (in_l ? r1) \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 (in_l ? r2)
-| k r1 ⇒ (in_l ? r1) \ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*].
+| k r1 ⇒ (in_l ? r1) \ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6].
notation "\sem{term 19 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).
-lemma rsem_star : ∀S.∀r: \ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S. \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{r\ 5a title="re star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*} \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{r}\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*.
+\ 5img class="anchor" src="icons/tick.png" id="rsem_star"\ 6lemma rsem_star : ∀S.∀r: \ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S. \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{r\ 5a title="re star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 5a title="re star" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{r\ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6.
// qed.
-(* We now introduce pointed regular expressions, that are the main tool we shall
+(*
+\ 5h2\ 6Pointed Regular expressions \ 5/h2\ 6
+We now introduce pointed regular expressions, that are the main tool we shall
use for the construction of the automaton.
A pointed regular expression is just a regular expression internally labelled
with some additional points. Intuitively, points mark the positions inside the
enough to mark positions preceding individual characters, so we shall have two kinds
of characters •a (pp a) and a (ps a) according to the case a is pointed or not. *)
-inductive pitem (S: \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) : Type[0] ≝
+\ 5img class="anchor" src="icons/tick.png" id="pitem"\ 6inductive pitem (S: \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) : Type[0] ≝
pz: pitem S (* empty *)
| pe: pitem S (* epsilon *)
| ps: S → pitem S (* symbol *)
understood as states of a DFA, and the boolean indicates if
the state is final or not. *)
-definition pre ≝ λS.\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
+\ 5img class="anchor" src="icons/tick.png" id="pre"\ 6definition pre ≝ λS.\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
interpretation "pitem star" 'star a = (pk ? a).
interpretation "pitem or" 'plus a b = (po ? a b).
removing all the points. Similarly, the carrier of a pointed regular expression
is the carrier of its item. *)
-let rec forget (S: DeqSet) (l : pitem S) on l: re S ≝
+\ 5img class="anchor" src="icons/tick.png" id="forget"\ 6let rec forget (S: \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (l : \ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S) on l: \ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S ≝
match l with
- [ pz ⇒ `∅
- | pe ⇒ ϵ
- | ps x ⇒ `x
- | pp x ⇒ `x
- | pc E1 E2 ⇒ (forget ? E1) · (forget ? E2)
- | po E1 E2 ⇒ (forget ? E1) + (forget ? E2)
- | pk E ⇒ (forget ? E)^* ].
+ [ pz ⇒ \ 5a href="cic:/matita/tutorial/chapter7/re.con(0,1,1)"\ 6z\ 5/a\ 6 ? (* `∅ *)
+ | pe ⇒ \ 5a title="re epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6
+ | ps x ⇒ \ 5a title="atom" href="cic:/fakeuri.def(1)"\ 6`\ 5/a\ 6x
+ | pp x ⇒ \ 5a title="atom" href="cic:/fakeuri.def(1)"\ 6`\ 5/a\ 6x
+ | pc E1 E2 ⇒ (forget ? E1) \ 5a title="re cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 (forget ? E2)
+ | po E1 E2 ⇒ (forget ? E1) \ 5a title="re or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6\ 5span class="error" title="Parse error: [term] expected after [sym+] (in [term])"\ 6\ 5/span\ 6 (forget ? E2)
+ | pk E ⇒ (forget ? E)\ 5a title="re star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 5a title="re star" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 ].
(* notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.*)
interpretation "forget" 'norm a = (forget ? a).
-lemma erase_dot : ∀S.∀e1,e2:pitem S. |e1 · e2| = c ? (|e1|) (|e2|).
+\ 5img class="anchor" src="icons/tick.png" id="erase_dot"\ 6lemma erase_dot : ∀S.∀e1,e2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S. \ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6e1 \ 5a title="pitem cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 e2\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter7/re.con(0,4,1)"\ 6c\ 5/a\ 6 ? (\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6e1\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6) (\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6e2\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6).
// qed.
-lemma erase_plus : ∀S.∀i1,i2:pitem S.
- |i1 + i2| = |i1| + |i2|.
+\ 5img class="anchor" src="icons/tick.png" id="erase_plus"\ 6lemma erase_plus : ∀S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
+ \ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i1 \ 5a title="pitem or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 i2\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i1\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="re or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i2\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6.
// qed.
-lemma erase_star : ∀S.∀i:pitem S.|i^*| = |i|^*.
+\ 5img class="anchor" src="icons/tick.png" id="erase_star"\ 6lemma erase_star : ∀S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="re star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 5a title="re star" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6.
// qed.
-(* Items and pres are very concrete datatypes: they can be effectively compared,
+(*
+\ 5h2\ 6Comparing items and pres\ 5/h2\ 6
+Items and pres are very concrete datatypes: they can be effectively compared,
and enumerated. In particular, we can define a boolean equality beqitem and a proof
beqitem_true that it refects propositional equality, enriching the set (pitem S)
to a DeqSet. *)
-let rec beqitem S (i1,i2: pitem S) on i1 ≝
+\ 5img class="anchor" src="icons/tick.png" id="beqitem"\ 6let rec beqitem S (i1,i2: \ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S) on i1 ≝
match i1 with
- [ pz ⇒ match i2 with [ pz ⇒ true | _ ⇒ false]
- | pe ⇒ match i2 with [ pe ⇒ true | _ ⇒ false]
- | ps y1 ⇒ match i2 with [ ps y2 ⇒ y1==y2 | _ ⇒ false]
- | pp y1 ⇒ match i2 with [ pp y2 ⇒ y1==y2 | _ ⇒ false]
+ [ pz ⇒ match i2 with [ pz ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 | _ ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6]
+ | pe ⇒ match i2 with [ pe ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 | _ ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6]
+ | ps y1 ⇒ match i2 with [ ps y2 ⇒ y1\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6y2 | _ ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6]
+ | pp y1 ⇒ match i2 with [ pp y2 ⇒ y1\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6y2 | _ ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6]
| po i11 i12 ⇒ match i2 with
- [ po i21 i22 ⇒ beqitem S i11 i21 ∧ beqitem S i12 i22
- | _ ⇒ false]
+ [ po i21 i22 ⇒ beqitem S i11 i21 \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 beqitem S i12 i22
+ | _ ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6\ 5span class="error" title="Parse error: SYMBOL '|' or SYMBOL ']' expected (in [term])"\ 6\ 5/span\ 6]
| pc i11 i12 ⇒ match i2 with
- [ pc i21 i22 ⇒ beqitem S i11 i21 ∧ beqitem S i12 i22
- | _ ⇒ false]
- | pk i11 ⇒ match i2 with [ pk i21 ⇒ beqitem S i11 i21 | _ ⇒ false]
+ [ pc i21 i22 ⇒ beqitem S i11 i21 \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 beqitem S i12 i22
+ | _ ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6]
+ | pk i11 ⇒ match i2 with [ pk i21 ⇒ beqitem S i11 i21 | _ ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6]
].
-lemma beqitem_true: ∀S,i1,i2. iff (beqitem S i1 i2 = true) (i1 = i2).
+\ 5img class="anchor" src="icons/tick.png" id="beqitem_true"\ 6lemma beqitem_true: ∀S,i1,i2. \ 5a href="cic:/matita/basics/logic/iff.def(1)"\ 6iff\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter7/beqitem.fix(0,1,4)"\ 6beqitem\ 5/a\ 6 S i1 i2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) (i1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 i2).
#S #i1 elim i1
[#i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % // normalize #H destruct
|#i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % // normalize #H destruct
|#x #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % normalize #H destruct
- [>(\P H) // | @(\b (refl …))]
+ [>(\P H) // | @(\b (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 …))]
|#x #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % normalize #H destruct
- [>(\P H) // | @(\b (refl …))]
+ [>(\P H) // | @(\b (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 …))]
|#i11 #i12 #Hind1 #Hind2 #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] %
normalize #H destruct
- [cases (true_or_false (beqitem S i11 i21)) #H1
- [>(proj1 … (Hind1 i21) H1) >(proj1 … (Hind2 i22)) // >H1 in H; #H @H
- |>H1 in H; normalize #abs @False_ind /2/
+ [cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter7/beqitem.fix(0,1,4)"\ 6beqitem\ 5/a\ 6 S i11 i21)) #H1
+ [>(\ 5a href="cic:/matita/basics/logic/proj1.def(2)"\ 6proj1\ 5/a\ 6 … (Hind1 i21) H1) >(\ 5a href="cic:/matita/basics/logic/proj1.def(2)"\ 6proj1\ 5/a\ 6 … (Hind2 i22)) // >H1 in H; #H @H
+ |>H1 in H; normalize #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
]
- |>(proj2 … (Hind1 i21) (refl …)) >(proj2 … (Hind2 i22) (refl …)) //
+ |>(\ 5a href="cic:/matita/basics/logic/proj2.def(2)"\ 6proj2\ 5/a\ 6 … (Hind1 i21) (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 …)) >(\ 5a href="cic:/matita/basics/logic/proj2.def(2)"\ 6proj2\ 5/a\ 6 … (Hind2 i22) (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 …)) //
]
|#i11 #i12 #Hind1 #Hind2 #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] %
normalize #H destruct
- [cases (true_or_false (beqitem S i11 i21)) #H1
- [>(proj1 … (Hind1 i21) H1) >(proj1 … (Hind2 i22)) // >H1 in H; #H @H
- |>H1 in H; normalize #abs @False_ind /2/
+ [cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter7/beqitem.fix(0,1,4)"\ 6beqitem\ 5/a\ 6 S i11 i21)) #H1
+ [>(\ 5a href="cic:/matita/basics/logic/proj1.def(2)"\ 6proj1\ 5/a\ 6 … (Hind1 i21) H1) >(\ 5a href="cic:/matita/basics/logic/proj1.def(2)"\ 6proj1\ 5/a\ 6 … (Hind2 i22)) // >H1 in H; #H @H
+ |>H1 in H; normalize #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
]
- |>(proj2 … (Hind1 i21) (refl …)) >(proj2 … (Hind2 i22) (refl …)) //
+ |>(\ 5a href="cic:/matita/basics/logic/proj2.def(2)"\ 6proj2\ 5/a\ 6 … (Hind1 i21) (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 …)) >(\ 5a href="cic:/matita/basics/logic/proj2.def(2)"\ 6proj2\ 5/a\ 6 … (Hind2 i22) (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 …)) //
]
|#i3 #Hind #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i4] %
normalize #H destruct
- [>(proj1 … (Hind i4) H) // |>(proj2 … (Hind i4) (refl …)) //]
+ [>(\ 5a href="cic:/matita/basics/logic/proj1.def(2)"\ 6proj1\ 5/a\ 6 … (Hind i4) H) // |>(\ 5a href="cic:/matita/basics/logic/proj2.def(2)"\ 6proj2\ 5/a\ 6 … (Hind i4) (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 …)) //]
]
qed.
-definition DeqItem ≝ λS.
- mk_DeqSet (pitem S) (beqitem S) (beqitem_true S).
+\ 5img class="anchor" src="icons/tick.png" id="DeqItem"\ 6definition DeqItem ≝ λS.
+ \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"\ 6mk_DeqSet\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S) (\ 5a href="cic:/matita/tutorial/chapter7/beqitem.fix(0,1,4)"\ 6beqitem\ 5/a\ 6 S) (\ 5a href="cic:/matita/tutorial/chapter7/beqitem_true.def(5)"\ 6beqitem_true\ 5/a\ 6 S).
(* We also add a couple of unification hints to allow the type inference system
to look at (pitem S) as the carrier of a DeqSet, and at beqitem as if it was the
equality function of a DeqSet. *)
-unification hint 0 ≔ S;
- X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S)
+unification hint 0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type1"\ 6≔\ 5/a\ 6 S;
+ X ≟ \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"\ 6mk_DeqSet\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S) (\ 5a href="cic:/matita/tutorial/chapter7/beqitem.fix(0,1,4)"\ 6beqitem\ 5/a\ 6 S) (\ 5a href="cic:/matita/tutorial/chapter7/beqitem_true.def(5)"\ 6beqitem_true\ 5/a\ 6 S)
(* ---------------------------------------- *) ⊢
- pitem S ≡ carr X.
+ \ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S ≡ \ 5a href="cic:/matita/tutorial/chapter4/carr.fix(0,0,2)"\ 6carr\ 5/a\ 6 X.
-unification hint 0 ≔ S,i1,i2;
- X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S)
+unification hint 0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type0"\ 6≔\ 5/a\ 6 S,i1,i2;
+ X ≟ \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"\ 6mk_DeqSet\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S) (\ 5a href="cic:/matita/tutorial/chapter7/beqitem.fix(0,1,4)"\ 6beqitem\ 5/a\ 6 S) (\ 5a href="cic:/matita/tutorial/chapter7/beqitem_true.def(5)"\ 6beqitem_true\ 5/a\ 6 S)
(* ---------------------------------------- *) ⊢
- beqitem S i1 i2 ≡ eqb X i1 i2.
+ \ 5a href="cic:/matita/tutorial/chapter7/beqitem.fix(0,1,4)"\ 6beqitem\ 5/a\ 6 S i1 i2 ≡ \ 5a href="cic:/matita/tutorial/chapter4/eqb.fix(0,0,3)"\ 6eqb\ 5/a\ 6 X i1 i2.
-(* The intuitive semantic of a point is to mark the position where
+(*
+\ 5h2\ 6Semantics of pointed regular expressions\ 5/h2\ 6
+The intuitive semantic of a point is to mark the position where
we should start reading the regular expression. The language associated
to a pre is the union of the languages associated with its points. *)
-let rec in_pl (S : DeqSet) (r : pitem S) on r : word S → Prop ≝
+\ 5img class="anchor" src="icons/tick.png" id="in_pl"\ 6let rec in_pl (S : \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (r : \ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S) on r : \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop ≝
match r with
-[ pz ⇒ ∅
-| pe ⇒ ∅
-| ps _ ⇒ ∅
-| pp x ⇒ { [x] }
-| pc r1 r2 ⇒ (in_pl ? r1) · \sem{forget ? r2} ∪ (in_pl ? r2)
-| po r1 r2 ⇒ (in_pl ? r1) ∪ (in_pl ? r2)
-| pk r1 ⇒ (in_pl ? r1) · \sem{forget ? r1}^* ].
+[ pz ⇒ \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
+| pe ⇒ \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
+| ps _ ⇒ \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6
+| pp x ⇒ \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6 (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6) \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6
+| pc r1 r2 ⇒ (in_pl ? r1) \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a href="cic:/matita/tutorial/chapter7/forget.fix(0,1,3)"\ 6forget\ 5/a\ 6 ? r2\ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6\ 5span class="error" title="Parse error: [term] expected after [sym∪] (in [term])"\ 6\ 5/span\ 6 (in_pl ? r2)
+| po r1 r2 ⇒ (in_pl ? r1) \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 (in_pl ? r2)
+| pk r1 ⇒ (in_pl ? r1) \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a href="cic:/matita/tutorial/chapter7/forget.fix(0,1,3)"\ 6forget\ 5/a\ 6 ? r1\ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 5a title="star lang" 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 in_prl ≝ λS : DeqSet.λp:pre S.
- if (\snd p) then \sem{\fst p} ∪ {ϵ} else \sem{\fst p}.
+\ 5img class="anchor" src="icons/tick.png" id="in_prl"\ 6definition in_prl ≝ λS : \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λp:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
+ if (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p) then \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6\ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 else \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6.
interpretation "in_prl mem" 'mem w l = (in_prl ? l w).
interpretation "in_prl" 'in_l E = (in_prl ? E).
(* The following, trivial lemmas are only meant for rewriting purposes. *)
-lemma sem_pre_true : ∀S.∀i:pitem S.
- \sem{〈i,true〉} = \sem{i} ∪ {ϵ}.
+\ 5img class="anchor" src="icons/tick.png" id="sem_pre_true"\ 6lemma sem_pre_true : ∀S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
+ \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6\ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6\ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6.
// qed.
-lemma sem_pre_false : ∀S.∀i:pitem S.
- \sem{〈i,false〉} = \sem{i}.
+\ 5img class="anchor" src="icons/tick.png" id="sem_pre_false"\ 6lemma sem_pre_false : ∀S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
+ \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i,\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6\ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6.
// qed.
-lemma sem_cat: ∀S.∀i1,i2:pitem S.
- \sem{i1 · i2} = \sem{i1} · \sem{|i2|} ∪ \sem{i2}.
+\ 5img class="anchor" src="icons/tick.png" id="sem_cat"\ 6lemma sem_cat: ∀S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
+ \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i1 \ 5a title="pitem cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 i2\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i1\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i2\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i2\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6.
// qed.
-lemma sem_cat_w: ∀S.∀i1,i2:pitem S.∀w.
- \sem{i1 · i2} w = ((\sem{i1} · \sem{|i2|}) w ∨ \sem{i2} w).
+\ 5img class="anchor" src="icons/tick.png" id="sem_cat_w"\ 6lemma sem_cat_w: ∀S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.∀w.
+ \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i1 \ 5a title="pitem cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 i2\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 w \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 ((\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i1\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i2\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6) w \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i2\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 w).
// qed.
-lemma sem_plus: ∀S.∀i1,i2:pitem S.
- \sem{i1 + i2} = \sem{i1} ∪ \sem{i2}.
+\ 5img class="anchor" src="icons/tick.png" id="sem_plus"\ 6lemma sem_plus: ∀S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
+ \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i1 \ 5a title="pitem or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 i2\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i1\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i2\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6.
// qed.
-lemma sem_plus_w: ∀S.∀i1,i2:pitem S.∀w.
- \sem{i1 + i2} w = (\sem{i1} w ∨ \sem{i2} w).
+\ 5img class="anchor" src="icons/tick.png" id="sem_plus_w"\ 6lemma sem_plus_w: ∀S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.∀w.
+ \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i1 \ 5a title="pitem or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 i2\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 w \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i1\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 w \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i2\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 w).
// qed.
-lemma sem_star : ∀S.∀i:pitem S.
- \sem{i^*} = \sem{i} · \sem{|i|}^*.
+\ 5img class="anchor" src="icons/tick.png" id="sem_star"\ 6lemma sem_star : ∀S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
+ \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 \ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6.
// qed.
-lemma sem_star_w : ∀S.∀i:pitem S.∀w.
- \sem{i^*} w = (∃w1,w2.w1 @ w2 = w ∧ \sem{i} w1 ∧ \sem{|i|}^* w2).
+\ 5img class="anchor" src="icons/tick.png" id="sem_star_w"\ 6lemma sem_star_w : ∀S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.∀w.
+ \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 w \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6w1,w2\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6.\ 5/a\ 6w1 \ 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 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 w1 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6\ 5a title="star lang" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 w2).
// qed.
(* Below are a few, simple, semantic properties of items. In particular:
The first property is proved by a simple induction on $i$; the other
results are easy corollaries. We need an auxiliary lemma first. *)
-lemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = ϵ → w1 = ϵ.
+\ 5img class="anchor" src="icons/tick.png" id="append_eq_nil"\ 6lemma append_eq_nil : ∀S.∀w1,w2:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S. 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 \ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6 → w1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6.
#S #w1 #w2 cases w1 // #a #tl normalize #H destruct qed.
-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/
- |#r1 #r2 #n1 #n2 % * /2/
- |#r #n % * #w1 * #w2 * * #H >(append_eq_nil …H…) /2/
+\ 5img class="anchor" src="icons/tick.png" id="not_epsilon_lp"\ 6lemma not_epsilon_lp : ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S. \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 (\ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6 \ 5a title="in_pl mem" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 e).
+#S #e elim e normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ [#r1 #r2 * #n1 #n2 % * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ * #w1 * #w2 * * #H
+ >(\ 5a href="cic:/matita/tutorial/chapter7/append_eq_nil.def(4)"\ 6append_eq_nil\ 5/a\ 6 …H…) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
+ |#r1 #r2 #n1 #n2 % * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ |#r #n % * #w1 * #w2 * * #H >(\ 5a href="cic:/matita/tutorial/chapter7/append_eq_nil.def(4)"\ 6append_eq_nil\ 5/a\ 6 …H…) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
]
qed.
-lemma epsilon_to_true : ∀S.∀e:pre S. ϵ ∈ e → \snd e = true.
-#S * #i #b cases b // normalize #H @False_ind /2/
+\ 5img class="anchor" src="icons/tick.png" id="epsilon_to_true"\ 6lemma epsilon_to_true : ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S. \ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6 \ 5a title="in_prl mem" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 e → \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 e \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
+#S * #i #b cases b // normalize #H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
-lemma true_to_epsilon : ∀S.∀e:pre S. \snd e = true → ϵ ∈ e.
+\ 5img class="anchor" src="icons/tick.png" id="true_to_epsilon"\ 6lemma true_to_epsilon : ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S. \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 e \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a title="epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6 \ 5a title="in_prl mem" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 e.
#S * #i #b #btrue normalize in btrue; >btrue %2 //
qed.
-lemma minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}.
+\ 5img class="anchor" src="icons/tick.png" id="minus_eps_item"\ 6lemma minus_eps_item: ∀S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S. \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6\ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6\ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6\ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6.
#S #i #w %
- [#H whd % // normalize @(not_to_not … (not_epsilon_lp …i)) //
+ [#H whd % // normalize @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter7/not_epsilon_lp.def(8)"\ 6not_epsilon_lp\ 5/a\ 6 …i)) //
|* //
]
qed.
-lemma minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
+\ 5img class="anchor" src="icons/tick.png" id="minus_eps_pre"\ 6lemma minus_eps_pre: ∀S.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S. \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6\ 5span class="error" title="Parse error: [sym{] expected after [sym\sem ] (in [term])"\ 6\ 5/span\ 6{\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e\ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6 \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e\ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6\ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6\ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6{\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6\ 5a title="singleton" href="cic:/fakeuri.def(1)"\ 6}\ 5/a\ 6.
#S * #i *
- [>sem_pre_true normalize in ⊢ (??%?); #w %
- [/3/ | * * // #H1 #H2 @False_ind @(absurd …H1 H2)]
- |>sem_pre_false normalize in ⊢ (??%?); #w % [ /3/ | * // ]
- ]
-qed.
-
-definition lo ≝ λS:DeqSet.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉.
-notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
-interpretation "oplus" 'oplus a b = (lo ? a b).
-
-lemma lo_def: ∀S.∀i1,i2:pitem S.∀b1,b2. 〈i1,b1〉⊕〈i2,b2〉=〈i1+i2,b1∨b2〉.
-// qed.
-
-definition pre_concat_r ≝ λS:DeqSet.λi:pitem S.λe:pre S.
- match e with [ mk_Prod i1 b ⇒ 〈i · i1, b〉].
-
-notation "i ◃ e" left associative with precedence 60 for @{'lhd $i $e}.
-interpretation "pre_concat_r" 'lhd i e = (pre_concat_r ? i e).
-
-lemma eq_to_ex_eq: ∀S.∀A,B:word S → Prop.
- A = B → A =1 B.
-#S #A #B #H >H /2/ qed.
-
-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: @eq_to_ex_eq //]
->sem_pre_true >sem_cat >sem_pre_true /2/
-qed.
-
-definition pre_concat_l ≝ λS:DeqSet.λbcast:∀S:DeqSet.pitem S → pre S.λe1:pre S.λi2:pitem S.
- match e1 with
- [ mk_Prod i1 b1 ⇒ match b1 with
- [ true ⇒ (i1 ◃ (bcast ? i2))
- | false ⇒ 〈i1 · i2,false〉
- ]
- ].
-
-notation "a ▹ b" left associative with precedence 60 for @{'tril eclose $a $b}.
-interpretation "item-pre concat" 'tril op a b = (pre_concat_l ? op a b).
-
-notation "•" non associative with precedence 60 for @{eclose ?}.
-
-let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝
- match i with
- [ pz ⇒ 〈 `∅, false 〉
- | pe ⇒ 〈 ϵ, true 〉
- | ps x ⇒ 〈 `.x, false〉
- | pp x ⇒ 〈 `.x, false 〉
- | po i1 i2 ⇒ •i1 ⊕ •i2
- | pc i1 i2 ⇒ •i1 ▹ i2
- | pk i ⇒ 〈(\fst (•i))^*,true〉].
-
-notation "• x" non associative with precedence 60 for @{'eclose $x}.
-interpretation "eclose" 'eclose x = (eclose ? x).
-
-lemma eclose_plus: ∀S:DeqSet.∀i1,i2:pitem S.
- •(i1 + i2) = •i1 ⊕ •i2.
-// qed.
-
-lemma eclose_dot: ∀S:DeqSet.∀i1,i2:pitem S.
- •(i1 · i2) = •i1 ▹ i2.
-// qed.
-
-lemma eclose_star: ∀S:DeqSet.∀i:pitem S.
- •i^* = 〈(\fst(•i))^*,true〉.
-// qed.
-
-definition lift ≝ λS.λf:pitem S →pre S.λe:pre S.
- match e with
- [ mk_Prod i b ⇒ 〈\fst (f i), \snd (f i) ∨ b〉].
-
-definition preclose ≝ λS. lift S (eclose S).
-interpretation "preclose" 'eclose x = (preclose ? x).
-
-(* theorem 16: 2 *)
-lemma sem_oplus: ∀S:DeqSet.∀e1,e2:pre S.
- \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}.
-#S * #i1 #b1 * #i2 #b2 #w %
- [cases b1 cases b2 normalize /2/ * /3/ * /3/
- |cases b1 cases b2 normalize /2/ * /3/ * /3/
- ]
-qed.
-
-lemma odot_true :
- ∀S.∀i1,i2:pitem S.
- 〈i1,true〉 ▹ i2 = i1 ◃ (•i2).
-// qed.
-
-lemma odot_true_bis :
- ∀S.∀i1,i2:pitem S.
- 〈i1,true〉 ▹ i2 = 〈i1 · \fst (•i2), \snd (•i2)〉.
-#S #i1 #i2 normalize cases (•i2) // qed.
-
-lemma odot_false:
- ∀S.∀i1,i2:pitem S.
- 〈i1,false〉 ▹ i2 = 〈i1 · i2, false〉.
-// qed.
-
-lemma LcatE : ∀S.∀e1,e2:pitem S.
- \sem{e1 · e2} = \sem{e1} · \sem{|e2|} ∪ \sem{e2}.
-// qed.
-
-lemma erase_bull : ∀S.∀i:pitem S. |\fst (•i)| = |i|.
-#S #i elim i //
- [ #i1 #i2 #IH1 #IH2 >erase_dot <IH1 >eclose_dot
- cases (•i1) #i11 #b1 cases b1 // <IH2 >odot_true_bis //
- | #i1 #i2 #IH1 #IH2 >eclose_plus >(erase_plus … i1) <IH1 <IH2
- cases (•i1) #i11 #b1 cases (•i2) #i21 #b2 //
- | #i #IH >eclose_star >(erase_star … i) <IH cases (•i) //
- ]
-qed.
-
-(*
-lemma sem_eclose_star: ∀S:DeqSet.∀i:pitem S.
- \sem{〈i^*,true〉} =1 \sem{〈i,false〉}·\sem{|i|}^* ∪ {ϵ}.
-/2/ qed.
-*)
-
-(* theorem 16: 1 → 3 *)
-lemma odot_dot_aux : ∀S.∀e1:pre S.∀i2:pitem S.
- \sem{•i2} =1 \sem{i2} ∪ \sem{|i2|} →
- \sem{e1 ▹ i2} =1 \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
-#S * #i1 #b1 #i2 cases b1
- [2:#th >odot_false >sem_pre_false >sem_pre_false >sem_cat /2/
- |#H >odot_true >sem_pre_true @(eqP_trans … (sem_pre_concat_r …))
- >erase_bull @eqP_trans [|@(eqP_union_l … H)]
- @eqP_trans [|@eqP_union_l[|@union_comm ]]
- @eqP_trans [|@eqP_sym @union_assoc ] /3/
- ]
-qed.
-
-lemma minus_eps_pre_aux: ∀S.∀e:pre S.∀i:pitem S.∀A.
- \sem{e} =1 \sem{i} ∪ A → \sem{\fst e} =1 \sem{i} ∪ (A - {[ ]}).
-#S #e #i #A #seme
-@eqP_trans [|@minus_eps_pre]
-@eqP_trans [||@eqP_union_r [|@eqP_sym @minus_eps_item]]
-@eqP_trans [||@distribute_substract]
-@eqP_substract_r //
-qed.
-
-(* theorem 16: 1 *)
-theorem sem_bull: ∀S:DeqSet. ∀i:pitem S. \sem{•i} =1 \sem{i} ∪ \sem{|i|}.
-#S #e elim e
- [#w normalize % [/2/ | * //]
- |/2/
- |#x normalize #w % [ /2/ | * [@False_ind | //]]
- |#x normalize #w % [ /2/ | * // ]
- |#i1 #i2 #IH1 #IH2 >eclose_dot
- @eqP_trans [|@odot_dot_aux //] >sem_cat
- @eqP_trans
- [|@eqP_union_r
- [|@eqP_trans [|@(cat_ext_l … IH1)] @distr_cat_r]]
- @eqP_trans [|@union_assoc]
- @eqP_trans [||@eqP_sym @union_assoc]
- @eqP_union_l //
- |#i1 #i2 #IH1 #IH2 >eclose_plus
- @eqP_trans [|@sem_oplus] >sem_plus >erase_plus
- @eqP_trans [|@(eqP_union_l … IH2)]
- @eqP_trans [|@eqP_sym @union_assoc]
- @eqP_trans [||@union_assoc] @eqP_union_r
- @eqP_trans [||@eqP_sym @union_assoc]
- @eqP_trans [||@eqP_union_l [|@union_comm]]
- @eqP_trans [||@union_assoc] /2/
- |#i #H >sem_pre_true >sem_star >erase_bull >sem_star
- @eqP_trans [|@eqP_union_r [|@cat_ext_l [|@minus_eps_pre_aux //]]]
- @eqP_trans [|@eqP_union_r [|@distr_cat_r]]
- @eqP_trans [|@union_assoc] @eqP_union_l >erase_star
- @eqP_sym @star_fix_eps
- ]
-qed.
-
-(* blank item *)
-let rec blank (S: DeqSet) (i: re S) on i :pitem S ≝
- match i with
- [ z ⇒ `∅
- | e ⇒ ϵ
- | s y ⇒ `y
- | o e1 e2 ⇒ (blank S e1) + (blank S e2)
- | c e1 e2 ⇒ (blank S e1) · (blank S e2)
- | k e ⇒ (blank S e)^* ].
-
-lemma forget_blank: ∀S.∀e:re S.|blank S e| = e.
-#S #e elim e normalize //
-qed.
-
-lemma sem_blank: ∀S.∀e:re S.\sem{blank S e} =1 ∅.
-#S #e elim e
- [1,2:@eq_to_ex_eq //
- |#s @eq_to_ex_eq //
- |#e1 #e2 #Hind1 #Hind2 >sem_cat
- @eqP_trans [||@(union_empty_r … ∅)]
- @eqP_trans [|@eqP_union_l[|@Hind2]] @eqP_union_r
- @eqP_trans [||@(cat_empty_l … ?)] @cat_ext_l @Hind1
- |#e1 #e2 #Hind1 #Hind2 >sem_plus
- @eqP_trans [||@(union_empty_r … ∅)]
- @eqP_trans [|@eqP_union_l[|@Hind2]] @eqP_union_r @Hind1
- |#e #Hind >sem_star
- @eqP_trans [||@(cat_empty_l … ?)] @cat_ext_l @Hind
- ]
-qed.
-
-theorem re_embedding: ∀S.∀e:re S.
- \sem{•(blank S e)} =1 \sem{e}.
-#S #e @eqP_trans [|@sem_bull] >forget_blank
-@eqP_trans [|@eqP_union_r [|@sem_blank]]
-@eqP_trans [|@union_comm] @union_empty_r.
-qed.
-
-(* lefted operations *)
-definition lifted_cat ≝ λS:DeqSet.λe:pre S.
- lift S (pre_concat_l S eclose e).
-
-notation "e1 ⊙ e2" left associative with precedence 70 for @{'odot $e1 $e2}.
-
-interpretation "lifted cat" 'odot e1 e2 = (lifted_cat ? e1 e2).
-
-lemma odot_true_b : ∀S.∀i1,i2:pitem S.∀b.
- 〈i1,true〉 ⊙ 〈i2,b〉 = 〈i1 · (\fst (•i2)),\snd (•i2) ∨ b〉.
-#S #i1 #i2 #b normalize in ⊢ (??%?); cases (•i2) //
-qed.
-
-lemma odot_false_b : ∀S.∀i1,i2:pitem S.∀b.
- 〈i1,false〉 ⊙ 〈i2,b〉 = 〈i1 · i2 ,b〉.
-//
-qed.
-
-lemma erase_odot:∀S.∀e1,e2:pre S.
- |\fst (e1 ⊙ e2)| = |\fst e1| · (|\fst e2|).
-#S * #i1 * * #i2 #b2 // >odot_true_b >erase_dot //
-qed.
-
-definition lk ≝ λS:DeqSet.λe:pre S.
- match e with
- [ mk_Prod i1 b1 ⇒
- match b1 with
- [true ⇒ 〈(\fst (eclose ? i1))^*, true〉
- |false ⇒ 〈i1^*,false〉
- ]
- ].
-
-(* notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $a}.*)
-interpretation "lk" 'lk a = (lk ? a).
-notation "a^⊛" non associative with precedence 90 for @{'lk $a}.
-
-
-lemma ostar_true: ∀S.∀i:pitem S.
- 〈i,true〉^⊛ = 〈(\fst (•i))^*, true〉.
-// qed.
-
-lemma ostar_false: ∀S.∀i:pitem S.
- 〈i,false〉^⊛ = 〈i^*, false〉.
-// qed.
-
-lemma erase_ostar: ∀S.∀e:pre S.
- |\fst (e^⊛)| = |\fst e|^*.
-#S * #i * // qed.
-
-lemma sem_odot_true: ∀S:DeqSet.∀e1:pre S.∀i.
- \sem{e1 ⊙ 〈i,true〉} =1 \sem{e1 ▹ i} ∪ { [ ] }.
-#S #e1 #i
-cut (e1 ⊙ 〈i,true〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ true〉) [//]
-#H >H cases (e1 ▹ i) #i1 #b1 cases b1
- [>sem_pre_true @eqP_trans [||@eqP_sym @union_assoc]
- @eqP_union_l /2/
- |/2/
- ]
-qed.
-
-lemma eq_odot_false: ∀S:DeqSet.∀e1:pre S.∀i.
- e1 ⊙ 〈i,false〉 = e1 ▹ i.
-#S #e1 #i
-cut (e1 ⊙ 〈i,false〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ false〉) [//]
-cases (e1 ▹ i) #i1 #b1 cases b1 #H @H
-qed.
-
-lemma sem_odot:
- ∀S.∀e1,e2: pre S. \sem{e1 ⊙ e2} =1 \sem{e1}· \sem{|\fst e2|} ∪ \sem{e2}.
-#S #e1 * #i2 *
- [>sem_pre_true
- @eqP_trans [|@sem_odot_true]
- @eqP_trans [||@union_assoc] @eqP_union_r @odot_dot_aux //
- |>sem_pre_false >eq_odot_false @odot_dot_aux //
- ]
-qed.
-
-(* theorem 16: 4 *)
-theorem sem_ostar: ∀S.∀e:pre S.
- \sem{e^⊛} =1 \sem{e} · \sem{|\fst e|}^*.
-#S * #i #b cases b
- [>sem_pre_true >sem_pre_true >sem_star >erase_bull
- @eqP_trans [|@eqP_union_r[|@cat_ext_l [|@minus_eps_pre_aux //]]]
- @eqP_trans [|@eqP_union_r [|@distr_cat_r]]
- @eqP_trans [||@eqP_sym @distr_cat_r]
- @eqP_trans [|@union_assoc] @eqP_union_l
- @eqP_trans [||@eqP_sym @epsilon_cat_l] @eqP_sym @star_fix_eps
- |>sem_pre_false >sem_pre_false >sem_star /2/
+ [>\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_true.def(9)"\ 6sem_pre_true\ 5/a\ 6 normalize in ⊢ (??%?); #w %
+ [/\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | * * // #H1 #H2 @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 …H1 H2)]
+ |>\ 5a href="cic:/matita/tutorial/chapter7/sem_pre_false.def(9)"\ 6sem_pre_false\ 5/a\ 6 normalize in ⊢ (??%?); #w % [ /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | * // ]
]
qed.
\ No newline at end of file
projects / helm.git / blobdiff