Ignore:
Timestamp:
Nov 15, 2012, 6:12:57 PM (8 years ago)
Author:
garnier
Message:

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/SimplifyCasts.ma

    r2441 r2468  
    581581                         ∃i. castee_val = Vint src_sz i ∧ result = Vint cast_sz (cast_int_int src_sz src_sg cast_sz i).
    582582#castee_val #src_sz #src_sg #cast_sz #cast_sg #m #result
    583 elim castee_val 
    584 [ 1: | 2: #sz' #i | 3: #f | 4: | 5: #ptr ]
     583elim castee_val
     584[ 1: | 2: #sz' #i | 3: | 4: #ptr ]
    585585[ 2: | *: whd in ⊢ ((??%?) → ?); #Habsurd destruct ]
    586586whd in ⊢ ((??%?) → ?);
     
    613613#sz #sg #v1 #v2 #m #r
    614614elim v1
    615 [ 1: | 2: #sz' #i | 3: #f | 4: | 5: #ptr ]
     615[ 1: | 2: #sz' #i | 3: | 4: #ptr ]
    616616whd in ⊢ ((??%?) → ?); normalize nodelta
    617617>classify_add_int normalize nodelta #H destruct
    618618elim v2 in H;
    619 [ 1: | 2: #sz'' #i' | 3: #f' | 4:  | 5: #ptr' ]
     619[ 1: | 2: #sz'' #i' | 3: | 4: #ptr' ]
    620620whd in ⊢ ((??%?) → ?); #H destruct
    621621elim (sz_eq_dec sz' sz'')
    622622[ 1: #Heq destruct >intsize_eq_elim_true in H; #Heq destruct %{sz''} %{i} %{i'} /3/
    623623| 2: #Hneq >intsize_eq_elim_false in H; try assumption #H destruct
    624 ] qed. 
     624] qed.
    625625
    626626(* Inversion principle for integer subtraction. *)
     
    629629#sz #sg #v1 #v2 #m #r
    630630elim v1
    631 [ 1: | 2: #sz' #i | 3: #f | 4:  | 5: #ptr ]
     631[ 1: | 2: #sz' #i | 3: | 4: #ptr ]
    632632whd in ⊢ ((??%?) → ?); normalize nodelta
    633633>classify_sub_int normalize nodelta #H destruct
    634634elim v2 in H;
    635 [ 1: | 2: #sz'' #i' | 3: #f' | 4:  | 5: #ptr' ]
     635[ 1: | 2: #sz'' #i' | 3: | 4: #ptr' ]
    636636whd in ⊢ ((??%?) → ?); #H destruct
    637637elim (sz_eq_dec sz' sz'')
     
    652652#sz #sg #v1 #v2 #m
    653653elim v1
    654 [ 1: | 2: #sz' #i | 3: #f | 4:  | 5: #ptr ]
     654[ 1: | 2: #sz' #i | 3: | 4: #ptr ]
    655655[ 2: | *: #_ %1 %1 % #H @H ]
    656656elim v2
    657 [ 1: | 2: #sz'' #i' | 3: #f' | 4:  | 5: #ptr' ]
     657[ 1: | 2: #sz'' #i' | 3: | 4: #ptr' ]
    658658[ 2: | *: #_ %1 %2 % #H @H ]
    659659whd in ⊢ ((??%?) → ?); normalize nodelta
     
    663663| 2: #Hneq >intsize_eq_elim_false try assumption #_
    664664     %2 %{sz'} %{sz''} %{i} %{i'} try @conj try @conj //
    665 ] qed. 
     665] qed.
    666666
    667667(* "negative" inversion principle for integer subtraction *)
     
    671671#sz #sg #v1 #v2 #m
    672672elim v1
    673 [ 1: | 2: #sz' #i | 3: #f | 4:  | 5: #ptr ]
     673[ 1: | 2: #sz' #i | 3: | 4: #ptr ]
    674674[ 2: | *: #_ %1 %1 % #H @H ]
    675675elim v2
    676 [ 1: | 2: #sz'' #i' | 3: #f' | 4:  | 5: #ptr' ]
     676[ 1: | 2: #sz'' #i' | 3: | 4: #ptr' ]
    677677[ 2: | *: #_ %1 %2 % #H @H ]
    678678whd in ⊢ ((??%?) → ?); normalize nodelta
     
    684684] qed.
    685685
    686 
    687686lemma simplifiable_op_inconsistent : ∀op,sz,sg,v1,v2,m.
    688687   ¬ (is_int v1) → binop_simplifiable op = true → sem_binary_operation op v1 (Tint sz sg) v2 (Tint sz sg) m = None ?.
     
    690689elim op normalize in match (binop_simplifiable ?); #H destruct
    691690elim v1 in H;
    692 [ 1,6: | 2,7: #sz' #i normalize in ⊢ (% → ?); * #H @(False_ind … (H I)) | 3,8: #f | 4,9: | 5,10: #ptr ]
     691[ 1,5: | 2,6: #sz' #i normalize in ⊢ (% → ?); * #H @(False_ind … (H I)) | 3,7: | 4,8: #ptr ]
    693692#_
    694693whd in match (sem_binary_operation ??????); normalize nodelta
     
    890889        «〈false, Expr (Ecost l e2) ty〉, ?»
    891890      ]               
    892   | Econst_float f ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?»
     891(*  | Econst_float f ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?» *)
    893892(* | Evar id ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?» *)
    894893  (* In order for the simplification function to be less dymp, we would have to use this line, which would in fact
     
    960959] (refl ? e).
    961960#ge #en #m
    962 [ 1,3,5,6,7,8,9,10,11,12: %1 try @refl
     961[ 1,3,5,6,7,8,9,10,11: %1 try @refl
    963962     cases (exec_expr ge en m e) #res
    964963     try (@(SimOk ???) //)
     
    975974     [ 1: @(simplify_int_implements_cast … Hsimpl_eq)
    976975     | 2: @(simplify_int_success_lt … Hsimpl_eq) ]
    977 | 13: %1 // >Hexpr_eq cases (exec_expr ge en m e) #res
    978       try (@(SimOk ???) //)
    979 | 14: elim (type_eq_dec ty (Tint target_sz target_sg))
     976(*| 14: %1 // >Hexpr_eq cases (exec_expr ge en m e) #res
     977      try (@(SimOk ???) //) *)
     978| 12: elim (type_eq_dec ty (Tint target_sz target_sg))
    980979      [ 1: #Heq >Heq >type_eq_identity @(Inv_coerce_ok ??????? target_sz target_sg)
    981980           destruct
     
    985984           @(SimOk ???) //
    986985      ]
    987 | 15: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
     986| 13: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
    988987    [ 1: (* Proving preservation of the semantics for expressions. *)
    989988      cases Hexpr_sim
     
    998997             [ 1: * #val' #trace' normalize nodelta
    999998                  cases val' normalize nodelta
    1000                   [ 1,2,3,4: #H1 destruct #H2 destruct #H3 destruct
    1001                   | 5: #pointer #Heq @(ex_intro … pointer) (* @(ex_intro … trace') *)
     999                  [ 1,2,3: #H1 destruct #H2 destruct #H3 destruct
     1000                  | 4: #pointer #Heq @(ex_intro … pointer) (* @(ex_intro … trace') *)
    10021001                       cases (load_value_of_type ty m (pblock pointer) (poff pointer)) in Heq;
    10031002                       normalize nodelta
     
    10271026             [ 1: * #val' #trace' normalize nodelta
    10281027                  cases val' normalize nodelta
    1029                   [ 1,2,3,4: #H1 destruct #H2 destruct #H3 destruct
    1030                   | 5: #pointer #Heq @(ex_intro … pointer) (* @(ex_intro … trace') *)
     1028                  [ 1,2,3: #H1 destruct #H2 destruct #H3 destruct
     1029                  | 4: #pointer #Heq @(ex_intro … pointer) (* @(ex_intro … trace') *)
    10311030                       destruct try @conj try @conj //
    10321031                  ]
     
    10421041     ]
    10431042   ]
    1044 | 16: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
     1043| 14: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
    10451044    [ 1: (* Proving preservation of the semantics for expressions. *)
    10461045      cases Hlvalue_sim
     
    10561055             [ 1: * * #block #offset #trace' normalize nodelta
    10571056                  cases ty
    1058                   [ 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
    1059                   | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
     1057                  [ 2: #sz #sg | 3: #ptr_ty | 4: #array_ty #array_sz | 5: #domain #codomain
     1058                  | 6: #structname #fieldspec | 7: #unionname #fieldspec | 8: #id ]
    10601059                  normalize nodelta try (#Heq destruct)
    10611060                  @(ex_intro … block) @(ex_intro … offset) @(ex_intro … ptr_ty)
     
    10711070         @SimFailNicely
    10721071    ]
    1073 | 17: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
     1072| 15: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
    10741073      [ 1: whd in match (exec_expr ge en m (Expr ??));
    10751074           whd in match (exec_expr ge en m (Expr ??));
     
    10851084      | 2: @SimFailNicely
    10861085      ]
    1087 | 18: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_lhs #Hdesired_rhs -Hdesired_eq
     1086| 16: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_lhs #Hdesired_rhs -Hdesired_eq
    10881087      inversion (Hinv_lhs ge en m)
    10891088      [ 1: #result_flag_lhs #Hresult_lhs #Htype_lhs #Hsim_expr_lhs #Hsim_lvalue_lhs #Hresult_flag_lhs_eq_true
     
    11131112                     whd in match (m_bind ?????);
    11141113                     (* specialize to the actual simplifiable operations. *)
    1115                      cases op in Hop_simplifiable_eq;                     
    1116                      [ 1,2: | *: normalize in ⊢ (% → ?); #H destruct (H) ] #_                     
     1114                     cases op in Hop_simplifiable_eq;                 
     1115                     [ 1,2: | *: normalize in ⊢ (% → ?); #H destruct (H) ] #_
    11171116                     [ 1: lapply (iadd_inv src_sz src_sg val_lhs val_rhs m)
    11181117                     | 2: lapply (isub_inv src_sz src_sg val_lhs val_rhs m) ]
     
    11801179                            ]
    11811180                     ] ] ] ]
    1182 | 19,20,21,22: destruct %1 try @refl
     1181| 17,18,19,20: destruct %1 try @refl
    11831182   elim (Hequiv_lhs ge en m) * #Hexpr_sim_lhs #Hlvalue_sim_lhs #Htype_eq_lhs
    11841183   elim (Hequiv_rhs ge en m) * #Hexpr_sim_rhs #Hlvalue_sim_rhs #Htype_eq_rhs
     
    12081207   ]
    12091208(* Jump to the cast cases *)   
    1210 | 23,30,31,32,33,34,35,36: %1 try @refl
     1209(*| 21,30,31,32,33,34,35,36: *)
     1210| 21,27,28,29,30,31,32,33:
     1211  %1 try @refl
    12111212  [ 1,4,7,10,13,16,19,22: destruct // ]
    12121213  elim (Hcastee_equiv ge en m) * #Hexec_sim #Hlvalue_sim #Htype_eq
     
    12381239  | 2,4,6,8,10,12,14,16: destruct  @SimFailNicely
    12391240  ]
    1240 | 24: destruct inversion (Hcastee_inv ge en m)
     1241| 22: destruct inversion (Hcastee_inv ge en m)
    12411242  [ 1: #result_flag #Hresult_flag #Htype_eq #Hexpr_sim #Hlvalue_sim #Hresult_flag_2
    12421243       <Hresult_flag_2 in Hresult_flag; #Hcontr destruct
     
    12691270                        [ 2,4: * #Heq >Heq #_ elim target_sz //
    12701271                        | 1,3: #Hlt @(size_lt_to_le ?? Hlt) ]
    1271  ] ] ] ] ]
    1272 | 25,27: destruct
     1272 ] ] ] ] ] 
     1273| 23,25: destruct
    12731274      inversion (Hcast2 ge en m)
    12741275      [ 1,3: (* Impossible case.  *)
     
    12981299                ] ]
    12991300      ] ]
    1300 | 26,28: destruct
     1301| 24,26: destruct
    13011302      inversion (Hcast2 ge en m)
    13021303      [ 2,4: (* Impossible case. *)
     
    13221323                 ]
    13231324      ]
     1325(*
    13241326| 29: destruct elim (Hcastee_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
    13251327      @(Inv_eq ???????) //
     
    13361338                     normalize nodelta #H @H
    13371339                ]
    1338            ]
    1339 | 37: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_true #Hdesired_false -Hdesired_eq
     1340           ] *)
     1341| 34: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_true #Hdesired_false -Hdesired_eq
    13401342      inversion (Htrue_inv ge en m)
    13411343      [ 1: #result_flag_true #Hresult_true #Htype_true #Hsim_expr_true #Hsim_lvalue_true #Hresult_flag_true_eq_false
     
    13931395                                           ] ]
    13941396      ] ] ] ] ] ] ]
    1395 | 38,39,40: destruct
     1397| 35,36,37: destruct
    13961398   elim (Hcond_equiv ge en m) * #Hsim_expr_cond #Hsim_vlalue_cond #Htype_cond_eq
    13971399   elim (Htrue_equiv ge en m) * #Hsim_expr_true #Hsim_vlalue_true #Htype_true_eq
     
    14451447   | 2,4,6: @SimFailNicely
    14461448   ]
    1447 | 41,42: destruct
     1449| 38,39: destruct
    14481450    elim (Hlhs_equiv ge en m) * #Hsim_expr_lhs #Hsim_lvalue_lhs #Htype_eq_lhs
    14491451    elim (Hrhs_equiv ge en m) * #Hsim_expr_rhs #Hsim_lvalue_rhs #Htype_eq_rhs
     
    14811483   | 2,4:  @SimFailNicely
    14821484   ]
    1483 | 43: destruct
     1485| 40: destruct
    14841486      cases (type_eq_dec ty (Tint target_sz target_sg))
    14851487      [ 1: #Htype_eq >Htype_eq >type_eq_identity
     
    14901492           %1 // @SimOk #a #H @H
    14911493      ]
    1492 | 44: destruct elim (Hrec_expr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
     1494| 41: destruct elim (Hrec_expr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
    14931495      %1 try @refl
    14941496      [ 1: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
     
    14981500           >Htype_eq
    14991501           cases (typeof rec_expr1) normalize nodelta
    1500            [ 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
    1501            [ 1,2,3,4,5,8,9: @SimFailNicely
    1502            | 6,7: cases Hsim_lvalue
     1502           [ 2: #sz #sg | 3: #ty | 4: #ty #n | 5: #tl #ty | 6: #id #fl | 7: #id #fl | 8: #ty ]
     1503           [ 1,2,3,4,7,8: @SimFailNicely
     1504           | 5,6: cases Hsim_lvalue
    15031505              [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFailNicely
    15041506              | 1,3: cases (exec_lvalue ge en m rec_expr)
     
    15131515           >Htype_eq
    15141516           cases (typeof rec_expr1) normalize nodelta
    1515            [ 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
    1516            [ 1,2,3,4,5,8,9: @SimFailNicely
    1517            | 6,7: cases Hsim_lvalue
     1517           [ 2: #sz #sg | 3: #ty | 4: #ty #n | 5: #tl #ty | 6: #id #fl | 7: #id #fl | 8: #ty ]
     1518           [ 1,2,3,4,7,8: @SimFailNicely
     1519           | 5,6: cases Hsim_lvalue
    15181520              [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFailNicely
    15191521              | 1,3: cases (exec_lvalue ge en m rec_expr)
     
    15261528           ]
    15271529     ]
    1528 | 45: destruct
     1530| 42: destruct
    15291531   inversion (Hinv ge en m)
    15301532   [ 2: #src_sz #src_sg #Htypeof_e1 #Htypeof_e2 #Hsmaller #Hdesired_eq #_
     
    15611563        ]
    15621564   ]
    1563 | 46: destruct elim (Hexpr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
     1565| 43: destruct elim (Hexpr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
    15641566      %1 try @refl
    15651567      [ 1: whd in match (exec_expr ??? (Expr ??));
     
    15741576(* simplify_inside cases. Amounts to propagate a simulation result, except for the /cast/ case which actually calls
    15751577 * simplify_expr *)     
    1576 | 47, 48, 49: (* trivial const_int, const_float and var cases *)
     1578| 44, 45: (* trivial const_int, const_float and var cases *)
    15771579  try @conj try @conj try @refl
    15781580  @SimOk #a #H @H
    1579 | 50: (* Deref case *) destruct
     1581| 46: (* Deref case *) destruct
    15801582  elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
    15811583  try @conj try @conj
     
    15961598         | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk #a #H @H ] ]
    15971599  | 3: // ]
    1598 | 51: (* Addrof *) destruct
     1600| 47: (* Addrof *) destruct
    15991601  elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
    16001602  try @conj try @conj   
     
    16091611  | 2: @SimFailNicely
    16101612  | 3: // ]
    1611 | 52: (* Unop *) destruct
     1613| 48: (* Unop *) destruct
    16121614  elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
    16131615  try @conj try @conj
     
    16231625  | 2: @SimFailNicely             
    16241626  | 3: // ]
    1625 | 53: (* Binop *) destruct
     1627| 49: (* Binop *) destruct
    16261628  elim (Hequiv_lhs ge en m) * #Hsim_expr_lhs #Hsim_lvalue_lhs #Htype_eq_lhs
    16271629  elim (Hequiv_rhs ge en m) * #Hsim_expr_rhs #Hsim_lvalue_rhs #Htype_eq_rhs
     
    16501652  | 3: //
    16511653  ]
    1652 | 54: (* Cast, fallback case *)
     1654| 50: (* Cast, fallback case *)
    16531655  try @conj try @conj try @refl
    16541656  @SimOk #a #H @H
    1655 | 55: (* Cast, success case *) destruct
     1657| 51: (* Cast, success case *) destruct
    16561658  inversion (Htrans_inv ge en m)
    16571659  [ 1: (* contradiction *)
     
    16801682      ]
    16811683  ]
    1682 | 56: (* Cast, "failure" case *) destruct
     1684| 52: (* Cast, "failure" case *) destruct
    16831685  inversion (Htrans_inv ge en m)
    16841686  [ 2: (* contradiction *)
     
    17001702       ]
    17011703  ]
    1702 | 57,58,59,60,61,62,63,64,68:       
     1704| 53,54,55,56,57,58,59,63:
    17031705  try @conj try @conj try @refl
    17041706  @SimOk #a #H @H
    1705 | 65: destruct
     1707| 60: destruct
    17061708  elim (Hequiv_cond ge en m) * #Hsim_exec_cond #Hsim_lvalue_cond #Htype_eq_cond
    17071709  elim (Hequiv_iftrue ge en m) * #Hsim_exec_true #Hsim_lvalue_true #Htype_eq_true
     
    17461748  | 3: //
    17471749  ]
    1748 | 66,67: destruct
     1750| 61,62: destruct
    17491751  elim (Hequiv_lhs ge en m) * #Hsim_exec_lhs #Hsim_lvalue_lhs #Htype_eq_lhs
    17501752  elim (Hequiv_rhs ge en m) * #Hsim_exec_rhs #Hsim_lvalue_rhs #Htype_eq_rhs
     
    17771779  | 3,6: //
    17781780  ]
    1779 | 69: (* record field *) destruct
     1781| 64: (* record field *) destruct
    17801782   elim (Hequiv_rec ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
    17811783   try @conj try @conj   
     
    17851787   whd in match (exec_lvalue' ??? (Efield rec_expr1 f) ty); 
    17861788   [ 1: >Htype_eq cases (typeof rec_expr1) normalize nodelta
    1787        [ 2: #sz #sg | 3: #fl | 4: #ty' | 5: #ty #n | 6: #tl #ty'
    1788        | 7: #id #fl | 8: #id #fl | 9: #id ]
     1789       [ 2: #sz #sg | 3: #ty' | 4: #ty #n | 5: #tl #ty'
     1790       | 6: #id #fl | 7: #id #fl | 8: #id ]
    17891791       try (@SimFailNicely)
    17901792       cases Hsim_lvalue
     
    17971799   | 2: (* Note: identical to previous case. Too lazy to merge and manually shift indices. *)
    17981800       >Htype_eq cases (typeof rec_expr1) normalize nodelta
    1799        [ 2: #sz #sg | 3: #fl | 4: #ty' | 5: #ty #n | 6: #tl #ty'
    1800        | 7: #id #fl | 8: #id #fl | 9: #id ]
     1801       [ 2: #sz #sg | 3: #ty' | 4: #ty #n | 5: #tl #ty'
     1802       | 6: #id #fl | 7: #id #fl | 8: #id ]
    18011803       try (@SimFailNicely)
    18021804       cases Hsim_lvalue
     
    18081810       ]
    18091811   | 3: // ]
    1810 | 70: (* cost label *) destruct
     1812| 65: (* cost label *) destruct
    18111813   elim (Hequiv ge en m) *  #Hsim_expr #Hsim_lvalue #Htype_eq
    18121814   try @conj try @conj
     
    19261928
    19271929definition expr_lvalue_ind_combined ≝
    1928 λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx.
     1930λP,Q,ci,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx.
    19291931conj ??
    1930  (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx)
    1931  (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx).
     1932 (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx)
     1933 (lvalue_expr_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx).
    19321934 
    19331935lemma simulation_transitive : ∀A,r0,r1,r2. res_sim A r0 r1 → res_sim A r1 r2 → res_sim A r0 r2.
     
    19441946#ge #ge' #en #m #Hrelated @expr_lvalue_ind_combined
    19451947[ 1: #sz #ty #i @SimOk #a normalize //
    1946 | 2: #ty #f @SimOk #a normalize //
    1947 | 3: *
    1948     [ 1: #sz #i | 2: #fl | 3: #id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
    1949     | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
     1948| 2: *
     1949    [ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
     1950    | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
    19501951    #ty #Hsim_lvalue try //
    19511952    whd in match (Plvalue ???);
     
    19591960              @SimOk // ]
    19601961    ]
    1961 | 4: #v #ty whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????);
     1962| 3: #v #ty whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????);
    19621963     cases (lookup SymbolTag block en v) normalize nodelta
    19631964     [ 2: #block @SimOk //
    19641965     | 1: elim Hrelated #Hsymbol #_ #_ >(Hsymbol v) @SimOk //
    19651966     ]
    1966 | 5: #e #ty #Hsim_expr whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????);
     1967| 4: #e #ty #Hsim_expr whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????);
    19671968     cases Hsim_expr
    19681969     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     
    19721973                @SimOk // ]
    19731974     ]
    1974 | 6: #ty #ed #ty' #Hsim_lvalue
     1975| 5: #ty #ed #ty' #Hsim_lvalue
    19751976     whd in match (exec_expr ????); whd in match (exec_expr ????);
    19761977     whd in match (exec_lvalue ????); whd in match (exec_lvalue ????);
     
    19821983              @SimOk // ]
    19831984    ]
    1984 | 7: #ty #op #e #Hsim whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
     1985| 6: #ty #op #e #Hsim whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
    19851986     cases Hsim
    19861987     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     
    19901991               @SimOk // ]
    19911992     ]
    1992 | 8: #ty #op #e1 #e2 #Hsim1 #Hsim2 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
     1993| 7: #ty #op #e1 #e2 #Hsim1 #Hsim2 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
    19931994     cases Hsim1
    19941995     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     
    20052006          ]
    20062007     ]
    2007 | 9: #ty #cast_ty #e #Hsim whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
     2008| 8: #ty #cast_ty #e #Hsim whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
    20082009     cases Hsim
    20092010     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     
    20132014               @SimOk // ]
    20142015     ] (* mergeable with 7 modulo intros *)
    2015 | 10: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
     2016| 9: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
    20162017     cases Hsim1
    20172018     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     
    20312032          ]
    20322033     ]
    2033 | 11,12: #ty #e1 #e2 #Hsim1 #Hsim2 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
     2034| 10,11: #ty #e1 #e2 #Hsim1 #Hsim2 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
    20342035     cases Hsim1
    20352036     [ 2,4: * #error #Hfail >Hfail @SimFailNicely
     
    20522053          ]
    20532054     ]
    2054 | 13: #ty #sizeof_ty @SimOk normalize //
    2055 | 14: #ty #e #ty' #field #Hsim_lvalue
     2055| 12: #ty #sizeof_ty @SimOk normalize //
     2056| 13: #ty #e #ty' #field #Hsim_lvalue
    20562057      whd in match (exec_lvalue' ? en m (Efield ??) ty);
    20572058      whd in match (exec_lvalue' ge' en m (Efield ??) ty);
    20582059      normalize in match (typeof (Expr ??));
    20592060      cases ty' in Hsim_lvalue; normalize nodelta
    2060       [ 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
    2061       | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
     2061      [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     2062      | #structname #fieldspec | #unionname #fieldspec | #id ]
    20622063      #Hsim_lvalue
    20632064      try (@SimFail /2 by ex_intro/)
     
    20712072                    @SimOk /2 by ex_intro/ ]
    20722073      ]
    2073 | 15: #ty #lab #e #Hsim
     2074| 14: #ty #lab #e #Hsim
    20742075      whd in match (exec_expr ??? (Expr ??));
    20752076      whd in match (exec_expr ??? (Expr ??));
     
    20812082               @SimOk // ]
    20822083     ] (* cf case 7, again *)
    2083 | 16: *
    2084       [ 1: #sz #i | 2: #fl | 3: #id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
    2085       | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
    2086       #ty normalize in match (is_not_lvalue ?);
    2087       [ 3,4,13: #Habsurd @(False_ind … Habsurd) ] #_
    2088       @SimFailNicely
     2084| 15: *
     2085    [ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
     2086    | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
     2087    #ty normalize in match (is_not_lvalue ?);
     2088    [ 2,3,12: #Habsurd @(False_ind … Habsurd) ] #_
     2089    @SimFailNicely
    20892090] qed.
    20902091
     
    20952096#ge #ge' #en #m #Hrelated #e whd in match (simplify_e ?);
    20962097cases e #ed #ty cases ed
    2097 [ 1: #sz #i | 2: #fl | 3: #id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
    2098 | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
     2098[ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
     2099| #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
    20992100elim (simplify_inside (Expr ??)) #e' #Hconservation whd in Hconservation; @conj lapply (Hconservation ge en m)
    21002101* * try //
     
    21112112#ge #ge' #en #m #Hrelated #e whd in match (simplify_e ?);
    21122113cases e #ed #ty cases ed
    2113 [ 1: #sz #i | 2: #fl | 3: #id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
    2114 | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
     2114[ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
     2115| #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
    21152116elim (simplify_inside (Expr ??)) #e' #Hconservation whd in Hconservation; @conj lapply (Hconservation ge en m)
    21162117* * try //
     
    24622463                    | 2: #fd #args #k0 #k0' #m0 #Hcont_cast0 #Habsurd destruct (Habsurd)
    24632464                    | 3: #res #k0 #k0' #m0 #Hcont_cast #Habsurd destruct (Habsurd)
    2464                     | 4: #r #Habsurd destruct (Habsurd) ]                   
    2465                | 3,4,9: #irrelevant #Habsurd destruct
     2465                    | 4: #r #Habsurd destruct (Habsurd) ]
     2466               | 3,8: #irrelevant #Habsurd destruct
    24662467               | *: #irrelevant1 #irrelevant2 #Habsurd destruct ]
    24672468          | 2: (* Kseq stm' k' *)
     
    25282529                                  (free_list m (blocks_of_env en)))} @conj
    25292530                    [ 1: // | 2: %3 @cc_call // ]                                 
    2530                | 3,4,9: #irrelevant #Habsurd destruct (Habsurd)
     2531               | 3,8: #irrelevant #Habsurd destruct (Habsurd)
    25312532               | *: #irrelevant1 #irrelevant2 #Habsurd destruct (Habsurd) ]
    25322533           ]
     
    27562757          [ 1: >fn_return_simplify cases (fn_return f) normalize nodelta
    27572758               whd in match (ret ??) in ⊢ (% → %);
    2758                [ 2: #sz #sg | 3: #fl | 4: #ty' | 5: #ty #n | 6: #tl #ty'
    2759                | 7: #id #fl | 8: #id #fl | 9: #id ]
     2759               [ | #sz #sg | #ty' | #ty #n | #tl #ty'
     2760               | #id #fl | #id #fl | #id ]
    27602761               #H destruct (H)
    27612762               %{(Returnstate Vundef (call_cont k') (free_list m (blocks_of_env en)))}
     
    28972898     whd in match (exec_step ??) in ⊢ (% → %);
    28982899     #Habsurd destruct (Habsurd)
    2899 ] qed. 
     2900] qed.
Note: See TracChangeset for help on using the changeset viewer.