Changeset 250 for Csemantics/Errors.ma
 Timestamp:
 Nov 22, 2010, 2:40:22 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/Errors.ma
r189 r250 15 15 16 16 include "datatypes/pairs.ma". 17 include "Plogic/equality.ma". 18 include "Plogic/connectives.ma". 17 19 18 20 (* * Error reporting and the error monad. *) … … 83 85 (at level 200, X ident, Y ident, A at level 100, B at level 200) 84 86 : error_monad_scope. 87 *) 88 nremark 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. 85 96 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. 97 nremark 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. 95 105 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 (* 106 107 Open Local Scope error_monad_scope. 107 108
Note: See TracChangeset
for help on using the changeset viewer.