weblib/tutorial/chapter10.ma

   1 include "cahpter9.ma".
   2
   3 (* bisimulation *)
   4 definition cofinal ≝ λS.λp:(pre S)×(pre S).
   5   \snd (\fst p) = \snd (\snd p).
   6
   7 theorem equiv_sem: ∀S:DeqSet.∀e1,e2:pre S.
   8   \sem{e1} =1 \sem{e2} ↔ ∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
   9 #S #e1 #e2 %
  10 [#same_sem #w
  11   cut (∀b1,b2. iff (b1 = true) (b2 = true) → (b1 = b2))
  12     [* * // * #H1 #H2 [@sym_eq @H1 //| @H2 //]]
  13   #Hcut @Hcut @iff_trans [|@decidable_sem]
  14   @iff_trans [|@same_sem] @iff_sym @decidable_sem
  15 |#H #w1 @iff_trans [||@decidable_sem] <H @iff_sym @decidable_sem]
  16 qed.
  17
  18 definition occ ≝ λS.λe1,e2:pre S.
  19   unique_append ? (occur S (|\fst e1|)) (occur S (|\fst e2|)).
  20
  21 lemma occ_enough: ∀S.∀e1,e2:pre S.
  22 (∀w.(sublist S w (occ S e1 e2))→ cofinal ? 〈moves ? w e1,moves ? w e2〉)
  23  →∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
  24 #S #e1 #e2 #H #w
  25 cases (decidable_sublist S w (occ S e1 e2)) [@H] -H #H
  26  >to_pit [2: @(not_to_not … H) #H1 #a #memba @sublist_unique_append_l1 @H1 //]
  27  >to_pit [2: @(not_to_not … H) #H1 #a #memba  @sublist_unique_append_l2 @H1 //]
  28  //
  29 qed.
  30
  31 lemma equiv_sem_occ: ∀S.∀e1,e2:pre S.
  32 (∀w.(sublist S w (occ S e1 e2))→ cofinal ? 〈moves ? w e1,moves ? w e2〉)
  33 → \sem{e1}=1\sem{e2}.
  34 #S #e1 #e2 #H @(proj2 … (equiv_sem …)) @occ_enough #w @H
  35 qed.
  36
  37 definition sons ≝ λS:DeqSet.λl:list S.λp:(pre S)×(pre S).
  38  map ?? (λa.〈move S a (\fst (\fst p)),move S a (\fst (\snd p))〉) l.
  39
  40 lemma memb_sons: ∀S,l.∀p,q:(pre S)×(pre S). memb ? p (sons ? l q) = true →
  41   ∃a.(move ? a (\fst (\fst q)) = \fst p ∧
  42       move ? a (\fst (\snd q)) = \snd p).
  43 #S #l elim l [#p #q normalize in ⊢ (%→?); #abs @False_ind /2/]
  44 #a #tl #Hind #p #q #H cases (orb_true_l … H) -H
  45   [#H @(ex_intro … a) >(\P H) /2/ |#H @Hind @H]
  46 qed.
  47
  48 definition is_bisim ≝ λS:DeqSet.λl:list ?.λalpha:list S.
  49   ∀p:(pre S)×(pre S). memb ? p l = true → cofinal ? p ∧ (sublist ? (sons ? alpha p) l).
  50
  51 lemma bisim_to_sem: ∀S:DeqSet.∀l:list ?.∀e1,e2: pre S.
  52   is_bisim S l (occ S e1 e2) → memb ? 〈e1,e2〉 l = true → \sem{e1}=1\sem{e2}.
  53 #S #l #e1 #e2 #Hbisim #Hmemb @equiv_sem_occ
  54 #w #Hsub @(proj1 … (Hbisim 〈moves S w e1,moves S w e2〉 ?))
  55 lapply Hsub @(list_elim_left … w) [//]
  56 #a #w1 #Hind #Hsub >moves_left >moves_left @(proj2 …(Hbisim …(Hind ?)))
  57   [#x #Hx @Hsub @memb_append_l1 //
  58   |cut (memb S a (occ S e1 e2) = true) [@Hsub @memb_append_l2 //] #occa
  59    @(memb_map … occa)
  60   ]
  61 qed.
  62
  63 (* the algorithm *)
  64 let rec bisim S l n (frontier,visited: list ?) on n ≝
  65   match n with
  66   [ O ⇒ 〈false,visited〉 (* assert false *)
  67   | S m ⇒
  68     match frontier with
  69     [ nil ⇒ 〈true,visited〉
  70     | cons hd tl ⇒
  71       if beqb (\snd (\fst hd)) (\snd (\snd hd)) then
  72         bisim S l m (unique_append ? (filter ? (λx.notb (memb ? x (hd::visited)))
  73         (sons S l hd)) tl) (hd::visited)
  74       else 〈false,visited〉
  75     ]
  76   ].
  77
  78 lemma unfold_bisim: ∀S,l,n.∀frontier,visited: list ?.
  79   bisim S l n frontier visited =
  80   match n with
  81   [ O ⇒ 〈false,visited〉 (* assert false *)
  82   | S m ⇒
  83     match frontier with
  84     [ nil ⇒ 〈true,visited〉
  85     | cons hd tl ⇒
  86       if beqb (\snd (\fst hd)) (\snd (\snd hd)) then
  87         bisim S l m (unique_append ? (filter ? (λx.notb(memb ? x (hd::visited)))
  88           (sons S l hd)) tl) (hd::visited)
  89       else 〈false,visited〉
  90     ]
  91   ].
  92 #S #l #n cases n // qed.
  93
  94 lemma bisim_never: ∀S,l.∀frontier,visited: list ?.
  95   bisim S l O frontier visited = 〈false,visited〉.
  96 #frontier #visited >unfold_bisim //
  97 qed.
  98
  99 lemma bisim_end: ∀Sig,l,m.∀visited: list ?.
 100   bisim Sig l (S m) [] visited = 〈true,visited〉.
 101 #n #visisted >unfold_bisim //
 102 qed.
 103
 104 lemma bisim_step_true: ∀Sig,l,m.∀p.∀frontier,visited: list ?.
 105 beqb (\snd (\fst p)) (\snd (\snd p)) = true →
 106   bisim Sig l (S m) (p::frontier) visited =
 107   bisim Sig l m (unique_append ? (filter ? (λx.notb(memb ? x (p::visited)))
 108     (sons Sig l p)) frontier) (p::visited).
 109 #Sig #l #m #p #frontier #visited #test >unfold_bisim normalize nodelta >test //
 110 qed.
 111
 112 lemma bisim_step_false: ∀Sig,l,m.∀p.∀frontier,visited: list ?.
 113 beqb (\snd (\fst p)) (\snd (\snd p)) = false →
 114   bisim Sig l (S m) (p::frontier) visited = 〈false,visited〉.
 115 #Sig #l #m #p #frontier #visited #test >unfold_bisim normalize nodelta >test //
 116 qed.
 117
 118 lemma notb_eq_true_l: ∀b. notb b = true → b = false.
 119 #b cases b normalize //
 120 qed.
 121
 122 let rec pitem_enum S (i:re S) on i ≝
 123   match i with
 124   [ z ⇒ [pz S]
 125   | e ⇒ [pe S]
 126   | s y ⇒ [ps S y; pp S y]
 127   | o i1 i2 ⇒ compose ??? (po S) (pitem_enum S i1) (pitem_enum S i2)
 128   | c i1 i2 ⇒ compose ??? (pc S) (pitem_enum S i1) (pitem_enum S i2)
 129   | k i ⇒ map ?? (pk S) (pitem_enum S i)
 130   ].
 131
 132 lemma pitem_enum_complete : ∀S.∀i:pitem S.
 133   memb (DeqItem S) i (pitem_enum S (|i|)) = true.
 134 #S #i elim i
 135   [1,2://
 136   |3,4:#c normalize >(\b (refl … c)) //
 137   |5,6:#i1 #i2 #Hind1 #Hind2 @(memb_compose (DeqItem S) (DeqItem S)) //
 138   |#i #Hind @(memb_map (DeqItem S)) //
 139   ]
 140 qed.
 141
 142 definition pre_enum ≝ λS.λi:re S.
 143   compose ??? (λi,b.〈i,b〉) (pitem_enum S i) [true;false].
 144
 145 lemma pre_enum_complete : ∀S.∀e:pre S.
 146   memb ? e (pre_enum S (|\fst e|)) = true.
 147 #S * #i #b @(memb_compose (DeqItem S) DeqBool ? (λi,b.〈i,b〉))
 148 // cases b normalize //
 149 qed.
 150
 151 definition space_enum ≝ λS.λi1,i2:re S.
 152   compose ??? (λe1,e2.〈e1,e2〉) (pre_enum S i1) (pre_enum S i2).
 153
 154 lemma space_enum_complete : ∀S.∀e1,e2: pre S.
 155   memb ? 〈e1,e2〉 (space_enum S (|\fst e1|) (|\fst e2|)) = true.
 156 #S #e1 #e2 @(memb_compose … (λi,b.〈i,b〉))
 157 // qed.
 158
 159 definition all_reachable ≝ λS.λe1,e2:pre S.λl: list ?.
 160 uniqueb ? l = true ∧
 161   ∀p. memb ? p l = true →
 162     ∃w.(moves S w e1 = \fst p) ∧ (moves S w e2 = \snd p).
 163
 164 definition disjoint ≝ λS:DeqSet.λl1,l2.
 165   ∀p:S. memb S p l1 = true →  memb S p l2 = false.
 166
 167 lemma bisim_correct: ∀S.∀e1,e2:pre S.\sem{e1}=1\sem{e2} →
 168  ∀l,n.∀frontier,visited:list ((pre S)×(pre S)).
 169  |space_enum S (|\fst e1|) (|\fst e2|)| < n + |visited|→
 170  all_reachable S e1 e2 visited →
 171  all_reachable S e1 e2 frontier →
 172  disjoint ? frontier visited →
 173  \fst (bisim S l n frontier visited) = true.
 174 #Sig #e1 #e2 #same #l #n elim n
 175   [#frontier #visited #abs * #unique #H @False_ind @(absurd … abs)
 176    @le_to_not_lt @sublist_length // * #e11 #e21 #membp
 177    cut ((|\fst e11| = |\fst e1|) ∧ (|\fst e21| = |\fst e2|))
 178    [|* #H1 #H2 <H1 <H2 @space_enum_complete]
 179    cases (H … membp) #w * #we1 #we2 <we1 <we2 % >same_kernel_moves //
 180   |#m #HI * [#visited #vinv #finv >bisim_end //]
 181    #p #front_tl #visited #Hn * #u_visited #r_visited * #u_frontier #r_frontier
 182    #disjoint
 183    cut (∃w.(moves ? w e1 = \fst p) ∧ (moves ? w e2 = \snd p))
 184     [@(r_frontier … (memb_hd … ))] #rp
 185    cut (beqb (\snd (\fst p)) (\snd (\snd p)) = true)
 186     [cases rp #w * #fstp #sndp <fstp <sndp @(\b ?)
 187      @(proj1 … (equiv_sem … )) @same] #ptest
 188    >(bisim_step_true … ptest) @HI -HI
 189      [<plus_n_Sm //
 190      |% [whd in ⊢ (??%?); >(disjoint … (memb_hd …)) whd in ⊢ (??%?); //
 191         |#p1 #H (cases (orb_true_l … H)) [#eqp >(\P eqp) // |@r_visited]
 192         ]
 193      |whd % [@unique_append_unique @(andb_true_r … u_frontier)]
 194       @unique_append_elim #q #H
 195        [cases (memb_sons … (memb_filter_memb … H)) -H
 196         #a * #m1 #m2 cases rp #w1 * #mw1 #mw2 @(ex_intro … (w1@[a]))
 197         >moves_left >moves_left >mw1 >mw2 >m1 >m2 % //
 198        |@r_frontier @memb_cons //
 199        ]
 200      |@unique_append_elim #q #H
 201        [@injective_notb @(filter_true … H)
 202        |cut ((q==p) = false)
 203          [|#Hpq whd in ⊢ (??%?); >Hpq @disjoint @memb_cons //]
 204         cases (andb_true … u_frontier) #notp #_ @(\bf ?)
 205         @(not_to_not … not_eq_true_false) #eqqp <notp <eqqp >H //
 206        ]
 207      ]
 208    ]
 209 qed.
 210
 211 definition all_true ≝ λS.λl.∀p:(pre S) × (pre S). memb ? p l = true →
 212   (beqb (\snd (\fst p)) (\snd (\snd p)) = true).
 213
 214 definition sub_sons ≝ λS,l,l1,l2.∀x:(pre S) × (pre S).
 215 memb ? x l1 = true → sublist ? (sons ? l x) l2.
 216
 217 lemma bisim_complete:
 218  ∀S,l,n.∀frontier,visited,visited_res:list ?.
 219  all_true S visited →
 220  sub_sons S l visited (frontier@visited) →
 221  bisim S l n frontier visited = 〈true,visited_res〉 →
 222  is_bisim S visited_res l ∧ sublist ? (frontier@visited) visited_res.
 223 #S #l #n elim n
 224   [#fron #vis #vis_res #_ #_ >bisim_never #H destruct
 225   |#m #Hind *
 226     [(* case empty frontier *)
 227      -Hind #vis #vis_res #allv #H normalize in  ⊢ (%→?);
 228      #H1 destruct % #p
 229       [#membp % [@(\P ?) @allv //| @H //]|#H1 @H1]
 230     |#hd cases (true_or_false (beqb (\snd (\fst hd)) (\snd (\snd hd))))
 231       [|(* case head of the frontier is non ok (absurd) *)
 232        #H #tl #vis #vis_res #allv >(bisim_step_false … H) #_ #H1 destruct]
 233      (* frontier = hd:: tl and hd is ok *)
 234      #H #tl #visited #visited_res #allv >(bisim_step_true … H)
 235      (* new_visited = hd::visited are all ok *)
 236      cut (all_true S (hd::visited))
 237       [#p #H1 cases (orb_true_l … H1) [#eqp >(\P eqp) @H |@allv]]
 238      (* we now exploit the induction hypothesis *)
 239      #allh #subH #bisim cases (Hind … allh … bisim) -bisim -Hind
 240       [#H1 #H2 % // #p #membp @H2 -H2 cases (memb_append … membp) -membp #membp
 241         [cases (orb_true_l … membp) -membp #membp
 242           [@memb_append_l2 >(\P membp) @memb_hd
 243           |@memb_append_l1 @sublist_unique_append_l2 //
 244           ]
 245         |@memb_append_l2 @memb_cons //
 246         ]
 247       |(* the only thing left to prove is the sub_sons invariant *)
 248      #x #membx cases (orb_true_l … membx)
 249       [(* case x = hd *)
 250        #eqhdx <(\P eqhdx) #xa #membxa
 251        (* xa is a son of x; we must distinguish the case xa
 252         was already visited form the case xa is new *)
 253        cases (true_or_false … (memb ? xa (x::visited)))
 254         [(* xa visited - trivial *) #membxa @memb_append_l2 //
 255         |(* xa new *) #membxa @memb_append_l1 @sublist_unique_append_l1 @memb_filter_l
 256           [>membxa //|//]
 257         ]
 258       |(* case x in visited *)
 259        #H1 #xa #membxa cases (memb_append … (subH x … H1 … membxa))
 260         [#H2 (cases (orb_true_l … H2))
 261           [#H3 @memb_append_l2 <(\P H3) @memb_hd
 262           |#H3 @memb_append_l1 @sublist_unique_append_l2 @H3
 263           ]
 264         |#H2 @memb_append_l2 @memb_cons @H2
 265         ]
 266       ]
 267     ]
 268   ]
 269 qed.
 270
 271 definition equiv ≝ λSig.λre1,re2:re Sig.
 272   let e1 ≝ •(blank ? re1) in
 273   let e2 ≝ •(blank ? re2) in
 274   let n ≝ S (length ? (space_enum Sig (|\fst e1|) (|\fst e2|))) in
 275   let sig ≝ (occ Sig e1 e2) in
 276   (bisim ? sig n [〈e1,e2〉] []).
 277
 278 theorem euqiv_sem : ∀Sig.∀e1,e2:re Sig.
 279    \fst (equiv ? e1 e2) = true ↔ \sem{e1} =1 \sem{e2}.
 280 #Sig #re1 #re2 %
 281   [#H @eqP_trans [|@eqP_sym @re_embedding] @eqP_trans [||@re_embedding]
 282    cut (equiv ? re1 re2 = 〈true,\snd (equiv ? re1 re2)〉)
 283      [<H //] #Hcut
 284    cases (bisim_complete … Hcut)
 285      [2,3: #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/]
 286    #Hbisim #Hsub @(bisim_to_sem … Hbisim)
 287    @Hsub @memb_hd
 288   |#H @(bisim_correct ? (•(blank ? re1)) (•(blank ? re2)))
 289     [@eqP_trans [|@re_embedding] @eqP_trans [|@H] @eqP_sym @re_embedding
 290     |//
 291     |% // #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/
 292     |% // #p #H >(memb_single … H) @(ex_intro … ϵ) /2/
 293     |#p #_ normalize //
 294     ]
 295   ]
 296 qed.
 297
 298 lemma eqbnat_true : ∀n,m. eqbnat n m = true ↔ n = m.
 299 #n #m % [@eqbnat_true_to_eq | @eq_to_eqbnat_true]
 300 qed.
 301
 302 definition DeqNat ≝ mk_DeqSet nat eqbnat eqbnat_true.
 303
 304 definition a ≝ s DeqNat O.
 305 definition b ≝ s DeqNat (S O).
 306 definition c ≝ s DeqNat (S (S O)).
 307
 308 definition exp1 ≝ ((a·b)^*·a).
 309 definition exp2 ≝ a·(b·a)^*.
 310 definition exp4 ≝ (b·a)^*.
 311
 312 definition exp6 ≝ a·(a ·a ·b^* + b^* ).
 313 definition exp7 ≝ a · a^* · b^*.
 314
 315 definition exp8 ≝ a·a·a·a·a·a·a·a·(a^* ).
 316 definition exp9 ≝ (a·a·a + a·a·a·a·a)^*.
 317
 318 example ex1 : \fst (equiv ? (exp8+exp9) exp9) = true.
 319 normalize // qed.
 320
 321
 322
 323
 324
 325
 326