Ignore:
Timestamp:
Jan 9, 2013, 6:33:44 PM (7 years ago)
Author:
campbell
Message:

Update labelling simulation proofs due to some changes elsewhere.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r2487 r2574  
    152152  @add_cost_expr_elim #u6 #l6
    153153  [ cases (IH2 … EX2 u2) | cases (IH3 … EX2 u4) ] #trx' * #EXx' #twelx
    154   [ %{(tr1'⧺trx'⧺(Echarge l4))} | %{(tr1'⧺trx'⧺(Echarge l6))} ]
     154  [ %{(tr1'⧺(Echarge l4)⧺trx')} | %{(tr1'⧺(Echarge l6)⧺trx')} ]
    155155  whd in ⊢ (?(??%?)?); >EX1'
    156156  whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
    157157  whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?); >EXx'
    158   normalize % // @twel_app // <(E0_right tr2) @twel_app /2/
     158  normalize % // @twel_app // /2/
    159159| #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u
    160160  cases (bind_inversion ????? EX) -EX * #v1 #tr1 * #EX1 #EX
     
    171171    cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
    172172    cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2
    173     [ %{(tr1'⧺(tr2'⧺Echarge l4)⧺Echarge l6)} | %{(tr1'⧺(tr2'⧺Echarge l5)⧺Echarge l6)} ]
     173    [ %{(tr1'⧺Echarge l6⧺tr2'⧺Echarge l4)} | %{(tr1'⧺Echarge l6⧺tr2'⧺Echarge l5)} ]
    174174    whd in ⊢ (?(??%?)?); >EX1'
    175175    whd in ⊢ (?(??%?)?); >label_expr_type >EX2' >EXguard
     
    177177    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2'
    178178    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3
    179     whd in EX:(??%%) ⊢ %; destruct % [ 1,3: normalize @refl | *: @twel_app // <(E0_right tr2) @twel_app [1,3: <(E0_right tr2) @twel_app ] /2/ ]
     179    whd in EX:(??%%) ⊢ %; destruct % [ 1,3: normalize @refl | *: @twel_app // @twel_new whd in ⊢ (??%); <(E0_right tr2) @twel_app /2/ ]
    180180  | cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
    181181    %{(tr1'⧺E0⧺Echarge l7)}
     
    203203    cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
    204204    cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2
    205     [ %{(tr1'⧺(tr2'⧺Echarge l4)⧺Echarge l6)} | %{(tr1'⧺(tr2'⧺Echarge l5)⧺Echarge l6)} ]
     205    [ %{(tr1'⧺Echarge l6⧺tr2'⧺Echarge l4)} | %{(tr1'⧺Echarge l6⧺tr2'⧺Echarge l5)} ]
    206206    whd in ⊢ (?(??%?)?); >EX1'
    207207    whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
     
    209209    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2'
    210210    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3
    211     whd in EX:(??%%) ⊢ %; destruct normalize % // @twel_app // <(E0_right tr2) @twel_app [1,3:<(E0_right tr2) @twel_app] /2/
     211    whd in EX:(??%%) ⊢ %; destruct normalize % [1,3: % | *: @twel_app // @twel_new <(E0_right tr2) @twel_app /2/ ]
    212212  ]
    213213| #ty #ty' #v #tr normalize /3/
     
    233233  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
    234234  whd in EX1rem:(???%); destruct
    235   cases (IH … EX1 u) #tr1' * #EX1' #twel1 %{(tr1'@Echarge l)}
     235  cases (IH … EX1 u) #tr1' * #EX1' #twel1 %{(EVcost l::tr1')}
    236236  >shift_fst >shift_fst whd in ⊢ (?(??%?)?); >EX1'
    237237  whd in ⊢ (?(??%?)?); /3/
Note: See TracChangeset for help on using the changeset viewer.