Changeset 250 for C-semantics/Errors.ma


Ignore:
Timestamp:
Nov 22, 2010, 2:40:22 PM (10 years ago)
Author:
campbell
Message:

Begin separating soundness from executable semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Errors.ma

    r189 r250  
    1515
    1616include "datatypes/pairs.ma".
     17include "Plogic/equality.ma".
     18include "Plogic/connectives.ma".
    1719
    1820(* * Error reporting and the error monad. *)
     
    8385 (at level 200, X ident, Y ident, A at level 100, B at level 200)
    8486 : error_monad_scope.
     87*)
     88nremark bind_inversion:
     89  ∀A,B: Type. ∀f: res A. ∀g: A → res B. ∀y: B.
     90  bind ?? f g = OK ? y →
     91  ∃x. f = OK ? x ∧ g x = OK ? y.
     92#A B f g y; ncases f;
     93##[ #a e; @a; nwhd in e:(??%?); /2/;
     94##| #H; nwhd in H:(??%?); ndestruct (H);
     95##] nqed.
    8596
    86 Remark bind_inversion:
    87   forall (A B: Type) (f: res A) (g: A -> res B) (y: B),
    88   bind f g = OK y ->
    89   exists x, f = OK x /\ g x = OK y.
    90 Proof.
    91   intros until y. destruct f; simpl; intros.
    92   exists a; auto.
    93   discriminate.
    94 Qed.
     97nremark bind2_inversion:
     98  ∀A,B,C: Type. ∀f: res (A×B). ∀g: A → B → res C. ∀z: C.
     99  bind2 ??? f g = OK ? z →
     100  ∃x. ∃y. f = OK ? 〈x, y〉 ∧ g x y = OK ? z.
     101#A B C f g z; ncases f;
     102##[ #ab; ncases ab; #a b e; @a; @b; nwhd in e:(??%?); /2/;
     103##| #H; nwhd in H:(??%?); ndestruct
     104##] nqed.
    95105
    96 Remark bind2_inversion:
    97   forall (A B C: Type) (f: res (A*B)) (g: A -> B -> res C) (z: C),
    98   bind2 f g = OK z ->
    99   exists x, exists y, f = OK (x, y) /\ g x y = OK z.
    100 Proof.
    101   intros until z. destruct f; simpl.
    102   destruct p; simpl; intros. exists a; exists b; auto.
    103   intros; discriminate.
    104 Qed.
    105 
     106(*
    106107Open Local Scope error_monad_scope.
    107108
Note: See TracChangeset for help on using the changeset viewer.