Ignore:
Timestamp:
Dec 6, 2010, 11:49:57 AM (9 years ago)
Author:
campbell
Message:

More work on equivalence of whole executions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIOcomplete.ma

    r366 r378  
    512512    ##]
    513513##] nqed.
     514
     515ninductive execution_characterisation : execution → Type ≝
     516| ec_terminates: ∀s,s',e,tr.
     517    execution_terminates tr s e s' →
     518    execution_characterisation (e_step E0 s e)
     519| ec_diverges: ∀s,e,tr.
     520    execution_diverges tr e →
     521    execution_characterisation (e_step E0 s e)
     522| ec_reacts: ∀s,e,tr.
     523    execution_reacts tr s e →
     524    execution_characterisation (e_step E0 s e)
     525| ec_wrong: ∀e,s,s',tr.
     526    execution_goes_wrong tr s e s' →
     527    execution_characterisation (e_step E0 s e).
     528
     529(* bit of a hack to avoid inability to reduce term in match *)
     530ndefinition interact_prop : ∀A:Type.(∀o:io_out. (io_in o → IO io_out io_in A) → Prop) → IO io_out io_in A → Prop ≝
     531λA,P,e. match e return λ_.Prop with [ Interact o k ⇒ P o k | _ ⇒ True ].
     532
     533nlemma err_does_not_interact: ∀A,B,P,e1,e2.
     534  (∀x:B.interact_prop A P (e2 x)) →
     535  interact_prop A P (bindIO ?? B A (err_to_io ??? e1) e2).
     536#A B P e1 e2 H;
     537ncases e1; //; nqed.
     538
     539nlemma err2_does_not_interact: ∀A,B,C,P,e1,e2.
     540  (∀x,y.interact_prop A P (e2 x y)) →
     541  interact_prop A P (bindIO2 ?? B C A (err_to_io ??? e1) e2).
     542#A B C P e1 e2 H;
     543ncases e1; ##[ #z; ncases z; ##] //; nqed.
     544
     545nlemma err_sig_does_not_interact: ∀A,B,P.∀Q:B→Prop.∀e1,e2.
     546  (∀x.interact_prop A P (e2 x)) →
     547  interact_prop A P (bindIO ?? (sigma B Q) A (err_to_io_sig ??? Q e1) e2).
     548#A B P Q e1 e2 H;
     549ncases e1; //; nqed.
     550
     551nlemma opt_does_not_interact: ∀A,B,P,e1,e2.
     552  (∀x:B.interact_prop A P (e2 x)) →
     553  interact_prop A P (bindIO ?? B A (opt_to_io ??? e1) e2).
     554#A B P e1 e2 H;
     555ncases e1; //; nqed.
     556
     557nlemma exec_step_interaction:
     558  ∀ge,s. interact_prop ? (λo,k. ∀i.∃tr.∃s'. k i = Value ??? 〈tr,s'〉 ∧ tr ≠ E0) (exec_step ge s).
     559#ge s; ncases s;
     560##[ #f st kk e m; ncases st;
     561  ##[ ##11,14: #a ##| ##2,4,6,7,12,13,15: #a b ##| ##3,5: #a b c ##| ##8: #a b c d ##]
     562  ##[ ##4,6,8,9: napply I ##]
     563  nwhd in ⊢ (???%);
     564  ##[ ncases a; ##[ ncases (fn_return f); //; ##| #e; nwhd nodelta in ⊢ (???%);
     565                    napply err_sig_does_not_interact; #x; napply err2_does_not_interact; // ##]
     566  ##| ncases (find_label a (fn_body f) (call_cont kk)); ##[ napply I ##| #z; ncases z; #x y; napply I ##]
     567  ##| napply err2_does_not_interact; #x1 x2; napply err2_does_not_interact; #x3 x4; napply opt_does_not_interact; #x5; napply I
     568  ##| ##4,7: napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; napply I
     569  ##| napply err2_does_not_interact; #x1 x2; ncases x1; //;
     570  ##| napply err2_does_not_interact; #x1 x2; napply err2_does_not_interact; #x3 x4; napply opt_does_not_interact; #x5;  napply err_does_not_interact; #x6; ncases a;
     571      ##[ napply I; ##| #x7; napply err2_does_not_interact; #x8 x9; napply I ##]
     572  ##| ncases (is_Sskip a); #H; ##[ napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; napply I
     573      ##| napply I ##]
     574  ##| ncases kk; ##[ ##1,8: ncases (fn_return f); //; ##| ##2,3,5,6,7: //;
     575      ##| #z1 z2 z3; napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; ncases x3; napply I ##]
     576  ##| ncases kk; //;
     577  ##| ncases kk; ##[ ##4: #z1 z2 z3;  napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; ncases x3; napply I
     578      ##| ##*: // ##]
     579  ##]
     580##| #f args kk m; ncases f;
     581  ##[ #f'; nwhd in ⊢ (???%); ncases (exec_alloc_variables empty_env m (fn_params f'@fn_vars f'));
     582      #x; ncases x; ##[ *; ##| #z; ncases z; #x1 x2 H;
     583                        napply err_sig_does_not_interact; //; ##]
     584  (* This is the only case that actually matters! *)
     585  ##| #fn argtys rty; nwhd in ⊢ (???%);
     586      napply  err_sig_does_not_interact; #x1;
     587      nwhd; #i; @; ##[ ##2: @; ##[ ##2: @; ##[ @; nwhd in ⊢ (??%?); napply refl;
     588        ##| @; #E; nwhd in E:(??%%); ndestruct (E); ##] ##] ##]
     589  ##]
     590##| #v kk m; nwhd in ⊢ (???%); ncases kk;
     591    ##[ ##8: #x1 x2 x3 x4; ncases x1;
     592      ##[ nwhd in ⊢ (???%); ncases v; // ##| #x5; nwhd in ⊢ (???%); ncases x5;
     593          #x6 x7; napply opt_does_not_interact; // ##]
     594    ##| ##*: // ##]
     595##] nqed.
     596
     597
     598(* Some classical logic (roughly like a fragment of Coq's library) *)
     599nlemma classical_doubleneg:
     600  ∀classic:(∀P:Prop.P ∨ ¬P).
     601  ∀P:Prop. ¬ (¬ P) → P.
     602#classic P; *; #H;
     603ncases (classic P);
     604##[ // ##| #H'; napply False_ind; /2/; ##]
     605nqed.
     606
     607nlemma classical_not_all_not_ex:
     608  ∀classic:(∀P:Prop.P ∨ ¬P).
     609  ∀A:Type.∀P:A → Prop. ¬ (∀x. ¬ P x) → ∃x. P x.
     610#classic A P; *; #H;
     611napply (classical_doubleneg classic); @; *; #H';
     612napply H; #x; @; #H''; napply H'; @x; napply H'';
     613nqed.
     614
     615nlemma classical_not_all_ex_not:
     616  ∀classic:(∀P:Prop.P ∨ ¬P).
     617  ∀A:Type.∀P:A → Prop. ¬ (∀x. P x) → ∃x. ¬ P x.
     618#classic A P; *; #H;
     619napply (classical_not_all_not_ex classic A (λx.¬ P x));
     620@; #H'; napply H; #x; napply (classical_doubleneg classic);
     621napply H';
     622nqed.
     623
     624nlemma not_imply_elim:
     625  ∀classic:(∀P:Prop.P ∨ ¬P).
     626  ∀P,Q:Prop. ¬ (P → Q) → P.
     627#classic P Q; *; #H;
     628napply (classical_doubleneg classic); @; *; #H';
     629napply H; #H''; napply False_ind; napply H'; napply H'';
     630nqed.
     631
     632nlemma not_imply_elim2:
     633  ∀P,Q:Prop. ¬ (P → Q) → ¬ Q.
     634#P Q; *; #H; @; #H';
     635napply H; #_; napply H';
     636nqed.
     637
     638nlemma imply_to_and:
     639  ∀classic:(∀P:Prop.P ∨ ¬P).
     640  ∀P,Q:Prop. ¬ (P → Q) → P ∧ ¬Q.
     641#classic P Q H; @;
     642##[ napply (not_imply_elim classic P Q H);
     643##| napply (not_imply_elim2 P Q H);
     644##] nqed.
     645
     646ninductive execution_not_over : execution → Prop ≝
     647| eno_step: ∀tr,s,e. execution_not_over (e_step tr s e)
     648| eno_interact: ∀o,k,tr,s,e,i.
     649    k i = e_step tr s e →
     650    execution_not_over (e_interact o k).
     651
     652nlemma eno_stop: ∀tr,r,m. execution_not_over (e_stop tr r m) → False.
     653#tr0 r0 m0 H; ninversion H;
     654##[ #tr s e E; ndestruct
     655##| #o k tr s e i K E; ndestruct
     656##] nqed.
     657
     658nlemma eno_wrong: execution_not_over e_wrong → False.
     659#H; ninversion H;
     660##[ #tr s e E; ndestruct
     661##| #o k tr s e i K E; ndestruct
     662##] nqed.
     663
     664nlet corec show_divergence s e
     665 (NONTERMINATING:∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 →
     666                 execution_not_over e1)
     667 (UNREACTIVE:∀tr2,s2,e2. execution_isteps tr2 s e s2 e2 → tr2 = E0)
     668 (CONTINUES:∀tr2,s2,o,k. execution_isteps tr2 s e s2 (e_interact o k) → ∃i.∃tr3.∃s3.∃e3. k i = e_step tr3 s3 e3 ∧ tr3 ≠ E0)
     669 : execution_diverging e ≝ ?.
     670nlapply (NONTERMINATING E0 s e ?); //;
     671ncases e in UNREACTIVE NONTERMINATING CONTINUES ⊢ %;
     672##[ #tr i m; #_; #_; #_; #ENO; nelim (eno_stop … ENO);
     673##| #tr s' e' UNREACTIVE; nlapply (UNREACTIVE tr s' e' ?);
     674  ##[ nrewrite < (E0_right tr) in ⊢ (?%????);
     675      napply isteps_one; napply isteps_none;
     676  ##| #TR; napply (match sym_eq ??? TR with [ refl ⇒ ? ]); (* nrewrite > TR in UNREACTIVE ⊢ %;*)
     677      #NONTERMINATING CONTINUES; #_; @;
     678      napply (show_divergence s');
     679      ##[ #tr1 s1 e1 S; napply (NONTERMINATING tr1 s1 e1);
     680        nchange in ⊢ (?%????) with (Eapp E0 tr1); napply isteps_one;
     681        napply S;
     682      ##| #tr2 s2 e2 S; nrewrite > TR in UNREACTIVE; #UNREACTIVE; napply (UNREACTIVE tr2 s2 e2);
     683          nchange in ⊢ (?%????) with (Eapp E0 tr2);
     684          napply isteps_one; napply S;
     685      ##| #tr2 s2 o k S; napply (CONTINUES tr2 s2 o k);
     686          nchange in ⊢ (?%????) with (Eapp E0 tr2);
     687          napply isteps_one; napply S;
     688      ##]
     689  ##]
     690##| #_; #_; #_; #ENO; nelim (eno_wrong … ENO);
     691##| #o k UNREACTIVE NONTERMINATING CONTINUES; #_;
     692    nlapply (CONTINUES E0 s o k ?);
     693    ##[ napply isteps_none;
     694    ##| *; #i; *; #tr'; *; #s'; *; #e'; *; #EXEC NOTSILENT;
     695        napply False_ind; napply (absurd ?? NOTSILENT);
     696        napply (UNREACTIVE … s' e');
     697        nrewrite < (E0_right tr') in ⊢ (?%????);
     698        napply (isteps_interact … EXEC); //;
     699    ##]
     700##] nqed.
     701
     702nlemma exec_over_isteps: ∀ge,tr,s,s',e,e'.
     703  execution_isteps tr s e s' e' →
     704  e = (exec_inf_aux ge (exec_step ge s)) →
     705  exec_inf_aux ge (exec_step ge s') = e'.
     706#ge tr0 s0 s0' e0 e0';
     707#ISTEPS; nelim ISTEPS;
     708##[ #s e E; nrewrite > E; napply refl;
     709##| #e1 e2 tr1 tr2 s1 s2 s3 ISTEPS' IH E;
     710    napply IH; napply sym_eq; napply exec_e_step;
     711    ##[ ##3: napply sym_eq; napply E ##]
     712##| #e1 e2 o k i s1 s2 s3 tr1 tr2 ISTEPS' EXECK IH E;
     713    napply IH;
     714    ncases (exec_step ge s3) in E;
     715    ##[ #o' k'; nrewrite > (exec_inf_aux_unfold …) in ⊢ (% → ?);
     716        #E'; nwhd in E':(???%); ndestruct (E');
     717        napply sym_eq; napply exec_e_step;
     718        ##[ ##3: napply EXECK; ##]
     719    ##| #z; ncases z; #tr' s';
     720        nrewrite > (exec_inf_aux_unfold …) in ⊢ (% → ?);
     721        nwhd in ⊢ (???% → ?); ncases (is_final_state s');
     722        #F E'; nwhd in E':(???%); ndestruct (E');
     723    ##| nrewrite > (exec_inf_aux_unfold …) in ⊢ (% → ?);
     724        #E'; nwhd in E':(???%); ndestruct (E');
     725    ##]
     726##] nqed.
     727
     728nlemma interaction_is_not_silent: ∀ge,o,k,i,tr,s,s',e.
     729  exec_inf_aux ge (exec_step ge s) = e_interact o k →
     730  k i = e_step tr s' e →
     731  tr ≠ E0.
     732#ge o k i tr s s' e; nrewrite > (exec_inf_aux_unfold …);
     733nlapply (exec_step_interaction ge s);
     734ncases (exec_step ge s);
     735##[ #o' k' ; nwhd in ⊢ (% → ??%? → ?); #H E K; ndestruct (E);
     736    nlapply (H i); *; #tr'; *; #s''; *; #K' TR;
     737    nrewrite > K' in K; nrewrite > (exec_inf_aux_unfold …);
     738    nwhd in ⊢ (??%? → ?);
     739    ncases (is_final_state s'');
     740    ##[ #F; nwhd in ⊢ (??%? → ?); #E; ndestruct (E);
     741    ##| #F; nwhd in ⊢ (??%? → ?); #E; ndestruct (E);
     742        napply TR
     743    ##]
     744##| #x; ncases x; #tr' s'' H; nwhd in ⊢ (??%? → ?);
     745    ncases (is_final_state s''); #F E; nwhd in E:(??%?); ndestruct (E);
     746##| #_; #E; nwhd in E:(??%?); ndestruct (E);
     747##] nqed.
     748
     749nlemma execution_characterisation_complete:
     750  ∀classic:(∀P:Prop.P ∨ ¬P).
     751   ∀ge,s. ¬ (∃r. final_state s r) →
     752   execution_characterisation (exec_inf_aux ge (Value ??? 〈E0,s〉)).
     753#classic ge s; *; #NOTFINAL;
     754nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (?%);
     755ncases (is_final_state s); ##[ #x; ncases x; #r FINAL; napply False_rect_Type0; napply NOTFINAL; @r; napply FINAL ##]
     756#NOTFINAL'; nwhd in ⊢ (?%);
     757ncases (classic (∀tr1,s1,e1. execution_isteps tr1 s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
     758                 execution_not_over e1));
     759##[ #NONTERMINATING;
     760    ncases (classic (∃tr,s1,e1. execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 ∧
     761                     ∀tr2,s2,e2. execution_isteps tr2 s1 e1 s2 e2 → tr2 = E0));
     762  ##[ *; #tr; *; #s1; *; #e1; *; #INITIAL UNREACTIVE;
     763      napply (ec_diverges … tr);
     764      napply (diverges_diverging … INITIAL);
     765      napply (show_divergence s1);
     766      ##[ #tr2 s2 e2 S; napply (NONTERMINATING (Eapp tr tr2) s2 e2);
     767          napply (isteps_trans … INITIAL S);
     768      ##| #tr2 s2 e2 S; napply (UNREACTIVE … S);
     769      ##| #tr2 s2 o; ncases o; #o_id o_args o_typ; ncases o_typ; #k S;
     770          nlapply (exec_over_isteps … INITIAL (refl ??)); #EXEC1;
     771          nlapply (exec_over_isteps … S (sym_eq … EXEC1));
     772          nlapply (NONTERMINATING (Eapp tr tr2) s2 (e_interact (mk_io_out o_id o_args ?) k) ?);
     773          ##[ ##1,3: napply (isteps_trans … INITIAL S); ##]
     774          #NOTOVER; ninversion NOTOVER;
     775          ##[ ##1,3: #tr' s' e' E; ndestruct (E);
     776          ##| ##*: #o' k' tr' s' e' i' KR E; ndestruct (E);
     777              #EXEC;
     778              @ i'; @ tr'; @s'; @e'; @;//; napply (interaction_is_not_silent … EXEC KR);
     779          ##]
     780      ##]
     781
     782 (* FINISH *)
     783  ##| *; #REACTIVE;
     784     (* napply ec_reacts;*)
     785 (* FINISH *)
     786  ##]
     787 
     788##| #NOTNONTERMINATING; nlapply (classical_not_all_ex_not classic … NOTNONTERMINATING);
     789    *; #tr NNT2; nlapply (classical_not_all_ex_not classic … NNT2);
     790    *; #s' NNT3; nlapply (classical_not_all_ex_not classic … NNT3);
     791    *; #e NNT4; nelim (imply_to_and classic … NNT4);
     792    ncases e;
     793    ##[ #tr' r m; #STEPS NOSTEP;
     794        napply (ec_terminates s (Returnstate (Vint r) Kstop m) ? (Eapp tr tr')); @;
     795        ##[ napply s'
     796        ##| napply STEPS
     797        ##]
     798    ##| #tr' s'' e' STEPS; *; #NOSTEP; napply False_rect_Type0;
     799        napply NOSTEP; //
     800    ##| #STEPS NOSTEP;
     801        napply (ec_wrong ? s s' tr); @; //;
     802    (* The following is stupidly complicated for an impossible case.
     803       It ought to be simplified. *)
     804    ##| #o; ncases o; #o_id o_args o_rty; ncases o_rty; #k STEPS NOSTEP;
     805        ##[ nletin i ≝ (repr 0) ##| nletin i ≝ Fzero ##]
     806        nlapply (refl ? (k i));
     807        ncases (k i) in ⊢ (???% → ?);
     808        ##[ ##1,5: #tr' r m K;
     809                   napply (ec_terminates s ???);
     810                   ##[ ##3,6: napply (annoying_corner_case_terminates … STEPS K);
     811                   ##| ##*: ##skip
     812                   ##]
     813        ##| ##2,6: #tr' s'' e' K; napply False_rect_Type0;
     814            napply (absurd ?? NOSTEP);
     815            napply (eno_interact … K);
     816        ##| ##3,7: #K;
     817            nlapply (exec_step_interaction ge s');
     818            nlapply (exec_over_isteps … STEPS (refl ??));
     819            nrewrite > (exec_inf_aux_unfold …); ncases (exec_step ge s');
     820            ##[ ##1,4: #o k E H; nwhd in E:(??%?) H;
     821                ndestruct (E);
     822                nlapply (H i); *; #tr'; *; #s'; *; #K'; nrewrite > K' in K;
     823                nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (??%? → ?);
     824                ncases (is_final_state s'); #F E; nwhd in E:(??%?);
     825                ndestruct (E);
     826            ##| ##2,5: #z; ncases z; #tr s; nwhd in ⊢ (??%? → ?);
     827                ncases (is_final_state s); #F E; nwhd in E:(??%?);
     828                ndestruct (E);
     829            ##| ##3,6: #E; nwhd in E:(??%?); ndestruct (E);
     830            ##]
     831        ##| ##4,8: #o0 k0 K;
     832            nlapply (exec_step_interaction ge s');
     833            nlapply (exec_over_isteps … STEPS (refl ??));
     834            nrewrite > (exec_inf_aux_unfold …); ncases (exec_step ge s');
     835            ##[ ##1,4: #o k E H; nwhd in E:(??%?) H;
     836                ndestruct (E);
     837                nlapply (H i); *; #tr'; *; #s'; *; #K'; nrewrite > K' in K;
     838                nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (??%? → ?);
     839                ncases (is_final_state s'); #F E; nwhd in E:(??%?);
     840                ndestruct (E);
     841            ##| ##2,5: #z; ncases z; #tr s; nwhd in ⊢ (??%? → ?);
     842                ncases (is_final_state s); #F E; nwhd in E:(??%?);
     843                ndestruct (E);
     844            ##| ##3,6: #E; nwhd in E:(??%?); ndestruct (E);
     845            ##]
     846        ##]
     847    ##]
     848##]
     849   
     850
     851ndefinition behaviour_of_execution:
     852 execution_characterisation → program_behavior ≝
     853λexec.match exec with
     854[ ec_terminates s s' e tr H ⇒ Terminates tr ?
     855| ec_diverges e tr H ⇒ Diverges tr
     856| ec_reacts s e tr H ⇒ Reacts tr
     857| ec_wrong e s s' tr H ⇒ Goes_wrong tr
     858].
     859
Note: See TracChangeset for help on using the changeset viewer.