Ignore:
Timestamp:
Jun 7, 2011, 4:53:53 PM (9 years ago)
Author:
campbell
Message:

Revise proofs affected by recent matita change.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecEquiv.ma

    r798 r891  
    5252 (∀r. final_state s r → P (Some ? r)) →
    5353 ((¬∃r.final_state s r) → P (None ?)) →
    54 P (is_final ?? clight_exec s).
    55 #s #P #F #NF lapply (refl ? (is_final ?? clight_exec s))
    56 cases (is_final ?? clight_exec s) in ⊢ (???% → %)
    57 [ #E @NF % * #r #H > (is_final_complete … H) in E #H destruct
     54P (is_final s).
     55#s #P #F #NF lapply (refl ? (is_final s))
     56cases (is_final s) in ⊢ (???% → %)
     57[ #E @NF % * #r #H whd in E:(??%?) > (is_final_complete … H) in E #H destruct
    5858| #r #E @F @is_final_sound @E
    5959] qed.
     60
     61lemma is_final_elim': ∀s.∀P:option int → Type[0].
     62 (∀r. final_state s r → P (Some ? r)) →
     63 ((¬∃r.final_state s r) → P (None ?)) →
     64P (is_final io_out io_in clight_fullexec s).
     65@is_final_elim qed.
    6066
    6167lemma exec_e_step: ∀ge,x,tr,s,e.
     
    6672[ #o #k #EXEC whd in EXEC:(??%?); destruct
    6773| #y cases y #tr' #s' whd in ⊢ (??%? → ?)
    68   @is_final_elim 
     74  @is_final_elim'
    6975  [ #r #FINAL | #FINAL ]
    7076  #EXEC whd in EXEC:(??%?); destruct @refl
     
    7985[ #o #k #EXEC whd in EXEC:(??%?); destruct
    8086| #y cases y; #tr' #s' whd in ⊢ (??%? → ?);
    81   @is_final_elim
     87  @is_final_elim'
    8288  [ #r ] #FINAL #EXEC whd in EXEC:(??%?);
    8389  destruct @refl
     
    9298[ #o #k #EXEC whd in EXEC:(??%?); destruct
    9399| #y cases y; #tr' #s' whd in ⊢ (??%? → ?)
    94   @is_final_elim [ #r ] #F #EXEC whd in EXEC:(??%?); destruct @F
     100  @is_final_elim' [ #r ] #F #EXEC whd in EXEC:(??%?); destruct @F
    95101| #msg #EXEC whd in EXEC:(??%?); destruct
    96102] qed.
     
    143149        ]
    144150    | #x cases x; #tr' #s' >(exec_inf_aux_unfold …)
    145         whd in ⊢ (??%? → ?); @is_final_elim
     151        whd in ⊢ (??%? → ?); @is_final_elim'
    146152        [ #r ] #F #E whd in E:(??%?); destruct
    147153    | #msg >(exec_inf_aux_unfold …)
     
    170176            [ #o2 #k2 #E whd in E:(??%?); destruct (E)
    171177            | #x cases x; #tr2 #s2 whd in ⊢ (??%? → ?);
    172                 @is_final_elim
     178                lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%)
     179                @IFE
    173180                [ #r' #FINAL #E whd in E:(??%?);
    174181                    destruct (E);
     
    184191       ]
    185192   | #x cases x; #tr #s whd in ⊢ (??%? → ?);
    186        @is_final_elim [ #r ] #F #E whd in E:(??%?); destruct (E)
     193       @is_final_elim' [ #r ] #F #E whd in E:(??%?); destruct (E)
    187194   | #msg #E whd in E:(??%?); destruct (E)
    188195   ]
     
    281288    [ #o #k #EXEC' whd in EXEC':(??%?); destruct (EXEC');
    282289    | #x cases x; #tr'' #s' whd in ⊢ (??%? → ?);
    283         @is_final_elim [ #r'' #FINAL | #F ]
     290        @is_final_elim' [ #r'' #FINAL | #F ]
    284291        #EXEC' whd in EXEC':(??%?); destruct (EXEC');
    285292    | #msg #EXEC' whd in EXEC':(??%?); destruct (EXEC');
     
    299306>(exec_inf_aux_unfold …) cases x;
    300307[ #o #k #EXEC whd in EXEC:(??%?); destruct;
    301 | #z cases z; #tr' #s' whd in ⊢ (??%? → ?); @is_final_elim
     308| #z cases z; #tr' #s' whd in ⊢ (??%? → ?); @is_final_elim'
    302309  [ #r' #FINAL cases FINAL; #r'' #m' #EXEC whd in EXEC:(??%?);
    303310      destruct (EXEC); @refl
     
    365372    cases (exec_step ge s);
    366373  [ #o #k #msg' #EXEC whd in EXEC:(??%?); destruct
    367   | #x cases x; #tr #s' #msg' whd in ⊢ (??%? → ?) @is_final_elim
     374  | #x cases x; #tr #s' #msg' whd in ⊢ (??%? → ?) @is_final_elim'
    368375      [ #r ] #F #EXEC whd in EXEC:(??%?); destruct
    369376  | #msg1 #msg2 #EXEC #E whd in EXEC:(??%?); destruct @refl
     
    381388    cases (exec_step ge s);
    382389    [ #o #k #EXEC whd in EXEC:(??%?); destruct
    383     | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?) @is_final_elim
     390    | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?) @is_final_elim'
    384391        [ #r ] #F #E whd in E:(??%?); destruct @F
    385392    | #msg #E whd in E:(??%?); destruct
     
    409416            [ #o2 #k2 #EXECK whd in EXECK:(??%?); destruct
    410417            | #x cases x; #tr2 #s2 whd in ⊢ (??%? → ?);
    411                 @is_final_elim [ #r ] #F #EXECK
     418                lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%)
     419                @IFE [ #r ] #F #EXECK
    412420                whd in EXECK:(??%?); destruct;
    413421                @(absurd ?? F)
     
    419427        ]
    420428    | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?);
    421         @is_final_elim [ #r ] #F #E whd in E:(??%?); destruct;
     429        @is_final_elim' [ #r ] #F #E whd in E:(??%?); destruct;
    422430    | #msg #E whd in E:(??%?); destruct
    423431    ]
     
    707715    ]
    708716| #x cases x; #tr' #s'' #H whd in ⊢ (?%? → ?)
    709     @is_final_elim [ #r ] #F #E whd in E:(?%?);
     717    @is_final_elim' [ #r ] #F #E whd in E:(?%?);
    710718    inversion E;
    711719    [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct
     
    898906                #F #S whd in S:(?%?); cases (se_inv … S);
    899907            | #x cases x; #tr' #s' whd in ⊢ (?%? → ?)
    900                 @is_final_elim [ #r ] #F #S whd in S:(?%?);
     908                @is_final_elim' [ #r ] #F #S whd in S:(?%?);
    901909                cases (se_inv … S);
    902910            | #msg #S cases (se_inv … S);
     
    915923                #F #S whd in S:(?%?); cases (se_inv … S);
    916924            | #x cases x; #tr' #s' whd in ⊢ (?%? → ?)
    917                 @is_final_elim [ #r ] #F #S whd in S:(?%?);
     925                @is_final_elim' [ #r ] #F #S whd in S:(?%?);
    918926                cases (se_inv … S);
    919927            | #msg #S cases (se_inv … S);
     
    9951003  ∃e'.e = e_step ??? E0 s e'.
    9961004#ge #s #e >(exec_inf_aux_unfold …)
    997 whd in ⊢ (??%? → ?) @is_final_elim
     1005whd in ⊢ (??%? → ?) @is_final_elim'
    9981006[ #r #FINAL #EXEC #NOTFINAL
    9991007    @False_ind @(absurd ?? NOTFINAL)
     
    10091017#classic #constructive_indefinite_description #p #e
    10101018whd in ⊢ (?%? → ??(λ_.?(?%?)%));
    1011 lapply (make_initial_state_sound p);
    1012 lapply (the_initial_state p);
    1013 cases (make_initial_state p);
     1019lapply (make_initial_state_sound p)
     1020lapply (the_initial_state p)
     1021whd in ⊢ (? → ? → ?(match % with [_ ⇒ ? | _ ⇒ ?])? → ?)
     1022cases (make_initial_state p)
    10141023[ #gs cases gs; #ge #s #INITIAL' #INITIAL whd in INITIAL ⊢ (?%? → ?);
    10151024    cases INITIAL; #Ege #INITIAL''
    1016     >(exec_inf_aux_unfold …)
     1025    >exec_inf_aux_unfold
    10171026    whd in ⊢ (?%? → ?)
    1018     @is_final_elim
     1027    @is_final_elim'
    10191028    [ #r #F @False_ind
    10201029        @(absurd ?? (initial_state_not_final … INITIAL''))
     
    10251034    lapply (behavior_of_execution ??
    10261035              (execution_characterisation_complete classic constructive_indefinite_description ge s ? EXEC'));
    1027         *; #b #MATCHES %{b} % //;
     1036        *; #b #MATCHES %{b} % [ @MATCHES ]
    10281037        #ge' >Ege #Ege' >(?:ge' = ge) [ 2: destruct (Ege') skip (INITIAL Ege EXEC0 EXEC'); // ]
    10291038        inversion MATCHES;
Note: See TracChangeset for help on using the changeset viewer.