Changeset 1603 for src/Clight


Ignore:
Timestamp:
Dec 13, 2011, 5:37:40 PM (8 years ago)
Author:
sacerdot
Message:

More proofs ported to new lib.

Location:
src/Clight
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r1599 r1603  
    5353
    5454lemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (Sig A P). ∀f:Sig A P → res B.
    55   (∀v:A. ∀p:P v. match f (dp A P v p) with [ Error _ ⇒ True | OK v' ⇒ P' v'] ) →
     55  (∀v:A. ∀p:P v. match f (mk_Sig A P v p) with [ Error _ ⇒ True | OK v' ⇒ P' v'] ) →
    5656  match bind (Sig A P) B e f with [ Error _ ⇒ True | OK v' ⇒ P' v' ].
    5757#A #B #P #P' #e #f elim e;
  • src/Clight/CexecComplete.ma

    r1566 r1603  
    1212
    1313definition yields_sig : ∀A,P. res (Sig A P) → A → Prop ≝
    14 λA,P,e,v. match e with [ OK v' ⇒ match v' with [ dp v'' _ ⇒ v = v'' ] | _ ⇒ False].
     14λA,P,e,v. match e with [ OK v' ⇒ match v' with [ mk_Sig v'' _ ⇒ v = v'' ] | _ ⇒ False].
    1515
    1616let rec yieldsIO_sig (A:Type[0]) (P:A → Prop) (e:IO io_out io_in (Sig A P)) (v:A) on e : Prop ≝
    1717match e with
    18 [ Value v' ⇒ match v' with [ dp v'' _ ⇒ v = v'' ]
     18[ Value v' ⇒ match v' with [ mk_Sig v'' _ ⇒ v = v'' ]
    1919| Interact _ k ⇒ ∃r.yieldsIO_sig A P (k r) v
    2020| _ ⇒ False].
     
    3333qed.
    3434
    35 lemma yields_sig_eq: ∀A,P,e,v. yields_sig A P e v → ∃p. e = OK ? (dp … v p).
     35lemma yields_sig_eq: ∀A,P,e,v. yields_sig A P e v → ∃p. e = OK ? (mk_Sig … v p).
    3636#A #P #e #v cases e;
    3737[ #vp cases vp; #v' #p #H whd in H; >H %{ p} @refl
Note: See TracChangeset for help on using the changeset viewer.