2 \ 5h1
\ 6Equivalence
\ 5/h1
\ 6*)
4 include "tutorial/chapter9.ma".
6 (* We say that two pres \langle i_1,b_1\rangle$ and
7 $\langle i_1,b_1\rangle$ are {\em cofinal} if and only if
10 definition cofinal ≝ λS.λp:(
\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"
\ 6pre
\ 5/a
\ 6 S)
\ 5a title="Product" href="cic:/fakeuri.def(1)"
\ 6×
\ 5/a
\ 6(
\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"
\ 6pre
\ 5/a
\ 6 S).
11 \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"
\ 6\snd
\ 5/a
\ 6 (
\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"
\ 6\fst
\ 5/a
\ 6 p)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"
\ 6\snd
\ 5/a
\ 6 (
\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"
\ 6\snd
\ 5/a
\ 6 p).
13 (* As a corollary of decidable_sem, we have that two expressions
14 e1 and e2 are equivalent iff for any word w the states reachable
15 through w are cofinal. *)
17 theorem equiv_sem: ∀S:
\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
\ 6DeqSet
\ 5/a
\ 6.∀e1,e2:
\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"
\ 6pre
\ 5/a
\ 6 S.
18 \ 5a title="in_prl" href="cic:/fakeuri.def(1)"
\ 6\sem
\ 5/a
\ 6{e1}
\ 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{e2}
\ 5a title="iff" href="cic:/fakeuri.def(1)"
\ 6↔
\ 5/a
\ 6 ∀w.
\ 5a href="cic:/matita/tutorial/chapter10/cofinal.def(2)"
\ 6cofinal
\ 5/a
\ 6 ?
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"
\ 6moves
\ 5/a
\ 6 ? w e1,
\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"
\ 6moves
\ 5/a
\ 6 ? w e2〉.
21 cut (∀b1,b2.
\ 5a href="cic:/matita/basics/logic/iff.def(1)"
\ 6iff
\ 5/a
\ 6 (b1
\ 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) (b2
\ 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) → (b1
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 b2))
22 [* * // * #H1 #H2 [@
\ 5a href="cic:/matita/basics/logic/sym_eq.def(2)"
\ 6sym_eq
\ 5/a
\ 6 @H1 //| @H2 //]]
23 #Hcut @Hcut @
\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"
\ 6iff_trans
\ 5/a
\ 6 [|@
\ 5a href="cic:/matita/tutorial/chapter9/decidable_sem.def(15)"
\ 6decidable_sem
\ 5/a
\ 6]
24 @
\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"
\ 6iff_trans
\ 5/a
\ 6 [|@same_sem] @
\ 5a href="cic:/matita/basics/logic/iff_sym.def(2)"
\ 6iff_sym
\ 5/a
\ 6 @
\ 5a href="cic:/matita/tutorial/chapter9/decidable_sem.def(15)"
\ 6decidable_sem
\ 5/a
\ 6
25 |#H #w1 @
\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"
\ 6iff_trans
\ 5/a
\ 6 [||@
\ 5a href="cic:/matita/tutorial/chapter9/decidable_sem.def(15)"
\ 6decidable_sem
\ 5/a
\ 6] <H @
\ 5a href="cic:/matita/basics/logic/iff_sym.def(2)"
\ 6iff_sym
\ 5/a
\ 6 @
\ 5a href="cic:/matita/tutorial/chapter9/decidable_sem.def(15)"
\ 6decidable_sem
\ 5/a
\ 6]
28 (* This does not directly imply decidability: we have no bound over the
29 length of w; moreover, so far, we made no assumption over the cardinality
30 of S. Instead of requiring S to be finite, we may restrict the analysis
31 to characters occurring in the given pres. *)
33 definition occ ≝ λS.λe1,e2:
\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"
\ 6pre
\ 5/a
\ 6 S.
34 \ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"
\ 6unique_append
\ 5/a
\ 6 ? (
\ 5a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"
\ 6occur
\ 5/a
\ 6 S (
\ 5a title="forget" href="cic:/fakeuri.def(1)"
\ 6|
\ 5/a
\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"
\ 6\fst
\ 5/a
\ 6 e1|)) (
\ 5a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"
\ 6occur
\ 5/a
\ 6 S (
\ 5a title="forget" href="cic:/fakeuri.def(1)"
\ 6|
\ 5/a
\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"
\ 6\fst
\ 5/a
\ 6 e2|)).
36 lemma occ_enough: ∀S.∀e1,e2:
\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"
\ 6pre
\ 5/a
\ 6 S.
37 (∀w.(
\ 5a href="cic:/matita/tutorial/chapter5/sublist.def(5)"
\ 6sublist
\ 5/a
\ 6 S w (
\ 5a href="cic:/matita/tutorial/chapter10/occ.def(7)"
\ 6occ
\ 5/a
\ 6 S e1 e2))→
\ 5a href="cic:/matita/tutorial/chapter10/cofinal.def(2)"
\ 6cofinal
\ 5/a
\ 6 ?
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"
\ 6moves
\ 5/a
\ 6 ? w e1,
\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"
\ 6moves
\ 5/a
\ 6 ? w e2〉)
38 →∀w.
\ 5a href="cic:/matita/tutorial/chapter10/cofinal.def(2)"
\ 6cofinal
\ 5/a
\ 6 ?
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"
\ 6moves
\ 5/a
\ 6 ? w e1,
\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"
\ 6moves
\ 5/a
\ 6 ? w e2〉.
40 cases (
\ 5a href="cic:/matita/tutorial/chapter5/decidable_sublist.def(6)"
\ 6decidable_sublist
\ 5/a
\ 6 S w (
\ 5a href="cic:/matita/tutorial/chapter10/occ.def(7)"
\ 6occ
\ 5/a
\ 6 S e1 e2)) [@H] -H #H
41 >
\ 5a href="cic:/matita/tutorial/chapter9/to_pit.def(10)"
\ 6to_pit
\ 5/a
\ 6 [2: @(
\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"
\ 6not_to_not
\ 5/a
\ 6 … H) #H1 #a #memba @
\ 5a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l1.def(6)"
\ 6sublist_unique_append_l1
\ 5/a
\ 6 @H1 //]
42 >
\ 5a href="cic:/matita/tutorial/chapter9/to_pit.def(10)"
\ 6to_pit
\ 5/a
\ 6 [2: @(
\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"
\ 6not_to_not
\ 5/a
\ 6 … H) #H1 #a #memba @
\ 5a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l2.def(6)"
\ 6sublist_unique_append_l2
\ 5/a
\ 6 @H1 //]
46 (* The following is a stronger version of equiv_sem, relative to characters
47 occurring the given regular expressions. *)
49 lemma equiv_sem_occ: ∀S.∀e1,e2:
\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"
\ 6pre
\ 5/a
\ 6 S.
50 (∀w.(
\ 5a href="cic:/matita/tutorial/chapter5/sublist.def(5)"
\ 6sublist
\ 5/a
\ 6 S w (
\ 5a href="cic:/matita/tutorial/chapter10/occ.def(7)"
\ 6occ
\ 5/a
\ 6 S e1 e2))→
\ 5a href="cic:/matita/tutorial/chapter10/cofinal.def(2)"
\ 6cofinal
\ 5/a
\ 6 ?
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"
\ 6moves
\ 5/a
\ 6 ? w e1,
\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"
\ 6moves
\ 5/a
\ 6 ? w e2〉)
51 →
\ 5a title="in_prl" href="cic:/fakeuri.def(1)"
\ 6\sem
\ 5/a
\ 6{e1}
\ 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{e2}.
52 #S #e1 #e2 #H @(
\ 5a href="cic:/matita/basics/logic/proj2.def(2)"
\ 6proj2
\ 5/a
\ 6 … (
\ 5a href="cic:/matita/tutorial/chapter10/equiv_sem.def(16)"
\ 6equiv_sem
\ 5/a
\ 6 …)) @
\ 5a href="cic:/matita/tutorial/chapter10/occ_enough.def(11)"
\ 6occ_enough
\ 5/a
\ 6 #w @H
56 \ 5h2
\ 6Bisimulations
\ 5/h2
\ 6
58 We say that a list of pairs of pres is a bisimulation if it is closed
59 w.r.t. moves, and all its members are cofinal.
62 definition sons ≝ λS:
\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
\ 6DeqSet
\ 5/a
\ 6.λl:
\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 S.λp:(
\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"
\ 6pre
\ 5/a
\ 6 S)
\ 5a title="Product" href="cic:/fakeuri.def(1)"
\ 6×
\ 5/a
\ 6(
\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"
\ 6pre
\ 5/a
\ 6 S).
63 \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"
\ 6map
\ 5/a
\ 6 ?? (λa.
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"
\ 6move
\ 5/a
\ 6 S a (
\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"
\ 6\fst
\ 5/a
\ 6 (
\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"
\ 6\fst
\ 5/a
\ 6 p)),
\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"
\ 6move
\ 5/a
\ 6 S a (
\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"
\ 6\fst
\ 5/a
\ 6 (
\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"
\ 6\snd
\ 5/a
\ 6 p))〉) l.
65 lemma memb_sons: ∀S,l.∀p,q:(
\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"
\ 6pre
\ 5/a
\ 6 S)
\ 5a title="Product" href="cic:/fakeuri.def(1)"
\ 6×
\ 5/a
\ 6(
\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"
\ 6pre
\ 5/a
\ 6 S).
\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"
\ 6memb
\ 5/a
\ 6 ? p (
\ 5a href="cic:/matita/tutorial/chapter10/sons.def(7)"
\ 6sons
\ 5/a
\ 6 ? l q)
\ 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 →
66 \ 5a title="exists" href="cic:/fakeuri.def(1)"
\ 6∃
\ 5/a
\ 6a.(
\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"
\ 6move
\ 5/a
\ 6 ? a (
\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"
\ 6\fst
\ 5/a
\ 6 (
\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"
\ 6\fst
\ 5/a
\ 6 q))
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"
\ 6\fst
\ 5/a
\ 6 p
\ 5a title="logical and" href="cic:/fakeuri.def(1)"
\ 6∧
\ 5/a
\ 6
67 \ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"
\ 6move
\ 5/a
\ 6 ? a (
\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"
\ 6\fst
\ 5/a
\ 6 (
\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"
\ 6\snd
\ 5/a
\ 6 q))
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"
\ 6\snd
\ 5/a
\ 6 p).
68 #S #l elim l [#p #q normalize in ⊢ (%→?); #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/]
69 #a #tl #Hind #p #q #H cases (
\ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"
\ 6orb_true_l
\ 5/a
\ 6 … H) -H
70 [#H @(
\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"
\ 6ex_intro
\ 5/a
\ 6 … a) >(\P H) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"
\ 6conj
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ |#H @Hind @H]
73 definition is_bisim ≝ λS:
\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
\ 6DeqSet
\ 5/a
\ 6.λl:
\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 ?.λalpha:
\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 S.
74 ∀p:(
\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"
\ 6pre
\ 5/a
\ 6 S)
\ 5a title="Product" href="cic:/fakeuri.def(1)"
\ 6×
\ 5/a
\ 6(
\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"
\ 6pre
\ 5/a
\ 6 S).
\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"
\ 6memb
\ 5/a
\ 6 ? p l
\ 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 href="cic:/matita/tutorial/chapter10/cofinal.def(2)"
\ 6cofinal
\ 5/a
\ 6 ? p
\ 5a title="logical and" href="cic:/fakeuri.def(1)"
\ 6∧
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter5/sublist.def(5)"
\ 6sublist
\ 5/a
\ 6 ? (
\ 5a href="cic:/matita/tutorial/chapter10/sons.def(7)"
\ 6sons
\ 5/a
\ 6 ? alpha p) l).
76 (* Using lemma equiv_sem_occ it is easy to prove the following result: *)
78 lemma bisim_to_sem: ∀S:
\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"
\ 6DeqSet
\ 5/a
\ 6.∀l:
\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 ?.∀e1,e2:
\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"
\ 6pre
\ 5/a
\ 6 S.
79 \ 5a href="cic:/matita/tutorial/chapter10/is_bisim.def(8)"
\ 6is_bisim
\ 5/a
\ 6 S l (
\ 5a href="cic:/matita/tutorial/chapter10/occ.def(7)"
\ 6occ
\ 5/a
\ 6 S e1 e2) →
\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"
\ 6memb
\ 5/a
\ 6 ?
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6e1,e2〉 l
\ 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="in_prl" href="cic:/fakeuri.def(1)"
\ 6\sem
\ 5/a
\ 6{e1}
\ 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{e2}.
80 #S #l #e1 #e2 #Hbisim #Hmemb @
\ 5a href="cic:/matita/tutorial/chapter10/equiv_sem_occ.def(17)"
\ 6equiv_sem_occ
\ 5/a
\ 6
81 #w #Hsub @(
\ 5a href="cic:/matita/basics/logic/proj1.def(2)"
\ 6proj1
\ 5/a
\ 6 … (Hbisim
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"
\ 6moves
\ 5/a
\ 6 S w e1,
\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"
\ 6moves
\ 5/a
\ 6 S w e2〉 ?))
82 lapply Hsub @(list_elim_left … w) [//]
83 #a #w1 #Hind #Hsub >moves_left >moves_left @(proj2 …(Hbisim …(Hind ?)))
84 [#x #Hx @Hsub @memb_append_l1 //
85 |cut (memb S a (occ S e1 e2) = true) [@Hsub @memb_append_l2 //] #occa
90 (* This is already an interesting result: checking if l is a bisimulation
91 is decidable, hence we could generate l with some untrusted piece of code
92 and then run a (boolean version of) is_bisim to check that it is actually
94 However, in order to prove that equivalence of regular expressions
95 is decidable we must prove that we can always effectively build such a list
96 (or find a counterexample).
97 The idea is that the list we are interested in is just the set of
98 all pair of pres reachable from the initial pair via some
101 The algorithm for computing reachable nodes in graph is a very
102 traditional one. We split nodes in two disjoint lists: a list of
103 visited nodes and a frontier, composed by all nodes connected
104 to a node in visited but not visited already. At each step we select a node
105 a from the frontier, compute its sons, add a to the set of
106 visited nodes and the (not already visited) sons to the frontier.
108 Instead of fist computing reachable nodes and then performing the
109 bisimilarity test we can directly integrate it in the algorithm:
110 the set of visited nodes is closed by construction w.r.t. reachability,
111 so we have just to check cofinality for any node we add to visited.
113 Here is the extremely simple algorithm: *)
115 let rec bisim S l n (frontier,visited: list ?) on n ≝
117 [ O ⇒ 〈false,visited〉 (* assert false *)
120 [ nil ⇒ 〈true,visited〉
122 if beqb (\snd (\fst hd)) (\snd (\snd hd)) then
123 bisim S l m (unique_append ? (filter ? (λx.notb (memb ? x (hd::visited)))
124 (sons S l hd)) tl) (hd::visited)
129 (* The integer n is an upper bound to the number of recursive call,
130 equal to the dimension of the graph. It returns a pair composed
131 by a boolean and a the set of visited nodes; the boolean is true
132 if and only if all visited nodes are cofinal.
134 The following results explicitly state the behaviour of bisim is the general
135 case and in some relevant instances *)
137 lemma unfold_bisim: ∀S,l,n.∀frontier,visited: list ?.
138 bisim S l n frontier visited =
140 [ O ⇒ 〈false,visited〉 (* assert false *)
143 [ nil ⇒ 〈true,visited〉
145 if beqb (\snd (\fst hd)) (\snd (\snd hd)) then
146 bisim S l m (unique_append ? (filter ? (λx.notb(memb ? x (hd::visited)))
147 (sons S l hd)) tl) (hd::visited)
151 #S #l #n cases n // qed.
153 lemma bisim_never: ∀S,l.∀frontier,visited: list ?.
154 bisim S l O frontier visited = 〈false,visited〉.
155 #frontier #visited >unfold_bisim //
158 lemma bisim_end: ∀Sig,l,m.∀visited: list ?.
159 bisim Sig l (S m) [] visited = 〈true,visited〉.
160 #n #visisted >unfold_bisim //
163 lemma bisim_step_true: ∀Sig,l,m.∀p.∀frontier,visited: list ?.
164 beqb (\snd (\fst p)) (\snd (\snd p)) = true →
165 bisim Sig l (S m) (p::frontier) visited =
166 bisim Sig l m (unique_append ? (filter ? (λx.notb(memb ? x (p::visited)))
167 (sons Sig l p)) frontier) (p::visited).
168 #Sig #l #m #p #frontier #visited #test >unfold_bisim normalize nodelta >test //
171 lemma bisim_step_false: ∀Sig,l,m.∀p.∀frontier,visited: list ?.
172 beqb (\snd (\fst p)) (\snd (\snd p)) = false →
173 bisim Sig l (S m) (p::frontier) visited = 〈false,visited〉.
174 #Sig #l #m #p #frontier #visited #test >unfold_bisim normalize nodelta >test //
177 (* In order to prove termination of bisim we must be able to effectively
178 enumerate all possible pres: *)
180 (* lemma notb_eq_true_l: ∀b. notb b = true → b = false.
181 #b cases b normalize //
184 let rec pitem_enum S (i:re S) on i ≝
188 | s y ⇒ [ps S y; pp S y]
189 | o i1 i2 ⇒ compose ??? (po S) (pitem_enum S i1) (pitem_enum S i2)
190 | c i1 i2 ⇒ compose ??? (pc S) (pitem_enum S i1) (pitem_enum S i2)
191 | k i ⇒ map ?? (pk S) (pitem_enum S i)
194 lemma pitem_enum_complete : ∀S.∀i:pitem S.
195 memb (DeqItem S) i (pitem_enum S (|i|)) = true.
198 |3,4:#c normalize >(\b (refl … c)) //
199 |5,6:#i1 #i2 #Hind1 #Hind2 @(memb_compose (DeqItem S) (DeqItem S)) //
200 |#i #Hind @(memb_map (DeqItem S)) //
204 definition pre_enum ≝ λS.λi:re S.
205 compose ??? (λi,b.〈i,b〉) (pitem_enum S i) [true;false].
207 lemma pre_enum_complete : ∀S.∀e:pre S.
208 memb ? e (pre_enum S (|\fst e|)) = true.
209 #S * #i #b @(memb_compose (DeqItem S) DeqBool ? (λi,b.〈i,b〉))
210 // cases b normalize //
213 definition space_enum ≝ λS.λi1,i2:re S.
214 compose ??? (λe1,e2.〈e1,e2〉) (pre_enum S i1) (pre_enum S i2).
216 lemma space_enum_complete : ∀S.∀e1,e2: pre S.
217 memb ? 〈e1,e2〉 (space_enum S (|\fst e1|) (|\fst e2|)) = true.
218 #S #e1 #e2 @(memb_compose … (λi,b.〈i,b〉))
221 definition all_reachable ≝ λS.λe1,e2:pre S.λl: list ?.
223 ∀p. memb ? p l = true →
224 ∃w.(moves S w e1 = \fst p) ∧ (moves S w e2 = \snd p).
226 definition disjoint ≝ λS:DeqSet.λl1,l2.
227 ∀p:S. memb S p l1 = true → memb S p l2 = false.
229 (* We are ready to prove that bisim is correct; we use the invariant
230 that at each call of bisim the two lists visited and frontier only contain
231 nodes reachable from \langle e_1,e_2\rangle, hence it is absurd to suppose
232 to meet a pair which is not cofinal. *)
234 lemma bisim_correct: ∀S.∀e1,e2:pre S.\sem{e1}=1\sem{e2} →
235 ∀l,n.∀frontier,visited:list ((pre S)×(pre S)).
236 |space_enum S (|\fst e1|) (|\fst e2|)| < n + |visited|→
237 all_reachable S e1 e2 visited →
238 all_reachable S e1 e2 frontier →
239 disjoint ? frontier visited →
240 \fst (bisim S l n frontier visited) = true.
241 #Sig #e1 #e2 #same #l #n elim n
242 [#frontier #visited #abs * #unique #H @False_ind @(absurd … abs)
243 @le_to_not_lt @sublist_length // * #e11 #e21 #membp
244 cut ((|\fst e11| = |\fst e1|) ∧ (|\fst e21| = |\fst e2|))
245 [|* #H1 #H2 <H1 <H2 @space_enum_complete]
246 cases (H … membp) #w * #we1 #we2 <we1 <we2 % >same_kernel_moves //
247 |#m #HI * [#visited #vinv #finv >bisim_end //]
248 #p #front_tl #visited #Hn * #u_visited #r_visited * #u_frontier #r_frontier
250 cut (∃w.(moves ? w e1 = \fst p) ∧ (moves ? w e2 = \snd p))
251 [@(r_frontier … (memb_hd … ))] #rp
252 cut (beqb (\snd (\fst p)) (\snd (\snd p)) = true)
253 [cases rp #w * #fstp #sndp <fstp <sndp @(\b ?)
254 @(proj1 … (equiv_sem … )) @same] #ptest
255 >(bisim_step_true … ptest) @HI -HI
257 |% [whd in ⊢ (??%?); >(disjoint … (memb_hd …)) whd in ⊢ (??%?); //
258 |#p1 #H (cases (orb_true_l … H)) [#eqp >(\P eqp) // |@r_visited]
260 |whd % [@unique_append_unique @(andb_true_r … u_frontier)]
261 @unique_append_elim #q #H
262 [cases (memb_sons … (memb_filter_memb … H)) -H
263 #a * #m1 #m2 cases rp #w1 * #mw1 #mw2 @(ex_intro … (w1@[a]))
264 >moves_left >moves_left >mw1 >mw2 >m1 >m2 % //
265 |@r_frontier @memb_cons //
267 |@unique_append_elim #q #H
268 [@injective_notb @(filter_true … H)
269 |cut ((q==p) = false)
270 [|#Hpq whd in ⊢ (??%?); >Hpq @disjoint @memb_cons //]
271 cases (andb_true … u_frontier) #notp #_ @(\bf ?)
272 @(not_to_not … not_eq_true_false) #eqqp <notp <eqqp >H //
278 (* For completeness, we use the invariant that all the nodes in visited are cofinal,
279 and the sons of visited are either in visited or in the frontier; since
280 at the end frontier is empty, visited is hence a bisimulation. *)
282 definition all_true ≝ λS.λl.∀p:(pre S) × (pre S). memb ? p l = true →
283 (beqb (\snd (\fst p)) (\snd (\snd p)) = true).
285 definition sub_sons ≝ λS,l,l1,l2.∀x:(pre S) × (pre S).
286 memb ? x l1 = true → sublist ? (sons ? l x) l2.
288 lemma bisim_complete:
289 ∀S,l,n.∀frontier,visited,visited_res:list ?.
291 sub_sons S l visited (frontier@visited) →
292 bisim S l n frontier visited = 〈true,visited_res〉 →
293 is_bisim S visited_res l ∧ sublist ? (frontier@visited) visited_res.
295 [#fron #vis #vis_res #_ #_ >bisim_never #H destruct
297 [(* case empty frontier *)
298 -Hind #vis #vis_res #allv #H normalize in ⊢ (%→?);
300 [#membp % [@(\P ?) @allv //| @H //]|#H1 @H1]
301 |#hd cases (true_or_false (beqb (\snd (\fst hd)) (\snd (\snd hd))))
302 [|(* case head of the frontier is non ok (absurd) *)
303 #H #tl #vis #vis_res #allv >(bisim_step_false … H) #_ #H1 destruct]
304 (* frontier = hd:: tl and hd is ok *)
305 #H #tl #visited #visited_res #allv >(bisim_step_true … H)
306 (* new_visited = hd::visited are all ok *)
307 cut (all_true S (hd::visited))
308 [#p #H1 cases (orb_true_l … H1) [#eqp >(\P eqp) @H |@allv]]
309 (* we now exploit the induction hypothesis *)
310 #allh #subH #bisim cases (Hind … allh … bisim) -bisim -Hind
311 [#H1 #H2 % // #p #membp @H2 -H2 cases (memb_append … membp) -membp #membp
312 [cases (orb_true_l … membp) -membp #membp
313 [@memb_append_l2 >(\P membp) @memb_hd
314 |@memb_append_l1 @sublist_unique_append_l2 //
316 |@memb_append_l2 @memb_cons //
318 |(* the only thing left to prove is the sub_sons invariant *)
319 #x #membx cases (orb_true_l … membx)
321 #eqhdx <(\P eqhdx) #xa #membxa
322 (* xa is a son of x; we must distinguish the case xa
323 was already visited form the case xa is new *)
324 cases (true_or_false … (memb ? xa (x::visited)))
325 [(* xa visited - trivial *) #membxa @memb_append_l2 //
326 |(* xa new *) #membxa @memb_append_l1 @sublist_unique_append_l1 @memb_filter_l
329 |(* case x in visited *)
330 #H1 #xa #membxa cases (memb_append … (subH x … H1 … membxa))
331 [#H2 (cases (orb_true_l … H2))
332 [#H3 @memb_append_l2 <(\P H3) @memb_hd
333 |#H3 @memb_append_l1 @sublist_unique_append_l2 @H3
335 |#H2 @memb_append_l2 @memb_cons @H2
342 (* We can now give the definition of the equivalence algorithm, and
343 prove that two expressions are equivalente if and only if they define
344 the same language. *)
346 definition equiv ≝ λSig.λre1,re2:re Sig.
347 let e1 ≝ •(blank ? re1) in
348 let e2 ≝ •(blank ? re2) in
349 let n ≝ S (length ? (space_enum Sig (|\fst e1|) (|\fst e2|))) in
350 let sig ≝ (occ Sig e1 e2) in
351 (bisim ? sig n [〈e1,e2〉] []).
353 theorem euqiv_sem : ∀Sig.∀e1,e2:re Sig.
354 \fst (equiv ? e1 e2) = true ↔ \sem{e1} =1 \sem{e2}.
356 [#H @eqP_trans [|@eqP_sym @re_embedding] @eqP_trans [||@re_embedding]
357 cut (equiv ? re1 re2 = 〈true,\snd (equiv ? re1 re2)〉)
359 cases (bisim_complete … Hcut)
360 [2,3: #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/]
361 #Hbisim #Hsub @(bisim_to_sem … Hbisim)
363 |#H @(bisim_correct ? (•(blank ? re1)) (•(blank ? re2)))
364 [@eqP_trans [|@re_embedding] @eqP_trans [|@H] @eqP_sym @re_embedding
366 |% // #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/
367 |% // #p #H >(memb_single … H) @(ex_intro … ϵ) /2/
373 lemma eqbnat_true : ∀n,m. eqbnat n m = true ↔ n = m.
374 #n #m % [@eqbnat_true_to_eq | @eq_to_eqbnat_true]
377 definition DeqNat ≝ mk_DeqSet nat eqbnat eqbnat_true.
379 definition a ≝ s DeqNat O.
380 definition b ≝ s DeqNat (S O).
381 definition c ≝ s DeqNat (S (S O)).
383 definition exp1 ≝ ((a·b)^*·a).
384 definition exp2 ≝ a·(b·a)^*.
385 definition exp4 ≝ (b·a)^*.
387 definition exp6 ≝ a·(a ·a ·b^* + b^* ).
388 definition exp7 ≝ a · a^* · b^*.
390 definition exp8 ≝ a·a·a·a·a·a·a·a·(a^* ).
391 definition exp9 ≝ (a·a·a + a·a·a·a·a)^*.
393 example ex1 : \fst (equiv ? (exp8+exp9) exp9) = true.