Changeset 398


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

This time actually prove the result I intended.

Location:
C-semantics
Files:
1 added
2 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r389 r398  
    13241324##] nqed.
    13251325
    1326 (* starting after state s, zero or more steps of execution e reach state s'
    1327    after which comes e'. *)
    1328 ninductive execution_isteps : trace → state → execution → state → execution → Prop ≝
    1329 | isteps_none : ∀s,e. execution_isteps E0 s e s e
    1330 | isteps_one : ∀e,e',tr,tr',s,s',s0.
    1331     execution_isteps tr' s e s' e' →
    1332     execution_isteps (tr⧺tr') s0 (e_step tr s e) s' e'
    1333 | isteps_interact : ∀e,e',o,k,i,s,s',s0,tr,tr'.
    1334     execution_isteps tr' s e s' e' →
    1335     k i = e_step tr s e →
    1336 (*    (¬ ∃r.final_state s r) → (* used to avoid showing that k i doesn't end prog *)*)
    1337     execution_isteps (tr⧺tr') s0 (e_interact o k) s' e'.
    1338 
    1339 nlemma isteps_trans: ∀tr1,tr2,s1,s2,s3,e1,e2,e3.
    1340   execution_isteps tr1 s1 e1 s2 e2 →
    1341   execution_isteps tr2 s2 e2 s3 e3 →
    1342   execution_isteps (tr1⧺tr2) s1 e1 s3 e3.
    1343 #tr1 tr2 s1 s2 s3 e1 e2 e3 H1; nelim H1;
    1344 ##[ #s e; //;
    1345 ##| #e e' tr tr' s1' s2' s3' H1 H2 H3;
    1346     nrewrite > (Eapp_assoc …);
    1347     napply isteps_one;
    1348     napply H2; napply H3;
    1349 ##| #e e' o k i s1' s2' s3' tr tr' H1 H2 H3 H4;
    1350     nrewrite > (Eapp_assoc …);
    1351     napply (isteps_interact … H2); /2/;
    1352 ##] nqed.
    1353 
    1354 nlemma exec_e_step: ∀ge,x,tr,s,e.
    1355   exec_inf_aux ge x = e_step tr s e →
    1356   exec_inf_aux ge (exec_step ge s) = e.
    1357 #ge x tr s e;
    1358 nrewrite > (exec_inf_aux_unfold …); ncases x;
    1359 ##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct
    1360 ##| #y; ncases y; #tr' s'; nwhd in ⊢ (??%? → ?);
    1361     ncases (is_final_state s'); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct;
    1362     napply refl;
    1363 ##| #EXEC; nwhd in EXEC:(??%?); ndestruct
    1364 ##] nqed.
    1365 
    1366 nlemma exec_e_step_inv: ∀ge,x,tr,s,e.
    1367   exec_inf_aux ge x = e_step tr s e →
    1368   x = Value ??? 〈tr,s〉.
    1369 #ge x tr s e;
    1370 nrewrite > (exec_inf_aux_unfold …); ncases x;
    1371 ##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct
    1372 ##| #y; ncases y; #tr' s'; nwhd in ⊢ (??%? → ?);
    1373     ncases (is_final_state s'); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct;
    1374     napply refl;
    1375 ##| #EXEC; nwhd in EXEC:(??%?); ndestruct
    1376 ##] nqed.
    1377 
    1378 nlemma exec_e_step_inv2: ∀ge,x,tr,s,e.
    1379   exec_inf_aux ge x = e_step tr s e →
    1380   ¬∃r.final_state s r.
    1381 #ge x tr s e;
    1382 nrewrite > (exec_inf_aux_unfold …); ncases x;
    1383 ##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct
    1384 ##| #y; ncases y; #tr' s'; nwhd in ⊢ (??%? → ?);
    1385     ncases (is_final_state s'); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct;
    1386     napply FINAL;
    1387 ##| #EXEC; nwhd in EXEC:(??%?); ndestruct
    1388 ##] nqed.
    1389 
    1390 (* NB: the E0 in the execs are irrelevant. *)
    1391 nlemma several_steps: ∀ge,tr,e,e',s,s'.
    1392   execution_isteps tr s e s' e' →
    1393   exec_inf_aux ge (Value ??? 〈E0,s〉) = e_step E0 s e →
    1394   star (mk_transrel … step) ge s tr s' ∧
    1395   exec_inf_aux ge (Value ??? 〈E0,s'〉) = e_step E0 s' e'.
    1396 #ge tr0 e0 e0' s0 s0' H;
    1397 nelim H;
    1398 ##[ #s e EXEC; @; //; napply EXEC;
    1399 ##| #e1 e2 tr1 tr2 s1 s2 s3 STEPS IH EXEC;
    1400     nrewrite > (exec_inf_aux_unfold ge ?) in EXEC;
    1401     nwhd in ⊢ (??%? → ?);
    1402     ncases (is_final_state s3); ##[ nwhd in ⊢ (? → ??%? → ?); #FINAL BAD; ndestruct (BAD) ##]
    1403     #NOTFINAL EXEC; nwhd in EXEC:(??%?); ndestruct;
    1404     nrewrite > (exec_inf_aux_unfold ge ?) in e3;
    1405     nlapply (refl ? (exec_step ge s3));
    1406     ncases (exec_step ge s3) in ⊢ (???% → %);
    1407     ##[ #o k E EXEC'; nwhd in EXEC':(??%?); ndestruct (EXEC');
    1408     ##| #x; ncases x; #tr' s' EXEC3;
    1409         nwhd in ⊢ (??%? → ?);
    1410         ncases (is_final_state s'); #FINAL' EXEC'; nwhd in EXEC':(??%?); ##[ ndestruct ##]
    1411         ncut (exec_inf_aux ge (exec_step ge s1) = e1); ##[ ndestruct (EXEC'); napply refl ##]
    1412         #EXEC'';
    1413         nlapply (IH ?);
    1414         ##[ nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (??%?);
    1415             ncases (is_final_state s1); #FINAL1;
    1416             ##[ napply False_ind; napply (absurd ?? FINAL'); ncases FINAL1;
    1417                 #r' Hr; @ r'; ndestruct (EXEC'); napply Hr;
    1418             ##| nwhd in ⊢ (??%?); nrewrite < EXEC''; napply refl
    1419             ##]
    1420         ##| *; #STARs1s2 EXEC2; @;
    1421             ##[ nlapply (exec_step_sound ge s3); nrewrite > EXEC3;
    1422                 nwhd in ⊢ (% → ?); #STEP3; ndestruct (EXEC');
    1423                 napply (star_step (mk_transrel ?? step) … STEP3 STARs1s2); //;
    1424             ##| napply EXEC2;
    1425             ##]
    1426         ##]
    1427     ##| #E EXEC'; nwhd in EXEC':(??%?); ndestruct (EXEC');
    1428     ##]
    1429 ##| #e e' o k i s s' s0 tr tr' H1 H2 IH;
    1430     nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (??%? → ?);
    1431     ncases (is_final_state s0); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct;
    1432    
    1433     nrewrite > (exec_inf_aux_unfold ge ?) in e1;
    1434     nlapply (exec_step_sound ge s0);
    1435     ncases (exec_step ge s0);
    1436     ##[ #i' k' SOUND E1; nwhd in SOUND E1:(??%?); ndestruct (E1);
    1437     ##| #x; ncases x; #tr' s'' SOUND; nwhd in ⊢ (??%? → ?);
    1438         ncases (is_final_state s''); #FINAL'; nwhd in ⊢ (??%? → ?); #EXEC';
    1439         ndestruct (EXEC');
    1440     ##| #_; nwhd in ⊢ (??%? → ?); #EXEC'; ndestruct (EXEC');
    1441     ##]
    1442     nlapply (IH ?);
    1443     ##[ nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (??%?);
    1444         ncases (is_final_state s);
    1445         ##[ #X; ncases X; #r FINAL'; napply False_ind;
    1446             ncases (exec_e_step_inv2 … H2); #H; napply H;
    1447             @ r; napply FINAL' ##]
    1448         #FINAL'; nwhd in ⊢ (??%?);
    1449         nrewrite > (exec_e_step … H2);
    1450         napply refl;
    1451     ##| *; #STARsTOs' EXECs'; @;
    1452       ##[ napply (star_step … STARsTOs');
    1453           ##[ ##2: nlapply (SOUND i);
    1454                    nrewrite > (exec_e_step_inv … H2); nwhd in ⊢ (% → ?);
    1455                    #STEP; napply STEP;
    1456           ##| ##skip;
    1457           ##| napply refl
    1458           ##]
    1459       ##| napply EXECs';
    1460       ##]
    1461     ##]
    1462 ##] nqed.
    1463 
    1464 ninductive execution_terminates : trace → state → execution → int → mem → Prop ≝
    1465 | terminates : ∀s,s',tr,tr',r,e,m.
    1466     execution_isteps tr s e s' (e_stop tr' r m) →
    1467     execution_terminates (tr⧺tr') s (e_step E0 s e) r m
    1468 (* We should only be able to get to here if main is an external function, which is silly. *)
    1469 | annoying_corner_case_terminates: ∀s,s',tr,tr',r,e,m,o,k,i.
    1470     execution_isteps tr s e s' (e_interact o k) →
    1471     k i = e_stop tr' r m →
    1472     execution_terminates (tr⧺tr') s (e_step E0 s e) r m.
    1473 
    1474 ncoinductive execution_diverging : execution → Prop ≝
    1475 | diverging_step : ∀s,e. execution_diverging e → execution_diverging (e_step E0 s e).
    1476 
    1477 (* Makes a finite number of interactions (including cost labels) before diverging. *)
    1478 ninductive execution_diverges : trace → state → execution → Prop ≝
    1479 | diverges_diverging: ∀tr,s,s',e,e'.
    1480     execution_isteps tr s e s' e' →
    1481     execution_diverging e' →
    1482     execution_diverges tr s (e_step E0 s e).
    1483 
    1484 (* NB: "reacting" includes hitting a cost label. *)
    1485 ncoinductive execution_reacting : traceinf → state → execution → Prop ≝
    1486 | reacting: ∀tr,tr',s,s',e,e'.
    1487     execution_reacting tr' s' e' →
    1488     execution_isteps tr s e s' e' →
    1489     tr ≠ E0 →
    1490     execution_reacting (tr⧻tr') s e.
    1491 
    1492 ninductive execution_reacts : traceinf → state → execution → Prop ≝
    1493 | reacts: ∀tr,s,e.
    1494     execution_reacting tr s e →
    1495     execution_reacts tr s (e_step E0 s e).
    1496 
    1497 ninductive execution_goes_wrong: trace → state → execution → state → Prop ≝
    1498 | go_wrong: ∀tr,s,s',e.
    1499     execution_isteps tr s e s' e_wrong →
    1500     execution_goes_wrong tr s (e_step E0 s e) s'.
    1501 
    1502 nlet corec silent_sound ge s e
    1503   (H0:execution_diverging e)
    1504   (EXEC:exec_inf_aux ge (Value ??? 〈E0,s〉) = e_step E0 s e)
    1505   : forever_silent (mk_transrel ?? step) … ge s ≝ ?.
    1506 ncut (∃s2.∃e2.execution_diverging e2 ∧ exec_inf_aux ge (exec_step ge s) = e_step E0 s2 e2);
    1507 ##[ ncases H0 in EXEC ⊢ %; #s1 e1 H1;
    1508     nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (??%? → ?);
    1509     ncases (is_final_state s); #p EXEC; nwhd in EXEC:(??%?); ndestruct;
    1510     @ s1; @ e1; @; //; napply e0;
    1511 ##| *; #s2; *; #e2; *; #H2 EXEC2;
    1512     napply (forever_silent_intro (mk_transrel ?? step) … ge s s2 ? (silent_sound ge s2 e2 ??));
    1513     ncut (exec_step ge s = Value ??? 〈E0,s2〉);
    1514     ##[ ##1,3,5: nrewrite > (exec_inf_aux_unfold …) in EXEC2; nelim (exec_step ge s);
    1515       ##[ ##1,4,7: #o k IH EXEC2; nwhd in EXEC2:(??%?); ndestruct;
    1516       ##| ##2,5,8: #x; ncases x; #tr s'; nwhd in ⊢ (??%? → ?);
    1517           ncases (is_final_state s'); #p' EXEC2; nwhd in EXEC2:(??%?); ndestruct;
    1518           napply refl;
    1519       ##| ##3,6,9: #EXEC2; nwhd in EXEC2:(??%?); ndestruct
    1520       ##]
    1521     ##| #EXEC1; nlapply (exec_step_sound ge s); nrewrite > EXEC1; nwhd in ⊢ (% → %); //
    1522     ##| #EXEC1; nrewrite > EXEC1 in EXEC2; #EXEC2; napply EXEC2;
    1523     ##| #EXEC1; napply H2;
    1524     ##]
    1525 ##]
    1526 nqed.
    1527 
    1528 nlemma final_step: ∀ge,tr,r,m,s.
    1529   exec_inf_aux ge (exec_step ge s) = e_stop tr r m →
    1530   step ge s tr (Returnstate (Vint r) Kstop m).
    1531 #ge tr r m s;
    1532 nrewrite > (exec_inf_aux_unfold …);
    1533 nlapply (exec_step_sound ge s);
    1534 ncases (exec_step ge s);
    1535 ##[ #o k H EXEC; nwhd in EXEC:(??%?); ndestruct
    1536 ##| #x; ncases x; #tr' s' SOUND; nwhd in ⊢ (??%? → ?); ncases (is_final_state s');
    1537     #FINAL EXEC; nwhd in SOUND EXEC:(??%?); ndestruct;
    1538     ncases FINAL; #r' FINAL'; ninversion FINAL';
    1539     #r'' m' E1 E2; ndestruct;
    1540     napply SOUND;
    1541 ##| #_; #EXEC; nwhd in EXEC:(??%?); ndestruct
    1542 ##] nqed.
    1543 
    1544 nlemma e_stop_inv: ∀ge,x,tr,r,m.
    1545   exec_inf_aux ge x = e_stop tr r m →
    1546   x = Value ??? 〈tr,Returnstate (Vint r) Kstop m〉.
    1547 #ge x tr r m;
    1548 nrewrite > (exec_inf_aux_unfold …); ncases x;
    1549 ##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct;
    1550 ##| #z; ncases z; #tr' s'; nwhd in ⊢ (??%? → ?); ncases (is_final_state s');
    1551   ##[ #F; ncases F; #r' FINAL; ncases FINAL; #r'' m' EXEC; nwhd in EXEC:(??%?);
    1552       ndestruct (EXEC); napply refl;
    1553   ##| #F EXEC; nwhd in EXEC:(??%?); ndestruct (EXEC);
    1554   ##]
    1555 ##| #EXEC; nwhd in EXEC:(??%?); ndestruct (EXEC);
    1556 ##] nqed.
    1557 
    1558 nlemma terminates_sound: ∀ge,tr,s,r,m,e.
    1559   execution_terminates tr s (e_step E0 s e) r m →
    1560   exec_inf_aux ge (Value ??? 〈E0, s〉) = (e_step E0 s e) →
    1561   star (mk_transrel … step) ge s tr (Returnstate (Vint r) Kstop m).
    1562 #ge tr0 s0 r m e0 H; ncases H;
    1563 ##[ #s s' tr tr' r e m ESTEPS EXEC;
    1564     ncases (several_steps … ESTEPS EXEC); #STARs' EXECs';
    1565     napply (star_right … STARs');
    1566     ##[ ##2: napply (final_step ge tr' r m s');
    1567              napply (exec_e_step … EXECs');
    1568     ##| ##skip
    1569     ##| napply refl
    1570     ##]
    1571 ##| #s s' tr tr' r e m o k i ESTEPS EXECK EXEC;
    1572     ncases (several_steps … ESTEPS EXEC); #STARs' EXECs';
    1573     napply (star_right … STARs');
    1574     ##[ ##2: nlapply (exec_step_sound ge s');
    1575              nlapply (exec_e_step … EXECs');
    1576              ncases (exec_step ge s');
    1577              ##[ #o' k'; nrewrite > (exec_inf_aux_unfold …); #EXECs'';
    1578                  nwhd in EXECs'':(??%?) ⊢ (% → ?);
    1579                  ncut (o' = o); ##[ ndestruct (EXECs''); // ##] #E1;
    1580                  nrewrite > E1 in k' EXECs'' ⊢ %; #k' EXECs'';
    1581                  ncut (k = λv.exec_inf_aux ge (k' v)); ##[ ndestruct (EXECs''); // ##] #E2;
    1582                  nrewrite > E2 in ESTEPS EXECK EXECs' EXECs'';
    1583                  #ESTEPS EXECK EXECs' EXECs'' STEP; nlapply (STEP i);
    1584                  nrewrite > (e_stop_inv … EXECK); nwhd in ⊢ (% → ?);
    1585                  //;
    1586              ##| #z; ncases z; #tr'' s''; nrewrite > (exec_inf_aux_unfold …);
    1587                  nwhd in ⊢ (??%? → ?); ncases (is_final_state s'');
    1588                  #H EXEC; nwhd in EXEC:(??%?); ndestruct (EXEC)
    1589              ##| nrewrite > (exec_inf_aux_unfold …);
    1590                  #EXEC; nwhd in EXEC:(??%?); ndestruct (EXEC)
    1591              ##]
    1592     ##| ##skip
    1593     ##| napply refl
    1594     ##]
    1595 ##] nqed.
    1596 
    1597 nlet corec reacts_sound ge tr s e
    1598   (REACTS:execution_reacting tr s e)
    1599   (EXEC:exec_inf_aux ge (Value ??? 〈E0, s〉) = e_step E0 s e) :
    1600   forever_reactive (mk_transrel … step) ge s tr ≝ ?.
    1601 ncut (∃s'.∃e'.∃tr'.∃tr''.execution_reacting tr'' s' e' ∧ execution_isteps tr' s e s' e' ∧ tr' ≠ E0 ∧ tr = tr'⧻tr'');
    1602 ##[ ninversion REACTS;
    1603     #tr0 tr' s0 s' e0 e' EREACTS ESTEPS REACTED E1 E2 E3; ndestruct (E2 E3);
    1604     @ s'; @ e'; @ tr0; @ tr'; @; ##[ @; ##[ @; //; ##| napply REACTED ##] ##| napply refl ##]
    1605 ##| *; #s'; *; #e'; *; #tr'; *; #tr'';
    1606     *; *; *; #REACTS' ESTEPS REACTED APPTR;
    1607 (*    nrewrite > APPTR;*)
    1608     napply (match sym_eq ??? APPTR return λx.λ_.forever_reactive (mk_transrel genv state step) ge s x with [ refl ⇒ ? ]);
    1609     @;
    1610     ncases (several_steps … ESTEPS EXEC); #STEPS EXEC';
    1611     ##[ ##2: napply STEPS;
    1612     ##| ##skip
    1613     ##| napply REACTED
    1614     ##| napply reacts_sound;
    1615       ##[ ##2: napply REACTS';
    1616       ##| ##skip
    1617       ##| napply EXEC'
    1618       ##]
    1619     ##]
    1620 nqed.
  • 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.