let rec move (S: DeqSet) (x:S) (E: pitem S) on E : pre S ≝
match E with
- [ pz ⇒ 〈 `∅, false 〉
- | pe ⇒ 〈 ϵ, false 〉
- | ps y ⇒ 〈 `y, false 〉
- | pp y ⇒ 〈 `y, x == y 〉
+ [ pz ⇒ 〈 pz ?, false 〉
+ | pe ⇒ 〈 pe ? , false 〉
+ | ps y ⇒ 〈 ps ? y, false 〉
+ | pp y ⇒ 〈 ps ? y, x == y 〉
| po e1 e2 ⇒ (move ? x e1) ⊕ (move ? x e2)
| pc e1 e2 ⇒ (move ? x e1) ⊙ (move ? x e2)
| pk e ⇒ (move ? x e)^⊛ ].
(* rhs = a::w1∈\sem{i1}\sem{|i2|} ∨ a::w∈\sem{i2} *)
@iff_trans[||@(iff_or_l … (HI2 w))]
(* rhs = a::w1∈\sem{i1}\sem{|i2|} ∨ w∈\sem{move S a i2} *)
- @iff_or_r
- check deriv_middot
+ @iff_or_r
(* we are left to prove that
w∈\sem{move S a i1}·\sem{|i2|} ↔ a::w∈\sem{i1}\sem{|i2|}
we use deriv_middot on the rhs *)
]
qed.
-notation > "x ↦* E" non associative with precedence 60 for @{moves ? $x $E}.
+notation > "x ↦* E" non associative with precedence 65 for @{moves ? $x $E}.
let rec moves (S : DeqSet) w e on w : pre S ≝
match w with
[ nil ⇒ e
#S #w elim w
[* #i #b >moves_empty cases b % /2/
|#a #w1 #Hind #e >moves_cons
- check not_epsilon_sem
@iff_trans [||@iff_sym @not_epsilon_sem]
@iff_trans [||@move_ok] @Hind
]
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 exp10 ≝ a·a·a·a·a·a·a·a·a·a·a·a·(a^* ).
definition exp11 ≝ (a·a·a·a·a + a·a·a·a·a·a·a)^*.
-example ex2 : \fst (equiv ? (exp10+exp11) exp10) = true.
+example ex2 : \fst (equiv ? (exp10+exp11) exp11) = false.
normalize // qed.
+definition exp12 ≝
+ (a·a·a·a·a·a·a·a)·(a·a·a·a·a·a·a·a)·(a·a·a·a·a·a·a·a)·(a^* ).
+
+example ex3 : \fst (equiv ? (exp12+exp11) exp11) = true.
+normalize // qed.
+let rec raw (n:nat) ≝
+ match n with
+ [ O ⇒ a
+ | S p ⇒ a · (raw p)
+ ].
+
+let rec alln (n:nat) ≝
+ match n with
+ [O ⇒ ϵ
+ |S m ⇒ raw m + alln m
+ ].
+definition testA ≝ λx,y,z,b.
+ let e1 ≝ raw x in
+ let e2 ≝ raw y in
+ let e3 ≝ (raw z) · a^* in
+ let e4 ≝ (e1 + e2)^* in
+ \fst (equiv ? (e3+e4) e4) = b.
+
+example ex4 : testA 2 4 7 true.
+normalize // qed.
+
+example ex5 : testA 3 4 10 false.
+normalize // qed.
+
+example ex6 : testA 3 4 11 true.
+normalize // qed.
+
+example ex7 : testA 4 5 18 false.
+normalize // qed.
+
+example ex8 : testA 4 5 19 true.
+normalize // qed.
+
+example ex9 : testA 4 6 22 false.
+normalize // qed.
-\v
\ No newline at end of file
+example ex10 : testA 4 6 23 true.
+normalize // qed.
+
+definition testB ≝ λn,b.
+ \fst (equiv ? ((alln n)·((raw n)^* )) a^* ) = b.
+
+example ex11 : testB 6 true.
+normalize // qed.
+
+example ex12 : testB 8 true.
+normalize // qed.
+
+example ex13 : testB 10 true.
+normalize // qed.
+
+example ex14 : testB 12 true.
+normalize // qed.
+
+example ex15 : testB 14 true.
+normalize // qed.
+
+example ex16 : testB 16 true.
+normalize // qed.
+
+example ex17 : testB 18 true.
+normalize // qed.