Changeset 3050 for src/RTLabs


Ignore:
Timestamp:
Apr 1, 2013, 5:18:05 PM (7 years ago)
Author:
piccolo
Message:

1) Added general commutation theorem for monads.

2) Added some commutation lemma for push and pop that can be useful
for sigle steps of correctness proof.

3) fixed some bugs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs_traces.ma

    r2895 r3050  
    11251125| Finalstate _ ⇒ None ?
    11261126].
    1127 
    1128 lemma nth_opt_Exists : ∀A,n,l,a.
    1129   nth_opt A n l = Some A a →
    1130   Exists A (λa'. a' = a) l.
    1131 #A #n elim n
    1132 [ * [ #a #E normalize in E; destruct | #a #l #a' #E normalize in E; destruct % // ]
    1133 | #m #IH *
    1134   [ #a #E normalize in E; destruct
    1135   | #a #l #a' #E %2 @IH @E
    1136   ]
    1137 ] qed.
    11381127
    11391128lemma eval_successor : ∀ge,f,fs,m,tr,s'.
Note: See TracChangeset for help on using the changeset viewer.