Changeset 2496 for src/common


Ignore:
Timestamp:
Nov 27, 2012, 5:50:51 PM (7 years ago)
Author:
garnier
Message:

Some tentative work on the simulation proof for expressions, in order to adjust the invariant
on memories.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Errors.ma

    r2453 r2496  
    270270notation > "vbox('do' 〈ident v1, ident v2〉 'as' ident E ← e; break e')" with precedence 48 for @{ bind2_eq ??? ${e} (λ${ident v1}.λ${ident v2}.λ${ident E}.${e'})}.
    271271
     272lemma bind2_eq_inversion:
     273  ∀A,B,C: Type[0]. ∀f: res (A×B). ∀g: ∀a:A.∀b:B. f = OK ? 〈a,b〉 → res C. ∀z.
     274  bind2_eq ??? f g = return z →
     275  ∃x. ∃y. ∃Eq. f = return 〈x, y〉 ∧ g x y Eq = return z.
     276#A #B #C #f cases f
     277[ * #a #b #g normalize #z #Heq %{a} %{b} %{(refl ??)} @conj try @refl @Heq
     278| #errmsg #g #z normalize #Habsurd destruct (Habsurd) ]
     279qed.
     280
    272281definition res_to_opt : ∀A:Type[0]. res A → option A ≝
    273282 λA.λv. match v with [ Error _ ⇒ None ? | OK v ⇒ Some … v].
Note: See TracChangeset for help on using the changeset viewer.