Changeset 2219 for src


Ignore:
Timestamp:
Jul 19, 2012, 6:45:52 PM (9 years ago)
Author:
campbell
Message:

Speed up cast simplification proof checking a bit.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/Clight/SimplifyCasts.ma

    r2184 r2219  
    214214| SimOk   :  (∀a:A. r1 = OK ? a → r2 = OK ? a) → res_sim A r1 r2
    215215| SimFail : (∃err. r1 = Error ? err) → res_sim A r1 r2.
     216
     217(* Trick to reduce checking time by eliminating a load of costly automation.
     218   It would be nice to do this by refactoring the type and code instead, but we
     219   don't want to spend lots of time on something that already works. *)
     220
     221lemma SimFailNicely : ∀A,err,r2. res_sim A (Error ? err) r2.
     222#A #err #r2 @SimFail %{err} %
     223qed.
    216224
    217225(* Invariant of simplify_expr *)
    … …  
    11261134      cases Hexpr_sim
    11271135      [ 2: (* Case where the evaluation of e1 as an expression fails *)     
    1128         normalize * #err #Hfail >Hfail normalize nodelta @(SimFail ???) /2 by ex_intro/
     1136        normalize * #err #Hfail >Hfail normalize nodelta @SimFailNicely
    11291137      | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *)
    11301138        #Hsim %1 * #val #trace normalize #Hstep
    … …  
    11561164      cases Hexpr_sim
    11571165      [ 2: (* Case where the evaluation of e1 as an lvalue fails *)
    1158         normalize * #err #Hfail >Hfail normalize nodelta @(SimFail ???) /2 by ex_intro/
     1166        normalize * #err #Hfail >Hfail normalize nodelta @SimFailNicely
    11591167      | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *)
    11601168        #Hsim %1 * * #block #offset #trace normalize #Hstep       
    … …  
    11831191      cases Hlvalue_sim
    11841192      [ 2: (* Case where the evaluation of e1 as an expression fails *)     
    1185         * #err #Hfail @SimFail whd in match (exec_expr ????); >Hfail normalize nodelta /2 by ex_intro/
     1193        * #err #Hfail whd in match (exec_expr ????); >Hfail @SimFailNicely
    11861194      | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *)
    11871195        #Hsim %1 * #val #trace whd in match (exec_expr ????); #Hstep
    … …  
    12061214     ]
    12071215    | 2: (* Proving preservation of the semantics of lvalues. *)
    1208          @SimFail /2 by ex_intro/
     1216         @SimFailNicely
    12091217    ]
    12101218| 17: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
    … …  
    12121220           whd in match (exec_expr ge en m (Expr ??));
    12131221           cases Hexpr_sim           
    1214            [ 2: * #error #Hexec >Hexec normalize nodelta @SimFail /2 by ex_intro/
     1222           [ 2: * #error #Hexec >Hexec normalize nodelta @SimFailNicely
    12151223           | 1: cases (exec_expr ge en m e1)
    1216                 [ 2: #error #Hexec normalize nodelta @SimFail /2 by ex_intro/
     1224                [ 2: #error #Hexec normalize nodelta @SimFailNicely
    12171225                | 1: * #val #trace #Hexec
    12181226                     >(Hexec ? (refl ? (OK ? 〈val,trace〉)))
    … …  
    12201228                ]
    12211229           ]
    1222       | 2: @SimFail /2 by ex_intro/
     1230      | 2: @SimFailNicely
    12231231      ]
    12241232| 18: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_lhs #Hdesired_rhs -Hdesired_eq
    … …  
    13231331      whd in match (exec_expr ????); whd in match (exec_expr ????);
    13241332      cases Hexpr_sim_lhs
    1325       [ 2,4,6,8: * #error #Herror >Herror @SimFail /2 by refl, ex_intro/
     1333      [ 2,4,6,8: * #error #Herror >Herror @SimFailNicely
    13261334      | *: cases (exec_expr ge en m lhs)
    1327            [ 2,4,6,8: #error #_ @SimFail /2 by refl, ex_intro/
     1335           [ 2,4,6,8: #error #_ @SimFailNicely
    13281336           | *: * #lval #ltrace #Hsim_lhs normalize nodelta         
    13291337                cases Hexpr_sim_rhs
    1330                 [ 2,4,6,8: * #error #Herror >Herror @SimFail /2 by refl, ex_intro/
     1338                [ 2,4,6,8: * #error #Herror >Herror @SimFailNicely
    13311339                | *: cases (exec_expr ge en m rhs)
    1332                      [ 2,4,6,8: #error #_  @SimFail /2 by refl, ex_intro/
     1340                     [ 2,4,6,8: #error #_  @SimFailNicely
    13331341                     | *: * #rval #rtrace #Hsim_rhs
    13341342                          whd in match (exec_expr ??? (Expr (Ebinop ???) ?));
    … …  
    13421350           ]
    13431351      ]
    1344    | *: @SimFail /2 by refl, ex_intro/ 
     1352   | *: @SimFailNicely
    13451353   ]
    13461354(* Jump to the cast cases *)   
    … …  
    13501358  (* exec_expr simulation *)
    13511359  [ 1,3,5,7,9,11,13,15: cases Hexec_sim
    1352        [ 2,4,6,8,10,12,14,16: destruct * #error #Hexec_fail @SimFail whd in match (exec_expr ge en m ?);
    1353             >Hexec_fail /2 by refl, ex_intro/
     1360       [ 2,4,6,8,10,12,14,16: destruct * #error #Hexec_fail whd in match (exec_expr ge en m ?);
     1361            >Hexec_fail @SimFailNicely
    13541362       | 1,3,5,7,9,11,13,15: #Hsim @SimOk * #val #trace <Hexpr_eq >Hdesc_eq
    13551363            whd in match (exec_expr ge en m ?); #Hstep
    … …  
    13731381            ]   
    13741382      ]
    1375   | 2,4,6,8,10,12,14,16: destruct  @SimFail /2 by refl, ex_intro/
     1383  | 2,4,6,8,10,12,14,16: destruct  @SimFailNicely
    13761384  ]
    13771385| 24: destruct inversion (Hcastee_inv ge en m)
    … …  
    14161424           #src_sz #src_sg #Htype_castee #Htype_castee2 #Hsmaller_eval #_ #Hinv_eq
    14171425           @(Inv_eq ???????) //
    1418            [ 1,4: >Htype_castee2 //
    1419            | 2,5: (* Prove simulation for exec_expr *)
     1426           [ 1,3: >Htype_castee2 //
     1427           | 2,4: (* Prove simulation for exec_expr *)
    14201428               whd in match (exec_expr ??? (Expr ??));
    14211429               cases (exec_expr ge en m castee) in Hsmaller_eval;
    14221430               [ 2,4: (* erroneous evaluation of the original expression *)
    1423                      #error #Hsmaller_eval @SimFail @(ex_intro … error) //
     1431                     #error #Hsmaller_eval @SimFailNicely
    14241432               | 1,3: * #val #trace normalize nodelta >Htype_castee
    14251433                      lapply (exec_cast_inv val src_sz src_sg cast_sz cast_sg m)
    14261434                      cases (exec_cast m val (Tint src_sz src_sg) (Tint cast_sz cast_sg))
    1427                       [ 2,4: #error #_ #_ @SimFail /2 by ex_intro/
     1435                      [ 2,4: #error #_ #_ @SimFailNicely
    14281436                      | 1,3: #result #Hinversion elim (Hinversion result (refl ??))
    14291437                             #val_int * #Hval_eq #Hresult_eq
    … …  
    14341442                                    destruct @SimOk normalize #a #H @H ]
    14351443                ] ]
    1436            | 3,6: @SimFail /2 by refl, ex_intro/
    14371444      ] ]
    14381445| 26,28: destruct
    … …  
    14471454            #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #_ #Hinv
    14481455            @(Inv_eq ???????) //
    1449             [ 1,3: (* Simulation for exec_expr *)
    14501456                 whd in match (exec_expr ??? (Expr ??));
    14511457                 whd in match (exec_expr ??? (Expr ??));
    14521458                 cases Hsim_expr
    1453                  [ 2,4: * #error #Hexec_err >Hexec_err @SimFail @(ex_intro … error) //
     1459                 [ 2,4: * #error #Hexec_err >Hexec_err @SimFailNicely
    14541460                 | 1,3: #Hexec_ok
    14551461                      cases (exec_expr ge en m castee) in Hexec_ok;
    1456                       [ 2,4: #error #Hsim @SimFail normalize nodelta /2/
     1462                      [ 2,4: #error #Hsim @SimFailNicely
    14571463                      | 1,3: * #val #trace #Hsim normalize nodelta
    14581464                           >Htype_eq >(Hsim 〈val,trace〉 (refl ? (OK ? 〈val,trace〉))) normalize nodelta
    … …  
    14601466                      ]
    14611467                 ]
    1462             | 2,4: @SimFail /2 by refl, ex_intro/
    1463             ]
    14641468      ]
    14651469| 29: destruct elim (Hcastee_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
    … …  
    14671471      whd in match (exec_expr ??? (Expr ??));
    14681472      whd in match (exec_expr ??? (Expr ??));
    1469       [ 1: cases Hsim_expr
    1470            [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by refl, ex_intro/
     1473      cases Hsim_expr
     1474           [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
    14711475           | 1: #Hexec_ok @SimOk * #val #trace
    14721476                cases (exec_expr ge en m castee) in Hexec_ok;
    … …  
    14781482                ]
    14791483           ]
    1480       | 2: @SimFail /2 by refl, ex_intro/
    1481       ]
    14821484| 37: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_true #Hdesired_false -Hdesired_eq
    14831485      inversion (Htrue_inv ge en m)
    … …  
    15431545   [ 1,3,5: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
    15441546            cases (exec_expr ge en m cond) in Hsim_expr_cond;
    1545             [ 2,4,6: #error #_ @SimFail /2 by ex_intro/
     1547            [ 2,4,6: #error #_ @SimFailNicely
    15461548            | 1,3,5: * #cond_val #cond_trace normalize nodelta
    15471549                cases (exec_expr ge en m cond1)
    … …  
    15551557                             #Hcond_eq normalize nodelta destruct (Hcond_eq)
    15561558                             >Htype_cond_eq cases (exec_bool_of_val cond_val (typeof cond1))
    1557                              [ 2,4,6: #error @SimFail normalize /2 by refl, ex_intro /
     1559                             [ 2,4,6: #error @SimFailNicely
    15581560                             | 1,3,5: * (* true branch *)
    15591561                                [ 1,3,5:
    … …  
    15611563                                 normalize in match (m_bind ?????);
    15621564                                 cases Hsim_expr_true
    1563                                  [ 2,4,6: * #error #Hexec_fail >Hexec_fail @SimFail /2 by refl, ex_intro/
     1565                                 [ 2,4,6: * #error #Hexec_fail >Hexec_fail @SimFailNicely
    15641566                                 | 1,3,5: cases (exec_expr ge en m iftrue)
    1565                                      [ 2,4,6: #error #_ normalize nodelta @SimFail /2 by refl, ex_intro/
     1567                                     [ 2,4,6: #error #_ normalize nodelta @SimFailNicely
    15661568                                     | 1,3,5: * #val_true #trace_true normalize nodelta #Hsim
    15671569                                              >(Hsim 〈val_true,trace_true〉 (refl ? (OK ? 〈val_true,trace_true〉)))
    … …  
    15731575                                 normalize in match (m_bind ?????);                             
    15741576                                 cases Hsim_expr_false
    1575                                  [ 2,4,6: * #error #Hexec_fail >Hexec_fail normalize nodelta @SimFail /2 by refl, ex_intro/
     1577                                 [ 2,4,6: * #error #Hexec_fail >Hexec_fail normalize nodelta @SimFailNicely
    15761578                                 | 1,3,5: cases (exec_expr ge en m iffalse)
    1577                                      [ 2,4,6: #error #_ normalize nodelta @SimFail /2 by refl, ex_intro/
     1579                                     [ 2,4,6: #error #_ normalize nodelta @SimFailNicely
    15781580                                     | 1,3,5: * #val_false #trace_false normalize nodelta #Hsim
    15791581                                              >(Hsim 〈val_false,trace_false〉 (refl ? (OK ? 〈val_false,trace_false〉)))
    … …  
    15861588                ]
    15871589            ]
    1588    | 2,4,6: @SimFail /2 by ex_intro/           
     1590   | 2,4,6: @SimFailNicely
    15891591   ]
    15901592| 41,42: destruct
    … …  
    15951597           whd in match (exec_expr ??? (Expr ??));
    15961598           cases Hsim_expr_lhs
    1597            [ 2,4: * #error #Hexec_fail >Hexec_fail normalize nodelta @SimFail /2 by refl, ex_intro/
     1599           [ 2,4: * #error #Hexec_fail >Hexec_fail normalize nodelta @SimFailNicely
    15981600           | 1,3: cases (exec_expr ge en m lhs)
    1599               [ 2,4: #error #_ @SimFail /2 by refl, ex_intro/
     1601              [ 2,4: #error #_ @SimFailNicely
    16001602              | 1,3: * #lhs_val #lhs_trace #Hsim normalize nodelta
    16011603                     >(Hsim 〈lhs_val,lhs_trace〉 (refl ? (OK ? 〈lhs_val,lhs_trace〉)))
    16021604                     normalize nodelta >Htype_eq_lhs
    16031605                     cases (exec_bool_of_val lhs_val (typeof lhs1))
    1604                        [ 2,4: #error normalize @SimFail /2 by refl, ex_intro/
     1606                       [ 2,4: #error normalize @SimFailNicely
    16051607                     | 1,3: *
    16061608                         whd in match (m_bind ?????);
    … …  
    16091611                            @SimOk #a #H @H
    16101612                         | 1,4: cases Hsim_expr_rhs
    1611                             [ 2,4: * #error #Hexec >Hexec @SimFail /2 by refl, ex_intro/
     1613                            [ 2,4: * #error #Hexec >Hexec @SimFailNicely
    16121614                            | 1,3: cases (exec_expr ge en m rhs)
    1613                                 [ 2,4: #error #_ @SimFail /2 by refl, ex_intro/
     1615                                [ 2,4: #error #_ @SimFailNicely
    16141616                                | 1,3: * #rhs_val #rhs_trace -Hsim #Hsim
    16151617                                       >(Hsim 〈rhs_val,rhs_trace〉 (refl ? (OK ? 〈rhs_val,rhs_trace〉)))
    … …  
    16221624              ]
    16231625          ]
    1624    | 2,4:  @SimFail /2 by ex_intro/
     1626   | 2,4:  @SimFailNicely
    16251627   ]
    16261628| 43: destruct
    … …  
    16421644           cases (typeof rec_expr1) normalize nodelta
    16431645           [ 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
    1644            [ 1,2,3,4,5,8,9: @SimFail /2 by refl, ex_intro/
     1646           [ 1,2,3,4,5,8,9: @SimFailNicely
    16451647           | 6,7: cases Hsim_lvalue
    1646               [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/
     1648              [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFailNicely
    16471649              | 1,3: cases (exec_lvalue ge en m rec_expr)
    1648                  [ 2,4: #error #_ normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/
     1650                 [ 2,4: #error #_ normalize in ⊢ (??%?); @SimFailNicely
    16491651                 | 1,3: #a #Hsim >(Hsim a (refl ? (OK ? a)))
    16501652                         whd in match (m_bind ?????);
    … …  
    16571659           cases (typeof rec_expr1) normalize nodelta
    16581660           [ 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
    1659            [ 1,2,3,4,5,8,9: @SimFail /2 by refl, ex_intro/
     1661           [ 1,2,3,4,5,8,9: @SimFailNicely
    16601662           | 6,7: cases Hsim_lvalue
    1661               [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/
     1663              [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFailNicely
    16621664              | 1,3: cases (exec_lvalue ge en m rec_expr)
    1663                  [ 2,4: #error #_ normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/
     1665                 [ 2,4: #error #_ normalize in ⊢ (??%?); @SimFailNicely
    16641666                 | 1,3: #a #Hsim >(Hsim a (refl ? (OK ? a)))
    16651667                         whd in match (m_bind ?????);
    … …  
    16941696             whd in match (exec_expr ??? (Expr ??));
    16951697             cases Hsim_expr
    1696              [ 2: * #error #Hexec_error >Hexec_error @SimFail /2 by ex_intro/
     1698             [ 2: * #error #Hexec_error >Hexec_error @SimFailNicely
    16971699             | 1: cases (exec_expr ge en m e1)
    1698                   [ 2: #error #_ @SimFail /2 by ex_intro/
     1700                  [ 2: #error #_ @SimFailNicely
    16991701                  | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #He2_exec >He2_exec
    17001702                        @SimOk #a #H @H
    17011703                  ]
    17021704             ]
    1703         | 3: @SimFail /2 by ex_intro/
     1705        | 3: @SimFailNicely
    17041706        ]
    17051707   ]
    … …  
    17091711           whd in match (exec_expr ??? (Expr ??));
    17101712           cases Hsim_expr
    1711            [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
     1713           [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
    17121714           | 1: cases (exec_expr ge en m e1)
    1713                 [ 2: #error #_ @SimFail /2 by ex_intro/
     1715                [ 2: #error #_ @SimFailNicely
    17141716                | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hsim2 >Hsim2 @SimOk #a #H @H ]
    17151717           ]
    … …  
    17341736  [ 1,2: 
    17351737    cases Hsim_expr
    1736     [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
     1738    [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFailNicely
    17371739    | 1,3: cases (exec_expr ge en m e1)
    1738          [ 2,4: #error #_ @SimFail /2 by ex_intro/
     1740         [ 2,4: #error #_ @SimFailNicely
    17391741         | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk #a #H @H ] ]
    17401742  | 3: // ]
    … …  
    17461748    whd in match (exec_expr ??? (Expr ??));
    17471749    cases Hsim_lvalue
    1748     [ 2: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/
     1750    [ 2: * #error #Hlvalue_fail >Hlvalue_fail @SimFailNicely
    17491751    | 1: cases (exec_lvalue ge en m e1)
    1750        [ 2: #error #_ @SimFail /2 by ex_intro/
     1752       [ 2: #error #_ @SimFailNicely
    17511753       | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk #a #H @H ] ]
    1752   | 2: @SimFail /2 by ex_intro/
     1754  | 2: @SimFailNicely
    17531755  | 3: // ]
    17541756| 52: (* Unop *) destruct
    … …  
    17591761    whd in match (exec_expr ??? (Expr ??));
    17601762    cases Hsim_expr
    1761     [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
     1763    [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
    17621764    | 1: cases (exec_expr ge en m e1)
    1763          [ 2: #error #_ @SimFail /2 by ex_intro/
     1765         [ 2: #error #_ @SimFailNicely
    17641766         | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk
    17651767              >Htype_eq #a #H @H ] ]
    1766   | 2: @SimFail /2 by ex_intro/             
     1768  | 2: @SimFailNicely             
    17671769  | 3: // ]
    17681770| 53: (* Binop *) destruct
    … …  
    17741776    whd in match (exec_expr ??? (Expr ??));
    17751777    cases Hsim_expr_lhs
    1776     [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
     1778    [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
    17771779    | 1: cases (exec_expr ge en m lhs)
    1778          [ 2: #error #_ @SimFail /2 by ex_intro/
     1780         [ 2: #error #_ @SimFailNicely
    17791781         | 1: #lhs_value #Hsim_lhs cases Hsim_expr_rhs
    1780               [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
     1782              [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
    17811783              | 1: cases (exec_expr ge en m rhs)
    1782                    [ 2: #error #_ @SimFail /2 by ex_intro/
     1784                   [ 2: #error #_ @SimFailNicely
    17831785                   | 1: #rhs_value #Hsim_rhs
    17841786                        lapply (Hsim_lhs lhs_value (refl ? (OK ? lhs_value)))
    … …  
    17901792         ]
    17911793    ]
    1792   | 2: @SimFail /2 by ex_intro/
     1794  | 2: @SimFailNicely
    17931795  | 3: //
    17941796  ]
    … …  
    18051807       [ 1: whd in match (exec_expr ??? (Expr ??));
    18061808            cases (exec_expr ge en m castee) in Hsmaller;
    1807             [ 2: #error #_ @SimFail /2 by ex_intro/
     1809            [ 2: #error #_ @SimFailNicely
    18081810            | 1: * #val #trace normalize nodelta >Hsrc_type_eq
    18091811                 lapply (exec_cast_inv val src_sz src_sg cast_sz cast_sg m)
    18101812                 cases (exec_cast m val ??)
    1811                  [ 2: #error #_ #_ @SimFail /2 by ex_intro/
     1813                 [ 2: #error #_ #_ @SimFailNicely
    18121814                 | 1: #result #Hinversion elim (Hinversion result (refl ??))
    18131815                      #val_int * #Hval_eq #Hcast
    … …  
    18191821                      ]
    18201822             ]
    1821       | 2: @SimFail /2 by ex_intro/
     1823      | 2: @SimFailNicely
    18221824      | 3: >Htarget_type_eq //
    18231825      ]
    … …  
    18331835            whd in match (exec_expr ??? (Expr ??));
    18341836            cases Hsim_expr
    1835             [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
     1837            [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
    18361838            | 1: cases (exec_expr ??? castee)
    1837                  [ 2: #error #_ @SimFail /2 by ex_intro/
     1839                 [ 2: #error #_ @SimFailNicely
    18381840                 | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec_ok >Hexec_ok
    18391841                       @SimOk >Htype_eq #a #H @H ]
    18401842            ]
    1841        | 2: @SimFail /2 by ex_intro/
     1843       | 2: @SimFailNicely
    18421844       | 3: //
    18431845       ]
    … …  
    18541856       whd in match (exec_expr ??? (Expr ??));
    18551857       cases Hsim_exec_cond
    1856        [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
     1858       [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
    18571859       | 1: cases (exec_expr ??? cond)
    1858             [ 2: #error #_ @SimFail /2 by ex_intro/
     1860            [ 2: #error #_ @SimFailNicely
    18591861            | 1: * #condb #condtrace #Hcond_sim lapply (Hcond_sim 〈condb, condtrace〉 (refl ? (OK ? 〈condb, condtrace〉)))
    18601862                 #Hcond_ok >Hcond_ok >Htype_eq_cond
    18611863                 normalize nodelta
    18621864                 cases (exec_bool_of_val condb (typeof cond1))
    1863                  [ 2: #error @SimFail /2 by ex_intro/
     1865                 [ 2: #error @SimFailNicely
    18641866                 | 1: * whd in match (m_bind ?????); whd in match (m_bind ?????);
    18651867                      normalize nodelta
    18661868                      [ 1: (* true branch taken *)
    18671869                           cases Hsim_exec_true
    1868                            [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
     1870                           [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
    18691871                           | 1: cases (exec_expr ??? iftrue)
    1870                                 [ 2: #error #_ @SimFail /2 by ex_intro/
     1872                                [ 2: #error #_ @SimFailNicely
    18711873                                | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H
    18721874                                     @SimOk #a #H @H
    … …  
    18751877                      | 2: (* false branch taken *)
    18761878                           cases Hsim_exec_false
    1877                            [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
     1879                           [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
    18781880                           | 1: cases (exec_expr ??? iffalse)
    1879                                 [ 2: #error #_ @SimFail /2 by ex_intro/
     1881                                [ 2: #error #_ @SimFailNicely
    18801882                                | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H
    18811883                                     @SimOk #a #H @H
    … …  
    18861888           ]
    18871889      ]
    1888   | 2: @SimFail /2 by ex_intro/
     1890  | 2: @SimFailNicely
    18891891  | 3: //
    18901892  ]
    … …  
    18961898  whd in match (exec_expr ??? (Expr ??));
    18971899  [ 1,4: cases Hsim_exec_lhs
    1898        [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
     1900       [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFailNicely
    18991901       | 1,3: cases (exec_expr ??? lhs)
    1900             [ 2,4: #error #_ @SimFail /2 by ex_intro/
     1902            [ 2,4: #error #_ @SimFailNicely
    19011903            | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hlhs >Hlhs >Htype_eq_lhs
    19021904                   normalize nodelta elim a #lhs_val #lhs_trace
    19031905                   cases (exec_bool_of_val lhs_val (typeof lhs1))
    1904                    [ 2,4: #error @SimFail /2 by ex_intro/
     1906                   [ 2,4: #error @SimFailNicely
    19051907                   | 1,3: * whd in match (m_bind ?????); whd in match (m_bind ?????);
    19061908                        [ 2,3: @SimOk //
    19071909                        | 1,4: cases Hsim_exec_rhs
    1908                             [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
     1910                            [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFailNicely
    19091911                            | 1,3: cases (exec_expr ??? rhs)
    1910                                [ 2,4: #error #_ @SimFail /2 by ex_intro/
     1912                               [ 2,4: #error #_ @SimFailNicely
    19111913                               | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrhs >Hrhs >Htype_eq_rhs
    19121914                                    @SimOk #a #H @H
    … …  
    19171919             ]
    19181920        ]
    1919   | 2,5: @SimFail /2 by ex_intro/
     1921  | 2,5: @SimFailNicely
    19201922  | 3,6: //
    19211923  ]
    … …  
    19301932       [ 2: #sz #sg | 3: #fl | 4: #ty' | 5: #ty #n | 6: #tl #ty'
    19311933       | 7: #id #fl | 8: #id #fl | 9: #id ]
    1932        try (@SimFail /2 by ex_intro/)
     1934       try (@SimFailNicely)
    19331935       cases Hsim_lvalue
    1934        [ 2,4: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/
     1936       [ 2,4: * #error #Hlvalue_fail >Hlvalue_fail @SimFailNicely
    19351937       | 1,3: cases (exec_lvalue ge en m rec_expr)
    1936             [ 2,4: #error #_ @SimFail /2 by ex_intro/
     1938            [ 2,4: #error #_ @SimFailNicely
    19371939            | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec >Hexec
    19381940                   @SimOk #a #H @H ]
    … …  
    19421944       [ 2: #sz #sg | 3: #fl | 4: #ty' | 5: #ty #n | 6: #tl #ty'
    19431945       | 7: #id #fl | 8: #id #fl | 9: #id ]
    1944        try (@SimFail /2 by ex_intro/)
     1946       try (@SimFailNicely)
    19451947       cases Hsim_lvalue
    1946        [ 2,4: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/
     1948       [ 2,4: * #error #Hlvalue_fail >Hlvalue_fail @SimFailNicely
    19471949       | 1,3: cases (exec_lvalue ge en m rec_expr)
    1948             [ 2,4: #error #_ @SimFail /2 by ex_intro/
     1950            [ 2,4: #error #_ @SimFailNicely
    19491951            | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec >Hexec
    19501952                   @SimOk #a #H @H ]
    … …  
    19581960   [ 1:
    19591961     cases Hsim_expr
    1960      [ 2: * #error #Hexec >Hexec @SimFail /2 by ex_intro/
     1962     [ 2: * #error #Hexec >Hexec @SimFailNicely
    19611963     | 1: cases (exec_expr ??? e1)
    1962           [ 2: #error #_ @SimFail /2 by ex_intro/
     1964          [ 2: #error #_ @SimFailNicely
    19631965          | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H
    19641966               @SimOk #a #H @H ]
    … …  
    21762178| 11,12: #ty #e1 #e2 #Hsim1 #Hsim2 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
    21772179     cases Hsim1
    2178      [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     2180     [ 2,4: * #error #Hfail >Hfail @SimFailNicely
    21792181     | 1,3: cases (exec_expr ge en m e1)
    2180           [ 2,4: #error #_ @SimFail /2 by ex_intro/
     2182          [ 2,4: #error #_ @SimFailNicely
    21812183          | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite normalize nodelta
    21822184                 cases (exec_bool_of_val ??)
    2183                  [ 2,4: #erro @SimFail /2 by ex_intro/
     2185                 [ 2,4: #erro @SimFailNicely
    21842186                 | 1,3: * whd in match (m_bind ?????); whd in match (m_bind ?????);
    21852187                        [ 2,3: @SimOk //
    … …  
    22292231      #ty normalize in match (is_not_lvalue ?);
    22302232      [ 3,4,13: #Habsurd @(False_ind … Habsurd) ] #_
    2231       @SimFail /2 by ex_intro/
     2233      @SimFailNicely
    22322234] qed.
    22332235
    … …  
    22432245* * try //
    22442246cases (exec_expr ge en m (Expr ??))
    2245 try (#error #_ #_ #_ @SimFail /2 by ex_intro/)
     2247try (#error #_ #_ #_ @SimFailNicely)
    22462248* #val #trace #Hsim_expr #Hsim_lvalue #Htype_eq
    22472249try @(simulation_transitive ???? Hsim_expr (proj1 ?? (sim_related_globals ge ge' en m Hrelated) ?))
    … …  
    22592261* * try //
    22602262cases (exec_lvalue ge en m (Expr ??))
    2261 try (#error #_ #_ #_ @SimFail /2 by ex_intro/)
     2263try (#error #_ #_ #_ @SimFailNicely)
    22622264* #val #trace #Hsim_expr #Hsim_lvalue #Htype_eq
    22632265(* Having to distinguish between exec_lvalue' and exec_lvalue is /ugly/. *)
Note: See TracChangeset for help on using the changeset viewer.