error.v 4.11 KB
 Robbert Krebbers committed Aug 09, 2014 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 ``````(* Copyright (c) 2012-2014, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) Require Export list. Instance error_ret {E} : MRet (sum E) := λ A, inr. Instance error_bind {E} : MBind (sum E) := λ A B f x, match x with inr a => f a | inl e => inl e end. Instance error_fmap {E} : FMap (sum E) := λ A B f x, match x with inr a => inr (f a) | inl e => inl e end. Definition error_guard {E} P {dec : Decision P} {A} (e : E) (f : P → E + A) : E + A := match decide P with left H => f H | right _ => inl e end. Notation "'guard' P 'with' e ; o" := (error_guard P e (λ _, o)) (at level 65, next at level 35, only parsing, right associativity) : C_scope. Definition error_of_option {A E} (x : option A) (e : E) : sum E A := match x with Some a => inr a | None => inl e end. `````` Robbert Krebbers committed Aug 22, 2014 19 20 21 22 23 24 25 26 27 28 ``````Lemma bind_inr {A B E} (f : A → E + B) x b : x ≫= f = inr b ↔ ∃ a, x = inr a ∧ f a = inr b. Proof. destruct x; naive_solver. Qed. Lemma fmap_inr {A B E} (f : A → B) (x : E + A) b : f <\$> x = inr b ↔ ∃ a, x = inr a ∧ f a = b. Proof. destruct x; naive_solver. Qed. Lemma error_of_option_inr {A E} (o : option A) (e : E) a : error_of_option o e = inr a ↔ o = Some a. Proof. destruct o; naive_solver. Qed. `````` Robbert Krebbers committed Aug 09, 2014 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 ``````Tactic Notation "case_error_guard" "as" ident(Hx) := match goal with | H : context C [@error_guard _ ?P ?dec _ ?e ?x] |- _ => let X := context C [ match dec with left H => x H | _ => inl e end ] in change X in H; destruct_decide dec as Hx | |- context C [@error_guard _ ?P ?dec _ ?e ?x] => let X := context C [ match dec with left H => x H | _ => inl e end ] in change X; destruct_decide dec as Hx end. Tactic Notation "case_error_guard" := let H := fresh in case_error_guard as H. Tactic Notation "simplify_error_equality" := repeat match goal with | _ => progress simplify_equality' `````` Robbert Krebbers committed Sep 30, 2014 44 45 46 `````` | H : appcontext [@mret (sum ?E) _ ?A] |- _ => change (@mret (sum E) _ A) with (@inr E A) in H | |- appcontext [@mret (sum ?E) _ ?A] => change (@mret _ _ A) with (@inr E A) `````` Robbert Krebbers committed Nov 06, 2014 47 48 49 50 `````` | _ : maybe _ ?x = Some _ |- _ => is_var x; destruct x | _ : maybe2 _ ?x = Some _ |- _ => is_var x; destruct x | _ : maybe3 _ ?x = Some _ |- _ => is_var x; destruct x | _ : maybe4 _ ?x = Some _ |- _ => is_var x; destruct x `````` Robbert Krebbers committed Aug 22, 2014 51 `````` | H : error_of_option ?o ?e = ?x |- _ => apply error_of_option_inr in H `````` Robbert Krebbers committed Aug 09, 2014 52 `````` | H : mbind (M:=sum _) ?f ?o = ?x |- _ => `````` Robbert Krebbers committed Aug 22, 2014 53 `````` apply bind_inr in H; destruct H as (?&?&?) `````` Robbert Krebbers committed Aug 09, 2014 54 `````` | H : fmap (M:=sum _) ?f ?o = ?x |- _ => `````` Robbert Krebbers committed Aug 22, 2014 55 56 57 58 59 `````` apply fmap_inr in H; destruct H as (?&?&?) | H : mbind (M:=option) ?f ?o = ?x |- _ => apply bind_Some in H; destruct H as (?&?&?) | H : fmap (M:=option) ?f ?o = ?x |- _ => apply fmap_Some in H; destruct H as (?&?&?) `````` Robbert Krebbers committed Aug 09, 2014 60 61 `````` | _ => progress case_decide | _ => progress case_error_guard `````` Robbert Krebbers committed Aug 22, 2014 62 `````` | _ => progress case_option_guard `````` Robbert Krebbers committed Aug 09, 2014 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 `````` end. Section mapM. Context {A B E : Type} (f : A → E + B). Lemma error_mapM_ext (g : A → sum E B) l : (∀ x, f x = g x) → mapM f l = mapM g l. Proof. intros Hfg. by induction l; simpl; rewrite ?Hfg, ?IHl. Qed. Lemma error_Forall2_mapM_ext (g : A → E + B) l k : Forall2 (λ x y, f x = g y) l k → mapM f l = mapM g k. Proof. induction 1 as [|???? Hfg ? IH]; simpl. done. by rewrite Hfg, IH. Qed. Lemma error_Forall_mapM_ext (g : A → E + B) l : Forall (λ x, f x = g x) l → mapM f l = mapM g l. Proof. induction 1 as [|?? Hfg ? IH]; simpl. done. by rewrite Hfg, IH. Qed. Lemma mapM_inr_1 l k : mapM f l = inr k → Forall2 (λ x y, f x = inr y) l k. Proof. revert k. induction l as [|x l]; intros [|y k]; simpl; try done. * destruct (f x); simpl; [discriminate|]. by destruct (mapM f l). `````` Robbert Krebbers committed Sep 30, 2014 81 `````` * destruct (f x) eqn:?; intros; simplify_error_equality; auto. `````` Robbert Krebbers committed Aug 09, 2014 82 83 84 85 86 87 88 89 90 91 92 `````` Qed. Lemma mapM_inr_2 l k : Forall2 (λ x y, f x = inr y) l k → mapM f l = inr k. Proof. induction 1 as [|???? Hf ? IH]; simpl; [done |]. rewrite Hf. simpl. by rewrite IH. Qed. Lemma mapM_inr l k : mapM f l = inr k ↔ Forall2 (λ x y, f x = inr y) l k. Proof. split; auto using mapM_inr_1, mapM_inr_2. Qed. Lemma error_mapM_length l k : mapM f l = inr k → length l = length k. Proof. intros. by eapply Forall2_length, mapM_inr_1. Qed. End mapM.``````