notation > "'if' term 46 e 'then' term 46 t 'else' term 46 f" non associative with precedence 46
for @{ match $e in bool with [ true ⇒ $t | false ⇒ $f] }.
notation < "hvbox('if' \nbsp term 46 e \nbsp break 'then' \nbsp term 46 t \nbsp break 'else' \nbsp term 49 f \nbsp)" non associative with precedence 46
- for @{ match $e with [ true ⇒ $t | false ⇒ $f] }.
+ for @{ match $e return $T with [ true ⇒ $t | false ⇒ $f] }.
theorem bool_to_decidable_eq:
∀b1,b2:bool. decidable (b1=b2).
(* extensional equality *)
definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a ↔ Q a.
-notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}.
+notation "A ≐ B" non associative with precedence 45 for @{'eqP $A $B}.
interpretation "extensional equality" 'eqP a b = (eqP ? a b).
lemma eqP_sym: ∀U.∀A,B:U →Prop.
- A =1 B → B =1 A.
+ A ≐ B → B ≐ A.
#U #A #B #eqAB #a @iff_sym @eqAB qed.
lemma eqP_trans: ∀U.∀A,B,C:U →Prop.
- A =1 B → B =1 C → A =1 C.
+ A ≐ B → B ≐ C → A ≐ C.
#U #A #B #C #eqAB #eqBC #a @iff_trans // qed.
lemma eqP_union_r: ∀U.∀A,B,C:U →Prop.
- A =1 C → A ∪ B =1 C ∪ B.
+ A ≐ C → A ∪ B ≐ C ∪ B.
#U #A #B #C #eqAB #a @iff_or_r @eqAB qed.
lemma eqP_union_l: ∀U.∀A,B,C:U →Prop.
- B =1 C → A ∪ B =1 A ∪ C.
+ B ≐ C → A ∪ B ≐ A ∪ C.
#U #A #B #C #eqBC #a @iff_or_l @eqBC qed.
lemma eqP_intersect_r: ∀U.∀A,B,C:U →Prop.
- A =1 C → A ∩ B =1 C ∩ B.
+ A ≐ C → A ∩ B ≐ C ∩ B.
#U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop.
- B =1 C → A ∩ B =1 A ∩ C.
+ B ≐ C → A ∩ B ≐ A ∩ C.
#U #A #B #C #eqBC #a @iff_and_l @eqBC qed.
lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop.
- A =1 C → A - B =1 C - B.
+ A ≐ C → A - B ≐ C - B.
#U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop.
- B =1 C → A - B =1 A - C.
+ B ≐ C → A - B ≐ A - C.
#U #A #B #C #eqBC #a @iff_and_l /2/ qed.
(* set equalities *)
lemma union_empty_r: ∀U.∀A:U→Prop.
- A ∪ ∅ =1 A.
+ A ∪ ∅ ≐ A.
#U #A #w % [* // normalize #abs @False_ind /2/ | /2/]
qed.
lemma union_comm : ∀U.∀A,B:U →Prop.
- A ∪ B =1 B ∪ A.
+ A ∪ B ≐ B ∪ A.
#U #A #B #a % * /2/ qed.
lemma union_assoc: ∀U.∀A,B,C:U → Prop.
- A ∪ B ∪ C =1 A ∪ (B ∪ C).
+ A ∪ B ∪ C ≐ A ∪ (B ∪ C).
#S #A #B #C #w % [* [* /3/ | /3/] | * [/3/ | * /3/]
qed.
lemma cap_comm : ∀U.∀A,B:U →Prop.
- A ∩ B =1 B ∩ A.
+ A ∩ B ≐ B ∩ A.
#U #A #B #a % * /2/ qed.
lemma union_idemp: ∀U.∀A:U →Prop.
- A ∪ A =1 A.
+ A ∪ A ≐ A.
#U #A #a % [* // | /2/] qed.
lemma cap_idemp: ∀U.∀A:U →Prop.
- A ∩ A =1 A.
+ A ∩ A ≐ A.
#U #A #a % [* // | /2/] qed.
(*distributivities *)
lemma distribute_intersect : ∀U.∀A,B,C:U→Prop.
- (A ∪ B) ∩ C =1 (A ∩ C) ∪ (B ∩ C).
+ (A ∪ B) ∩ C ≐ (A ∩ C) ∪ (B ∩ C).
#U #A #B #C #w % [* * /3/ | * * /3/]
qed.
lemma distribute_substract : ∀U.∀A,B,C:U→Prop.
- (A ∪ B) - C =1 (A - C) ∪ (B - C).
+ (A ∪ B) - C ≐ (A - C) ∪ (B - C).
#U #A #B #C #w % [* * /3/ | * * /3/]
qed.
(* substraction *)
-lemma substract_def:∀U.∀A,B:U→Prop. A-B =1 A ∩ ¬B.
+lemma substract_def:∀U.∀A,B:U→Prop. A-B ≐ A ∩ ¬B.
#U #A #B #w normalize /2/
qed.
\ No newline at end of file
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.
+ A ≐ C → A · B ≐ 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.
+ B ≐ C → A · B ≐ A · C.
#S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
cases (H w2) /6/
qed.
-lemma cat_empty_l: ∀S.∀A:word S→Prop. ∅ · A =1 ∅.
+lemma cat_empty_l: ∀S.∀A:word S→Prop. ∅ · A ≐ ∅.
#S #A #w % [|*] * #w1 * #w2 * * #_ *
qed.
lemma distr_cat_r: ∀S.∀A,B,C:word S →Prop.
- (A ∪ B) · C =1 A · C ∪ B · C.
+ (A ∪ B) · C ≐ A · C ∪ B · C.
#S #A #B #C #w %
[* #w1 * #w2 * * #eqw * /6/ |* * #w1 * #w2 * * /6/]
qed.
definition deriv ≝ λS.λA:word S → Prop.λa,w. A (a::w).
lemma deriv_middot: ∀S,A,B,a. ¬ A ϵ →
- deriv S (A·B) a =1 (deriv S A a) · B.
+ deriv S (A·B) a ≐ (deriv S A a) · B.
#S #A #B #a #noteps #w normalize %
[* #w1 cases w1
[* #w2 * * #_ #Aeps @False_ind /2/
qed.
lemma fix_star: ∀S.∀A:word S → Prop.
- A^* =1 A · A^* ∪ {ϵ}.
+ A^* ≐ A · A^* ∪ {ϵ}.
#S #A #w %
[* #l generalize in match w; -w cases l [normalize #w * /2/]
#w1 #tl #w * whd in ⊢ ((??%?)→?); #eqw whd in ⊢ (%→?); *
qed.
lemma star_fix_eps : ∀S.∀A:word S → Prop.
- A^* =1 (A - {ϵ}) · A^* ∪ {ϵ}.
+ A^* ≐ (A - {ϵ}) · A^* ∪ {ϵ}.
#S #A #w %
[* #l elim l
[* whd in ⊢ ((??%?)→?); #eqw #_ %2 <eqw //
qed.
lemma star_epsilon: ∀S:DeqSet.∀A:word S → Prop.
- A^* ∪ {ϵ} =1 A^*.
+ A^* ∪ {ϵ} ≐ A^*.
#S #A #w % /2/ * //
qed.
lemma epsilon_cat_r: ∀S.∀A:word S →Prop.
- A · {ϵ} =1 A.
+ A · {ϵ} ≐ 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.
+ {ϵ} · A ≐ 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.
+ (A ∪ {ϵ}) · C ≐ A · C ∪ C.
#S #A #C @eqP_trans [|@distr_cat_r |@eqP_union_l @epsilon_cat_l]
qed.
through w are cofinal. *)
theorem equiv_sem: ∀S:DeqSet.∀e1,e2:pre S.
- \sem{e1} =1 \sem{e2} ↔ ∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
+ \sem{e1} ≐ \sem{e2} ↔ ∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
#S #e1 #e2 %
[#same_sem #w
cut (∀b1,b2. iff (b1 = true) (b2 = true) → (b1 = b2))
lemma equiv_sem_occ: ∀S.∀e1,e2:pre S.
(∀w.(sublist S w (occ S e1 e2))→ cofinal ? 〈moves ? w e1,moves ? w e2〉)
-→ \sem{e1}=1\sem{e2}.
+→ \sem{e1}≐\sem{e2}.
#S #e1 #e2 #H @(proj2 … (equiv_sem …)) @occ_enough #w @H
qed.
(* Using lemma equiv_sem_occ it is easy to prove the following result: *)
lemma bisim_to_sem: ∀S:DeqSet.∀l:list ?.∀e1,e2: pre S.
- is_bisim S l (occ S e1 e2) → memb ? 〈e1,e2〉 l = true → \sem{e1}=1\sem{e2}.
+ is_bisim S l (occ S e1 e2) → memb ? 〈e1,e2〉 l = true → \sem{e1}≐\sem{e2}.
#S #l #e1 #e2 #Hbisim #Hmemb @equiv_sem_occ
#w #Hsub @(proj1 … (Hbisim 〈moves S w e1,moves S w e2〉 ?))
lapply Hsub @(list_elim_left … w) [//]
definition disjoint ≝ λS:DeqSet.λl1,l2.
∀p:S. memb S p l1 = true → memb S p l2 = false.
-lemma bisim_correct: ∀S.∀e1,e2:pre S.\sem{e1}=1\sem{e2} →
+lemma bisim_correct: ∀S.∀e1,e2:pre S.\sem{e1}≐\sem{e2} →
∀l,n.∀frontier,visited:list ((pre S)×(pre S)).
|space_enum S (|\fst e1|) (|\fst e2|)| < n + |visited|→
all_reachable S e1 e2 visited →
(bisim ? sig n [〈e1,e2〉] []).
theorem euqiv_sem : ∀Sig.∀e1,e2:re Sig.
- \fst (equiv ? e1 e2) = true ↔ \sem{e1} =1 \sem{e2}.
+ \fst (equiv ? e1 e2) = true ↔ \sem{e1} ≐ \sem{e2}.
#Sig #re1 #re2 %
[#H @eqP_trans [|@eqP_sym @re_embedding] @eqP_trans [||@re_embedding]
cut (equiv ? re1 re2 = 〈true,\snd (equiv ? re1 re2)〉)
definition exp11 ≝ (a·a·a·a·a + a·a·a·a·a·a·a)^*.
example ex2 : \fst (equiv ? (exp10+exp11) exp10) = true.
-normalize // qed.
-
-
-
-
-\v
\ No newline at end of file
+normalize // qed.
\ No newline at end of file
(* Below are a few, simple, semantic properties of items. In particular:
- not_epsilon_item : ∀S:DeqSet.∀i:pitem S. ¬ (\sem{i} ϵ).
- epsilon_pre : ∀S.∀e:pre S. (\sem{i} ϵ) ↔ (\snd e = true).
-- minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}.
-- minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
+- minus_eps_item: ∀S.∀i:pitem S. \sem{i} ≐ \sem{i}-{[ ]}.
+- minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} ≐ \sem{e}-{[ ]}.
The first property is proved by a simple induction on $i$; the other
results are easy corollaries. We need an auxiliary lemma first. *)
#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:pitem S. \sem{i} ≐ \sem{i}-{[ ]}.
#S #i #w %
[#H whd % // normalize @(not_to_not … (not_epsilon_lp …i)) //
|* //
]
qed.
-lemma minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
+lemma minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} ≐ \sem{e}-{[ ]}.
#S * #i *
[>sem_pre_true normalize in ⊢ (??%?); #w %
[/3/ | * * // #H1 #H2 @False_ind @(absurd …H1 H2)]
(* The behaviour of ◃ is summarized by the following, easy lemma: *)
lemma eq_to_ex_eq: ∀S.∀A,B:word S → Prop.
- A = B → A =1 B.
+ A = B → A ≐ 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}.
+ \sem{i ◃ e} ≐ \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.
(* We are now ready to state the main semantic properties of ⊕, ◃ and •(-):
-sem_oplus: \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}
-sem_pcl: \sem{e1 ▹ i2} =1 \sem{e1} · \sem{|i2|} ∪ \sem{i2}
-sem_bullet \sem{•i} =1 \sem{i} ∪ \sem{|i|}
+sem_oplus: \sem{e1 ⊕ e2} ≐ \sem{e1} ∪ \sem{e2}
+sem_pcl: \sem{e1 ▹ i2} ≐ \sem{e1} · \sem{|i2|} ∪ \sem{i2}
+sem_bullet \sem{•i} ≐ \sem{i} ∪ \sem{|i|}
The proof of sem_oplus is straightforward. *)
lemma sem_oplus: ∀S:DeqSet.∀e1,e2:pre S.
- \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}.
+ \sem{e1 ⊕ e2} ≐ \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/
auxiliary lemma, that assumes sem_bullet:
sem_pcl_aux:
- \sem{•i2} =1 \sem{i2} ∪ \sem{|i2|} →
- \sem{e1 ▹ i2} =1 \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
+ \sem{•i2} ≐ \sem{i2} ∪ \sem{|i2|} →
+ \sem{e1 ▹ i2} ≐ \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
Then, using the previous result, we prove sem_bullet by induction
on i. Finally, sem_pcl_aux and sem_bullet give sem_pcl. *)
// qed.
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}.
+ \sem{•i2} ≐ \sem{i2} ∪ \sem{|i2|} →
+ \sem{e1 ▹ i2} ≐ \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 …))
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 - {[ ]}).
+ \sem{e} ≐ \sem{i} ∪ A → \sem{\fst e} ≐ \sem{i} ∪ (A - {[ ]}).
#S #e #i #A #seme
@eqP_trans [|@minus_eps_pre]
@eqP_trans [||@eqP_union_r [|@eqP_sym @minus_eps_item]]
@eqP_substract_r //
qed.
-theorem sem_bull: ∀S:DeqSet. ∀i:pitem S. \sem{•i} =1 \sem{i} ∪ \sem{|i|}.
+theorem sem_bull: ∀S:DeqSet. ∀i:pitem S. \sem{•i} ≐ \sem{i} ∪ \sem{|i|}.
#S #e elim e
[#w normalize % [/2/ | * //]
|/2/
#S #e elim e normalize //
qed.
-lemma sem_blank: ∀S.∀e:re S.\sem{blank S e} =1 ∅.
+lemma sem_blank: ∀S.∀e:re S.\sem{blank S e} ≐ ∅.
#S #e elim e
[1,2:@eq_to_ex_eq //
|#s @eq_to_ex_eq //
qed.
theorem re_embedding: ∀S.∀e:re S.
- \sem{•(blank S e)} =1 \sem{e}.
+ \sem{•(blank S e)} ≐ \sem{e}.
#S #e @eqP_trans [|@sem_bull] >forget_blank
@eqP_trans [|@eqP_union_r [|@sem_blank]]
@eqP_trans [|@union_comm] @union_empty_r.
#S * #i * // qed.
lemma sem_odot_true: ∀S:DeqSet.∀e1:pre S.∀i.
- \sem{e1 ⊙ 〈i,true〉} =1 \sem{e1 ▹ i} ∪ { [ ] }.
+ \sem{e1 ⊙ 〈i,true〉} ≐ \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
of ⊙ and ⊛. *)
lemma sem_odot:
- ∀S.∀e1,e2: pre S. \sem{e1 ⊙ e2} =1 \sem{e1}· \sem{|\fst e2|} ∪ \sem{e2}.
+ ∀S.∀e1,e2: pre S. \sem{e1 ⊙ e2} ≐ \sem{e1}· \sem{|\fst e2|} ∪ \sem{e2}.
#S #e1 * #i2 *
[>sem_pre_true
@eqP_trans [|@sem_odot_true]
qed.
theorem sem_ostar: ∀S.∀e:pre S.
- \sem{e^⊛} =1 \sem{e} · \sem{|\fst e|}^*.
+ \sem{e^⊛} ≐ \sem{e} · \sem{|\fst e|}^*.
#S * #i #b cases b
[(* lhs = \sem{〈i,true〉^⊛} *)
>sem_pre_true (* >sem_pre_true *)
interpretation "reclose" 'eclose x = (reclose ? x).
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}.
+notation "A ≐ B" non associative with precedence 45 for @{'eq_f1 $A $B}.
interpretation "eq f1" 'eq_f1 a b = (eq_f1 ? a b).
(*
-lemma epsilon_or : ∀S:Alpha.∀b1,b2. ϵ(b1 || b2) =1 ϵ b1 ∪ ϵ b2.
+lemma epsilon_or : ∀S:Alpha.∀b1,b2. ϵ(b1 || b2) ≐ ϵ b1 ∪ ϵ b2.
##[##2: napply S]
#S b1 b2; ncases b1; ncases b2; napply extP; #w; nnormalize; @; /2/; *; //; *;
nqed.
#S a b; napply extP; #w; @; *; nnormalize; /2/; nqed.*)
(* theorem 16: 2 *)
-lemma oplus_cup : ∀S:Alpha.∀e1,e2:pre S.\sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}.
+lemma oplus_cup : ∀S:Alpha.∀e1,e2:pre S.\sem{e1 ⊕ e2} ≐ \sem{e1} ∪ \sem{e2}.
#S * #i1 #b1 * #i2 #b2 >lo_def normalize in ⊢ (?%?);
#w cases b1 cases b2 normalize % #w r1; ncases r1; #e1 b1 r2; ncases r2; #e2 b2;
projects / helm.git / commitdiff