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

More proofs ported to new lib.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.