Ignore:
Timestamp:
Jul 17, 2012, 6:57:40 PM (8 years ago)
Author:
campbell
Message:

A general result about simulations of executions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r2202 r2203  
    314314.
    315315
    316 (* TODO: this (or something like it) ought to be elsewhere. *)
    317 inductive plus (ge:genv) : state → trace → state → Prop ≝
    318 | plus_one : ∀s1,tr,s2. exec_step ge s1 = OK … 〈tr,s2〉 → plus ge s1 tr s2
    319 | plus_succ : ∀s1,tr,s2,tr',s3. exec_step ge s1 = OK … 〈tr,s2〉 → plus ge s2 tr' s3 → plus ge s1 (tr⧺tr') s3.
    320 
    321316(* Some details are invariant under labelling. *)
    322317lemma label_function_return : ∀f.
     
    653648  state_with_labels_partial s1 s1' →
    654649  exec_step ge s1 = Value … 〈tr,s2〉 →
    655    ∃tr',s2'. plus ge' s1' tr' s2' ∧
     650   ∃tr',s2'. plus … clight_exec ge' s1' tr' s2' ∧
    656651             trace_with_extra_labels tr tr' ∧
    657652             state_with_labels s2 s2'.
     
    669664      lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?);
    670665      [ #E >E in EX; whd in ⊢ (??%% → ?); #EX' destruct %{(Returnstate Vundef Kstop (free_list m (blocks_of_env e)))}
    671         % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E @refl
     666        % [ % [ @cl_plus_one whd in ⊢ (??%?); >label_function_return >E @refl
    672667        | // ] | /3/ ]
    673668      | *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct
     
    676671      %{(State (label_function f) (\fst (label_statement s0 u)) k0' e m)}
    677672      whd in EX:(??%%); destruct
    678       % [ % [ @plus_one @refl | // ] | /3/ ]
     673      % [ % [ @cl_plus_one @refl | // ] | /3/ ]
    679674    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr}
    680675      whd in EX:(??%%); destruct
    681       % [ 2: % [ % [ @plus_one @refl | // ] | @swl_partial @swl_whilestate // ] | skip ]
     676      % [ 2: % [ % [ @cl_plus_one @refl | // ] | @swl_partial @swl_whilestate // ] | skip ]
    682677    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
    683678      cases (bindIO_inversion ??????? EX) * #ve #tre * #EXe #EXrem
     
    685680      normalize in EXbrem; destruct
    686681      cases ((proj1 ?? (label_expr_ok ge ge' e m RG)) ??? EXe ue) #tre' * #EXe' #Te
    687       [ % [ 2: % [ 2: % [ % [ @plus_one
     682      [ % [ 2: % [ 2: % [ % [ @cl_plus_one
    688683        whd in ⊢ (??%?); >EXe' in ⊢ (??%?);
    689684        whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?);
     
    691686        | // ]
    692687        | @swl_partial @swl_dowhilestate // ] | skip ] | skip ]
    693       | % [ 2: % [ 2: % [ % [ @plus_succ [
     688      | % [ 2: % [ 2: % [ % [ @cl_plus_succ [
    694689        4: whd in ⊢ (??%?); >EXe' in ⊢ (??%?);
    695690           whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?);
    696691           whd in ⊢ (??%?); @refl
    697692        | skip | skip
    698         | 5: @plus_succ [ 4: @refl | skip | skip
    699         | 5: @plus_one @refl | skip ] | skip ]
     693        | 5: @cl_plus_succ [ 4: @refl | skip | skip
     694        | 5: @cl_plus_one @refl | skip ] | skip ]
    700695        | <(E0_right tr) @twel_app /2/ ]
    701696        | /3/ ] | skip ] | skip ]
     
    703698    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
    704699      whd in EX:(??%?); destruct
    705       %{E0} % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ]
     700      %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | /3/ ] | skip ]
    706701    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
    707702      whd in EX:(??%?); destruct
    708       %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ]
     703      %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | /4/ ] | skip ]
    709704    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
    710705      whd in EX:(??%?); destruct
    711       %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ]
     706      %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | /4/ ] | skip ]
    712707    | #k0 #k0' #K #_ #E1 #E2 #E3 destruct
    713708      whd in EX:(??%?); destruct
    714       %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ]
     709      %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | /4/ ] | skip ]
    715710    | #r #f0 #en #k0 #k0' #K #_ #E1 #E2 #E3 destruct
    716711      whd in EX:(??%?);
    717712      lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?);
    718713      [ #E >E in EX; whd in ⊢ (??%? → ?); #EX destruct
    719         %{E0} % [2: % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?);
     714        %{E0} % [2: % [ % [ @cl_plus_one whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?);
    720715        @refl | // ] | /4/ ] | skip ]
    721716      | *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct
    722717      ]
    723718    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    724       % [2: % [2: % [ % [ @plus_one @refl | // ] | /3/ ]| skip ]| skip ]
     719      % [2: % [2: % [ % [ @cl_plus_one @refl | // ] | /3/ ]| skip ]| skip ]
    725720    ]
    726721  | * #a1 #ty1 #a2 #EX
     
    734729    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX2 ua1) #tr2' * #EX2' #T2
    735730    % [2: % [2: % [ % [
    736       @plus_one whd in ⊢ (??%?);     
     731      @cl_plus_one whd in ⊢ (??%?);     
    737732      >exec_lvalue_labelled >EX1' in ⊢ (??%?);
    738733      whd in ⊢ (??%?); >EX2' in ⊢ (??%?);
     
    757752    [ cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX5 us) #tr5' * #EX5' #T5 ]
    758753    % [2,4: % [2,4: % [1,3: % [1,3:
    759       @plus_one whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX why do I need the repetition? *)
     754      @cl_plus_one whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX why do I need the repetition? *)
    760755      whd in ⊢ (??%?); [ >EX2' in ⊢ (??%?); | >EX2' in ⊢ (??%?); ]
    761756      whd in ⊢ (??%?); >(opt_find_funct … RG … EX3) in ⊢ (??%?);
     
    766761    whd in EX:(??%%); destruct
    767762    whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2
    768     %{E0} % [2: % [ % [ @plus_one @refl | // ] | @swl_partial @swl_state /2/ ] | skip ]
     763    %{E0} % [2: % [ % [ @cl_plus_one @refl | // ] | @swl_partial @swl_state /2/ ] | skip ]
    769764  | #a #st1 #st2 #EX
    770765    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
     
    777772    whd in match (add_cost_before ??); cases (fresh ??) #c7 #u7
    778773    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
    779     % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9:
     774    % [2,4: % [2,4: % [1,3: % [1,3: @cl_plus_succ [ 4,9:
    780775      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
    781776      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
    782777      whd in ⊢ (??%?); @refl
    783778    | 1,2,6,7: skip
    784     | 5,10: @plus_one @refl
     779    | 5,10: @cl_plus_one @refl
    785780    | *: skip
    786781    ]
     
    797792    >shift_fst
    798793    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
    799     % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9: @refl | 1,2,6,7: skip
    800       | 5,10: @plus_succ [ 4,9:
     794    % [2,4: % [2,4: % [1,3: % [1,3: @cl_plus_succ [ 4,9: @refl | 1,2,6,7: skip
     795      | 5,10: @cl_plus_succ [ 4,9:
    801796      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
    802797      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
    803798      whd in ⊢ (??%?); @refl
    804799    | 1,2,6,7: skip
    805     | 5: @plus_one @refl
    806     | 10: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ]
     800    | 5: @cl_plus_one @refl
     801    | 10: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl | *: skip ] |*: skip ]
    807802    | *: skip
    808803    ]
     
    815810    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6 >shift_fst
    816811    whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7 >shift_fst
    817     % [2: % [2: % [ % [ @plus_succ [ 4: @refl | 1,2: skip
    818       | 5: @plus_succ [ 4: @refl | 1,2: skip | 5: @plus_one // | skip ] | skip ]
     812    % [2: % [2: % [ % [ @cl_plus_succ [ 4: @refl | 1,2: skip
     813      | 5: @cl_plus_succ [ 4: @refl | 1,2: skip | 5: @cl_plus_one // | skip ] | skip ]
    819814      | /2/ ] | /4/ ] | skip ] | skip ]
    820815  | #st1 #a #st2 #st #EX
     
    829824      normalize in EX; destruct
    830825      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
    831       % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9: @refl | 1,2,6,7: skip
    832       | 5,10: @plus_succ [ 4,9:
     826      % [2,4: % [2,4: % [1,3: % [1,3: @cl_plus_succ [ 4,9: @refl | 1,2,6,7: skip
     827      | 5,10: @cl_plus_succ [ 4,9:
    833828      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
    834829      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
    835830      whd in ⊢ (??%?); @refl
    836831      | 1,2,6,7: skip
    837       | 5: @plus_one @refl
    838       | 10: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ]
     832      | 5: @cl_plus_one @refl
     833      | 10: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl | *: skip ] |*: skip ]
    839834      | *: skip
    840835      ]
     
    842837      ]| 2,4: /4/ ] | *: skip ] | *: skip ]
    843838    | whd in EX:(??%%); destruct
    844       % [2: % [2: %[ %[ @plus_succ [ 4: @refl | 5: @plus_one
     839      % [2: % [2: %[ %[ @cl_plus_succ [ 4: @refl | 5: @cl_plus_one
    845840        whd in ⊢ (??%?); cases (labelled_is_not_skip ? u1 Esk) #Esk' #Eskip'
    846841        >Eskip' whd in ⊢ (??%?); @refl | *: skip ]| // ] | @swl_partial @swl_state /2/ ]
     
    861856    whd in match (label_statement ??);
    862857    % [2,4,6,8,10,12,14: % [2,4,6,8,10,12,14: % [1,3,5,7,9,11,13: %
    863     [1,11,13: @plus_one @refl | 2,12,14: //
    864     | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/
    865     | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/
    866     | @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip] | /2/
    867     | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/
    868     ]| *: /3/ ]|*: skip]|*: skip ]
     858    [1,11,13: @cl_plus_one @refl | 2,12,14: //
     859    | @cl_plus_succ [ 4: @refl | 5: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl |*:skip]|*:skip] | /2/
     860    | @cl_plus_succ [ 4: @refl | 5: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl |*:skip]|*:skip] | /2/
     861    | @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl |*:skip] | /2/
     862    | @cl_plus_succ [ 4: @refl | 5: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl |*:skip]|*:skip] | /2/
     863    ]| *: /3 by swl_partial, swl_state/ ]|*: skip]|*: skip ]
    869864  | #EX inversion KL
    870865    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
     
    881876    whd in match (label_statement ??);
    882877    [ 1,2,4,5,6,7: % [2,4,6,8,10,12: % [2,4,6,8,10,12: % [1,3,5,7,9,11: %
    883       [1,3,7,9,11: @plus_one @refl | 5: @plus_succ [4:@refl | 5:@plus_one @refl | *: skip ]
     878      [1,3,7,9,11: @cl_plus_one @refl | 5: @cl_plus_succ [4:@refl | 5:@cl_plus_one @refl | *: skip ]
    884879      | *: // ] | *: @swl_partial /3 by cwl_for3, swl_state, swl_whilestate/ ]| *:skip ]| *: skip ]
    885880    | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
     
    887882      normalize in EX; destruct
    888883      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ue) #tr1' * #EX1' #T1
    889       % [2,4: % [2,4: % [1,3: % [1,3: [ @plus_one | @plus_succ ] [ 1,5:
     884      % [2,4: % [2,4: % [1,3: % [1,3: [ @cl_plus_one | @cl_plus_succ ] [ 1,5:
    890885        whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
    891886      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
    892887      whd in ⊢ (??%?); @refl
    893       | 6: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ]
     888      | 6: @cl_plus_succ [ 4: @refl | 5: @cl_plus_one @refl | *: skip ] |*: skip ]
    894889      | // | <(E0_right tr) @twel_app /2/
    895890      ]
     
    911906    [ @label_gen_elim #u' whd in match (label_opt_expr ??); @label_gen_elim #u'' ]
    912907    whd in EX:(??%%); destruct
    913     % [2,4: % [2,4: % [1,3: %[1,3: @plus_one
     908    % [2,4: % [2,4: % [1,3: %[1,3: @cl_plus_one
    914909      whd in ⊢ (??%?);
    915910      [ >label_function_return @(dec_false ? (type_eq_dec ??) Ety) #Ety''
     
    927922    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
    928923    whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2
    929     % [2: % [2: % [ % [ @plus_one whd in ⊢ (??%?); >EX1' in ⊢ (??%?); @refl
     924    % [2: % [2: % [ % [ @cl_plus_one whd in ⊢ (??%?); >EX1' in ⊢ (??%?); @refl
    930925      | // ]| cases (label_select_ls … sz i ls u1) #u3 #Els >Els /3/
    931926      ]|skip ]| skip ]
     
    934929    whd in match (label_statement ??); @label_gen_elim #u1 >shift_fst
    935930    whd in match (add_cost_before ??); cases (fresh ??) #cs #u2 >shift_fst
    936     %[2: %[2: %[ %[ @plus_succ
    937       [ 4: @refl | 5: @plus_one @refl | *: skip ]
     931    %[2: %[2: %[ %[ @cl_plus_succ
     932      [ 4: @refl | 5: @cl_plus_one @refl | *: skip ]
    938933      | /2/ ] | /3/ ] |skip ]| skip ]
    939934  | #l #EX
     
    946941      cases (label_find_label_fn … KL F)
    947942      #u' * #cs * #k1' * #F' #K'
    948       % [2: %[2: %[ %[ @plus_succ
    949         [ 4: whd in ⊢ (??%?); >F' in ⊢ (??%?); @refl | 5: @plus_one @refl | *: skip ]
     943      % [2: %[2: %[ %[ @cl_plus_succ
     944        [ 4: whd in ⊢ (??%?); >F' in ⊢ (??%?); @refl | 5: @cl_plus_one @refl | *: skip ]
    950945        | /2/ ] | /3/ ] | skip ] | skip ]
    951946    ]
    952947  | #c #st #EX whd in EX:(??%?); destruct @blindly_label #u1
    953     % [2: % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ]| skip ]
     948    % [2: % [2: % [ % [ @cl_plus_one @refl | // ] | /3/ ] | skip ]| skip ]
    954949  ]
    955950| #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
     
    959954  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua) #tr1' * #EX1' #T1
    960955  [ % [2: % [2: % [ % [
    961     @plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
     956    @cl_plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
    962957                   whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
    963                |5: @plus_one @refl | *: skip ]
    964     | <(E0_right tr) /3/ ]| /4/ ]| skip ]| skip ]
     958               |5: @cl_plus_one @refl | *: skip ]
     959    | <(E0_right tr) /3/ ]| /4 by swl_partial, swl_state, cwl_while/ ]| skip ]| skip ]
    965960  | % [2: % [2: % [ % [
    966     @plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
     961    @cl_plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
    967962                   whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
    968     | 5: @plus_succ [4: @refl
    969     | 5: @plus_one @refl | *: skip ] | *: skip ]
     963    | 5: @cl_plus_succ [4: @refl
     964    | 5: @cl_plus_one @refl | *: skip ] | *: skip ]
    970965    | <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip ]
    971966  ]
     
    973968  whd in EX:(??%%); destruct
    974969  % [2: % [2: % [ % [
    975     @plus_succ [4: % | 5: @plus_one % | *: skip ]
     970    @cl_plus_succ [4: % | 5: @cl_plus_one % | *: skip ]
    976971    | /2/ ]| /4/ ]| skip ]| skip ]
    977972| #f #ua2 #a2 #us3 #s3 #us #s #cs #cpost #k #k' #e #m #K #EX
     
    981976  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua2) #tr1' * #EX1' #T1
    982977  [ % [2: % [2: % [ % [
    983     @plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
     978    @cl_plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
    984979                    whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
    985     | 5: whd in ⊢ (??(??%%??)??); @plus_one @refl
     980    | 5: whd in ⊢ (?????(??%%??)??); @cl_plus_one @refl
    986981    | *: skip ]| <(E0_right tr) /3/ ] | /4/ ]| skip ]| skip ]
    987982  | % [2: % [2: % [ % [
    988     @plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
     983    @cl_plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
    989984                    whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
    990     | 5: whd in ⊢ (??(??%%??)??); @plus_succ [4: @refl
    991     | 5: @plus_one @refl ]| *: skip ]| <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip
     985    | 5: whd in ⊢ (?????(??%%??)??); @cl_plus_succ [4: @refl
     986    | 5: @cl_plus_one @refl ]| *: skip ]| <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip
    992987    ]
    993988  ]
     
    1000995    lapply (refl ? (label_function f)) whd in ⊢ (???% → ?);
    1001996    @label_gen_elim #u1 @label_gen_elim #u2 >shift_fst #Ef
    1002     % [2: % [2: % [ % [ @plus_succ [4: whd in ⊢ (??%?); >EX1 in ⊢ (??%?);
     997    % [2: % [2: % [ % [ @cl_plus_succ [4: whd in ⊢ (??%?); >EX1 in ⊢ (??%?);
    1003998      whd in ⊢ (??%?); >EX2 in ⊢ (??%?); @refl
    1004     | 5: @plus_one @refl | *: skip ] | /2/ ]| <Ef @swl_partial @swl_state @K ]| skip ]| skip ]
     999    | 5: @cl_plus_one @refl | *: skip ] | /2/ ]| <Ef @swl_partial @swl_state @K ]| skip ]| skip ]
    10051000  | #id #tys #ty #args #k #k' #m #K #EX
    10061001    cases (bindIO_inversion ??????? EX) -EX #vs * #EX1 #EX
     
    10131008    | *: normalize #A try #B try #C destruct
    10141009    ]
    1015     % [2: % [2: % [ % [ @plus_one @refl | // ]| /2/ ]| skip ]| skip ]
     1010    % [2: % [2: % [ % [ @cl_plus_one @refl | // ]| /2/ ]| skip ]| skip ]
    10161011  | 9: #r #f #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct cases r in EX ⊢ %;
    10171012    [ #EX whd in EX:(??%?); destruct
    1018       % [2: % [2: % [ % [ @plus_one @refl | // ]| /3/ ]| skip ]| skip ]
     1013      % [2: % [2: % [ % [ @cl_plus_one @refl | // ]| /3/ ]| skip ]| skip ]
    10191014    | * * #b #o #ty #EX
    10201015      cases (bindIO_inversion ??????? EX) -EX #m2 * #EX1 #EX
    10211016      whd in EX:(??%%); destruct
    1022       % [2: % [2: % [ % [ @plus_one whd in ⊢ (??%?); >EX1 in ⊢ (??%?); @refl | // ]| /3/ ]| skip ]| skip ]
     1017      % [2: % [2: % [ % [ @cl_plus_one whd in ⊢ (??%?); >EX1 in ⊢ (??%?); @refl | // ]| /3/ ]| skip ]| skip ]
    10231018    ]
    10241019  | *: #A #B #C #D #E #F #G try #H try #I try #J try #L try #M try #N try #O
     
    10341029  state_with_labels s1 s1' →
    10351030  (exec_step ge s1 = Value … 〈tr,s2〉 →
    1036    ∃tr',s2'. plus ge' s1' tr' s2' ∧
     1031   ∃tr',s2'. plus … clight_exec ge' s1' tr' s2' ∧
    10371032             trace_with_extra_labels tr tr' ∧
    10381033             state_with_labels s2 s2').
     
    10481043    cases (step_with_labels_partial … RG (State f s k e m) (State (label_function f) (\fst (label_statement s u)) k' e m) tr s2 (swl_state … K) EX)
    10491044    #tr' * #s2' * * #P #T #S
    1050     % [2: % [2: % [ % [ @plus_succ [4: @refl | 5: @P | *: skip ] | /2/ ]| @S ]| skip ]| skip ]
     1045    % [2: % [2: % [ % [ @cl_plus_succ [4: @refl | 5: @P | *: skip ] | /2/ ]| @S ]| skip ]| skip ]
    10511046(* but for LScase it's just like the cases in step_with_labels_partial *)
    10521047  | #sz #i #s #ls #k #k' #e #m #K #EX
     
    10551050    @label_gen_elim #u3 >shift_fst whd in match (seq_of_labeled_statement ?);
    10561051    whd in EX:(??%?); destruct
    1057     % [2: % [2: % [ % [ @plus_succ [4: @refl | 5: @plus_one @refl | *: skip ] | /2/ ]| /4/ ]| skip ]| skip ]
     1052    % [2: % [2: % [ % [ @cl_plus_succ [4: @refl | 5: @cl_plus_one @refl | *: skip ] | /2/ ]| /4/ ]| skip ]| skip ]
    10581053  ]   
    10591054] qed.
     
    11881183
    11891184
    1190 lemma not_wrong_init : ∀p.
    1191   not_wrong state (exec_inf … clight_fullexec p) →
    1192   ∃s. make_initial_state … p = OK ? s.
    1193 #p whd in ⊢ (??% → ?); change with (make_initial_state p) in match (make_initial_state ??? p);
    1194 cases (make_initial_state p)
    1195 [ /2/
    1196 | normalize #m #NW @⊥
    1197   inversion NW #H1 #H2 #H3 #H4 try #H5 destruct
    1198 ] qed.
    11991185
    12001186lemma final_related : ∀s1,s2.
     
    12041190[ #s1y #s2y * //
    12051191| //
    1206 ] qed.
    1207 
    1208 lemma plus_not_final : ∀ge,s,tr,s'.
    1209   plus ge s tr s' →
    1210   is_final s = None ?.
    1211 #ge #s0 #tr0 #s0' *
    1212 [ #s1 #tr #s2 #EX | #s1 #tr #s2 #tr' #s3 #EX #PL ]
    1213 lapply (refl ? (is_final s1))
    1214 cases (is_final s1) in ⊢ (???% → %);
    1215 //
    1216 #r cases s1 in EX ⊢ %;
    1217 #H9 #H10 #H11 try #H12 try #H13 try #H14 try #H15
    1218 [ 1,5: whd in H15:(??%?); | 2,6: whd in H14:(??%?); | 3,7: whd in H13:(??%?); | 4,8: whd in H11:(??%?); ]
    1219 destruct
    1220 normalize in H10;
    1221 destruct
    1222 qed.
    1223 
    1224 lemma plus_exec : ∀ge,s,tr,s'.
    1225   plus ge s tr s' →
    1226   is_final s' = None ? →
    1227   steps state tr
    1228     (exec_inf_aux … clight_fullexec ge (exec_step ge s))
    1229     (exec_inf_aux … clight_fullexec ge (exec_step ge s')).
    1230 #ge #s0 #tr0 #s0' #P elim P
    1231 [ #s1 #tr #s2 #EX #NF >EX >exec_inf_aux_unfold
    1232   whd in ⊢ (???%?);
    1233   whd in match (is_final ?????); >NF
    1234   %2
    1235 | #s1 #tr #s2 #tr' #s3 #EX1 #P2 #IH #NF
    1236   >exec_inf_aux_unfold >EX1
    1237   whd in ⊢ (???%?);
    1238   whd in match (is_final ?????); >(plus_not_final … P2)
    1239   %3 @IH //
    1240 ] qed.
    1241 
    1242 lemma plus_exec_final : ∀ge,s,tr,s',r.
    1243   plus ge s tr s' →
    1244   is_final s' = Some ? r →
    1245   ∃tr'. steps state tr
    1246           (exec_inf_aux … clight_fullexec ge (exec_step ge s))
    1247           (e_stop … tr' r s').
    1248 #ge #s0 #tr0 #s0' #r #P elim P
    1249 [ #s1 #tr #s2 #EX #F >EX >exec_inf_aux_unfold
    1250   %{tr} whd in ⊢ (???%?);
    1251   whd in match (is_final ?????); >F
    1252   %1
    1253 | #s1 #tr #s2 #tr' #s3 #EX1 #P2 #IH #F
    1254   cases (IH … F)
    1255   #tr' #S' %{tr'}
    1256   >exec_inf_aux_unfold >EX1
    1257   whd in ⊢ (???%?);
    1258   whd in match (is_final ?????); >(plus_not_final … P2)
    1259   %3 @S'
    12601192] qed.
    12611193
     
    12781210  #tr2 * #s2' * * #PL #TWL #S'
    12791211  lapply F1 whd in ⊢ (??%? → ?); >(final_related … S') #F2
    1280   cases (plus_exec_final ????? PL F2)
     1212  cases (plus_final … clight_fullexec … PL F2)
    12811213  #tr2' #S2
    12821214  @(swl_stop … S2 TWL)
     
    12861218  cases (step_with_labels … RG … S EX1)
    12871219  #tr2 * #s2' * * #EX2 #TR #S' (*>E1' in NW1 ⊢ %; #NW1*)
    1288   @(swl_steps … (plus_exec … EX2 ?))
    1289   [ <(final_related … S') @(exec_e_step_not_final ?? clight_fullexec … E1)
     1220  @(swl_steps … (plus_exec … clight_fullexec … EX2 ?))
     1221  [ whd in ⊢ (??%?); <(final_related … S') @(exec_e_step_not_final ?? clight_fullexec … E1)
    12901222  | //
    12911223  | (* Manual rewrite to prevent guardedness condition getting upset. *)
     
    13301262#p
    13311263#NW
    1332 cases (not_wrong_init p NW)
    1333 #s1 #I1
     1264cases (not_wrong_init clight_fullexec p NW)
     1265whd in ⊢ (% → ??%? → ?); #s1 #I1
    13341266cases (initial_state_in_simulation … I1)
    13351267#s2 * #I2
Note: See TracChangeset for help on using the changeset viewer.