-definition all_reachable ≝ λS.λe1,e2: pre S.λl: list ?.
-uniqueb ? l = true ∧
- ∀p. memb ? p l = true →
- ∃w.(moves S w e1 = \fst p) ∧ (moves S w e2 = \snd p).
-
-definition disjoint ≝ λS:DeqSet.λl1,l2.
- ∀p:S. memb S p l1 = true → memb S p l2 = false.
-
-(* We are ready to prove that bisim is correct; we use the invariant
-that at each call of bisim the two lists visited and frontier only contain
-nodes reachable from 〈e_1,e_2〉, hence it is absurd to suppose to meet a pair
-which is not cofinal. *)
-
-lemma bisim_correct: ∀S.∀e1,e2:pre S.\sem{e1}=1\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 →
- all_reachable S e1 e2 frontier →
- disjoint ? frontier visited →
- \fst (bisim S l n frontier visited) = true.
-#Sig #e1 #e2 #same #l #n elim n
- [#frontier #visited #abs * #unique #H @False_ind @(absurd … abs)
- @le_to_not_lt @sublist_length // * #e11 #e21 #membp
- cut ((|\fst e11| = |\fst e1|) ∧ (|\fst e21| = |\fst e2|))
- [|* #H1 #H2 <H1 <H2 @space_enum_complete]
- cases (H … membp) #w * #we1 #we2 <we1 <we2 % >same_kernel_moves //
- |#m #HI * [#visited #vinv #finv >bisim_end //]
- #p #front_tl #visited #Hn * #u_visited #r_visited * #u_frontier #r_frontier
- #disjoint
- cut (∃w.(moves ? w e1 = \fst p) ∧ (moves ? w e2 = \snd p))
- [@(r_frontier … (memb_hd … ))] #rp
- cut (beqb (\snd (\fst p)) (\snd (\snd p)) = true)
- [cases rp #w * #fstp #sndp <fstp <sndp @(\b ?)
- @(proj1 … (equiv_sem … )) @same] #ptest
- >(bisim_step_true … ptest) @HI -HI
- [<plus_n_Sm //
- |% [whd in ⊢ (??%?); >(disjoint … (memb_hd …)) whd in ⊢ (??%?); //
- |#p1 #H (cases (orb_true_l … H)) [#eqp >(\P eqp) // |@r_visited]
- ]
- |whd % [@unique_append_unique @(andb_true_r … u_frontier)]
- @unique_append_elim #q #H
- [cases (memb_sons … (memb_filter_memb … H)) -H
- #a * #m1 #m2 cases rp #w1 * #mw1 #mw2 @(ex_intro … (w1@(a::[])))
- >moves_left >moves_left >mw1 >mw2 >m1 >m2 % //
- |@r_frontier @memb_cons //
- ]
- |@unique_append_elim #q #H
- [@injective_notb @(memb_filter_true … H)
- |cut ((q==p) = false)
- [|#Hpq whd in ⊢ (??%?); >Hpq @disjoint @memb_cons //]
- cases (andb_true … u_frontier) #notp #_ @(\bf ?)
- @(not_to_not … not_eq_true_false) #eqqp <notp <eqqp >H //
- ]
- ]
- ]
-qed.
-
-(* For completeness, we use the invariant that all the nodes in visited are cofinal,
-and the sons of visited are either in visited or in the frontier; since
-at the end frontier is empty, visited is hence a bisimulation. *)
-
-definition all_true ≝ λS.λl.∀p:(pre S) × (pre S). memb ? p l = true →
- (beqb (\snd (\fst p)) (\snd (\snd p)) = true).
-
-definition sub_sons ≝ λS,l,l1,l2.∀x:(pre S) × (pre S).
-memb ? x l1 = true → sublist ? (sons ? l x) l2.
-
-lemma bisim_complete:
- ∀S,l,n.∀frontier,visited,visited_res:list ?.
- all_true S visited →
- sub_sons S l visited (frontier@visited) →
- bisim S l n frontier visited = 〈true,visited_res〉 →
- is_bisim S visited_res l ∧ sublist ? (frontier@visited) visited_res.
-#S #l #n elim n
- [#fron #vis #vis_res #_ #_ >bisim_never #H destruct
- |#m #Hind *
- [(* case empty frontier *)
- -Hind #vis #vis_res #allv #H normalize in ⊢ (%→?);
- #H1 destruct % #p
- [#membp % [@(\P ?) @allv //| @H //]|#H1 @H1]
- |#hd cases (true_or_false (beqb (\snd (\fst hd)) (\snd (\snd hd))))
- [|(* case head of the frontier is non ok (absurd) *)
- #H #tl #vis #vis_res #allv >(bisim_step_false … H) #_ #H1 destruct]
- (* frontier = hd:: tl and hd is ok *)
- #H #tl #visited #visited_res #allv >(bisim_step_true … H)
- (* new_visited = hd::visited are all ok *)
- cut (all_true S (hd::visited))
- [#p #H1 cases (orb_true_l … H1) [#eqp >(\P eqp) @H |@allv]]
- (* we now exploit the induction hypothesis *)
- #allh #subH #bisim cases (Hind … allh … bisim) -bisim -Hind
- [#H1 #H2 % // #p #membp @H2 -H2 cases (memb_append … membp) -membp #membp
- [cases (orb_true_l … membp) -membp #membp
- [@memb_append_l2 >(\P membp) @memb_hd
- |@memb_append_l1 @sublist_unique_append_l2 //
- ]
- |@memb_append_l2 @memb_cons //
- ]
- |(* the only thing left to prove is the sub_sons invariant *)
- #x #membx cases (orb_true_l … membx)
- [(* case x = hd *)
- #eqhdx <(\P eqhdx) #xa #membxa
- (* xa is a son of x; we must distinguish the case xa
- was already visited form the case xa is new *)
- cases (true_or_false … (memb ? xa (x::visited)))
- [(* xa visited - trivial *) #membxa @memb_append_l2 //
- |(* xa new *) #membxa @memb_append_l1 @sublist_unique_append_l1 @memb_filter_l
- [>membxa //|//]
- ]
- |(* case x in visited *)
- #H1 #xa #membxa cases (memb_append … (subH x … H1 … membxa))
- [#H2 (cases (orb_true_l … H2))
- [#H3 @memb_append_l2 <(\P H3) @memb_hd
- |#H3 @memb_append_l1 @sublist_unique_append_l2 @H3
- ]
- |#H2 @memb_append_l2 @memb_cons @H2
- ]
- ]
- ]
- ]
-qed.