•((a + ϵ)(b^*a + b)b) = 〈(•a + ϵ)((•b)^*•a + •b)b, false〉
*)
+include "tutorial/chapter7.ma".
+
+(* Broadcasting a point inside an item generates a pre, since the point could possibly reach
+the end of the expression.
+Broadcasting inside a i1+i2 amounts to broadcast in parallel inside i1 and i2.
+If we define
+ 〈i1,b1〉 ⊕ 〈i2,b2〉 = 〈i1 + i2, b1∨ b2〉
+then, we just have •(i1+i2) = •(i1)⊕ •(i2).
+*)
include "tutorial/chapter7.ma".
-definition lo ≝ λS:DeqSet.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉.
+definition lo ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λa,b:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 a \ 5a title="pitem or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 b,\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 a \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 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〉.
+lemma lo_def: ∀S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.∀b1,b2. \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i1,b1〉\ 5a title="oplus" href="cic:/fakeuri.def(1)"\ 6⊕\ 5/a\ 6\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i2,b2〉\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i1\ 5a title="pitem or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6i2,b1\ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6b2〉.
// qed.
-definition pre_concat_r ≝ λS:DeqSet.λi:pitem S.λe:pre S.
- match e with [ mk_Prod i1 b ⇒ 〈i · i1, b〉].
+(*
+Concatenation is a bit more complex. In order to broadcast a point inside i1 · i2
+we should start broadcasting it inside i1 and then proceed into i2 if and only if a
+point reached the end of i1. This suggests to define •(i1 · i2) as •(i1) ▹ i2, where
+e ▹ i is a general operation of concatenation between a pre and an item, defined by
+cases on the boolean in e:
+
+ 〈i1,true〉 ▹ i2 = i1 ◃ •(i_2)
+ 〈i1,false〉 ▹ i2 = i1 · i2
+In turn, ◃ says how to concatenate an item with a pre, that is however extremely simple:
+ i1 ◃ 〈i1,b〉 = 〈i_1 · i2, b〉
+Let us come to the formalized definitions:
+*)
+
+definition pre_concat_r ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λi:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.λe:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
+ match e with [ mk_Prod i1 b ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i \ 5a title="pitem cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 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 eq_to_ex_eq: ∀S.∀A,B:\ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S → Prop.
+ A \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 B → A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 B.
+#S #A #B #H >H #x % // qed.
+
+(* The behaviour of \triangleleft is summarized by the following, easy lemma: *)
lemma sem_pre_concat_r : ∀S,i.∀e:pre S.
\sem{i ◃ e} =1 \sem{i} · \sem{|\fst e|} ∪ \sem{e}.
>sem_pre_true >sem_cat >sem_pre_true /2/
qed.
+(* The definition of $\bullet(-)$ (\verb+eclose+) and
+$\triangleright$ (\verb+pre_concat_l+) are mutually recursive.
+In this situation, a viable alternative that is usually simpler
+to reason about, is to abstract one of the two functions with respect
+to the other. We make the notation declarations explicit in this
+case, for the sake of clarity.
+*)
+
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
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).
+(* We are ready to give the formal definition of the broadcasting operation. *)
+
notation "•" non associative with precedence 60 for @{eclose ?}.
let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝
notation "• x" non associative with precedence 60 for @{'eclose $x}.
interpretation "eclose" 'eclose x = (eclose ? x).
+(* Here are a few simple properties of •(-) *)
+
lemma eclose_plus: ∀S:DeqSet.∀i1,i2:pitem S.
•(i1 + i2) = •i1 ⊕ •i2.
// qed.
•i^* = 〈(\fst(•i))^*,true〉.
// qed.
+(* The definition of •(-) (eclose) can then be lifted from items to pres
+in the obvious way. *)
+
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 *)
+(* Obviously, broadcasting does not change the carrier of the item,
+as it is easily proved by structural induction. *)
+
+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.
+
+(* We are now ready to state the main semantic properties of $\oplus,
+\triangleleft$ and $\bullet(-)$:
+
+\begin{lstlisting}[language=grafite]
+lemma sem_oplus: ∀S:DeqSet.∀e1,e2:pre S.
+ \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}.
+lemma sem_pcl : ∀S.∀e1:pre S.∀i2:pitem S.
+ \sem{e1 ▹ i2} =1 \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
+theorem sem_bullet: ∀S:DeqSet. ∀i:pitem S.
+ \sem{•i} =1 \sem{i} ∪ \sem{|i|}.
+\end{lstlisting}
+The proof of \verb+sem_oplus+ is straightforward. *)
+
lemma sem_oplus: ∀S:DeqSet.∀e1,e2:pre S.
\sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}.
#S * #i1 #b1 * #i2 #b2 #w %
]
qed.
-lemma odot_true :
- ∀S.∀i1,i2:pitem S.
- 〈i1,true〉 ▹ i2 = i1 ◃ (•i2).
-// qed.
+(* For the others, we proceed as follow: we first prove the following
+auxiliary lemma, that assumes sem_bullet:
-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 sem_pcl_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}.
-lemma odot_false:
- ∀S.∀i1,i2:pitem S.
- 〈i1,false〉 ▹ i2 = 〈i1 · i2, false〉.
-// qed.
+Then, using the previous result, we prove sem_bullet by induction
+on i. Finally, sem_pcl_aux and sem_bullet give sem_pcl. *)
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.
+lemma sem_pcl_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
projects / helm.git / blobdiff