Ignore:
Timestamp:
Dec 9, 2010, 8:35:41 PM (10 years ago)
Author:
campbell
Message:

This time actually prove the result I intended.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIOcomplete.ma

    r393 r398  
    1 include "CexecIO.ma".
     1include "CexecIOequiv.ma".
    22include "Plogic/connectives.ma".
    33
     
    474474##| #f l s k env m; napply refl
    475475##] nqed.
    476  
     476
     477nlemma exec_from_wrong: ∀ge,s.
     478  exec_from ge s se_wrong →
     479  exec_step ge s = Wrong ???.
     480#ge s H; nwhd in H;
     481ninversion H;
     482##[ #tr r m EXEC E; ndestruct (E)
     483##| #tr s' e e' H EXEC E; ndestruct (E)
     484##| nrewrite > (exec_inf_aux_unfold …);
     485    ncases (exec_step ge s);
     486  ##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct
     487  ##| #x; ncases x; #tr s'; nwhd in ⊢ (??%? → ?); ncases (is_final_state s');
     488      #F EXEC; nwhd in EXEC:(??%?); ndestruct
     489  ##| //
     490  ##]
     491##| #o k i e H EXEC E; ndestruct
     492##] nqed.
     493
     494nlemma exec_from_step_notfinal: ∀ge,s,tr,s',e.
     495  exec_from ge s (se_step tr s' e) →
     496  ¬(∃r. final_state s' r).
     497#ge s tr s' e H; nwhd in H; ninversion H;
     498##[ #tr' r m EXEC E; ndestruct
     499##| #tr' s'' e' e'' H EXEC E; ndestruct (E);
     500    nrewrite > (exec_inf_aux_unfold …) in EXEC;
     501    ncases (exec_step ge s);
     502    ##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct
     503    ##| #x; ncases x; #tr1 s1; nwhd in ⊢ (??%? → ?); ncases (is_final_state s1);
     504        #F E; nwhd in E:(??%?); ndestruct; napply F;
     505    ##| #E; nwhd in E:(??%?); ndestruct
     506    ##]
     507##| #EXEC E; ndestruct
     508##| #o k i e' H EXEC E; ndestruct
     509##] nqed.
     510
     511nlemma exec_from_interact_step_notfinal: ∀ge,s,o,k,i,tr,s',e.
     512  exec_from ge s (se_interact o k i (se_step tr s' e)) →
     513  ¬(∃r. final_state s' r).
     514#ge s o k i tr s' e H;
     515@; *; #r F; ncases F in H; #r' m H;
     516ninversion H;
     517##[ #tr' r m EXEC E; ndestruct
     518##| #tr' s'' e' e'' H EXEC E; ndestruct (E);
     519##| #EXEC E; ndestruct
     520##| #o' k' i' e' H EXEC E; ndestruct;
     521    nrewrite > (exec_inf_aux_unfold …) in EXEC;
     522    ncases (exec_step ge s);
     523    ##[ #o1 k1 EXEC1; nwhd in EXEC1:(??%?); ndestruct (EXEC1);
     524        ninversion H;
     525        ##[ #tr1 r1 m1 EXECK E; ndestruct (E);
     526        ##| #tr1 s1 e1 e2 H1 EXECK E; ndestruct (E);
     527            nrewrite > (exec_inf_aux_unfold …) in EXECK;
     528            ncases (k1 i');
     529            ##[ #o2 k2 EXECK; nwhd in EXECK:(??%?); ndestruct
     530            ##| #x; ncases x; #tr2 s2; nwhd in ⊢ (??%? → ?);
     531                ncases (is_final_state s2); #F EXECK;
     532                nwhd in EXECK:(??%?); ndestruct;
     533                napply (absurd ?? F);
     534                @ r'; //;
     535            ##| #E; nwhd in E:(??%?); ndestruct
     536            ##]
     537        ##| #EXECK E;  nwhd in E:(??%?); ndestruct
     538        ##| #o2 k2 i2 e2 H2 EXECK E; ndestruct
     539        ##]
     540    ##| #x; ncases x; #tr1 s1; nwhd in ⊢ (??%? → ?);
     541        ncases (is_final_state s1); #F E; nwhd in E:(??%?); ndestruct;
     542    ##| #E; nwhd in E:(??%?); ndestruct
     543    ##]
     544##] nqed.
     545
    477546nlemma wrong_sound: ∀ge,tr,s,s',e.
    478   execution_goes_wrong tr s (e_step E0 s e) s' →
    479   exec_inf_aux ge (Value ??? 〈E0, s〉) = e_step E0 s e →
     547  execution_goes_wrong tr s (se_step E0 s e) s' →
     548  exec_from ge s e →
     549  (¬∃r. final_state s r) →
    480550  star (mk_transrel … step) ge s tr s' ∧
    481551  nostep (mk_transrel … step) ge s' ∧
    482552  (¬∃r. final_state s' r).
    483 #ge tr0 s0 s0' e0 WRONG; ncases WRONG;
    484 #tr s s' e ESTEPS EXEC;
     553#ge tr0 s0 s0' e0 WRONG; ninversion WRONG;
     554#tr s s' e ESTEPS E1 E2 E3 E4 EXEC NOTFINAL; ndestruct (E1 E2 E3 E4);
    485555ncases (several_steps … ESTEPS EXEC);
    486556#STAR EXEC'; @;
     
    488558       ##| #badtr bads; @; #badSTEP;
    489559           nlapply (step_complete … badSTEP);
    490            nlapply (exec_e_step … EXEC');
    491            ncases (exec_step ge s');
    492            ##[ #o k; nrewrite > (execution_cases (exec_inf_aux …)); #E; nwhd in E:(??%?);
    493                ndestruct
    494            ##| #x; ncases x; #trx stx; nrewrite > (exec_inf_aux_unfold …);
    495                nwhd in ⊢ (??%? → ?); ncases (is_final_state stx);
    496                #FINAL E; nwhd in E:(??%?); ndestruct
    497            ##| #E H; nwhd in H; napply H
    498            ##]
     560           nrewrite > (exec_from_wrong … EXEC');
     561           //;
    499562       ##]
    500 ##| @; #FINAL;
    501     nrewrite > (exec_inf_aux_unfold …) in EXEC';
    502     nwhd in ⊢ (??%? → ?);
    503     ncases (is_final_state s'); #FINAL';
    504     ##[ nwhd in ⊢ (??%? → ?); #E; ndestruct;
    505     ##| napply False_ind; napply (absurd … FINAL FINAL');
     563##| @;
     564    nelim ESTEPS in NOTFINAL EXEC ⊢ %;
     565    ##[ #s1 e1 NF EX F; napply (absurd ? F NF);
     566    ##| #e1 e2 tr1 tr2 s1 s2 s3 ESTEPS1 IH NF EXEC;
     567        ncases (exec_from_step … EXEC); #EXEC3 EXEC1;
     568        napply (IH … EXEC1);
     569        napply (exec_from_step_notfinal … EXEC);
     570    ##| #e1 e2 o k i s1 s2 s3 tr1 tr2 ESTEPS1 IH NF EXEC;
     571        napply IH;
     572        ##[ napply (exec_from_interact_step_notfinal … EXEC);
     573        ##| ncases (exec_from_interact … EXEC); //;
     574        ##]
    506575    ##]
    507 ##] nqed. 
    508 
    509 ninductive execution_characterisation : state → execution → Prop ≝
     576##] nqed.
     577
     578ninductive execution_characterisation : state → s_execution → Prop ≝
    510579| ec_terminates: ∀s,r,m,e,tr.
    511580    execution_terminates tr s e r m →
     
    651720nqed.
    652721
    653 ninductive execution_not_over : execution → Prop ≝
    654 | eno_step: ∀tr,s,e. execution_not_over (e_step tr s e)
    655 | eno_interact: ∀o,k,tr,s,e,i.
    656     k i = e_step tr s e →
    657     execution_not_over (e_interact o k).
    658 
    659 nlemma eno_stop: ∀tr,r,m. execution_not_over (e_stop tr r m) → False.
     722ninductive execution_not_over : s_execution → Prop ≝
     723| eno_step: ∀tr,s,e. execution_not_over (se_step tr s e)
     724| eno_interact: ∀o,k,tr,s,e,i. execution_not_over (se_interact o k i (se_step tr s e)).
     725
     726nlemma eno_stop: ∀tr,r,m. execution_not_over (se_stop tr r m) → False.
    660727#tr0 r0 m0 H; ninversion H;
    661728##[ #tr s e E; ndestruct
    662 ##| #o k tr s e i K E; ndestruct
    663 ##] nqed.
    664 
    665 nlemma eno_wrong: execution_not_over e_wrong → False.
     729##| #o k tr s e i E; ndestruct
     730##] nqed.
     731
     732nlemma eno_wrong: execution_not_over se_wrong → False.
    666733#H; ninversion H;
    667734##[ #tr s e E; ndestruct
    668 ##| #o k tr s e i K E; ndestruct
     735##| #o k tr s e i E; ndestruct
    669736##] nqed.
    670737
     
    673740                 execution_not_over e1)
    674741 (UNREACTIVE:∀tr2,s2,e2. execution_isteps tr2 s e s2 e2 → tr2 = E0)
    675  (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)
     742 (CONTINUES:∀tr2,s2,o,k,i,e'. execution_isteps tr2 s e s2 (se_interact o k i e') → ∃tr3.∃s3.∃e3. e' = se_step tr3 s3 e3 ∧ tr3 ≠ E0)
    676743 : execution_diverging e ≝ ?.
    677744nlapply (NONTERMINATING E0 s e ?); //;
     
    690757          nchange in ⊢ (?%????) with (Eapp E0 tr2);
    691758          napply isteps_one; napply S;
    692       ##| #tr2 s2 o k S; napply (CONTINUES tr2 s2 o k);
     759      ##| #tr2 s2 o k i e2 S; napply (CONTINUES tr2 s2 o k i);
    693760          nchange in ⊢ (?%????) with (Eapp E0 tr2);
    694           napply isteps_one; napply S;
     761          napply (isteps_one … S);
    695762      ##]
    696763  ##]
    697764##| #_; #_; #_; #ENO; nelim (eno_wrong … ENO);
    698 ##| #o k UNREACTIVE NONTERMINATING CONTINUES; #_;
    699     nlapply (CONTINUES E0 s o k ?);
    700     ##[ napply isteps_none;
    701     ##| *; #i; *; #tr'; *; #s'; *; #e'; *; #EXEC NOTSILENT;
    702         napply False_ind; napply (absurd ?? NOTSILENT);
    703         napply (UNREACTIVE … s' e');
    704         nrewrite < (E0_right tr') in ⊢ (?%????);
    705         napply (isteps_interact … EXEC); //;
    706     ##]
    707 ##] nqed.
    708 
     765##| #o k i e' UNREACTIVE NONTERMINATING CONTINUES; #_;
     766    nlapply (CONTINUES E0 s o k i e' (isteps_none …));
     767    *; #tr'; *; #s'; *; #e'; *; #EXEC NOTSILENT;
     768    napply False_ind; napply (absurd ?? NOTSILENT);
     769    napply (UNREACTIVE … s' e');
     770    nrewrite < (E0_right tr') in ⊢ (?%????);
     771    nrewrite > EXEC;
     772    napply isteps_interact; //;
     773##] nqed.
     774(*
    709775nlemma exec_over_isteps: ∀ge,tr,s,s',e,e'.
    710776  execution_isteps tr s e s' e' →
     
    739805napply (exec_over_isteps … H (refl ??));
    740806nqed.
     807*)
     808include "Plogic/jmeq.ma".
     809
     810nlemma se_inv: ∀e1,e2.
     811  single_exec_of e1 e2 →
     812  match e1 with
     813  [ e_stop tr r m ⇒ match e2 with [ se_stop tr' r' m' ⇒ tr = tr' ∧ r = r' ∧ m = m' | _ ⇒ False ]
     814  | e_step tr s e1' ⇒ match e2 with [ se_step tr' s' e2' ⇒ tr = tr' ∧ s = s' ∧ single_exec_of e1' e2' | _ ⇒ False ]
     815  | e_wrong ⇒ match e2 with [ se_wrong ⇒ True | _ ⇒ False ]
     816  | e_interact o k ⇒ match e2 with [ se_interact o' k' i e ⇒ o' = o ∧ k' ≃ k ∧ single_exec_of (k' i) e | _ ⇒ False ]
     817  ].
     818#e01 e02 H;
     819ncases H;
     820##[ #tr r m; nwhd; @; ##[ @ ##] //
     821##| #tr s e1' e2' H'; nwhd; @; ##[ @ ##] //
     822##| nwhd; //
     823##| #o k i e H'; nwhd; @; ##[ @ ##] //
     824##] nqed.
    741825
    742826nlemma interaction_is_not_silent: ∀ge,o,k,i,tr,s,s',e.
    743   exec_inf_aux ge (exec_step ge s) = e_interact o k →
    744   k i = e_step tr s' e →
     827  exec_from ge s (se_interact o k i (se_step tr s' e)) →
    745828  tr ≠ E0.
    746 #ge o k i tr s s' e; nrewrite > (exec_inf_aux_unfold …);
     829#ge o k i tr s s' e; nwhd in ⊢ (% → ?); nrewrite > (exec_inf_aux_unfold …);
    747830nlapply (exec_step_interaction ge s);
    748831ncases (exec_step ge s);
    749 ##[ #o' k' ; nwhd in ⊢ (% → ??%? → ?); #H E K; ndestruct (E);
     832##[ #o' k' ; nwhd in ⊢ (% → ?%? → ?); #H K; ncases (se_inv … K);
     833    *; #E1 E2 H1; ndestruct (E1);
    750834    nlapply (H i); *; #tr'; *; #s''; *; #K' TR;
    751     nrewrite > K' in K; nrewrite > (exec_inf_aux_unfold …);
    752     nwhd in ⊢ (??%? → ?);
     835    nrewrite > E2 in H1; #H1; nwhd in H1:(?%?); nrewrite > K' in H1;
     836    nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (?%? → ?);
    753837    ncases (is_final_state s'');
    754     ##[ #F; nwhd in ⊢ (??%? → ?); #E; ndestruct (E);
    755     ##| #F; nwhd in ⊢ (??%? → ?); #E; ndestruct (E);
    756         napply TR
     838    ##[ #F; nwhd in ⊢ (?%? → ?); #S;
     839        napply False_ind; napply (absurd ? S); ncases (se_inv … S)
     840    ##| #NF S; nwhd in S:(?%?); ncases (se_inv … S);
     841        *; #E1 E2 S'; nrewrite < E1; napply TR
    757842    ##]
    758 ##| #x; ncases x; #tr' s'' H; nwhd in ⊢ (??%? → ?);
    759     ncases (is_final_state s''); #F E; nwhd in E:(??%?); ndestruct (E);
    760 ##| #_; #E; nwhd in E:(??%?); ndestruct (E);
    761 ##] nqed.
    762 
    763 nlet corec reactive_traceinf' ge s
     843##| #x; ncases x; #tr' s'' H; nwhd in ⊢ (?%? → ?);
     844    ncases (is_final_state s''); #F E; nwhd in E:(?%?);
     845    ninversion E;
     846    ##[ ##1,5: #tr1 e1 m1 E1 E2; ndestruct
     847    ##| ##2,6: #tr s1 e1 e2 H E1 E2; ndestruct
     848    ##| ##3,7: #E; ndestruct
     849    ##| ##4,8: #o1 k1 i1 e1 H1 E1 E2; ndestruct
     850    ##]
     851##| #_; #E; nwhd in E:(?%?);
     852    ninversion E;
     853    ##[ ##1,5: #tr1 e1 m1 E1 E2; ndestruct
     854    ##| ##2,6: #tr s1 e1 e2 H E1 E2; ndestruct
     855    ##| ##3,7: #E1 E2; ndestruct
     856    ##| ##4,8: #o1 k1 i1 e1 H1 E1 E2; ndestruct
     857    ##]
     858##] nqed.
     859
     860nlet corec reactive_traceinf' ge s e
     861  (EXEC:exec_from ge s e)
    764862  (REACTIVE: ∀tr,s1,e1.
    765     execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
     863    execution_isteps tr s e s1 e1 →
    766864    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
    767865  : traceinf' ≝ ?.
    768 nlapply (REACTIVE E0 s (exec_inf_aux ge (exec_step ge s)) ?);
    769 ##[ napply isteps_none
    770 ##| *; #x; ncases x; #tr; #y; ncases y; #s' e; *; #STEPS H;
    771     @ tr ? H;
    772     napply (reactive_traceinf' ge s');
    773     #tr1 s1 e1 STEPS1;
     866nlapply (REACTIVE E0 s e (isteps_none …));
     867*; #x; ncases x; #tr; #y; ncases y; #s' e'; *; #STEPS H;
     868@ tr ? H;
     869napply (reactive_traceinf' ge s' e' ?);
     870##[ ncases (several_steps … STEPS EXEC); #_; //
     871##| #tr1 s1 e1 STEPS1;
    774872    napply REACTIVE;
    775     ##[ ##2: nrewrite > (exec_over_isteps' … STEPS) in STEPS1; #STEPS1;
     873    ##[ ##2:
    776874        napply (isteps_trans … STEPS STEPS1);
    777875    ##| ##skip
     
    782880(* A slightly different version of the above, to work around a problem with the
    783881   next result. *)
    784 nlet corec reactive_traceinf'' ge s
    785   (REACTIVE0: Σx.execution_isteps (\fst x) s (exec_inf_aux ge (exec_step ge s)) (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
     882nlet corec reactive_traceinf'' ge s e
     883  (EXEC:exec_from ge s e)
     884  (REACTIVE0: Σx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
    786885  (REACTIVE: ∀tr,s1,e1.
    787     execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
     886    execution_isteps tr s e s1 e1 →
    788887    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
    789888  : traceinf' ≝ ?.
    790 ncases REACTIVE0; #x; ncases x; #tr; #y; ncases y; #s' e; *; #STEPS H;
    791     @ tr ? H;
    792     napply (reactive_traceinf'' ge s');
    793     ##[ napply REACTIVE; ##[ ##2: nlapply (exec_over_isteps' … STEPS);
    794                                   #E; nrewrite > E in STEPS;
    795                                   #STEPS; napply STEPS; ##]
    796     ##|
    797     #tr1 s1 e1 STEPS1;
     889ncases REACTIVE0; #x; ncases x; #tr; #y; ncases y; #s' e'; *; #STEPS H;
     890@ tr ? H;
     891napply (reactive_traceinf'' ge s' e' ?);
     892##[ ncases (several_steps … STEPS EXEC); #_; //
     893##| napply (REACTIVE … STEPS);
     894##| #tr1 s1 e1 STEPS1;
    798895    napply REACTIVE;
    799     ##[ ##2: nrewrite > (exec_over_isteps' … STEPS) in STEPS1; #STEPS1;
     896    ##[ ##2:
    800897        napply (isteps_trans … STEPS STEPS1);
    801898    ##| ##skip
    802899    ##]
    803 ##]
    804 nqed.
     900##] nqed.
    805901
    806902(* We want to prove
     
    816912we can do case analysis on, then get it into the desired form afterwards.
    817913*)
    818 nlet corec show_reactive' ge s
    819   (REACTIVE0: Σx.execution_isteps (\fst x) s (exec_inf_aux ge (exec_step ge s)) (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
     914nlet corec show_reactive' ge s e
     915  (EXEC:exec_from ge s e)
     916  (REACTIVE0: Σx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
    820917  (REACTIVE: ∀tr1,s1,e1.
    821     execution_isteps tr1 s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
     918    execution_isteps tr1 s e s1 e1 →
    822919    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
    823   : execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s REACTIVE0 REACTIVE)) s (exec_inf_aux ge (exec_step ge s)) ≝ ?.
     920  : execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s e EXEC REACTIVE0 REACTIVE)) s e ≝ ?.
    824921(*nrewrite > (unroll_traceinf' (reactive_traceinf'' …));*)
    825922napply (match sym_eq ??? (unroll_traceinf' (reactive_traceinf'' …)) with [ refl ⇒ ? ]);
     
    830927napply (match sym_eq ??? (traceinf_traceinfp_app …) with [ refl ⇒ ? ]);
    831928napply (reacting … STEPS NOTSILENT);
    832 (*nrewrite < (exec_over_isteps' … STEPS) in ⊢ (???%);*)
    833 napply (match (exec_over_isteps' … STEPS) return λe'.λ_.
    834 ?(?(reactive_traceinf'' ??
    835 (REACTIVE ??? (eq_ind_r execution e1 (λx.λ_.execution_isteps ???? e1 → ?) (λS.S) ? (exec_over_isteps' ???? e1 STEPS) STEPS))
    836 (λtr2,s2,e2,S1.REACTIVE ? s2 e2 (eq_ind_r execution e1 (λx.λ_:x=e1.execution_isteps tr2 s1 x s2 e2 → ?) (λS.isteps_trans ?????? e1 ? STEPS S) ? (exec_over_isteps' ???? e1 STEPS) S1))
    837 ))? e'
    838  with [ refl ⇒ ? ]);
    839929napply show_reactive';
    840930nqed.
    841931
    842 nlemma show_reactive : ∀ge,s.
     932nlemma show_reactive : ∀ge,s,e.
     933  ∀EXEC:exec_from ge s e.
    843934  ∀REACTIVE:∀tr,s1,e1.
    844     execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
     935    execution_isteps tr s e s1 e1 →
    845936    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0.
    846   execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s ? REACTIVE)) s (exec_inf_aux ge (exec_step ge s)).
    847 ##[
    848 #ge s REACTIVE;
    849 napply show_reactive';
     937  execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s e EXEC ? REACTIVE)) s e.
     938##[ #ge s e EXEC REACTIVE;
     939    napply show_reactive';
    850940##| napply (REACTIVE … (isteps_none …));
    851941##] nqed.
     
    854944  ∀classic:(∀P:Prop.P ∨ ¬P).
    855945  ∀constructive_indefinite_description:(∀A:Type. ∀P:A→Prop. (∃x. P x) → Σx : A. P x).
    856    ∀ge,s. ¬ (∃r. final_state s r) →
    857    execution_characterisation s (exec_inf_aux ge (Value ??? 〈E0,s〉)).
    858 #classic constructive_indefinite_description ge s; *; #NOTFINAL;
    859 nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (??%);
    860 ncases (is_final_state s); ##[ #x; ncases x; #r FINAL; napply False_rect_Type0; napply NOTFINAL; @r; napply FINAL ##]
    861 #NOTFINAL'; nwhd in ⊢ (??%);
    862 ncases (classic (∀tr1,s1,e1. execution_isteps tr1 s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
     946   ∀ge,s,e.
     947   exec_from ge s e →
     948   execution_characterisation s (se_step E0 s e).
     949#classic constructive_indefinite_description ge s e EXEC;
     950ncases (classic (∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 →
    863951                 execution_not_over e1));
    864952##[ #NONTERMINATING;
    865     ncases (classic (∃tr,s1,e1. execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 ∧
     953    ncases (classic (∃tr,s1,e1. execution_isteps tr s e s1 e1 ∧
    866954                     ∀tr2,s2,e2. execution_isteps tr2 s1 e1 s2 e2 → tr2 = E0));
    867955  ##[ *; #tr; *; #s1; *; #e1; *; #INITIAL UNREACTIVE;
    868956      napply (ec_diverges … s ? tr);
    869957      napply (diverges_diverging … INITIAL);
    870       napply (show_divergence s1);
     958      napply (show_divergence s1 e1);
    871959      ##[ #tr2 s2 e2 S; napply (NONTERMINATING (Eapp tr tr2) s2 e2);
    872960          napply (isteps_trans … INITIAL S);
    873961      ##| #tr2 s2 e2 S; napply (UNREACTIVE … S);
    874       ##| #tr2 s2 o; ncases o; #o_id o_args o_typ; ncases o_typ; #k S;
    875           nlapply (exec_over_isteps … INITIAL (refl ??)); #EXEC1;
    876           nlapply (exec_over_isteps … S (sym_eq … EXEC1));
    877           nlapply (NONTERMINATING (Eapp tr tr2) s2 (e_interact (mk_io_out o_id o_args ?) k) ?);
    878           ##[ ##1,3: napply (isteps_trans … INITIAL S); ##]
     962      ##| #tr2 s2 o k i e2 STEPS;
     963          nlapply (NONTERMINATING (Eapp tr tr2) s2 (se_interact o k i e2) ?);
     964          ##[ napply (isteps_trans … INITIAL STEPS) ##]
    879965          #NOTOVER; ninversion NOTOVER;
    880           ##[ ##1,3: #tr' s' e' E; ndestruct (E);
    881           ##| ##*: #o' k' tr' s' e' i' KR E; ndestruct (E);
    882               #EXEC;
    883               @ i'; @ tr'; @s'; @e'; @;//; napply (interaction_is_not_silent … EXEC KR);
     966          ##[ #tr' s' e' E; ndestruct (E);
     967          ##| #o' k' tr' s' e' i' E; ndestruct (E);
     968              @ tr'; @s'; @e'; @;//;
     969              ncases (several_steps … INITIAL EXEC); #_; #EXEC1;
     970              ncases (several_steps … STEPS EXEC1); #_; #EXEC2;
     971              napply (interaction_is_not_silent … EXEC2);
    884972          ##]
    885973      ##]
    886974
    887975  ##| *; #NOTUNREACTIVE;
    888       ncut (∀tr,s1,e1.execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
     976      ncut (∀tr,s1,e1.execution_isteps tr s e s1 e1 →
    889977            ∃x.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0);
    890978      ##[ #tr s1 e1 STEPS;
     
    900988          napply ec_reacts;
    901989          ##[ ##2: napply reacts;
    902                    napply (show_reactive ge s …);
     990                   napply (show_reactive ge s … EXEC);
    903991                   #tr s1 e1 STEPS;
    904992                   napply constructive_indefinite_description;
     
    9251013    (* The following is stupidly complicated when most of the cases are impossible.
    9261014       It ought to be simplified. *)
    927     ##| #o; ncases o; #o_id o_args o_rty; ncases o_rty; #k STEPS NOSTEP;
    928         ##[ nletin i ≝ (repr 0) ##| nletin i ≝ Fzero ##]
    929         nlapply (refl ? (k i));
    930         ncases (k i) in ⊢ (???% → ?);
    931         ##[ ##1,5: #tr' r m K;
    932                    napply (ec_terminates s ???);
    933                    ##[ ##4,8: napply (annoying_corner_case_terminates … STEPS K);
    934                    ##| ##*: ##skip
    935                    ##]
    936         ##| ##2,6: #tr' s'' e' K; napply False_rect_Type0;
    937             napply (absurd ?? NOSTEP);
    938             napply (eno_interact … K);
    939         ##| ##3,7: #K;
     1015    ##| #o k i e' STEPS NOSTEP;
     1016        ncases e' in STEPS NOSTEP;
     1017        ##[ #tr' r m STEPS NOSTEP;
     1018            napply (ec_terminates s ???);
     1019           ##[ ##4: napply (annoying_corner_case_terminates … STEPS); ##]
     1020        ##| #tr1 s1 e1 STEPS; *; #NOSTEP;
     1021            napply False_ind; napply NOSTEP; //
     1022        ##| #STEPS NOSTEP;
    9401023            nlapply (exec_step_interaction ge s');
    941             nlapply (exec_over_isteps … STEPS (refl ??));
    942             nrewrite > (exec_inf_aux_unfold …); ncases (exec_step ge s');
    943             ##[ ##1,4: #o k E H; nwhd in E:(??%?) H;
    944                 ndestruct (E);
    945                 nlapply (H i); *; #tr'; *; #s'; *; #K'; nrewrite > K' in K;
    946                 nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (??%? → ?);
    947                 ncases (is_final_state s'); #F E; nwhd in E:(??%?);
    948                 ndestruct (E);
    949             ##| ##2,5: #z; ncases z; #tr s; nwhd in ⊢ (??%? → ?);
    950                 ncases (is_final_state s); #F E; nwhd in E:(??%?);
    951                 ndestruct (E);
    952             ##| ##3,6: #E; nwhd in E:(??%?); ndestruct (E);
     1024            ncases (several_steps … STEPS EXEC); #_;
     1025            nwhd in ⊢ (% → ?);
     1026            nrewrite > (exec_inf_aux_unfold …);
     1027            ncases (exec_step ge s');
     1028            ##[ #o1 k1 EXEC' H; nwhd in EXEC':(?%?) H;
     1029                ncases (se_inv … EXEC'); *; #E1 E2 H2; ndestruct (E1 E2);
     1030                ncases (H i); #tr1; *; #s1; *; #K E; nrewrite > K in H2;
     1031                nrewrite > (exec_inf_aux_unfold …);
     1032                nwhd in ⊢ (?%? → ?); ncases (is_final_state s1);
     1033                #F S; nwhd in S:(?%?); ncases (se_inv … S);
     1034            ##| #x; ncases x; #tr' s'; nwhd in ⊢ (?%? → ?);
     1035                ncases (is_final_state s'); #F S; nwhd in S:(?%?);
     1036                ncases (se_inv … S);
     1037            ##| #S; ncases (se_inv … S);
    9531038            ##]
    954         ##| ##4,8: #o0 k0 K;
     1039        ##| #o1 k1 i1 e1 STEPS NOSTEP;
    9551040            nlapply (exec_step_interaction ge s');
    956             nlapply (exec_over_isteps … STEPS (refl ??));
    957             nrewrite > (exec_inf_aux_unfold …); ncases (exec_step ge s');
    958             ##[ ##1,4: #o k E H; nwhd in E:(??%?) H;
    959                 ndestruct (E);
    960                 nlapply (H i); *; #tr'; *; #s'; *; #K'; nrewrite > K' in K;
    961                 nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (??%? → ?);
    962                 ncases (is_final_state s'); #F E; nwhd in E:(??%?);
    963                 ndestruct (E);
    964             ##| ##2,5: #z; ncases z; #tr s; nwhd in ⊢ (??%? → ?);
    965                 ncases (is_final_state s); #F E; nwhd in E:(??%?);
    966                 ndestruct (E);
    967             ##| ##3,6: #E; nwhd in E:(??%?); ndestruct (E);
     1041            ncases (several_steps … STEPS EXEC); #_;
     1042            nwhd in ⊢ (% → ?);
     1043            nrewrite > (exec_inf_aux_unfold …);
     1044            ncases (exec_step ge s');
     1045            ##[ #o1 k1 EXEC' H; nwhd in EXEC':(?%?) H;
     1046                ncases (se_inv … EXEC'); *; #E1 E2 H2; ndestruct (E1 E2);
     1047                ncases (H i); #tr1; *; #s1; *; #K E; nrewrite > K in H2;
     1048                nrewrite > (exec_inf_aux_unfold …);
     1049                nwhd in ⊢ (?%? → ?); ncases (is_final_state s1);
     1050                #F S; nwhd in S:(?%?); ncases (se_inv … S);
     1051            ##| #x; ncases x; #tr' s'; nwhd in ⊢ (?%? → ?);
     1052                ncases (is_final_state s'); #F S; nwhd in S:(?%?);
     1053                ncases (se_inv … S);
     1054            ##| #S; ncases (se_inv … S);
    9681055            ##]
    9691056        ##]
     
    9721059nqed.   
    9731060
    974 ninductive execution_matches_behavior: execution → program_behavior → Prop ≝
     1061ninductive execution_matches_behavior: s_execution → program_behavior → Prop ≝
    9751062| emb_terminates: ∀s,e,tr,r,m.
    9761063    execution_terminates tr s e r m →
     
    9861073    execution_matches_behavior e (Goes_wrong tr)
    9871074| emb_initially_wrong:
    988     execution_matches_behavior e_wrong (Goes_wrong E0).
     1075    execution_matches_behavior se_wrong (Goes_wrong E0).
    9891076
    9901077nlemma exec_state_terminates: ∀tr,tr',s,s',e,r,m.
    991   execution_terminates tr s (e_step tr' s' e) r m → s = s'.
     1078  execution_terminates tr s (se_step tr' s' e) r m → s = s'.
    9921079#tr tr' s s' e r m H; ninversion H;
    9931080##[ #s1 s2 tr1 tr2 r' e' m' H' E1 E2 E3 E4 E5; ndestruct; napply refl
    994 ##| #s1 s2 tr1 tr2 r' e' m' o k i H' E1 E2 E3 E4 E5 E6; ndestruct; napply refl
     1081##| #s1 s2 tr1 tr2 r' e' m' o k i H' E1 E2 E3 E4 E5; ndestruct; napply refl
    9951082##] nqed.
    9961083
    9971084nlemma exec_state_diverges: ∀tr,tr',s,s',e.
    998   execution_diverges tr s (e_step tr' s' e) → s = s'.
     1085  execution_diverges tr s (se_step tr' s' e) → s = s'.
    9991086#tr tr' s s' e H; ninversion H;
    10001087#tr1 s1 s2 e1 e2 H' E1 E2 E3 E4; ndestruct; napply refl; nqed.
    10011088
    10021089nlemma exec_state_reacts: ∀tr,tr',s,s',e.
    1003   execution_reacts tr s (e_step tr' s' e) → s = s'.
     1090  execution_reacts tr s (se_step tr' s' e) → s = s'.
    10041091#tr tr' s s' e H; ninversion H;
    10051092#tr1 s1 e1 H' E1 E2 E3; ndestruct; napply refl; nqed.
    10061093
    10071094nlemma exec_state_wrong: ∀tr,tr',s,s',s'',e.
    1008   execution_goes_wrong tr s (e_step tr' s' e) s'' → s = s'.
     1095  execution_goes_wrong tr s (se_step tr' s' e) s'' → s = s'.
    10091096#tr tr' s s' s'' e H; ninversion H;
    10101097#tr1 s1 s2 e1 H' E1 E2 E3 E4; ndestruct; napply refl; nqed.
     
    10541141  ∀classic:(∀P:Prop.P ∨ ¬P).
    10551142  ∀constructive_indefinite_description:(∀A:Type. ∀P:A→Prop. (∃x. P x) → Σx : A. P x).
    1056   ∀p. ∃b.execution_matches_behavior (exec_inf p) b ∧ exec_program p b.
    1057 #classic constructive_indefinite_description p;
    1058 nwhd in ⊢ (??(λ_.?(?%?)%)); nletin ge ≝ (globalenv Genv fundef type p);
     1143  ∀p,e. single_exec_of (exec_inf p) e →
     1144   ∃b.execution_matches_behavior e b ∧ exec_program p b.
     1145#classic constructive_indefinite_description p e;
     1146nwhd in ⊢ (?%? → ??(λ_.?(?%?)%)); nletin ge ≝ (globalenv Genv fundef type p);
    10591147nlapply (make_initial_state_sound p);
    10601148nlapply (the_initial_state p);
    10611149ncases (make_initial_state p);
    1062 ##[ #s INITIAL' INITIAL; nwhd in INITIAL ⊢ (??(λ_.?(?(??%)?)?));
     1150##[ #s INITIAL' INITIAL; nwhd in INITIAL ⊢ (?(??%)? → ?);
     1151    nrewrite > (exec_inf_aux_unfold …);
     1152    nwhd in ⊢ (?%? → ?);
     1153    ncases (is_final_state s);
     1154    ##[ #F; napply False_ind;
     1155        napply (absurd ?? (initial_state_not_final … INITIAL));
     1156        ncases F; #r F'; @r; napply F';
     1157    ##| #NOTFINAL; nwhd in ⊢ (?%? → ?); ncases e;
     1158        ##[ #tr r m EXEC0 ##| #tr s' e0 EXEC0 ##| #EXEC0 ##| #o k i e EXEC0 ##]
     1159        ncases (se_inv … EXEC0); *; #E1 E2; nrewrite < E1; nrewrite < E2; #EXEC';
    10631160    nlapply (behavior_of_execution ??
    1064               (execution_characterisation_complete classic constructive_indefinite_description ge s ?));
    1065     ##[ napply (initial_state_not_final … INITIAL);
    1066     ##| *; #b MATCHES; @b; @; //;
     1161              (execution_characterisation_complete classic constructive_indefinite_description ge s ? EXEC'));
     1162        *; #b MATCHES; @b; @; //;
    10671163        ninversion MATCHES;
    1068         ##[ #s0 e tr r m TERM EXEC BEHAVES;
    1069             nlapply (initial_step … EXEC ?);
    1070             ##[ napply initial_state_not_final; //; ##]
    1071             *; #e' E2; nrewrite > E2 in EXEC TERM; #EXEC TERM;
     1164        ##[ #s0 e1 tr1 r m TERM EXEC BEHAVES; nrewrite < EXEC in TERM;
     1165            #TERM;
    10721166            nlapply (exec_state_terminates … TERM); #E1;
    10731167            nrewrite > E1 in TERM; #TERM;
    10741168            napply (program_terminates (mk_transrel … step) ?? ge s);
    10751169            ##[ ##2: napply INITIAL
    1076             ##| ##3: napply (terminates_sound … TERM EXEC);
     1170            ##| ##3: napply (terminates_sound … TERM EXEC');
    10771171            ##| ##skip
    10781172            ##| //;
    10791173            ##]
    1080         ##| #s0 e tr DIVERGES EXEC E2;
    1081             nlapply (initial_step … EXEC ?);
    1082             ##[ napply initial_state_not_final; //; ##]
    1083             *; #e' E3; nrewrite > E3 in DIVERGES EXEC ⊢ %;
    1084             #DIVERGES EXEC; nlapply (exec_state_diverges … DIVERGES);
     1174        ##| #s0 e tr DIVERGES EXEC E2; nrewrite < EXEC in DIVERGES; #DIVERGES;
     1175            nlapply (exec_state_diverges … DIVERGES);
    10851176            #E1; nrewrite > E1 in DIVERGES; #DIVERGES;
    10861177            ninversion DIVERGES; #tr' s1 s2 e1 e2 INITSTEPS DIVERGING E4 E5 E6;
    10871178            nrewrite < E4 in INITSTEPS ⊢ %; nrewrite < E5 in E6 ⊢ %; #E6 INITSTEPS;
    1088             ncut (e' = e1); ##[ ndestruct (E6) skip (MATCHES EXEC); // ##]
     1179            ncut (e0 = e1); ##[ ndestruct (E6) skip (MATCHES EXEC0 EXEC'); // ##]
    10891180            #E7; nrewrite < E7 in INITSTEPS; #INITSTEPS;
    1090             ncases (several_steps … INITSTEPS EXEC); #INITSTAR EXECDIV;
     1181            ncases (several_steps … INITSTEPS EXEC'); #INITSTAR EXECDIV;
    10911182            napply (program_diverges (mk_transrel … step) ?? ge s … INITIAL INITSTAR);
    10921183            napply (silent_sound … DIVERGING EXECDIV);
    1093         ##| #s0 e tr REACTS EXEC E2;
    1094             nlapply (initial_step … EXEC ?);
    1095             ##[ napply initial_state_not_final; //; ##]
    1096             *; #e' E3; nrewrite > E3 in EXEC REACTS ⊢ %;
    1097             #EXEC REACTS;
     1184        ##| #s0 e tr REACTS EXEC E2; nrewrite < EXEC in REACTS; #REACTS;
    10981185            nlapply (exec_state_reacts … REACTS);
    10991186            #E1; nrewrite > E1 in REACTS; #REACTS;
    11001187            ninversion REACTS; #tr' s' e'' REACTING E4 E5;
    11011188            nrewrite < E4 in REACTING ⊢ %; nrewrite < E5; #REACTING E6;
    1102             ncut (e' = e''); ##[ ndestruct (E6) skip (MATCHES EXEC); // ##]
     1189            ncut (e0 = e''); ##[ ndestruct (E6) skip (MATCHES EXEC0 EXEC'); // ##]
    11031190            #E7; nrewrite < E7 in REACTING; #REACTING;
    11041191            napply (program_reacts (mk_transrel … step) ?? ge s … INITIAL);
    1105             napply (reacts_sound … REACTING EXEC);
    1106         ##| #e s1 s2 tr WRONG EXEC E2;
    1107             nlapply (initial_step … EXEC ?);
    1108             ##[ napply initial_state_not_final; //; ##]
    1109             *; #e' E3; nrewrite > E3 in EXEC WRONG ⊢ %;
    1110             #EXEC WRONG;
     1192            napply (reacts_sound … REACTING EXEC');
     1193        ##| #e s1 s2 tr WRONG EXEC E2; nrewrite < EXEC in WRONG; #WRONG;
    11111194            nlapply (exec_state_wrong … WRONG);
    11121195            #E1; nrewrite > E1 in WRONG; #WRONG;
    11131196            ninversion WRONG; #tr' s1' s2' e'' GOESWRONG E4 E5 E6 E7;
    11141197            nrewrite < E4 in GOESWRONG ⊢ %; nrewrite < E5; nrewrite < E7; #GOESWRONG;
    1115             ncut (e' = e''); ##[ ndestruct (E6) skip (MATCHES EXEC); // ##]
     1198            ncut (e0 = e''); ##[ ndestruct (E6) skip (MATCHES EXEC0 EXEC'); // ##]
    11161199            #E8; nrewrite < E8 in GOESWRONG; #GOESWRONG;
    1117             nelim (wrong_sound … WRONG EXEC); *; #STAR STOP FINAL;
     1200            nelim (wrong_sound … WRONG EXEC' NOTFINAL); *; #STAR STOP FINAL;
    11181201            napply (program_goes_wrong (mk_transrel … step) ?? ge s … INITIAL STAR STOP);
    11191202            #r; @; #F; napply (absurd ?? FINAL); @r; napply F;
    1120         ##| nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (??%? → ?);
    1121             ncases (is_final_state s); #F EXEC; nwhd in EXEC:(??%?); ndestruct (EXEC);
     1203        ##| #E; ndestruct (E);
    11221204        ##]
    11231205   ##]
    11241206##| nwhd in ⊢ ((∀_.? → %) → ?);
    1125     #NOINIT WHATEVER;
     1207    #NOINIT; #_; #EXEC;
    11261208    @ (Goes_wrong E0); @;
    1127     ##[ nwhd in ⊢ (?(??%)?);
    1128         nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (?%?);
     1209    ##[ nwhd in EXEC:(?(??%)?);
     1210        nrewrite > (exec_inf_aux_unfold …) in EXEC; nwhd in ⊢ (?%? → ?);
     1211        ncases e;
     1212        ##[ #tr r m EXEC0 ##| #tr s' e0 EXEC0 ##| #EXEC0 ##| #o k i e EXEC0 ##]
     1213        ncases (se_inv … EXEC0);
    11291214        napply emb_initially_wrong;
    11301215    ##| napply program_goes_initially_wrong;
Note: See TracChangeset for help on using the changeset viewer.