# Module AlarmMon

Require Import

Set Implicit Arguments.

Definition alarm_mon (T:Type) : Type := (T*list (unit -> string))%type.

Instance block_mon_gamma T T' `(gamma_op T T') : gamma_op (alarm_mon T) (option T') :=
λ t, match snd t with
| nil => fun x => match x with Some x => x ∈ γ(fst t) | None => False end
| _ => λ _, True
end.

Definition am_get {T} (x: alarm_mon T) : option T :=
match x with (y, nil) => Some y | _ => None end.

{ bind A B x f :=
let '(x, err) := x in
match err with
| nil => f x
| _ =>
let '(y, err') := f x in
(y, err++err')
end;
ret A x := (x, nil)
}.

Notation alarm_am s := ((tt, (fun _ => s)::nil):(alarm_mon _)).

Lemma bind_am_assoc {A B C} (m: alarm_mon A) (f: Aalarm_mon B) (g: Balarm_mon C) :
bind (bind m f) g = bind ma, bind (f a) g).
Proof.
destruct m as (a, q). destruct q; simpl. auto.
destruct (f a) as (b, q'). simpl. destruct (g b) as (c, q'').
destruct q'; rewrite <- app_assoc; reflexivity.
Qed.

Lemma am_bind_case {T T'} (f: alarm_mon T) (b: Talarm_mon T') :
∀ P : alarm_mon T' → Prop,
(∀ x y z, P (x, y :: z)) →
(∀ x, f = (x, nil) → P (b x)) →
P (do a <- f; b a).
Proof.
intros P A B.
destruct f as (x & [|]). generalize (B _ eq_refl); simpl; destruct (b x); exact id.
simpl. destruct (b x). exact (A _ _ _).
Defined.

Notation am_assert b err :=
(if b then ret tt else alarm_am err).

Lemma am_assert_spec b err B (k: alarm_mon B) :
∀ P : _Prop,
(∀ x y z, P (x, y :: z)) →
(b = trueP k) →
P (do _ <- am_assert b err; k).
Proof.
intros P U V.
apply am_bind_case. eauto.
intros (). destruct b. auto. inversion 1.
Qed.

Lemma am_assert_inv (b: bool) err :
am_assert b err = (tt, nil) →
b = true.
Proof.
now destruct b; intros; eq_some_inv.
Qed.

Lemma am_get_ret A (a: A) : am_get (ret a) = Some a.
Proof.
reflexivity. Qed.

Definition am_fold A B (f: ABalarm_mon A) (l: list B) (a: A) : alarm_mon A :=
fold_leftacc b, do acc' <- acc; f acc' b) l (ret a).

Lemma am_fold_app A B f l l' a :
@am_fold A B f (l ++ l') a = do a' <- am_fold f l a; am_fold f l' a'.
Proof.
revert l' l a. induction l' as [|x l' IH] using rev_ind.
intros. rewrite app_nil_r. destruct (am_fold f l a). simpl. rewrite app_nil_r. destruct l0; reflexivity.
intros l a. unfold am_fold at 1. rewrite app_assoc. rewrite fold_left_app.
fold (am_fold f (l ++ l') a). rewrite IH. clear IH. simpl. rewrite bind_am_assoc.
destruct (am_fold f l a) as (a', q). simpl.
unfold am_fold at 3 4. rewrite fold_left_app. reflexivity.
Qed.

Definition am_rev_map A B (f: Balarm_mon A) (l: list B) : alarm_mon (list A) :=
am_foldacc b, do a <- f b; ret (a :: acc)) l nil.

Inductive am_map_t (A: Type) : Type :=
| Result (a: A)
| Errorc (a: option A) (msg: unit -> string).
Notation Error a msg := (Errorc a (fun _ => msg)).
Lemma Result_Error {A} (a: A) a' m : Result a = Errorc a' m → ∀ P : Prop, P.
ProofE, match E in _ = t return match t return Prop with Result _ => True | _ => _ end with eq_refl => I end).
Lemma Result_eq_inv {A} (a a': A) : Result a = Result a' → a = a'.
ProofE, match E in _ = t return match t with Result x => a = x | _ => False end with eq_refl => eq_refl end).
Ltac result_eq_inv :=
repeat match goal with
| H : Result _ = Errorc _ _ |- _ => exact (Result_Error H _)
| H : Errorc _ _ = Result _ |- _ => exact (Result_Error (eq_sym H) _)
| H : Result _ = Result _ |- _ => apply Result_eq_inv in H
end.

Definition am_map' A B (f: Bam_map_t A) (l: list B) : alarm_mon (list A) :=
am_foldacc b, match f b with
| Result a => ret (a :: acc)
| Errorc a msg =>
do _ <- (tt, msg::nil);
ret match a with
| None => acc
| Some a => a :: acc
end
end) l nil.

Lemma am_rev_map_correct A B (f: Balarm_mon A) :
∀ l,
match am_get (am_rev_map f l) with
| Some m =>
(∀ y, In y m → ∃ x, am_get (f x) = Some yIn x l)
∧ (∀ x, In x l → ∃ y, am_get (f x) = Some yIn y m)
| None => ∃ x, In x lam_get (f x) = None
end.
Proof.
induction l using rev_ind.
+ split; intros ? ().
+ unfold am_rev_map, am_fold. rewrite fold_left_app. simpl.
change (fold_leftacc b, do acc' <- acc; do a <- f b; (a :: acc', nil)) l (nil, nil))
with (am_rev_map f l).
destruct (am_rev_map f l) as (acc', [|]).
destruct IHl as (IH & HI).
destruct (f x) as (a, [|]) eqn: FX.
simpl. split.
- intros y [->|IN].
exists x; split. rewrite FX. reflexivity. rewrite in_app. right. left. reflexivity.
destruct (IH _ IN) as (? & ? & ?).
eexists; split; eauto. rewrite in_app. simpl. eauto.
- intros x' IN. rewrite in_app in IN. destruct IN as [IN|[->|()]].
destruct (HI x' IN) as (? & ? & H). eauto.
rewrite FX. eexists. split. reflexivity. auto.
- exists x. split. rewrite in_app. right. left. reflexivity.
rewrite FX. reflexivity.
- destruct IHl as (x' & ? & ?).
simpl. destruct (do a <- f x; (a::acc', nil)).
exists x'. intuition.
Qed.

Lemma am_rev_map_inv A B (f: Balarm_mon A) :
∀ l,
match am_get (am_rev_map f l) with
| Some m =>
m = rev (map (fstf) l)
| None => True
end.
Proof.
induction l using rev_ind.
+ split; intros ? ().
+ unfold am_rev_map, am_fold. rewrite fold_left_app. simpl.
change (fold_leftacc b, do acc' <- acc; do a <- f b; (a :: acc', nil)) l (nil, nil))
with (am_rev_map f l).
destruct (am_rev_map f l) as (acc', [|]).
destruct (f x) as (a, [|]) eqn: FX.
simpl. rewrite map_app, rev_app_distr, IHl. simpl.
rewrite FX. simpl.
simpl. reflexivity.
exact I.
simpl. destruct (do a <- f x; (a::acc', nil)). exact I.
Qed.

Lemma am_map'_correct A B (f: Bam_map_t A) :
∀ l,
match am_get (am_map' f l) with
| Some m =>
(∀ y, In y m → ∃ x, f x = Result yIn x l)
∧ (∀ x, In x l → ∃ y, f x = Result yIn y m)
| None => True
end.
Proof.
induction l using rev_ind.
+ split; intros ? ().
+ unfold am_map', am_fold. rewrite fold_left_app. simpl.
apply am_bind_case. intros; exact I.
intros al.
intros AL.
destruct (f x) eqn: FX. 2: exact I.
unfold am_map', am_fold in IHl. simpl in IHl.
rewrite AL in IHl.
destruct IHl as (IH & HI).
simpl; split.
- intros y [->|IN].
exists x; split. rewrite FX. reflexivity. rewrite in_app. right. left. reflexivity.
destruct (IH _ IN) as (? & ? & ?).
eexists; split; eauto. rewrite in_app. simpl. eauto.
- intros x' IN. rewrite in_app in IN. destruct IN as [IN|[->|()]].
destruct (HI x' IN) as (? & ? & H). eauto.
rewrite FX. eexists. split. reflexivity. auto.
Qed.

Ltac with_am_map' :=
match goal with
|- appcontext[ am_map' ?f ?l ] =>
let map_f := fresh "map_f" in
remember f as map_f;
generalize (am_map'_correct map_f l);
destruct (am_map' map_f l) as (? & [|]);
[subst map_f| easy ]
end.