Changeset 3252 for src/ERTL/ERTLToLTLProof.ma
 Timestamp:
 May 3, 2013, 5:29:36 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToLTLProof.ma
r3217 r3252 1446 1446 let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in 1447 1447 let stacksizes ≝ lookup_stack_cost … m in 1448 let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in 1449 b_graph_transform_program_props ERTL_semantics LTL_semantics stacksizes 1450 init prog init_regs f_lbls f_regs → 1448 let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in 1451 1449 cond_commutation_statement ERTL_semantics LTL_semantics prog stacksizes 1452 1450 init init_regs … … 1454 1452 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs). 1455 1453 [2: @hide_prf %] 1456 #fix_comp #colour #prog #init_regs #f_lbls #f_regs #good1454 #fix_comp #colour #prog #init_regs #f_lbls #f_regs 1457 1455 whd in match cond_commutation_statement; normalize nodelta 1458 1456 #st1 #st2 #f #fn #r #ltrue #lfalse #bv #b * #Hbl #EQfetch … … 1553 1551 qed. 1554 1552 1555 1556 axiom ERTLToLTL_ok : 1553 lemma seq_commute :∀fix_comp,colour,prog,init_regs,f_lbls,f_regs. 1554 let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in 1555 let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in 1556 let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in 1557 let stacksizes ≝ lookup_stack_cost … m in 1558 let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in 1559 seq_commutation_statement ERTL_semantics LTL_semantics prog stacksizes 1560 init init_regs 1561 f_lbls f_regs (state_rel fix_comp colour prog) 1562 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs). 1563 [2: @hide_prf %] 1564 cases daemon (*TODO*) 1565 qed. 1566 1567 lemma return_commute :∀fix_comp,colour,prog,init_regs,f_lbls,f_regs. 1568 let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in 1569 let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in 1570 let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in 1571 let stacksizes ≝ lookup_stack_cost … m in 1572 let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in 1573 return_commutation_statement ERTL_semantics LTL_semantics prog stacksizes 1574 init init_regs 1575 f_lbls f_regs (state_rel fix_comp colour prog) 1576 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs). 1577 [2: @hide_prf %] 1578 cases daemon (*TODO*) 1579 qed. 1580 1581 lemma pre_main_commute : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs. 1582 let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in 1583 let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in 1584 let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in 1585 let stacksizes ≝ lookup_stack_cost … m in 1586 let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in 1587 b_graph_transform_program_props ERTL_semantics LTL_semantics stacksizes 1588 init prog init_regs f_lbls f_regs → 1589 pre_main_commutation_statement ERTL_semantics LTL_semantics prog stacksizes 1590 init init_regs 1591 f_lbls f_regs (state_rel fix_comp colour prog) 1592 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs). 1593 [2: @hide_prf %] 1594 cases daemon qed. 1595 1596 (* 1597 #fix_comp #colour #prog #init_regs #f_lbls #f_regs #good whd 1598 #st1 #st1' #st2 #EQbl whd in match eval_state; normalize nodelta 1599 whd in match fetch_statement; whd in match fetch_internal_function; normalize nodelta 1600 whd in match fetch_function; normalize nodelta @eqZb_elim [2: * #H @⊥ @H assumption] 1601 #_ normalize nodelta >m_return_bind #H @('bind_inversion H) H ** #f #fn #stmt 1602 #H lapply(err_eq_from_io ????? H) H #H @('bind_inversion H) H #stmt1 1603 #H lapply(opt_eq_from_res ???? H) H whd in ⊢ (??%% → ?); cases st1 in EQbl; st1 1604 #st1 * #bl1 #pos1 #lp1 #EQbl1 normalize nodelta cases pos1 pos1 normalize nodelta 1605 [ #EQ destruct(EQ) 1606 *: * [2,3,5,6: #x ] whd in ⊢ (??%% → ?); #EQ destruct 1607 ] 1608 whd in ⊢ (??%% → ?); #EQ destruct(EQ) normalize nodelta whd in match eval_statement_no_pc; normalize inversion(point_of_pc ERTL_semantics (pc … st1)) 1609 *) 1610 1611 lemma call_commute : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs. 1612 let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in 1613 let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in 1614 let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in 1615 let stacksizes ≝ lookup_stack_cost … m in 1616 let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in 1617 call_commutation_statement ERTL_semantics LTL_semantics prog stacksizes 1618 init init_regs 1619 f_lbls f_regs (state_rel fix_comp colour prog) 1620 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs). 1621 [2: @hide_prf %] 1622 cases daemon qed. 1623 1624 lemma goto_commute : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs. 1625 let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in 1626 let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in 1627 let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in 1628 let stacksizes ≝ lookup_stack_cost … m in 1629 let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in 1630 goto_commutation_statement ERTL_semantics LTL_semantics prog stacksizes 1631 init init_regs 1632 f_lbls f_regs (state_rel fix_comp colour prog) 1633 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs). 1634 [2: @hide_prf %] 1635 cases daemon qed. 1636 1637 lemma tailcall_commute : ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs. 1638 let p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour prog))) in 1639 let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in 1640 let n ≝ \snd (ertl_to_ltl fix_comp colour prog) in 1641 let stacksizes ≝ lookup_stack_cost … m in 1642 let init ≝ (λglobals,fn.«translate_data fix_comp colour globals fn,?») in 1643 tailcall_commutation_statement ERTL_semantics LTL_semantics prog stacksizes 1644 init init_regs 1645 f_lbls f_regs (state_rel fix_comp colour prog) 1646 (state_pc_rel fix_comp colour prog init_regs f_lbls f_regs). 1647 [2: @hide_prf %] 1648 #fix_comp #colour #prog #init_regs #f_lbls #f_regs whd #st1 #st2 1649 #f #fn * 1650 qed. 1651 1652 1653 theorem ERTLToLTL_ok : 1557 1654 ∀fix_comp : fixpoint_computer. 1558 1655 ∀colour : coloured_graph_computer. … … 1560 1657 let 〈p_out, m, n〉 ≝ ertl_to_ltl fix_comp colour p_in in 1561 1658 (* what should we do with n? *) 1562 let stacksizes ≝ stack_sizesm in1659 let stacksizes ≝ lookup_stack_cost m in 1563 1660 ∀init_in.make_initial_state 1564 1661 (mk_prog_params ERTL_semantics p_in stacksizes) = OK … init_in → … … 1572 1669 (joint_status LTL_semantics p_out stacksizes) 1573 1670 R init_in init_out. 1671 #fix_comp #colour #p_in #init_in #EQinit_in 1672 letin p_out ≝ (\fst (\fst (ertl_to_ltl fix_comp colour p_in))) 1673 letin m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour p_in))) 1674 letin n ≝ (\snd (ertl_to_ltl fix_comp colour p_in)) 1675 letin stacksizes ≝ (lookup_stack_cost m) 1676 cases(make_b_graph_transform_program_props ERTL_semantics LTL_semantics stacksizes 1677 (λglobals : list ident.λfn.«translate_data fix_comp colour globals fn,(refl …)») p_in) 1678 #init_regs * #f_lbls * #f_regs #good 1679 @(joint_correctness ERTL_semantics LTL_semantics p_in stacksizes 1680 (λglobals : list ident.λfn.«translate_data fix_comp colour globals fn,(refl …)») 1681 init_regs f_lbls f_regs (state_rel fix_comp colour p_in) 1682 (state_pc_rel fix_comp colour p_in init_regs f_lbls f_regs) ? ? init_in EQinit_in) 1683 % 1684 [ @good 1685  #st1 #st2 #f #fn #Rst1st2 #EQfn whd %{f} %{fn} %{EQfn} 1686 @(fetch_ok_sigma_state_ok fix_comp colour p_in … Rst1st2 EQfn) 1687  #st1 #st2 #f #fn #Rst1st2 #EQfn @(fetch_ok_pc_ok fix_comp colour p_in … Rst1st2 EQfn) 1688  #st1 #st2 #f #fn #Rst1st2 #EQfn lapply Rst1st2 whd in match state_pc_rel; 1689 normalize nodelta cases(st_frms … st1) [*] #frames normalize nodelta 1690 whd in match sigma_fb_state_pc; whd in match sigma_sb_state_pc; normalize nodelta 1691 >EQfn normalize nodelta <(fetch_ok_pc_ok … Rst1st2 EQfn) >EQfn normalize nodelta 1692 #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct(EQ) assumption 1693  #st1 #st2 #pc #lp1 #lp2 #f #fn #EQfn #Rst1st2 #EQ destruct(EQ) whd 1694 lapply Rst1st2 whd in match state_rel; normalize nodelta * #f1 * #fn1 >EQfn * 1695 whd in ⊢ (??%% → ?); #EQ destruct(EQ) cases(st_frms … st1) [*] #frames 1696 normalize nodelta #EQst whd in match sigma_fb_state_pc; 1697 whd in match sigma_sb_state_pc; normalize nodelta >EQfn 1698 normalize nodelta @eq_f3 [2,3: %  assumption] 1699  @pre_main_commute assumption 1700  #f #fn * #bl #pos #EQbl whd in match fetch_statement; 1701 whd in match fetch_internal_function; whd in match fetch_function; 1702 normalize nodelta @eqZb_elim [2: * #H @⊥ @H assumption] 1703 #_ normalize nodelta >m_return_bind #H @('bind_inversion H) H #stmt 1704 #H lapply(opt_eq_from_res ???? H) H whd in ⊢ (??%% → ?); 1705 whd in match point_of_pc; normalize nodelta cases pos normalize nodelta 1706 [ #EQ destruct(EQ) 1707 *: * [2,3,5,6: #x ] whd in ⊢ (??%% → ?); #EQ destruct 1708 ] 1709 whd in ⊢ (??%% → ?); #EQ destruct(EQ) 1710  @cond_commute 1711  @seq_commute 1712  #f #fn #bl #EQfn #id #args #dest #lbl whd #bl' 1713 %{(match id with [inl f1 ⇒ inl ?? f1  inr x ⇒ inr ?? 〈it,it〉])} 1714 %{args} %{it} normalize nodelta cases id [ #f1 %  * #dpl #dph %] 1715  cases daemon (*TODO*) 1716  @return_commute 1717  @call_commute 1718  @goto_commute 1719  @tailcall_commute 1720  cases daemon (*TODO*) 1721  cases daemon (*TODO*) 1722  cases daemon (*TODO*) 1723  cases daemon (*TODO*) 1724 ] 1725 qed.
Note: See TracChangeset
for help on using the changeset viewer.