-(* <h1>Regular Expressions</h1>
+(*
+\ 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. *)
(* 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 ≝
+let rec in_l (S : \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 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 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
+[ 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}
-| 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]}
+| s 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="nil" 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*].
// qed.
-(* <h2>Pointed Regular expressions </h2>
+(*
+\ 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
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 ≝
+let 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 (forget ? E2)
+ | pk E ⇒ (forget ? E)\ 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|).
+lemma 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="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\ 6e2|).
// qed.
-lemma erase_plus : ∀S.∀i1,i2:pitem S.
- |i1 + i2| = |i1| + |i2|.
+lemma 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="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="re or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i2|.
// qed.
-lemma erase_star : ∀S.∀i:pitem S.|i^*| = |i|^*.
+lemma 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="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="re star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6*.
// qed.
-(* <h2>Comparing items and pres<h2>
+(*
+\ 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 ≝
+let 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=y2 | _ ⇒ \ 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=y2 | _ ⇒ \ 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]
| 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).
+lemma 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).
+ \ 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.
-(* <h2>Semantics of pointed regular expression<h2>
+(*
+\ 5h2\ 6Semantics of pointed regular expression\ 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 ≝
+let 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="nil" 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="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 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="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}.
+definition 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="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} 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}.
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} ∪ {ϵ}.
+lemma 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="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="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}.
// qed.
-lemma sem_pre_false : ∀S.∀i:pitem S.
- \sem{〈i,false〉} = \sem{i}.
+lemma 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="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}.
// qed.
-lemma sem_cat: ∀S.∀i1,i2:pitem S.
- \sem{i1 · i2} = \sem{i1} · \sem{|i2|} ∪ \sem{i2}.
+lemma 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="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="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="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}.
// qed.
-lemma sem_cat_w: ∀S.∀i1,i2:pitem S.∀w.
- \sem{i1 · i2} w = ((\sem{i1} · \sem{|i2|}) w ∨ \sem{i2} w).
+lemma 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} 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="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|}) 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} w).
// qed.
-lemma sem_plus: ∀S.∀i1,i2:pitem S.
- \sem{i1 + i2} = \sem{i1} ∪ \sem{i2}.
+lemma 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="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="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}.
// qed.
-lemma sem_plus_w: ∀S.∀i1,i2:pitem S.∀w.
- \sem{i1 + i2} w = (\sem{i1} w ∨ \sem{i2} w).
+lemma 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} 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} 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} w).
// qed.
-lemma sem_star : ∀S.∀i:pitem S.
- \sem{i^*} = \sem{i} · \sem{|i|}^*.
+lemma 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="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="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="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).
+lemma 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*} 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.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 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i} 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="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 = ϵ.
+lemma 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/
+lemma 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/
+lemma 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.
+lemma 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}-{[ ]}.
+lemma 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="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="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 ]}.
#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}-{[ ]}.
+lemma 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{\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e} \ 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="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 ]}.
#S * #i *
- [>sem_pre_true normalize in ⊢ (??%?); #w %
- [/3/ | * * // #H1 #H2 @False_ind @(absurd …H1 H2)]
- |>sem_pre_false normalize in ⊢ (??%?); #w % [ /3/ | * // ]
+ [>\ 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.
-
+qed.
\ No newline at end of file
projects / helm.git / commitdiff