Set Implicit Arguments.
The computation monad |
CoInductive computation : Set -> Set :=
| Return : forall (T : Set),
T
-> computation T
| Bind : forall (T1 T2 : Set),
computation T1
-> (T1 -> computation T2)
-> computation T2.
Bounded erasure; potentially-infinite to finite computations parameterized over unknowns |
Inductive erase : forall T, computation T -> forall (S : Set), (S -> T) -> Prop :=
| EraseReturn : forall (T : Set) (v : T),
erase (Return v) (fun _ : unit => v)
| EraseBind : forall (T1 T2 : Set)
(c1 : computation T1) (c2 : T1 -> computation T2)
(S1 S2 : Set) (f1 : S1 -> _) (f2 : _ -> S2 -> _),
erase c1 f1
-> (forall v1, erase (c2 v1) (f2 v1))
-> erase (Bind c1 c2) (fun data => f2 (f1 (fst data)) (snd data))
| EraseDrop : forall (T : Set) (c : computation T),
erase c (fun data => data).
Implicit Arguments EraseReturn [T v].
Implicit Arguments EraseBind [T1 T2 c1 c2 S1 S2 f1 f2].
Implicit Arguments EraseDrop [T c].
Hint Constructors erase.
Inductive run (T : Set) (c : computation T) (v : T) : Prop :=
| Run : forall (S : Set) (f : S -> T),
erase c f
-> (forall data, f data = v)
-> run c v.
Unfolding helpers |
Theorem unfold_computation : forall T (c : computation T),
c = match c in computation T return computation T with
| Return _ v => Return v
| Bind _ _ c1 c2 => Bind c1 c2
end.
Proving
|