Changeset 2254


Ignore:
Timestamp:
Jul 24, 2012, 7:40:23 PM (7 years ago)
Author:
campbell
Message:

Fix up invariants in Cminor semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/semantics.ma

    r2251 r2254  
    169169//
    170170try @(π2 Inv)
    171 try @(π2 (π1 Inv))
    172 [ % [ @(π2 Inv) | @kInv ]
     171try @(π1 (π2 Inv))
     172try @(π2 (π2 Inv))
     173[ % [ @(π2 (π2 Inv)) | @kInv ]
    173174| % [ @(π2 Inv) | @kInv ]
    174175] qed.
     
    180181try (try #a try #b try #c try #d try #e try #f try #g try #h try #i try #j try #m % * (* *) )
    181182[ #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%));
    182   lapply (IH1 (Kseq s2 k) f en (π2 (π1 Inv)) (conj ?? (π2 Inv) kInv))
     183  lapply (IH1 (Kseq s2 k) f en (π1 (π2 Inv)) (conj ?? (π2 (π2 Inv)) kInv))
    183184  cases (find_label l s1 (Kseq s2 k) f en ??)
    184185  [ #H1 whd in ⊢ (??%? → ?);
    185     lapply (IH2 k f en (π2 Inv) kInv) cases (find_label l s2 k f en ??)
     186    lapply (IH2 k f en (π2 (π2 Inv)) kInv) cases (find_label l s2 k f en ??)
    186187    [ #H2 #_ % #H cases (Exists_append … H)
    187188      [ #H' cases (H1 (refl ??)) /2/
     
    193194  ]
    194195| #sz #sg #e #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%));
    195   lapply (IH1 k f en (π2 (π1 Inv)) kInv)
     196  lapply (IH1 k f en (π1 (π2 Inv)) kInv)
    196197  cases (find_label l s1 k f en ??)
    197198  [ #H1 whd in ⊢ (??%? → ?);
    198     lapply (IH2 k f en (π2 Inv) kInv) cases (find_label l s2 k f en ??)
     199    lapply (IH2 k f en (π2 (π2 Inv)) kInv) cases (find_label l s2 k f en ??)
    199200    [ #H2 #_ % #H cases (Exists_append … H)
    200201      [ #H' cases (H1 (refl ??)) /2/
     
    382383try @kInv
    383384try @(π1 (π1 Inv))
    384 try (@cont_inv_update @kInv)
    385 try @(π2 (π1 (π1 Inv)))
     385try (@cont_inv_update @kInv) 
     386try @(π2 (π1 (π1 Inv))) 
    386387try @(π1 (π1 (π1 Inv)))
    387 try @(π1 Inv)
    388388try @(π2 Inv)
     389try @(π1 (π2 Inv))
    389390[ @fInv
    390391| @(π2 Inv')
    391392| @(π1 Inv')
    392 | cases b [ @(π2 (π1 Inv)) | @(π2 Inv) ]
    393 | % [ @(π2 Inv) | @kInv ]
     393| cases b [ @(π1 (π2 Inv)) | @(π2 (π2 Inv)) ]
     394| % [ @(π2 (π2 Inv)) | @kInv ]
     395| @(π1 (π1 (π1 (π1 Inv))))
     396| @(π2 (π1 (π1 (π1 Inv))))
     397| /3/
    394398| @stmt_inv_update @fInv
    395 | 7,8:
     399| /3/
     400| /3/
     401| 12,13:
    396402  @(stmt_P_mp … (f_inv f))
    397403  #s * #V #L #R %
     
    406412| @I
    407413| @cont_inv_update @Inv
     414| /3/
    408415| @stmt_inv_update @fInv
    409416| @Inv
     417| /3/
    410418| @fInv
    411419] qed.
Note: See TracChangeset for help on using the changeset viewer.