Changeset 2530 for src/common


Ignore:
Timestamp:
Dec 4, 2012, 6:29:43 PM (7 years ago)
Author:
tranquil
Message:

temporary switch to cl_jump treated as cl_other
fixed script for new statement of not_costed_as_label

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StatusSimulation.ma

    r2477 r2530  
    120120      ret_rel … sim_status_rel st1' st2_after_ret ∧
    121121      label_rel … st1' st2'
    122     | cl_other
     122    | _
    123123        (*         
    124124        st1 → st1'
     
    137137      sim_status_rel st1' st2' ∧
    138138      label_rel … st1' st2'
    139     | cl_jump ⇒
     139(*    | cl_jump ⇒
    140140      (*
    141141          st1 → st1'           st1 → st1'--------\
     
    149149      (∃st2'.∃tal : trace_any_label … doesnt_end_with_ret st2 st2'.
    150150        tal_collapsable … tal ∧
    151         sim_status_rel st1' st2' ∧ label_rel … st1' st2')
     151        sim_status_rel st1' st2' ∧ label_rel … st1' st2')*)
    152152    ].
    153153
     
    485485  (* without try it fails... why? *)
    486486  try >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
    487   [ (* jump to none *)
    488     ** #K' #st1_R_st2' #st1_L_st2' %2 /4 by conj/
    489   | (* jump to some *)
    490     * #st2' * #tal2 ** #tal2_coll #st1_R_st2' #st1_L_st2'
    491     %1
    492     %{st2'} %{tal2} % [ /3 by conj/ ]
    493     @tal_collapsable_to_rel_symm assumption
    494   | (* other *)
    495     #st2' ** -st2 -st2'
    496     [1,3: #st2 (* taa2 empty → st1' must be not cost_labelled *)
    497       ** whd in ⊢ (%→?); *
    498       [1,3: #ncost #R' #L' %2 /4 by conj/
    499       |*: * #ABS elim (ABS K)
    500       ]
    501     |*: #st2 #st2_mid #st2' #taa2 #H2 #I2 *** #st1_R_st2' #st1_L_st2' %1
    502       %{st2'} %{(taa_append_tal … taa2 (tal_base_not_return … H2 (or_intror ?? I2) ?))}
    503       [1,3: whd <st1_L_st2' assumption ]
    504       % [1,3: /2 by conj/]
    505       % try @refl %{st2_mid} %{taa2} %{H2} %[2,4: %[2,4: %]]
     487  #st2' ** -st2 -st2'
     488  [1,3: #st2 (* taa2 empty → st1' must be not cost_labelled *)
     489    ** whd in ⊢ (%→?); *
     490    [1,3: #ncost #R' #L' %2 /4 by conj/
     491    |*: * #ABS elim (ABS K)
    506492    ]
     493  |*: #st2 #st2_mid #st2' #taa2 #H2 #I2 *** #st1_R_st2' #st1_L_st2' %1
     494    %{st2'} %{(taa_append_tal … taa2 (tal_base_not_return … H2 (or_intror ?? I2) ?))}
     495    [1,3: whd <st1_L_st2' assumption ]
     496    % [1,3: /2 by conj/]
     497    % try @refl %{st2_mid} %{taa2} %{H2} %[2,4: %[2,4: %]]
    507498  ]
    508499| (* tal_base_return *) whd
     
    705696[ #st3 #H #G
    706697| #st3 #st4 #st5 #ex #H' #G' #taa #H #G
    707   whd in match (as_label ? st3); >(not_costed_no_label … G)
     698  >(not_costed_no_label … G)
    708699] >append_nil whd in ⊢ (??%?); >ft_observables_aux_def >append_nil %
    709700qed.
     
    723714[ #st2 * #ft #H #G >append_nil %
    724715| #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H #G
    725   whd in match (as_label ? st3); >(not_costed_no_label … K)
     716  >(not_costed_no_label … K)
    726717  normalize nodelta //
    727718]
     
    740731[ #st2 * #ft #H >append_nil %
    741732| #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H
    742   whd in match (as_label ? st3); >(not_costed_no_label … K)
     733  >(not_costed_no_label … K)
    743734  normalize nodelta //
    744735]
     
    757748[ #st2 * #ft #H >append_nil %
    758749| #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H
    759   whd in match (as_label ? st3); >(not_costed_no_label … K)
     750  >(not_costed_no_label … K)
    760751  normalize nodelta >append_nil //
    761752]
     
    807798|*: #st1_mid #st1' #stack [3: #f] #ft1 #ex [2: *] #cl
    808799  (* IH *) * #st2_lab * #st2_mid * #ft2 * #taa ** #L' #G' #S
    809   [ (* jump *)
     800  [1,2: (* jump *)
    810801    lapply (sim_execute … ex G')
    811     >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
    812     [ ** #ncost #G'' #H''
     802    try >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
     803(*    [ ** #ncost #G'' #H''
    813804      %{st2_mid} %{st2_mid}
    814805      %[@(ft_extend_taa … taa)
     
    817808      whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
    818809      >ft_extend_taa_obs <L'
    819       whd in match (as_label ? st1_mid);
    820810      >(not_costed_no_label … ncost) >if_eq >S %
    821811    | * #st2' * #tal ** #coll
     
    833823  | (* other *)
    834824    lapply (sim_execute … ex G')
    835     >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
     825    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); **)
    836826    #st2' *#taaf ** #ncost #G'' #H''
    837827    %{st2'} %{st2'}
     
    846836    [1,3: #st2' #H'' #taa * #ncost
    847837      >ft_extend_taa_obs <L'
    848       [1,3: whd in match (as_label ? st1_mid);
    849         >(not_costed_no_label … ncost) >if_eq >S %
     838      [1,3: >(not_costed_no_label … ncost) >if_eq >S %
    850839      |*: lapply L' lapply H'' lapply S lapply ft2 cases taa -st2_lab -st2'
    851840        [1,3: #st2' #ft2 #S #H'' #L' >append_nil
    852           whd in match (as_label ??); >not_costed_no_label
     841          >not_costed_no_label
    853842          [1,3: >append_nil @S ]
    854843          whd in ⊢ (?%); >L' <H'' assumption
     
    880869    [ #st2' * >append_nil
    881870    | #st2_after_ret #st2_after_ret' #st2' #taa2' #ex'' #cl'' #ncost
    882       whd in match (as_label ? st2_after_ret); >(not_costed_no_label … ncost)
     871      >(not_costed_no_label … ncost)
    883872      >if_eq >append_nil
    884873    ]
Note: See TracChangeset for help on using the changeset viewer.