Changeset 2474


Ignore:
Timestamp:
Nov 19, 2012, 10:57:08 AM (7 years ago)
Author:
tranquil
Message:

changed form of a statement

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/extraGlobalenvs.ma

    r2473 r2474  
    5151     [ Some v ⇒ λprf.c1 v prf | None ⇒ λprf.c2 prf]
    5252     (refl …))) [ #A #B #P * // ] #aux
    53 whd in ⊢ (???(??%)); @aux [//] #H @⊥
    54 (* cut and paste from global env *)
    55 whd in H:(??%?);
    56 cases b in FFP H ⊢ %; * * -b [2,3,5,6: #b ] normalize in ⊢ (% → ?); [4: #FFP | *: * #H cases (H (refl ??)) ]
    57 cases (functions_inv … ge b FFP)
    58 #id #L lapply (find_lookup ?? (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))
    59 lapply (find_none … (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b)))
    60 cases (find ????)
    61 [ #H #_ #_ lapply (H (refl ??) L) @eq_block_elim [ #_ * | * #H' cases (H' (refl ??)) ]
    62 | * #id' #b' #_ normalize #_ #E destruct
    63 ] qed.
     53whd in ⊢ (???(??%)); @aux [//] #H
     54generalize in match (? : False); *
     55qed.
    6456
    6557definition funct_of_block : ∀F,ge.
     
    253245  let prog_out : program (λvars.fundef (B vars)) V≝
    254246    transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
    255   ∀i,prf1,prf2.
    256   prog_if_of_function ?? prog_out «i,prf1» = trans … (prog_if_of_function ?? prog_in «i,prf2»).
    257 #A #B #V #trans #prog #i #i_prf #i_prf'
     247  ∀i1,i2.pi1 ?? i1 = pi1 ?? i2 →
     248  prog_if_of_function ?? prog_out i1 = trans … (prog_if_of_function ?? prog_in i2).
     249#A #B #V #trans #prog * #i1 #i_prf1 * #i #i_prf2 #EQ
    258250change with (opt_safe ??? = ?)
    259251@opt_safe_elim #ifn >find_map
    260252cut (∀vars.∀x.
    261   if eq_identifier ? (\fst x) i then
     253  if eq_identifier ? (\fst x) i1 then
    262254    match transf_fundef … (trans vars) (\snd x) with
    263255    [ Internal x ⇒ return x
    264256    | _ ⇒ None ?
    265257    ] else None ? =
    266   ! y ← if eq_identifier ? (\fst x) i then
     258  ! y ← if eq_identifier ? (\fst x) i1 then
    267259        match \snd x with
    268260        [ Internal x ⇒ return x
     
    275267#EQfind
    276268change with (? = trans ? (opt_safe ???))
    277 @opt_safe_elim #ifn' #EQfind'
     269@opt_safe_elim #ifn' #EQfind' destruct(EQ)
    278270>EQfind' in EQfind; >m_return_bind whd in ⊢ (??%?→?); #EQ destruct(EQ) %
    279271qed.
  • src/joint/linearise.ma

    r2473 r2474  
    173173    ] n_prf
    174174  ] (chop_ok ? (λx.x∈visited) visiting).
     175(*cases daemon qed. *)
    175176whd
    176177[ (* base case, visiting is all visited *)
     
    746747    \snd (linearise_int_fun … fn_in))
    747748%{sigma}
    748 * #i #i_prf >(prog_if_of_function_transform … i_prf)
     749#i >(prog_if_of_function_transform … i) [2: % ]
    749750normalize nodelta
    750751cases (linearise_int_fun ???) * #fn_out #sigma_loc
Note: See TracChangeset for help on using the changeset viewer.