Changeset 708


Ignore:
Timestamp:
Mar 23, 2011, 2:28:55 PM (9 years ago)
Author:
campbell
Message:

Use a more normalize-friendly definition of clight_exec to make the destruct
tactic usable again, and recomplete the equivalence proof.

Location:
src/Clight
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r702 r708  
    667667  OK ? 〈ge,Callstate f (nil ?) Kstop m0〉.
    668668
     669let rec is_final (s:state) : option int ≝
     670match s with
     671[ Returnstate res k m ⇒
     672  match k with
     673  [ Kstop ⇒
     674    match res with
     675    [ Vint r ⇒ Some ? r
     676    | _ ⇒ None ?
     677    ]
     678  | _ ⇒ None ?
     679  ]
     680| _ ⇒ None ?
     681].
     682
    669683definition is_final_state : ∀st:state. (Sig ? (final_state st)) + (¬∃r. final_state st r).
    670684#st elim st;
     
    713727λs.match s with [ State f s k e m ⇒ m | Callstate f a k m ⇒ m | Returnstate r k m ⇒ m ].
    714728
    715 definition is_final : state → option int ≝
    716 λs.match is_final_state s with
    717 [ inl r ⇒ Some ? (sig_eject … r)
    718 | inr _ ⇒ None ?
    719 ].
    720 
    721729definition clight_exec : execstep ≝
    722730  mk_execstep … is_final mem_of_state exec_step.
  • src/Clight/CexecComplete.ma

    r700 r708  
    455455| #f #l #s #k #env #m @refl
    456456] qed.
     457
     458lemma is_final_complete : ∀s,r. final_state s r → is_final s = Some ? r.
     459#s0 #r0 * #r #m @refl qed.
     460 
  • src/Clight/CexecEquiv.ma

    r702 r708  
    5353 ((¬∃r.final_state s r) → P (None ?)) →
    5454P (is_final clight_exec s).
    55 #s #P #F #NF whd in ⊢ (?%) cases (is_final_state s)
    56 [ * #r #FINAL @F @FINAL
    57 | #NOTFINAL @NF @NOTFINAL
     55#s #P #F #NF lapply (refl ? (is_final clight_exec s))
     56cases (is_final clight_exec s) in ⊢ (???% → %)
     57[ #E @NF % * #r #H > (is_final_complete … H) in E #H destruct
     58| #r #E @F @is_final_sound @E
    5859] qed.
    5960
     
    6465>(exec_inf_aux_unfold …) cases x;
    6566[ #o #k #EXEC whd in EXEC:(??%?); destruct
    66 | #y cases y; #tr' #s' whd in ⊢ (??%? → ?)
     67| #y cases y #tr' #s' whd in ⊢ (??%? → ?)
    6768  @is_final_elim
    6869  [ #r #FINAL | #FINAL ]
    69   (* Some trickery to prevent destruct normalizing clight_exec *)
    70   #EXEC whd in EXEC:(??%?); [ @False_ind destruct |
    71   cut (s = s') [ generalize in EXEC:(??(??????%)?) ⊢ ? #e0 #E destruct @refl ]
    72   #Es <Es in EXEC #EXEC
    73   generalize in EXEC:(??(??????%)?) ⊢ (??%?)
    74   #e0 #E destruct @refl
    75   ]
     70  #EXEC whd in EXEC:(??%?); destruct @refl
    7671| #EXEC whd in EXEC:(??%?); destruct
    7772] qed.
     
    8580| #y cases y; #tr' #s' whd in ⊢ (??%? → ?);
    8681  @is_final_elim
    87   [ #r ] #FINAL #EXEC whd in EXEC:(??%?)
    88   (* Again, prevent destruct blowing up *)
    89   [ 2: generalize in EXEC:(??(??????%)?) ⊢ ? #e0 #EXEC ]
    90   destruct;
    91     @refl
     82  [ #r ] #FINAL #EXEC whd in EXEC:(??%?);
     83  destruct @refl
    9284| #EXEC whd in EXEC:(??%?); destruct
    9385] qed.
     
    10092[ #o #k #EXEC whd in EXEC:(??%?); destruct
    10193| #y cases y; #tr' #s' whd in ⊢ (??%? → ?)
    102   @is_final_elim [ #r #F #EXEC whd in EXEC:(??%?); destruct
    103   | #F whd in ⊢ (??%? → ?) generalize in ⊢ (??(??????%)? → ?) #e0 #EXEC destruct  @F ]
     94  @is_final_elim [ #r ] #F #EXEC whd in EXEC:(??%?); destruct @F
    10495| #EXEC whd in EXEC:(??%?); destruct
    10596] qed.
     
    111102 se_step tr s e = se_step tr' s' e' →
    112103 tr = tr' ∧ s = s' ∧ e = e'.
    113 #tr #s #e #tr' #s' #e' #E
    114 (* destruct  This takes a hideous amount of time, not sure why. *)
    115 @(match E return λl.λ_. match l with [ se_step tr0 s0 e0 ⇒ tr = tr0 ∧ s = s0 ∧ e = e0 | _ ⇒ False ] with [ refl ⇒ ? ])
    116 whd % try % @refl qed.
     104#tr #s #e #tr' #s' #e' #E destruct
     105% try % @refl qed.
    117106
    118107lemma exec_from_step : ∀ge,s,tr,s',e.
     
    121110#ge #s0 #tr0 #s0' #e0 #H inversion H;
    122111[ #tr #r #m #E1 #E2 destruct
    123 | #tr #s #e #se #H1 #H2 #E (*destruct (E);*)
    124   lapply (se_step_eq … E) * * #E1 #E2 #E3 >E1 >E2 >E3
     112| #tr #s #e #se #H1 #H2 #E (* destruct (E) ;*)
     113  cases (se_step_eq … E) * #E1 #E2 #E3 >E1 >E2 >E3
    125114    >(exec_e_step_inv … H2)
    126115    <(exec_e_step … H2) in H1 #H1 % //
     
    129118] qed.
    130119
    131 axiom exec_from_interact : ∀ge,s,o,k,i,tr,s',e.
     120lemma exec_from_interact : ∀ge,s,o,k,i,tr,s',e.
    132121exec_from ge s (se_interact o k i (se_step tr s' e)) →
    133122step ge s tr s' ∧
    134123(*exec_step ge s = Value ??? 〈tr,s'〉 ∧*) exec_from ge s' e.
    135 (*
    136124#ge #s0 #o0 #k0 #i0 #tr0 #s0' #e0 #H inversion H;
    137125[ #tr #r #m #E1 #E2 destruct
    138126| #tr #s #e #se #H1 #H2 #E destruct (E)
    139127| #_ #E destruct
    140 | #o #k #i #se #H1 #H2 #E (*destruct (E);*)
     128| #o #k #i #se #H1 #H2 #E destruct (E);
    141129    lapply (exec_step_sound ge s0);
    142130    cases (exec_step ge s0) in H2 ⊢ %;
     
    147135        [ #tr #r #m #E1 #E2 destruct
    148136        | #tr' #s' #e' #se' #H2 #H3 #E2 destruct (E2);
    149             <(exec_e_step … H3) in H2 #H2 % //;
     137            <(exec_e_step … H3) in H2 #H2 % [ 2: @H2 ]
    150138            lapply (STEP i);
    151139            >(exec_e_step_inv … H3)
     
    155143        ]
    156144    | #x cases x; #tr' #s' >(exec_inf_aux_unfold …)
    157         whd in ⊢ (??%? → ?); cases (is_final_state s');
    158         #F #E whd in E:(??%?); destruct
     145        whd in ⊢ (??%? → ?); @is_final_elim
     146        [ #r ] #F #E whd in E:(??%?); destruct
    159147    | >(exec_inf_aux_unfold …)
    160148        #E' whd in E':(??%?); destruct (E');
    161149    ]
    162 ] qed.*)
    163 
    164 axiom exec_from_interact_stop : ∀ge,s,o,k,i,tr,r,m.
     150] qed.
     151
     152lemma exec_from_interact_stop : ∀ge,s,o,k,i,tr,r,m.
    165153exec_from ge s (se_interact o k i (se_stop tr r m)) →
    166154step ge s tr (Returnstate (Vint r) Kstop m).
    167 (*
    168155#ge #s0 #o0 #k0 #i0 #tr0 #s0' #e0 #H inversion H;
    169156[ #tr #r #m #E1 #E2 destruct
     
    183170            [ #o2 #k2 #E whd in E:(??%?); destruct (E)
    184171            | #x cases x; #tr2 #s2 whd in ⊢ (??%? → ?);
    185                 cases (is_final_state s2);
    186                 [ #F cases F; #r' #FINAL #E whd in E:(??%?);
     172                @is_final_elim
     173                [ #r' #FINAL #E whd in E:(??%?);
    187174                    destruct (E);
    188175                    inversion FINAL;
     
    197184       ]
    198185   | #x cases x; #tr #s whd in ⊢ (??%? → ?);
    199        cases (is_final_state s); #F #E whd in E:(??%?); destruct (E)
     186       @is_final_elim [ #r ] #F #E whd in E:(??%?); destruct (E)
    200187   | #E whd in E:(??%?); destruct (E)
    201188   ]
    202 ] qed.*)
     189] qed.
    203190
    204191(* NB: the E0 in the execs are irrelevant. *)
     
    282269] qed.
    283270
    284 axiom final_step: ∀ge,tr,r,m,s.
     271lemma final_step: ∀ge,tr,r,m,s.
    285272  exec_from ge s (se_stop tr r m) →
    286273  step ge s tr (Returnstate (Vint r) Kstop m).
    287   (*
    288274#ge #tr #r #m #s #EXEC
    289275whd in EXEC;
     
    295281    [ #o #k #EXEC' whd in EXEC':(??%?); destruct (EXEC');
    296282    | #x cases x; #tr'' #s' whd in ⊢ (??%? → ?);
    297         cases (is_final_state s'); #F [ 1: cases F; #r'' #FINAL ]
     283        @is_final_elim [ #r'' #FINAL | #F ]
    298284        #EXEC' whd in EXEC':(??%?); destruct (EXEC');
    299285    | #EXEC' whd in EXEC':(??%?); destruct (EXEC');
     
    304290| #EXEC' #E destruct
    305291| #o #k #i #e #H #EXEC #E destruct
    306 ] qed.*)
     292] qed.
    307293
    308294
     
    396382    [ #o #k #EXEC whd in EXEC:(??%?); destruct
    397383    | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?) @is_final_elim
    398         [ #r ] #F #E whd in E:(??%?); [ destruct | generalize in E:(??(??????%)?) ⊢ ? #e0 #E destruct; @F ]
     384        [ #r ] #F #E whd in E:(??%?); destruct @F
    399385    | #E whd in E:(??%?); destruct
    400386    ]
     
    423409            [ #o2 #k2 #EXECK whd in EXECK:(??%?); destruct
    424410            | #x cases x; #tr2 #s2 whd in ⊢ (??%? → ?);
    425                 cases (is_final_state s2); #F #EXECK
     411                @is_final_elim [ #r ] #F #EXECK
    426412                whd in EXECK:(??%?); destruct;
    427413                @(absurd ?? F)
     
    433419        ]
    434420    | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?);
    435         cases (is_final_state s1); #F #E whd in E:(??%?); destruct;
     421        @is_final_elim [ #r ] #F #E whd in E:(??%?); destruct;
    436422    | #E whd in E:(??%?); destruct
    437423    ]
     
    465451        @IH
    466452        [ @(exec_from_interact_step_notfinal … EXEC)
    467         | cases (exec_from_interact … EXEC); //;
     453        | cases (exec_from_interact … EXEC) #STEP #EF1 @EF1
    468454        ]
    469455    ]
     
    714700    >E2 in H1 #H1 whd in H1:(?%?); >K' in H1
    715701    >(exec_inf_aux_unfold …) whd in ⊢ (?%? → ?);
    716     cases (is_final_state s'');
    717     [ #F whd in ⊢ (?%? → ?); #S
     702    @is_final_elim
     703    [ #r #F whd in ⊢ (?%? → ?); #S
    718704        @False_ind @(absurd ? S) cases (se_inv … S)
    719705    | #NF #S whd in S:(?%?); cases (se_inv … S);
    720706        *; #E1 #E2 #S' <E1 @TR
    721707    ]
    722 | #x cases x; #tr' #s'' #H whd in ⊢ (?%? → ?);
    723     cases (is_final_state s''); #F #E whd in E:(?%?);
     708| #x cases x; #tr' #s'' #H whd in ⊢ (?%? → ?)
     709    @is_final_elim [ #r ] #F #E whd in E:(?%?);
    724710    inversion E;
    725711    [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct
     
    909895                cases (H i); #tr1 *; #s1 *; #K #E >K in H2
    910896                >(exec_inf_aux_unfold …)
    911                 whd in ⊢ (?%? → ?); cases (is_final_state s1);
     897                whd in ⊢ (?%? → ?) @is_final_elim [ #r ]
    912898                #F #S whd in S:(?%?); cases (se_inv … S);
    913             | #x cases x; #tr' #s' whd in ⊢ (?%? → ?);
    914                 cases (is_final_state s'); #F #S whd in S:(?%?);
     899            | #x cases x; #tr' #s' whd in ⊢ (?%? → ?)
     900                @is_final_elim [ #r ] #F #S whd in S:(?%?);
    915901                cases (se_inv … S);
    916902            | #S cases (se_inv … S);
     
    926912                cases (H i); #tr1 *; #s1 *; #K #E >K in H2
    927913                >(exec_inf_aux_unfold …)
    928                 whd in ⊢ (?%? → ?); cases (is_final_state s1);
     914                whd in ⊢ (?%? → ?) @is_final_elim [ #r ]
    929915                #F #S whd in S:(?%?); cases (se_inv … S);
    930             | #x cases x; #tr' #s' whd in ⊢ (?%? → ?);
    931                 cases (is_final_state s'); #F #S whd in S:(?%?);
     916            | #x cases x; #tr' #s' whd in ⊢ (?%? → ?)
     917                @is_final_elim [ #r ] #F #S whd in S:(?%?);
    932918                cases (se_inv … S);
    933919            | #S cases (se_inv … S);
     
    1005991
    1006992lemma initial_step: ∀ge,s,e.
    1007   exec_inf_aux ge (Value ??? 〈E0,s〉) = e →
     993  exec_inf_aux clight_exec ge (Value ??? 〈E0,s〉) = e →
    1008994  ¬(∃r.final_state s r) →
    1009   ∃e'.e = e_step E0 s e'.
     995  ∃e'.e = e_step ??? E0 s e'.
    1010996#ge #s #e >(exec_inf_aux_unfold …)
    1011 whd in ⊢ (??%? → ?); cases (is_final_state s);
    1012 [ #FINAL #EXEC #NOTFINAL
     997whd in ⊢ (??%? → ?) @is_final_elim
     998[ #r #FINAL #EXEC #NOTFINAL
    1013999    @False_ind @(absurd ?? NOTFINAL)
    1014     cases FINAL;
    1015     #r #F %{r} @F
     1000    %{r} @FINAL
    10161001| #F1 #EXEC #F2 whd in EXEC:(??%?); % [ 2: <EXEC @refl ]
    10171002qed.
     
    10301015    cases INITIAL; #Ege #INITIAL''
    10311016    >(exec_inf_aux_unfold …)
    1032     whd in ⊢ (?%? → ?);
    1033     cases (is_final_state s);
    1034     [ #F @False_ind
     1017    whd in ⊢ (?%? → ?)
     1018    @is_final_elim
     1019    [ #r #F @False_ind
    10351020        @(absurd ?? (initial_state_not_final … INITIAL''))
    1036         cases F; #r #F' %{r} @F'
     1021        %{r} @F
    10371022    | #NOTFINAL whd in ⊢ (?%? → ?); cases e;
    10381023        [ #tr #r #m #EXEC0 | #tr #s' #e0 #EXEC0 | #EXEC0 | #o #k #i #e #EXEC0 ]
  • src/Clight/CexecSound.ma

    r700 r708  
    536536  ]
    537537qed.
     538
     539lemma is_final_sound: ∀s,r. is_final s = Some ? r → final_state s r.
     540* [ 3: #v * [ #m #r cases v [ 2: #r' #E normalize in E; destruct %
     541                            | *: normalize #x1 try #x2 try #x3 try #x4 try #x5 destruct
     542                            ]
     543            | *: normalize #x1 try #x2 try #x3 try #x4 try #x5 try #x6 try #x7 destruct
     544            ]
     545  | *: normalize #x1 #x2 #x3 #x4 #x5 #x6 try #x7 destruct
     546  ] qed.
Note: See TracChangeset for help on using the changeset viewer.