[WIP] Moving to stdpp

coq-itree-extra.opam

@@ -13,7 +13,6 @@ bug-reports: "https://github.com/DeepSpec/InteractionTrees/issues"
 depends: [
   "dune" {>= "3.14"}
   "coq"
-  "coq-ext-lib"
   "coq-paco"
   "coq-itree"
   "odoc" {with-doc}

coq-itree.opam

@@ -20,7 +20,6 @@ bug-reports: "https://github.com/DeepSpec/InteractionTrees/issues"
 depends: [
   "dune" {>= "3.14"}
   "coq" {>= "8.13"}
-  "coq-ext-lib" {>= "0.11.1"}
   "coq-paco" {>= "4.0.1"}
   "odoc" {with-doc}
 ]

dune-project

@@ -11,7 +11,6 @@
   (synopsis "Library for representing recursive and impure programs with equational reasoning")
   (depends
     (coq (>= 8.13))
-    (coq-ext-lib (>= 0.11.1))
     (coq-paco (>= 4.0.1)))
   (tags ("org:deepspec"))
   (authors
@@ -29,7 +28,6 @@
   (synopsis "Extensions to coq-itree")
   (depends
     coq
-    coq-ext-lib
     coq-paco
     coq-itree)
   (tags ("org:deepspec"))

theories/Basics/Basics.v

@@ -3,26 +3,16 @@
 (** Not specific to itrees. *)
 
 (* begin hide *)
-From Coq Require
-     Ensembles.
-
 From Coq Require Import
      RelationClasses.
 
-From ExtLib Require Import
-     Structures.Functor
-     Structures.Monad
-     Data.Monads.StateMonad
-     Data.Monads.ReaderMonad
-     Data.Monads.OptionMonad
-     Data.Monads.EitherMonad.
-
-Import
-  FunctorNotation
-  MonadNotation.
-Local Open Scope monad.
+From stdpp Require Export
+  prelude.
+
+Set Primitive Projections.
 (* end hide *)
 
+
 (** ** Parametric functions *)
 
 (** A notation for a certain class of parametric functions.
@@ -45,41 +35,176 @@ Definition idM {E : Type -> Type} : E ~> E := fun _ e => e.
 (** [void] is a shorthand for [Empty_set]. *)
 Notation void := Empty_set.
 
+(* Canonical equivalence relation for a unary type family. *)
+Class Eq1 (M : Type -> Type) : Type :=
+  eq1 : forall A, M A -> M A -> Prop.
+
+Arguments eq1 {M _ _}.
+Declare Scope monad_scope.
+Open Scope monad_scope.
+Infix "≈" := eq1 (at level 70) : monad_scope.
+
+Class App (T : Type → Type) := ap : ∀ {A B}, T (A → B) → T A → T B.
+
+(* Proof that [eq1] is an equivalence relation. *)
+Class Eq1Equivalence (M : Type -> Type) `{Eq1 M} :=
+  eq1_equiv : forall A, Equivalence (eq1 (A := A)).
+
+#[global] Existing Instance eq1_equiv.
+
+(* Monad laws up to [M]'s canonical equivalence relation. *)
+Class MonadLawsE (M : Type -> Type) `{@Eq1 M, MRet M, MBind M} : Prop :=
+  { bind_ret_l : forall A B (f : A -> M B) (x : A), mret x ≫= f ≈ f x
+  ; bind_ret_r : forall A (x : M A), x ≫= (fun y => mret y) ≈ x
+  ; bind_bind : forall A B C (x : M A) (f : A -> M B) (g : B -> M C),
+      (x ≫= f) ≫= g ≈ x ≫= (fun y => f y ≫= g)
+  ; Proper_bind : forall {A B},
+      (@Proper ((A -> M B) -> M A -> M B)
+         (pointwise_relation _ eq1 ==> eq1 ==> eq1)
+         mbind)
+  }.
+
+#[global] Existing Instance Proper_bind.
+
+Arguments bind_ret_l {M _ _ _ _}.
+Arguments bind_ret_r {M _ _ _ _}.
+Arguments bind_bind {M _ _ _ _}.
+Arguments Proper_bind {M _ _ _ _}.
 (** ** Common monads and transformers. *)
 
-Module Monads.
+Section Monads.
 
+(* id *)
 Definition identity (a : Type) : Type := a.
 
+#[global] Instance FMap_identity : FMap identity
+  := fun _ _ f => f.
+
+#[global] Instance MRet_identity : MRet identity
+  := fun _ a => a.
+
+#[global] Instance MBind_identity : MBind identity
+  := fun _ _ k c => k c.
+
+(* either *)
+Definition either (e a : Type) : Type := sum e a.
+
+#[global] Instance FMap_either {e} : FMap (either e)
+  := fun _ _ f ea => match ea with | inl e => inl e | inr a => inr (f a) end.
+
+#[global] Instance MRet_either {e} : MRet (either e)
+  := fun _ a => inr a.
+
+#[global] Instance MBind_either {e} : MBind (either e)
+  := fun _ _ k c => match c with | inl e => inl e | inr a => k a end.
+
+(* state *)
+Definition state (s a : Type) := s -> prod s a.
+
+#[global] Instance FMap_state {s} : FMap (state s)
+  :=  fun _ _ f run s => (fun sa => (fst sa, f (snd sa))) (run s).
+
+#[global] Instance MRet_state {s} : MRet (state s)
+  := fun _ a s => (s, a).
+
+#[global] Instance MBind_state {s} : MBind (state s) :=
+  fun _ _ k c => fun s => let sa := c s in
+                    k (snd sa) (fst sa).
+
+(* reader *)
+Definition reader (r a : Type) := r -> a.
+
+#[global] Instance FMap_reader {r} : FMap (reader r)
+  :=  fun _ _ f run r => f (run r).
+
+#[global] Instance MRet_reader {r} : MRet (reader r)
+  := fun _ a _ => a.
+
+#[global] Instance MBind_reader {r} : MBind (reader r) :=
+  fun _ _ k c => fun r => k (c r) r.
+
+(* writer *)
+Definition writer := prod.
+
+(* optionT *)
+
+Definition optionT (m : Type -> Type) (a : Type) : Type :=
+  m (option a).
+
+#[global] Instance FMap_optionT {m} {Fm : FMap m} : FMap (optionT m)
+  := fun _ _ f c => (fun x => match x with | None => None | Some x => Some (f x) end ) <$> c.
+
+#[global] Instance MRet_optionT {m} {Fm : MRet m} : MRet (optionT m)
+  := fun _ a => mret (Some a).
+
+#[global] Instance MBind_optionT {m} `{MRet m, MBind m} : MBind (optionT m) :=
+  fun _ _ k c => mbind (M := m) (fun oa => match oa with
+                                     | None   => mret (M := m) None
+                                     | Some a => k a
+                                     end) c.
+
+Definition run_optionT {m a} (x : optionT m a) : m (option a)%type := x.
+
+Definition liftOption {a f} `{FMap f} (fa : f a) : optionT f a :=
+  Some <$> fa.
+
+(* eitherT *)
+Definition eitherT (e : Type) (m : Type -> Type) (a : Type) : Type := m (sum e a).
+
+#[global] Instance FMap_eitherT {e m} `{FMap m} : FMap (eitherT e m)
+  := fun _ _ f c => (fun ea => match ea with | inl e => inl e | inr a => inr (f a) end) <$> c.
+
+#[global] Instance MRet_eitherT {e m} `{MRet m} : MRet (eitherT e m)
+  := fun _ a => mret (inr a).
+
+#[global] Instance MBind_eitherT {e m} `{MRet m, MBind m} : MBind (eitherT e m)
+  := fun _ _ f => mbind (M := m) (fun ea => match ea with | inl e => mret (inl e) | inr a => f a end).
+
+Definition runEither {e m a} (x : eitherT e m a) : m (sum e a) := x.
+
+Definition liftEither {e f a} `{FMap f} (fa : f a) : eitherT e f a := inr <$> fa.
+
+(* stateT *)
 Definition stateT (s : Type) (m : Type -> Type) (a : Type) : Type :=
   s -> m (prod s a).
-Definition state (s a : Type) := s -> prod s a.
+
+#[global] Instance FMap_stateT {m s} {Fm : FMap m} : FMap (stateT s m)
+  :=  fun _ _ f run s => fmap (fun sa => (fst sa, f (snd sa))) (run s).
+
+#[global] Instance MRet_stateT {m s} {Fm : MRet m} : MRet (stateT s m)
+  := fun _ a s => mret (s, a).
+
+#[global] Instance MBind_stateT {m s} {Fm : MBind m} : MBind (stateT s m) :=
+  fun _ _ k c => fun s => sa ← c s ;
+                    k (snd sa) (fst sa).
 
 Definition run_stateT {s m a} (x : stateT s m a) : s -> m (s * a)%type := x.
 
-Definition liftState {s a f} `{Functor f} (fa : f a) : Monads.stateT s f a :=
+Definition liftState {s a f} `{FMap f} (fa : f a) : stateT s f a :=
   fun s => pair s <$> fa.
 
+(* readerT *)
 Definition readerT (r : Type) (m : Type -> Type) (a : Type) : Type :=
   r -> m a.
-Definition reader (r a : Type) := r -> a.
 
-Definition writerT (w : Type) (m : Type -> Type) (a : Type) : Type :=
-  m (prod w a).
-Definition writer := prod.
+#[global] Instance FMap_readerT {m r} {Fm : FMap m} : FMap (readerT r m)
+  :=  fun _ _ f run r => fmap f (run r).
 
-#[global] Instance Functor_stateT {m s} {Fm : Functor m} : Functor (stateT s m)
-  := {|
-    fmap _ _ f := fun run s => fmap (fun sa => (fst sa, f (snd sa))) (run s)
-    |}.
+#[global] Instance MRet_readerT {m r} {Fm : MRet m} : MRet (readerT r m)
+  := fun _ a _ => mret a.
 
-#[global] Instance Monad_stateT {m s} {Fm : Monad m} : Monad (stateT s m)
-  := {|
-    ret _ a := fun s => ret (s, a)
-  ; bind _ _ t k := fun s =>
-      sa <- t s ;;
-      k (snd sa) (fst sa)
-    |}.
+#[global] Instance MBind_readerT {m r} {Fm : MBind m} : MBind (readerT r m) :=
+  fun _ _ k c => fun r => v ← c r ;
+                    k v r.
+
+Definition run_readerT {r m a} (x : readerT r m a) : r -> m a%type := x.
+
+Definition liftReader {r a f} `{FMap f} (fa : f a) : readerT r f a :=
+  fun _ => fa.
+
+(* writerT *)
+Definition writerT (w : Type) (m : Type -> Type) (a : Type) : Type :=
+  m (prod w a).
 
 End Monads.
 
@@ -101,71 +226,62 @@ Polymorphic Class MonadIter (M : Type -> Type) : Type :=
     Quite easily in fact, no [Monad] assumption needed.
  *)
 
-#[global] Instance MonadIter_stateT {M S} {MM : Monad M} {AM : MonadIter M}
+#[global] Polymorphic Instance MonadIter_stateT {M S} `{MRet M, MBind M, MonadIter M}
   : MonadIter (stateT S M) :=
-  fun _ _ step i => mkStateT (fun s =>
-    iter (fun is =>
-      let i := fst is in
-      let s := snd is in
-      is' <- runStateT (step i) s ;;
-      ret match fst is' with
-          | inl i' => inl (i', snd is')
-          | inr r => inr (r, snd is')
-          end) (i, s)).
-
-#[global] Polymorphic Instance MonadIter_stateT0 {M S} {MM : Monad M} {AM : MonadIter M}
-  : MonadIter (Monads.stateT S M) :=
   fun _ _ step i s =>
     iter (fun si =>
-      let s := fst si in
-      let i := snd si in
-      si' <- step i s;;
-      ret match snd si' with
-          | inl i' => inl (fst si', i')
-          | inr r => inr (fst si', r)
-          end) (s, i).
+            let s := fst si in
+            let i := snd si in
+            si' ← step i s;
+            mret match snd si' with
+              | inl i' => inl (fst si', i')
+              | inr r => inr (fst si', r)
+              end) (s, i).
 
 #[global] Instance MonadIter_readerT {M S} {AM : MonadIter M} : MonadIter (readerT S M) :=
-  fun _ _ step i => mkReaderT (fun s =>
-    iter (fun i => runReaderT (step i) s) i).
+  fun _ _ step i => fun r =>
+    iter (fun i => run_readerT (step i) r) i.
 
-#[global] Instance MonadIter_optionT {M} {MM : Monad M} {AM : MonadIter M}
+#[global] Instance MonadIter_optionT {M} `{MRet M, MBind M, MonadIter M}
   : MonadIter (optionT M) :=
-  fun _ _ step i => mkOptionT (
+  fun _ _ step i =>
     iter (fun i =>
-      oi <- unOptionT (step i) ;;
-      ret match oi with
-          | None => inr None
-          | Some (inl i) => inl i
-          | Some (inr r) => inr (Some r)
-          end) i).
-
-#[global] Instance MonadIter_eitherT {M E} {MM : Monad M} {AM : MonadIter M}
+            oi ← step i ;
+            mret match oi with
+              | None => inr None
+              | Some (inl i) => inl i
+              | Some (inr r) => inr (Some r)
+              end) i.
+
+#[global] Instance MonadIter_eitherT {M E} `{MRet M, MBind M, MonadIter M} {AM : MonadIter M}
   : MonadIter (eitherT E M) :=
-  fun _ _ step i => mkEitherT (
+  fun _ _ step i =>
     iter (fun i =>
-      ei <- unEitherT (step i) ;;
-      ret match ei with
-          | inl e => inr (inl e)
-          | inr (inl i) => inl i
-          | inr (inr r) => inr (inr r)
-          end) i).
+            ei ← step i ;
+            mret match ei with
+              | inl e => inr (inl e)
+              | inr (inl i) => inl i
+              | inr (inr r) => inr (inr r)
+              end) i.
 
 (** And the nondeterminism monad [_ -> Prop] also has one. *)
+From stdpp Require Import propset.
 
-Inductive iter_Prop {R I : Type} (step : I -> I + R -> Prop) (i : I) (r : R)
+Inductive iter_Prop {R I : Type} (step : I -> propset (I + R)) (i : I) (r : R)
   : Prop :=
 | iter_done
-  : step i (inr r) -> iter_Prop step i r
+  : propset_car (step i) (inr r) -> iter_Prop step i r
 | iter_step i'
-  : step i (inl i') ->
+  : propset_car (step i) (inl i') ->
     iter_Prop step i' r ->
     iter_Prop step i r
 .
 
-#[global] Polymorphic Instance MonadIter_Prop : MonadIter Ensembles.Ensemble := @iter_Prop.
+#[global] Polymorphic Instance MonadIter_Prop : MonadIter propset :=
+  fun _ _ step i => PropSet (iter_Prop step i).
 
 (* Elementary constructs for predicates. To be moved in their own file eventually *)
+(* TODO: should they be entirely replaced with constructions in [propset]? *)
 Definition equiv_pred {A : Type} (R S: A -> Prop): Prop :=
   forall a, R a <-> S a.
 
@@ -194,4 +310,3 @@ Qed.
 Proof.
   split; typeclasses eauto.
 Qed.
-