weblib/tutorial/chapter10.ma

   1 (*
   2 \ 5h1\ 6Equivalence\ 5/h1\ 6*)
   3
   4 include "tutorial/chapter9.ma".
   5
   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
   8 $b_1 = b_2$. *)
   9
  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).
  12
  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. *)
  16
  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〉.
  19 #S #e1 #e2 %
  20 [#same_sem #w
  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]
  26 qed.
  27
  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. *)
  32
  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|)).
  35
  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〉.
  39 #S #e1 #e2 #H #w
  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 //]
  43  //
  44 qed.
  45
  46 (* The following is a stronger version of equiv_sem, relative to characters
  47 occurring the given regular expressions. *)
  48
  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
  53 qed.
  54
  55 (*
  56 \ 5h2\ 6Bisimulations\ 5/h2\ 6
  57
  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.
  60 *)
  61
  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.
  64
  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]
  71 qed.
  72
  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).
  75
  76 (* Using lemma equiv_sem_occ it is easy to prove the following result: *)
  77
  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
  86    @(memb_map … occa)
  87   ]
  88 qed.
  89
  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
  93 a bisimulation.
  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
  99 sequence of moves.
 100
 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.
 107
 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.
 112
 113 Here is the extremely simple algorithm: *)
 114
 115 let rec bisim S l n (frontier,visited: list ?) on n ≝
 116   match n with
 117   [ O ⇒ 〈false,visited〉 (* assert false *)
 118   | S m ⇒
 119     match frontier with
 120     [ nil ⇒ 〈true,visited〉
 121     | cons hd tl ⇒
 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)
 125       else 〈false,visited〉
 126     ]
 127   ].
 128
 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.
 133
 134 The following results explicitly state the behaviour of bisim is the general
 135 case and in some relevant instances *)
 136
 137 lemma unfold_bisim: ∀S,l,n.∀frontier,visited: list ?.
 138   bisim S l n frontier visited =
 139   match n with
 140   [ O ⇒ 〈false,visited〉 (* assert false *)
 141   | S m ⇒
 142     match frontier with
 143     [ nil ⇒ 〈true,visited〉
 144     | cons hd tl ⇒
 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)
 148       else 〈false,visited〉
 149     ]
 150   ].
 151 #S #l #n cases n // qed.
 152
 153 lemma bisim_never: ∀S,l.∀frontier,visited: list ?.
 154   bisim S l O frontier visited = 〈false,visited〉.
 155 #frontier #visited >unfold_bisim //
 156 qed.
 157
 158 lemma bisim_end: ∀Sig,l,m.∀visited: list ?.
 159   bisim Sig l (S m) [] visited = 〈true,visited〉.
 160 #n #visisted >unfold_bisim //
 161 qed.
 162
 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 //
 169 qed.
 170
 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 //
 175 qed.
 176
 177 (* In order to prove termination of bisim we must be able to effectively
 178 enumerate all possible pres: *)
 179
 180 (* lemma notb_eq_true_l: ∀b. notb b = true → b = false.
 181 #b cases b normalize //
 182 qed. *)
 183
 184 let rec pitem_enum S (i:re S) on i ≝
 185   match i with
 186   [ z ⇒ [pz S]
 187   | e ⇒ [pe S]
 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)
 192   ].
 193
 194 lemma pitem_enum_complete : ∀S.∀i:pitem S.
 195   memb (DeqItem S) i (pitem_enum S (|i|)) = true.
 196 #S #i elim i
 197   [1,2://
 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)) //
 201   ]
 202 qed.
 203
 204 definition pre_enum ≝ λS.λi:re S.
 205   compose ??? (λi,b.〈i,b〉) (pitem_enum S i) [true;false].
 206
 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 //
 211 qed.
 212
 213 definition space_enum ≝ λS.λi1,i2:re S.
 214   compose ??? (λe1,e2.〈e1,e2〉) (pre_enum S i1) (pre_enum S i2).
 215
 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〉))
 219 // qed.
 220
 221 definition all_reachable ≝ λS.λe1,e2:pre S.λl: list ?.
 222 uniqueb ? l = true ∧
 223   ∀p. memb ? p l = true →
 224     ∃w.(moves S w e1 = \fst p) ∧ (moves S w e2 = \snd p).
 225
 226 definition disjoint ≝ λS:DeqSet.λl1,l2.
 227   ∀p:S. memb S p l1 = true →  memb S p l2 = false.
 228
 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. *)
 233
 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
 249    #disjoint
 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
 256      [<plus_n_Sm //
 257      |% [whd in ⊢ (??%?); >(disjoint … (memb_hd …)) whd in ⊢ (??%?); //
 258         |#p1 #H (cases (orb_true_l … H)) [#eqp >(\P eqp) // |@r_visited]
 259         ]
 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 //
 266        ]
 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 //
 273        ]
 274      ]
 275    ]
 276 qed.
 277
 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. *)
 281
 282 definition all_true ≝ λS.λl.∀p:(pre S) × (pre S). memb ? p l = true →
 283   (beqb (\snd (\fst p)) (\snd (\snd p)) = true).
 284
 285 definition sub_sons ≝ λS,l,l1,l2.∀x:(pre S) × (pre S).
 286 memb ? x l1 = true → sublist ? (sons ? l x) l2.
 287
 288 lemma bisim_complete:
 289  ∀S,l,n.∀frontier,visited,visited_res:list ?.
 290  all_true S visited →
 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.
 294 #S #l #n elim n
 295   [#fron #vis #vis_res #_ #_ >bisim_never #H destruct
 296   |#m #Hind *
 297     [(* case empty frontier *)
 298      -Hind #vis #vis_res #allv #H normalize in  ⊢ (%→?);
 299      #H1 destruct % #p
 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 //
 315           ]
 316         |@memb_append_l2 @memb_cons //
 317         ]
 318       |(* the only thing left to prove is the sub_sons invariant *)
 319      #x #membx cases (orb_true_l … membx)
 320       [(* case x = hd *)
 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
 327           [>membxa //|//]
 328         ]
 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
 334           ]
 335         |#H2 @memb_append_l2 @memb_cons @H2
 336         ]
 337       ]
 338     ]
 339   ]
 340 qed.
 341
 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. *)
 345
 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〉] []).
 352
 353 theorem euqiv_sem : ∀Sig.∀e1,e2:re Sig.
 354    \fst (equiv ? e1 e2) = true ↔ \sem{e1} =1 \sem{e2}.
 355 #Sig #re1 #re2 %
 356   [#H @eqP_trans [|@eqP_sym @re_embedding] @eqP_trans [||@re_embedding]
 357    cut (equiv ? re1 re2 = 〈true,\snd (equiv ? re1 re2)〉)
 358      [<H //] #Hcut
 359    cases (bisim_complete … Hcut)
 360      [2,3: #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/]
 361    #Hbisim #Hsub @(bisim_to_sem … Hbisim)
 362    @Hsub @memb_hd
 363   |#H @(bisim_correct ? (•(blank ? re1)) (•(blank ? re2)))
 364     [@eqP_trans [|@re_embedding] @eqP_trans [|@H] @eqP_sym @re_embedding
 365     |//
 366     |% // #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/
 367     |% // #p #H >(memb_single … H) @(ex_intro … ϵ) /2/
 368     |#p #_ normalize //
 369     ]
 370   ]
 371 qed.
 372
 373 lemma eqbnat_true : ∀n,m. eqbnat n m = true ↔ n = m.
 374 #n #m % [@eqbnat_true_to_eq | @eq_to_eqbnat_true]
 375 qed.
 376
 377 definition DeqNat ≝ mk_DeqSet nat eqbnat eqbnat_true.
 378
 379 definition a ≝ s DeqNat O.
 380 definition b ≝ s DeqNat (S O).
 381 definition c ≝ s DeqNat (S (S O)).
 382
 383 definition exp1 ≝ ((a·b)^*·a).
 384 definition exp2 ≝ a·(b·a)^*.
 385 definition exp4 ≝ (b·a)^*.
 386
 387 definition exp6 ≝ a·(a ·a ·b^* + b^* ).
 388 definition exp7 ≝ a · a^* · b^*.
 389
 390 definition exp8 ≝ a·a·a·a·a·a·a·a·(a^* ).
 391 definition exp9 ≝ (a·a·a + a·a·a·a·a)^*.
 392
 393 example ex1 : \fst (equiv ? (exp8+exp9) exp9) = true.
 394 normalize // qed.
 395
 396
 397
 398
 399