Lvc.Infra.Status
Require Import String List Get.
Set Implicit Arguments.
Inductive status A :=
| Success : A → status A
| Error : string → status A.
Definition bind (A B : Type) (f : status A) (g : A → status B) : status B :=
match f with
| Success a ⇒ g a
| Error e ⇒ Error e
end.
Notation "´sdo´ X <- A ; B" := (bind A (fun X ⇒ B))
(at level 200, X ident, A at level 100, B at level 200).
Definition option2status {A} : option A → string → status A.
Defined.
Lemma option2status_inv {A} o s (v:A)
: option2status o s = Success v
→ o = Some v.
Lemma bind_inversion (A B : Type) (f : status A) (g : A → status B) (y : B) :
bind f g = Success y → ∃ x, f = Success x ∧ g x = Success y.
Lemma bind_inversion´ (A B : Type) (f : status A) (g : A → status B) (y : B) :
bind f g = Success y → { x : A | f = Success x ∧ g x = Success y }.
Set Implicit Arguments.
Inductive status A :=
| Success : A → status A
| Error : string → status A.
Definition bind (A B : Type) (f : status A) (g : A → status B) : status B :=
match f with
| Success a ⇒ g a
| Error e ⇒ Error e
end.
Notation "´sdo´ X <- A ; B" := (bind A (fun X ⇒ B))
(at level 200, X ident, A at level 100, B at level 200).
Definition option2status {A} : option A → string → status A.
Defined.
Lemma option2status_inv {A} o s (v:A)
: option2status o s = Success v
→ o = Some v.
Lemma bind_inversion (A B : Type) (f : status A) (g : A → status B) (y : B) :
bind f g = Success y → ∃ x, f = Success x ∧ g x = Success y.
Lemma bind_inversion´ (A B : Type) (f : status A) (g : A → status B) (y : B) :
bind f g = Success y → { x : A | f = Success x ∧ g x = Success y }.
Reasoning over monadic computations
H: (do x <- a; b) = OK res
By definition of the bind operation, both computations a and
b must succeed for their composition to succeed. The tactic
therefore generates the following hypotheses:
Ltac monadS_inv1 H :=
match type of H with
| (Success _ = Success _) ⇒
inversion H; clear H; try subst
| (Error _ = Success _) ⇒
discriminate
| (bind ?F ?G = Success ?X) ⇒
let x := fresh "x" in (
let EQ1 := fresh "EQ" in (
let EQ2 := fresh "EQ" in (
destruct (bind_inversion´ F G H) as [x [EQ1 EQ2]];
clear H;
try (monadS_inv1 EQ2))))
end.
Ltac monadS_inv H :=
match type of H with
| (Success _ = Success _) ⇒ monadS_inv1 H
| (Error _ = Success _) ⇒ monadS_inv1 H
| (bind ?F ?G = Success ?X) ⇒ monadS_inv1 H
| (@eq _ (@bind _ _ _ _ _ ?G) (?X)) ⇒
let X := fresh in remember G as X; simpl in H; subst X; monadS_inv1 H
end.
Section ParametricOptionMapIndex.
Variables X Y : Type.
Hypothesis f : nat → X → status Y : Type.
Fixpoint smapi_impl (n:nat) (L:list X) : status (list Y) :=
match L with
| x::L ⇒
sdo v <- f n x;
sdo vl <- smapi_impl (S n) L;
Success (v::vl)
| _ ⇒ Success nil
end.
Definition smapi := smapi_impl 0.
End ParametricOptionMapIndex.
Section ParametricZip.
Variables X Y Z : Type.
Hypothesis f : X → Y → status Z : Type.
Fixpoint szip (L:list X) (L´:list Y) : status (list Z) :=
match L, L´ with
| x::L, y::L´ ⇒
sdo z <- f x y;
sdo ZL <- szip L L´;
Success (z::ZL)
| _, _ ⇒ Success nil
end.
End ParametricZip.
Section ParametricStatusMap.
Variables X Y : Type.
Hypothesis f : X → status Y : Type.
Fixpoint smap (L:list X) : status (list Y) :=
match L with
| x::L ⇒
sdo v <- f x;
sdo vl <- smap L;
Success (v::vl)
| _ ⇒ Success nil
end.
Lemma smap_spec L L´
: smap L = Success L´
→ ∀ n x, get L n x → ∃ y, f x = Success y ∧ get L´ n y.
Lemma smap_length L L´
: smap L = Success L´
→ length L´ = length L.
End ParametricStatusMap.
Lemma smap_agree_2 X X´ Y (f: X → status Y) (g: X´ → status Y) L L´
: (∀ n x y, get L n x → get L´ n y → f x = g y)
→ length L = length L´
→ smap f L = smap g L´.