blob: d13bfee5aef3af4503e9515704ba218375aa7be4 (
about) (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
|
From mininix Require Export utils.
From stdpp Require Import options.
Variant res A :=
| Res (x : option A)
| NoFuel.
Arguments Res {_} _.
Arguments NoFuel {_}.
Instance res_fail : MFail res := λ {A} _, Res None.
Instance res_mret : MRet res := λ {A} x, Res (Some x).
Instance res_mbind : MBind res := λ {A B} f rx,
match rx with
| Res mx => default mfail (f <$> mx)
| NoFuel => NoFuel
end.
Instance res_fmap : FMap res := λ {A B} f rx,
match rx with
| Res mx => Res (f <$> mx)
| NoFuel => NoFuel
end.
Instance Res_inj A : Inj (=) (=) (@Res A).
Proof. by injection 1. Qed.
Ltac simplify_res :=
repeat match goal with
| H : Res _ = mfail |- _ => apply (inj Res) in H
| H : mfail = Res _ |- _ => apply (inj Res) in H
| H : Res _ = mret _ |- _ => apply (inj Res) in H
| H : mret _ = Res _ |- _ => apply (inj Res) in H
| _ => progress simplify_eq/=
end.
Lemma mapM_Res_impl {A B} (f g : A → res B) (xs : list A) ys :
mapM f xs = Res ys →
(∀ x y, f x = Res y → g x = Res y) →
mapM g xs = Res ys.
Proof.
intros Hxs Hf. revert ys Hxs.
induction xs as [|x xs IH]; intros ys ?; simplify_res; [done|].
destruct (f x) as [my|] eqn:?; simplify_res. rewrite (Hf x my) //=.
destruct my as [y|]; simplify_res; [|done].
destruct (mapM f _) as [mys|]; simplify_res; [|done..].
by rewrite (IH _ eq_refl).
Qed.
Lemma map_mapM_sorted_Res_impl `{FinMap K M}
(R : relation K) `{!RelDecision R, !PartialOrder R, !Total R}
{A B} (f g : A → res B) (m1 : M A) m2 :
map_mapM_sorted R f m1 = Res m2 →
(∀ x y, f x = Res y → g x = Res y) →
map_mapM_sorted R g m1 = Res m2.
Proof.
intros Hm Hf. revert m2 Hm.
induction m1 as [|i x m1 ?? IH] using (map_sorted_ind R); intros m2.
{ by rewrite !map_mapM_sorted_empty. }
rewrite !map_mapM_sorted_insert //. intros.
destruct (f x) as [my|] eqn:?; simplify_res. rewrite (Hf x my) //=.
destruct my as [y|]; simplify_res; [|done].
destruct (map_mapM_sorted _ f _) as [mm2'|]; simplify_res; [|done..].
by rewrite (IH _ eq_refl).
Qed.
Lemma mapM_res_app {A B} (f : A → res B) xs1 xs2 :
mapM f (xs1 ++ xs2) = ys1 ← mapM f xs1; ys2 ← mapM f xs2; mret (ys1 ++ ys2).
Proof.
induction xs1 as [|x1 xs1 IH]; simpl.
{ by destruct (mapM f xs2) as [[]|]. }
destruct (f x1) as [[y1|]|]; simpl; [|done..].
rewrite IH. by destruct (mapM f xs1) as [[]|], (mapM f xs2) as [[]|].
Qed.
|
