From Tealeaves Require Import
  Functors.Early.Subset
  Functors.Early.Reader (map_strength_cobind_spec)
  Classes.Kleisli.DecoratedTraversableFunctor
  Classes.Kleisli.DecoratedMonad
  Classes.Categorical.DecoratedMonad (shift).

Export Functors.Early.Subset.

Import Comonad.Notations.
Import Kleisli.Monad.Notations.
Import Categorical.Monad.Notations.
Import Product.Notations.
Import Functors.Early.Subset.Notations.
Import Monoid.Notations.
Import DecoratedMonad.Notations.

#[local] Generalizable Variables W A B.

(** * The <<ctxset>> Decorated Functor *)
(**********************************************************************)
Definition ctxset (E: Type) := fun A => subset (E * A).

Section ctxset.

  Context
    (E: Type).

  (** ** Operations and Specifications *)
  (********************************************************************)
  #[export] Instance Mapd_ctxset: Mapd E (ctxset E) :=
    fun `(f: E * A -> B) (s: ctxset E A) =>
    fun '(e, b) => exists (a: A), s (e, a) /\ f (e, a) = b.

  #[export] Instance Map_ctxset: Map (ctxset E) :=
    fun `(f: A -> B) (s: ctxset E A) =>
    fun '(e, b) => exists (a: A), s (e, a) /\ f a = b.

  Lemma ctxset_mapd_spec: forall (A B: Type) `(f: E * A -> B),
      mapd (T := ctxset E) f = map (F := subset) (cobind f).
E: Type
forall (A B : Type) (f : E * A -> B),
mapd f = map (cobind f)
  Proof.
E: Type
forall (A B : Type) (f : E * A -> B),
mapd f = map (cobind f)
    intros.
E, A, B: Type
f: E * A -> B
mapd f = map (cobind f) ext s [e b].
E, A, B: Type
f: E * A -> B
s: ctxset E A
e: E
b: B
mapd f s (e, b) = map (cobind f) s (e, b)
    cbv.
E, A, B: Type
f: E * A -> B
s: ctxset E A
e: E
b: B
(exists a : A, s (e, a) /\ f (e, a) = b) =
(exists a : E * A,
   s a /\
   (let '(e, a0) := a in (e, f (e, a0))) = (e, b)) propext.
E, A, B: Type
f: E * A -> B
s: ctxset E A
e: E
b: B
(exists a : A, s (e, a) /\ f (e, a) = b) ->
exists a : E * A,
  s a /\
  (let '(e, a0) := a in (e, f (e, a0))) = (e, b)
E, A, B: Type
f: E * A -> B
s: ctxset E A
e: E
b: B
(exists a : E * A,
   s a /\
   (let '(e, a0) := a in (e, f (e, a0))) = (e, b)) ->
exists a : A, s (e, a) /\ f (e, a) = b
    -
E, A, B: Type
f: E * A -> B
s: ctxset E A
e: E
b: B
(exists a : A, s (e, a) /\ f (e, a) = b) ->
exists a : E * A,
  s a /\
  (let '(e, a0) := a in (e, f (e, a0))) = (e, b) intros [a [Hin Heq]].
E, A, B: Type
f: E * A -> B
s: ctxset E A
e: E
b: B
a: A
Hin: s (e, a)
Heq: f (e, a) = b
exists a : E * A,
  s a /\
  (let '(e, a0) := a in (e, f (e, a0))) = (e, b)
      exists (e, a).
E, A, B: Type
f: E * A -> B
s: ctxset E A
e: E
b: B
a: A
Hin: s (e, a)
Heq: f (e, a) = b
s (e, a) /\ (e, f (e, a)) = (e, b) now subst.
    -
E, A, B: Type
f: E * A -> B
s: ctxset E A
e: E
b: B
(exists a : E * A,
   s a /\
   (let '(e, a0) := a in (e, f (e, a0))) = (e, b)) ->
exists a : A, s (e, a) /\ f (e, a) = b intros [[e' a] [Hin Heq]].
E, A, B: Type
f: E * A -> B
s: ctxset E A
e: E
b: B
e': E
a: A
Hin: s (e', a)
Heq: (e', f (e', a)) = (e, b)
exists a : A, s (e, a) /\ f (e, a) = b
      exists a.
E, A, B: Type
f: E * A -> B
s: ctxset E A
e: E
b: B
e': E
a: A
Hin: s (e', a)
Heq: (e', f (e', a)) = (e, b)
s (e, a) /\ f (e, a) = b inversion Heq.
E, A, B: Type
f: E * A -> B
s: ctxset E A
e: E
b: B
e': E
a: A
Hin: s (e', a)
Heq: (e', f (e', a)) = (e, b)
H0: e' = e
H1: f (e, a) = b
s (e, a) /\ f (e, a) = f (e, a) now subst.
  Qed.

  Lemma ctxset_map_spec: forall (A B: Type) `(f: A -> B),
      map (F := ctxset E) f = map (F := subset) (map f).
E: Type
forall (A B : Type) (f : A -> B), map f = map (map f)
  Proof.
E: Type
forall (A B : Type) (f : A -> B), map f = map (map f)
    intros.
E, A, B: Type
f: A -> B
map f = map (map f) ext s [e b].
E, A, B: Type
f: A -> B
s: ctxset E A
e: E
b: B
map f s (e, b) = map (map f) s (e, b)
    cbv.
E, A, B: Type
f: A -> B
s: ctxset E A
e: E
b: B
(exists a : A, s (e, a) /\ f a = b) =
(exists a : E * A,
   s a /\ (let (x, y) := a in (x, f y)) = (e, b)) propext.
E, A, B: Type
f: A -> B
s: ctxset E A
e: E
b: B
(exists a : A, s (e, a) /\ f a = b) ->
exists a : E * A,
  s a /\ (let (x, y) := a in (x, f y)) = (e, b)
E, A, B: Type
f: A -> B
s: ctxset E A
e: E
b: B
(exists a : E * A,
   s a /\ (let (x, y) := a in (x, f y)) = (e, b)) ->
exists a : A, s (e, a) /\ f a = b
    -
E, A, B: Type
f: A -> B
s: ctxset E A
e: E
b: B
(exists a : A, s (e, a) /\ f a = b) ->
exists a : E * A,
  s a /\ (let (x, y) := a in (x, f y)) = (e, b) intros [a [Hin Heq]].
E, A, B: Type
f: A -> B
s: ctxset E A
e: E
b: B
a: A
Hin: s (e, a)
Heq: f a = b
exists a : E * A,
  s a /\ (let (x, y) := a in (x, f y)) = (e, b)
      exists (e, a).
E, A, B: Type
f: A -> B
s: ctxset E A
e: E
b: B
a: A
Hin: s (e, a)
Heq: f a = b
s (e, a) /\ (e, f a) = (e, b) now subst.
    -
E, A, B: Type
f: A -> B
s: ctxset E A
e: E
b: B
(exists a : E * A,
   s a /\ (let (x, y) := a in (x, f y)) = (e, b)) ->
exists a : A, s (e, a) /\ f a = b intros [[e' a] [Hin Heq]].
E, A, B: Type
f: A -> B
s: ctxset E A
e: E
b: B
e': E
a: A
Hin: s (e', a)
Heq: (e', f a) = (e, b)
exists a : A, s (e, a) /\ f a = b
      exists a.
E, A, B: Type
f: A -> B
s: ctxset E A
e: E
b: B
e': E
a: A
Hin: s (e', a)
Heq: (e', f a) = (e, b)
s (e, a) /\ f a = b inversion Heq.
E, A, B: Type
f: A -> B
s: ctxset E A
e: E
b: B
e': E
a: A
Hin: s (e', a)
Heq: (e', f a) = (e, b)
H0: e' = e
H1: f a = b
s (e, a) /\ f a = f a now subst.
  Qed.

  Lemma ctxset_map_to_mapd: forall (A B: Type) (f: A -> B),
      map f = mapd (T := ctxset E) (f ∘ extract).
E: Type
forall (A B : Type) (f : A -> B),
map f = mapd (f ∘ extract)
  Proof.
E: Type
forall (A B : Type) (f : A -> B),
map f = mapd (f ∘ extract)
    intros.
E, A, B: Type
f: A -> B
map f = mapd (f ∘ extract)
    rewrite ctxset_mapd_spec, ctxset_map_spec.
E, A, B: Type
f: A -> B
map (map f) = map (cobind (f ∘ extract))
    rewrite (map_to_cobind (W := (E ×))).
E, A, B: Type
f: A -> B
map (cobind (f ∘ extract)) =
map (cobind (f ∘ extract))
    reflexivity.
  Qed.

  (** ** Decorated Functor Laws *)
  (********************************************************************)
  Lemma kdf_subset_mapd1:
    forall A: Type,
      mapd (T := ctxset E) extract = @id (ctxset E A).
E: Type
forall A : Type, mapd extract = id
  Proof.
E: Type
forall A : Type, mapd extract = id
    intros.
E, A: Type
mapd extract = id cbv.
E, A: Type
(fun (s : E * A -> Prop) '(e, b) =>
 exists a : A, s (e, a) /\ a = b) =
(fun x : E * A -> Prop => x) ext f [e a].
E, A: Type
f: E * A -> Prop
e: E
a: A
(exists a0 : A, f (e, a0) /\ a0 = a) = f (e, a) propext.
E, A: Type
f: E * A -> Prop
e: E
a: A
(exists a0 : A, f (e, a0) /\ a0 = a) -> f (e, a)
E, A: Type
f: E * A -> Prop
e: E
a: A
f (e, a) -> exists a0 : A, f (e, a0) /\ a0 = a
    -
E, A: Type
f: E * A -> Prop
e: E
a: A
(exists a0 : A, f (e, a0) /\ a0 = a) -> f (e, a) intros [a' Heq].
E, A: Type
f: E * A -> Prop
e: E
a, a': A
Heq: f (e, a') /\ a' = a
f (e, a) now preprocess.
    -
E, A: Type
f: E * A -> Prop
e: E
a: A
f (e, a) -> exists a0 : A, f (e, a0) /\ a0 = a intros H.
E, A: Type
f: E * A -> Prop
e: E
a: A
H: f (e, a)
exists a0 : A, f (e, a0) /\ a0 = a exists a.
E, A: Type
f: E * A -> Prop
e: E
a: A
H: f (e, a)
f (e, a) /\ a = a intuition.
  Qed.

  Lemma kdf_subset_mapd2:
    forall (A B C: Type) (g: E * B -> C) (f: E * A -> B),
      mapd g ∘ mapd f = mapd (g ⋆1 f).
E: Type
forall (A B C : Type) (g : E * B -> C)
  (f : E * A -> B), mapd g ∘ mapd f = mapd (g ⋆1 f)
  Proof.
E: Type
forall (A B C : Type) (g : E * B -> C)
  (f : E * A -> B), mapd g ∘ mapd f = mapd (g ⋆1 f)
    intros.
E, A, B, C: Type
g: E * B -> C
f: E * A -> B
mapd g ∘ mapd f = mapd (g ⋆1 f) do 2 rewrite ctxset_mapd_spec.
E, A, B, C: Type
g: E * B -> C
f: E * A -> B
map (cobind g) ∘ map (cobind f) = mapd (g ⋆1 f)
    rewrite (fun_map_map (E * A) (E * B) (E * C) (F := subset)).
E, A, B, C: Type
g: E * B -> C
f: E * A -> B
map (cobind g ∘ cobind f) = mapd (g ⋆1 f)
    rewrite (kcom_cobind2).
E, A, B, C: Type
g: E * B -> C
f: E * A -> B
map (cobind (g ⋆1 f)) = mapd (g ⋆1 f)
    rewrite <- ctxset_mapd_spec.
E, A, B, C: Type
g: E * B -> C
f: E * A -> B
mapd (g ⋆1 f) = mapd (g ⋆1 f)
    reflexivity.
  Qed.

  (** ** Typeclass Instance *)
  (********************************************************************)
  #[export] Instance DecoratedTraversableFunctor_ctxset:
    DecoratedFunctor E (ctxset E) :=
    {| kdf_mapd1 := kdf_subset_mapd1;
       kdf_mapd2 := kdf_subset_mapd2;
    |}.

  #[export] Instance Compat_Map_Mapd_ctxset:
    `{Compat_Map_Mapd E (ctxset E)}.
E: Type
Compat_Map_Mapd E (ctxset E)
  Proof.
E: Type
Compat_Map_Mapd E (ctxset E)
    hnf.
E: Type
Map_ctxset = DerivedOperations.Map_Mapd E (ctxset E) ext A B f.
E, A, B: Type
f: A -> B
Map_ctxset A B f =
DerivedOperations.Map_Mapd E (ctxset E) A B f
    rewrite ctxset_map_to_mapd.
E, A, B: Type
f: A -> B
mapd (f ∘ extract) =
DerivedOperations.Map_Mapd E (ctxset E) A B f
    reflexivity.
  Qed.

  #[export] Instance Functor_ctxset:
    Functor (ctxset E) :=
    DerivedInstances.Functor_DecoratedFunctor E (ctxset E).

  (** * Monoid Instance *)
  (********************************************************************)
  Instance Monoid_op_ctxset {A: Type}: Monoid_op (ctxset E A) :=
    @Monoid_op_subset (E * A).

  Instance Monoid_unit_ctxset {A: Type}: Monoid_unit (ctxset E A) :=
    @Monoid_unit_subset (E * A).

  Instance Monoid_ctxset {A: Type}: Monoid (ctxset E A) :=
    @Monoid_subset (E * A).

  (** ** <<map>> and <<mapd>> are Homomorphisms *)
  (********************************************************************)
  #[export] Instance Monmor_ctxset_mapd: forall `(f: E * A -> B),
      Monoid_Morphism (ctxset E A) (ctxset E B) (mapd f).
E: Type
forall (A B : Type) (f : E * A -> B),
Monoid_Morphism (ctxset E A) (ctxset E B) (mapd f)
  Proof.
E: Type
forall (A B : Type) (f : E * A -> B),
Monoid_Morphism (ctxset E A) (ctxset E B) (mapd f)
    intros.
E, A, B: Type
f: E * A -> B
Monoid_Morphism (ctxset E A) (ctxset E B) (mapd f) unfold ctxset.
E, A, B: Type
f: E * A -> B
Monoid_Morphism (E * A -> Prop) (E * B -> Prop)
  (mapd f)
    rewrite ctxset_mapd_spec.
E, A, B: Type
f: E * A -> B
Monoid_Morphism (E * A -> Prop) (E * B -> Prop)
  (map (cobind f))
    typeclasses eauto.
  Qed.

  #[export] Instance map_ctxset_morphism: forall `(f: A -> B),
      Monoid_Morphism (ctxset E A) (ctxset E B) (map f).
E: Type
forall (A B : Type) (f : A -> B),
Monoid_Morphism (ctxset E A) (ctxset E B) (map f)
  Proof.
E: Type
forall (A B : Type) (f : A -> B),
Monoid_Morphism (ctxset E A) (ctxset E B) (map f)
    intros.
E, A, B: Type
f: A -> B
Monoid_Morphism (ctxset E A) (ctxset E B) (map f) unfold ctxset.
E, A, B: Type
f: A -> B
Monoid_Morphism (E * A -> Prop) (E * B -> Prop)
  (map f)
    rewrite ctxset_map_spec.
E, A, B: Type
f: A -> B
Monoid_Morphism (E * A -> Prop) (E * B -> Prop)
  (map (map f))
    typeclasses eauto.
  Qed.

End ctxset.

(** * The <<ctxset>> Monad (Kleisli) *)
(**********************************************************************)
Section ctxset.

  Context `{Monoid W}.

  (** ** Operations and Specifications *)
  (********************************************************************)
  #[export] Instance Return_ctxset: Return (ctxset W) :=
    fun A a '(w, b) => a = b /\ w = Ƶ.

  #[export] Instance Bindd_ctxset: Bindd W (ctxset W) (ctxset W) :=
    fun A B f s_a =>
      (fun '(w, b) => exists (wa: W) (a: A),
           s_a (wa, a) /\
             exists (wb: W), f (wa, a) (wb, b) /\ w = wa ● wb).

  #[export] Instance Bind_ctxset: Bind (ctxset W) (ctxset W) :=
    fun A B f s_a =>
      (fun '(w, b) => exists (wa: W) (a: A),
           s_a (wa, a) /\
             exists (wb: W), f a (wb, b) /\ w = wa ● wb).

  Lemma ctxset_ret_spec: forall (A: Type),
      ret (T := ctxset W) (A := A) =
        ret (T := subset) ∘ ret (T := (W ×)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall A : Type, η = η ∘ η
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall A : Type, η = η ∘ η
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
η = η ∘ η ext a.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
a: A
η a = (η ∘ η) a ext [w b].
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
a: A
w: W
b: A
η a (w, b) = (η ∘ η) a (w, b) propext.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
a: A
w: W
b: A
η a (w, b) -> (η ∘ η) a (w, b)
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
a: A
w: W
b: A
(η ∘ η) a (w, b) -> η a (w, b)
    -
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
a: A
w: W
b: A
η a (w, b) -> (η ∘ η) a (w, b) cbv.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
a: A
w: W
b: A
a = b /\ w = unit0 -> (unit0, a) = (w, b) now intuition subst.
    -
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
a: A
w: W
b: A
(η ∘ η) a (w, b) -> η a (w, b) cbv.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
a: A
w: W
b: A
(unit0, a) = (w, b) -> a = b /\ w = unit0 now inversion 1.
  Qed.

  Lemma ctxset_bindd_spec: forall (A B: Type) (f: W * A -> ctxset W B),
      bindd (T := ctxset W) f =
        bind (T := subset) (shift subset ∘ cobind (W := (W ×)) f).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (A B : Type) (f : W * A -> ctxset W B),
bindd f = bind (shift subset ∘ cobind f)
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (A B : Type) (f : W * A -> ctxset W B),
bindd f = bind (shift subset ∘ cobind f)
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
bindd f = bind (shift subset ∘ cobind f) ext s [w b].
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
s: ctxset W A
w: W
b: B
bindd f s (w, b) =
bind (shift subset ∘ cobind f) s (w, b) unfold shift.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
s: ctxset W A
w: W
b: B
bindd f s (w, b) =
bind (map (uncurry incr) ∘ strength ∘ cobind f) s
  (w, b)
    rewrite (map_strength_cobind_spec _ (G := subset)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
s: ctxset W A
w: W
b: B
bindd f s (w, b) =
bind
  (fun '(e, a) =>
   map (uncurry incr ∘ pair e) (f (e, a))) s (w, b)
    unfold_ops @Bind_subset @Bindd_ctxset @Map_subset.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
s: ctxset W A
w: W
b: B
(exists (wa : W) (a : A),
   s (wa, a) /\
   (exists wb : W, f (wa, a) (wb, b) /\ w = wa ● wb)) =
(exists a : W * A,
   s a /\
   (let
    '(e, a0) := a in
     fun b : W * B =>
     exists a1 : W * B,
       f (e, a0) a1 /\ (uncurry incr ∘ pair e) a1 = b)
     (w, b))
    propext.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
s: ctxset W A
w: W
b: B
(exists (wa : W) (a : A),
   s (wa, a) /\
   (exists wb : W, f (wa, a) (wb, b) /\ w = wa ● wb)) ->
exists a : W * A,
  s a /\
  (let
   '(e, a0) := a in
    fun b : W * B =>
    exists a1 : W * B,
      f (e, a0) a1 /\ (uncurry incr ∘ pair e) a1 = b)
    (w, b)
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
s: ctxset W A
w: W
b: B
(exists a : W * A,
   s a /\
   (let
    '(e, a0) := a in
     fun b : W * B =>
     exists a1 : W * B,
       f (e, a0) a1 /\ (uncurry incr ∘ pair e) a1 = b)
     (w, b)) ->
exists (wa : W) (a : A),
  s (wa, a) /\
  (exists wb : W, f (wa, a) (wb, b) /\ w = wa ● wb)
    -
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
s: ctxset W A
w: W
b: B
(exists (wa : W) (a : A),
   s (wa, a) /\
   (exists wb : W, f (wa, a) (wb, b) /\ w = wa ● wb)) ->
exists a : W * A,
  s a /\
  (let
   '(e, a0) := a in
    fun b : W * B =>
    exists a1 : W * B,
      f (e, a0) a1 /\ (uncurry incr ∘ pair e) a1 = b)
    (w, b) intros [wa [a [contra [w' [Hin Heq]]]]].
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
s: ctxset W A
w: W
b: B
wa: W
a: A
contra: s (wa, a)
w': W
Hin: f (wa, a) (w', b)
Heq: w = wa ● w'
exists a : W * A,
  s a /\
  (let
   '(e, a0) := a in
    fun b : W * B =>
    exists a1 : W * B,
      f (e, a0) a1 /\ (uncurry incr ∘ pair e) a1 = b)
    (w, b)
      subst.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
s: ctxset W A
b: B
wa: W
a: A
contra: s (wa, a)
w': W
Hin: f (wa, a) (w', b)
exists a : W * A,
  s a /\
  (let
   '(e, a0) := a in
    fun b : W * B =>
    exists a1 : W * B,
      f (e, a0) a1 /\ (uncurry incr ∘ pair e) a1 = b)
    (wa ● w', b) exists (wa, a).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
s: ctxset W A
b: B
wa: W
a: A
contra: s (wa, a)
w': W
Hin: f (wa, a) (w', b)
s (wa, a) /\
(exists a0 : W * B,
   f (wa, a) a0 /\
   (uncurry incr ∘ pair wa) a0 = (wa ● w', b)) split.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
s: ctxset W A
b: B
wa: W
a: A
contra: s (wa, a)
w': W
Hin: f (wa, a) (w', b)
s (wa, a)
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
s: ctxset W A
b: B
wa: W
a: A
contra: s (wa, a)
w': W
Hin: f (wa, a) (w', b)
exists a0 : W * B,
  f (wa, a) a0 /\
  (uncurry incr ∘ pair wa) a0 = (wa ● w', b)
      +
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
s: ctxset W A
b: B
wa: W
a: A
contra: s (wa, a)
w': W
Hin: f (wa, a) (w', b)
s (wa, a) assumption.
      +
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
s: ctxset W A
b: B
wa: W
a: A
contra: s (wa, a)
w': W
Hin: f (wa, a) (w', b)
exists a0 : W * B,
  f (wa, a) a0 /\
  (uncurry incr ∘ pair wa) a0 = (wa ● w', b) exists (w', b).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
s: ctxset W A
b: B
wa: W
a: A
contra: s (wa, a)
w': W
Hin: f (wa, a) (w', b)
f (wa, a) (w', b) /\
(uncurry incr ∘ pair wa) (w', b) = (wa ● w', b) easy.
    -
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
s: ctxset W A
w: W
b: B
(exists a : W * A,
   s a /\
   (let
    '(e, a0) := a in
     fun b : W * B =>
     exists a1 : W * B,
       f (e, a0) a1 /\ (uncurry incr ∘ pair e) a1 = b)
     (w, b)) ->
exists (wa : W) (a : A),
  s (wa, a) /\
  (exists wb : W, f (wa, a) (wb, b) /\ w = wa ● wb) intros [[wa a] [Hin [[wb b'] [Hin' Heq]]]].
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
s: ctxset W A
w: W
b: B
wa: W
a: A
Hin: s (wa, a)
wb: W
b': B
Hin': f (wa, a) (wb, b')
Heq: (uncurry incr ∘ pair wa) (wb, b') = (w, b)
exists (wa : W) (a : A),
  s (wa, a) /\
  (exists wb : W, f (wa, a) (wb, b) /\ w = wa ● wb)
      inversion Heq.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
s: ctxset W A
w: W
b: B
wa: W
a: A
Hin: s (wa, a)
wb: W
b': B
Hin': f (wa, a) (wb, b')
Heq: (uncurry incr ∘ pair wa) (wb, b') = (w, b)
H1: wa ● wb = w
H2: b' = b
exists (wa0 : W) (a : A),
  s (wa0, a) /\
  (exists wb0 : W,
     f (wa0, a) (wb0, b) /\ wa ● wb = wa0 ● wb0) subst.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
s: ctxset W A
b: B
wa: W
a: A
Hin: s (wa, a)
wb: W
Heq: (uncurry incr ∘ pair wa) (wb, b) = (wa ● wb, b)
Hin': f (wa, a) (wb, b)
exists (wa0 : W) (a : A),
  s (wa0, a) /\
  (exists wb0 : W,
     f (wa0, a) (wb0, b) /\ wa ● wb = wa0 ● wb0)
      exists wa a.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
s: ctxset W A
b: B
wa: W
a: A
Hin: s (wa, a)
wb: W
Heq: (uncurry incr ∘ pair wa) (wb, b) = (wa ● wb, b)
Hin': f (wa, a) (wb, b)
s (wa, a) /\
(exists wb0 : W,
   f (wa, a) (wb0, b) /\ wa ● wb = wa ● wb0) split.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
s: ctxset W A
b: B
wa: W
a: A
Hin: s (wa, a)
wb: W
Heq: (uncurry incr ∘ pair wa) (wb, b) = (wa ● wb, b)
Hin': f (wa, a) (wb, b)
s (wa, a)
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
s: ctxset W A
b: B
wa: W
a: A
Hin: s (wa, a)
wb: W
Heq: (uncurry incr ∘ pair wa) (wb, b) = (wa ● wb, b)
Hin': f (wa, a) (wb, b)
exists wb0 : W,
  f (wa, a) (wb0, b) /\ wa ● wb = wa ● wb0
      +
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
s: ctxset W A
b: B
wa: W
a: A
Hin: s (wa, a)
wb: W
Heq: (uncurry incr ∘ pair wa) (wb, b) = (wa ● wb, b)
Hin': f (wa, a) (wb, b)
s (wa, a) assumption.
      +
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
s: ctxset W A
b: B
wa: W
a: A
Hin: s (wa, a)
wb: W
Heq: (uncurry incr ∘ pair wa) (wb, b) = (wa ● wb, b)
Hin': f (wa, a) (wb, b)
exists wb0 : W,
  f (wa, a) (wb0, b) /\ wa ● wb = wa ● wb0 exists wb.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
s: ctxset W A
b: B
wa: W
a: A
Hin: s (wa, a)
wb: W
Heq: (uncurry incr ∘ pair wa) (wb, b) = (wa ● wb, b)
Hin': f (wa, a) (wb, b)
f (wa, a) (wb, b) /\ wa ● wb = wa ● wb easy.
  Qed.

  Lemma ctxset_bind_to_bindd: forall (A B: Type) (f: A -> ctxset W B),
      bind (T := ctxset W) f =
        bindd (T := ctxset W) (f ∘ extract).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (A B : Type) (f : A -> ctxset W B),
bind f = bindd (f ∘ extract)
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (A B : Type) (f : A -> ctxset W B),
bind f = bindd (f ∘ extract)
    reflexivity.
  Qed.

  Lemma ctxset_mapd_to_bindd: forall (A B: Type) (f: W * A -> B),
      mapd (T := ctxset W) f =
        bindd (T := ctxset W) (ret ∘ f).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (A B : Type) (f : W * A -> B),
mapd f = bindd (η ∘ f)
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (A B : Type) (f : W * A -> B),
mapd f = bindd (η ∘ f)
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
mapd f = bindd (η ∘ f)
    rewrite ctxset_mapd_spec.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
map (cobind f) = bindd (η ∘ f)
    rewrite ctxset_bindd_spec.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
map (cobind f) = bind (shift subset ∘ cobind (η ∘ f))
    rewrite Monad.map_to_bind.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
bind (η ∘ cobind f) =
bind (shift subset ∘ cobind (η ∘ f))
    fequal.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
η ∘ cobind f = shift subset ∘ cobind (η ∘ f)
    rewrite ctxset_ret_spec.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
η ∘ cobind f = shift subset ∘ cobind (η ∘ η ∘ f)
    unfold_ops @Return_subset @Return_Writer.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
(fun a b : W * B => a = b) ∘ cobind f =
shift subset
∘ cobind
    ((fun a b : W * B => a = b)
     ∘ (fun a : B => (Ƶ, a)) ∘ f)
    ext [w a] [w' b].
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
w: W
a: A
w': W
b: B
((fun a b : W * B => a = b) ∘ cobind f) (w, a) (w', b) =
(shift subset
 ∘ cobind
     ((fun a b : W * B => a = b)
      ∘ (fun a : B => (Ƶ, a)) ∘ f)) (w, a) (w', b) unfold shift, compose; cbn.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
w: W
a: A
w': W
b: B
((w, f (w, a)) = (w', b)) =
map (uncurry incr)
  (map (pair w) (fun b : W * B => (Ƶ, f (w, a)) = b))
  (w', b)
    unfold_ops @Map_subset; unfold uncurry.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
w: W
a: A
w': W
b: B
((w, f (w, a)) = (w', b)) =
(exists a0 : W * (W * B),
   (exists a1 : W * B,
      (Ƶ, f (w, a)) = a1 /\ (w, a1) = a0) /\
   (let '(x, y) := a0 in incr x y) = (w', b))
    propext.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
w: W
a: A
w': W
b: B
(w, f (w, a)) = (w', b) ->
exists a0 : W * (W * B),
  (exists a1 : W * B,
     (Ƶ, f (w, a)) = a1 /\ (w, a1) = a0) /\
  (let '(x, y) := a0 in incr x y) = (w', b)
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
w: W
a: A
w': W
b: B
(exists a0 : W * (W * B),
   (exists a1 : W * B,
      (Ƶ, f (w, a)) = a1 /\ (w, a1) = a0) /\
   (let '(x, y) := a0 in incr x y) = (w', b)) ->
(w, f (w, a)) = (w', b)
    -
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
w: W
a: A
w': W
b: B
(w, f (w, a)) = (w', b) ->
exists a0 : W * (W * B),
  (exists a1 : W * B,
     (Ƶ, f (w, a)) = a1 /\ (w, a1) = a0) /\
  (let '(x, y) := a0 in incr x y) = (w', b) inversion 1.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
w: W
a: A
w': W
b: B
H0: (w, f (w, a)) = (w', b)
H2: w = w'
H3: f (w', a) = b
exists a0 : W * (W * B),
  (exists a1 : W * B,
     (Ƶ, f (w', a)) = a1 /\ (w', a1) = a0) /\
  (let '(x, y) := a0 in incr x y) = (w', f (w', a)) subst.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
a: A
w': W
H0: (w', f (w', a)) = (w', f (w', a))
exists a0 : W * (W * B),
  (exists a1 : W * B,
     (Ƶ, f (w', a)) = a1 /\ (w', a1) = a0) /\
  (let '(x, y) := a0 in incr x y) = (w', f (w', a))
      exists (w', (Ƶ, f (w', a))).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
a: A
w': W
H0: (w', f (w', a)) = (w', f (w', a))
(exists a0 : W * B,
   (Ƶ, f (w', a)) = a0 /\
   (w', a0) = (w', (Ƶ, f (w', a)))) /\
incr w' (Ƶ, f (w', a)) = (w', f (w', a)) splits.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
a: A
w': W
H0: (w', f (w', a)) = (w', f (w', a))
exists a0 : W * B,
  (Ƶ, f (w', a)) = a0 /\
  (w', a0) = (w', (Ƶ, f (w', a)))
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
a: A
w': W
H0: (w', f (w', a)) = (w', f (w', a))
incr w' (Ƶ, f (w', a)) = (w', f (w', a))
      +
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
a: A
w': W
H0: (w', f (w', a)) = (w', f (w', a))
exists a0 : W * B,
  (Ƶ, f (w', a)) = a0 /\
  (w', a0) = (w', (Ƶ, f (w', a))) eauto.
      +
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
a: A
w': W
H0: (w', f (w', a)) = (w', f (w', a))
incr w' (Ƶ, f (w', a)) = (w', f (w', a)) cbn.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
a: A
w': W
H0: (w', f (w', a)) = (w', f (w', a))
(w' ● Ƶ, f (w', a)) = (w', f (w', a)) now simpl_monoid.
    -
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
w: W
a: A
w': W
b: B
(exists a0 : W * (W * B),
   (exists a1 : W * B,
      (Ƶ, f (w, a)) = a1 /\ (w, a1) = a0) /\
   (let '(x, y) := a0 in incr x y) = (w', b)) ->
(w, f (w, a)) = (w', b) intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
w: W
a: A
w': W
b: B
H0: exists a0 : W * (W * B),
  (exists a1 : W * B,
     (Ƶ, f (w, a)) = a1 /\ (w, a1) = a0) /\
  (let '(x, y) := a0 in incr x y) = (w', b)
(w, f (w, a)) = (w', b) preprocess.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
a: A
w0: W
(w0, f (w0, a)) = (w0 ● Ƶ, f (w0, a)) now simpl_monoid.
  Qed.

  Lemma ctxset_map_to_bindd: forall (A B: Type) (f: A -> B),
      map f = bindd (T := ctxset W) (ret ∘ f ∘ extract).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (A B : Type) (f : A -> B),
map f = bindd (η ∘ f ∘ extract)
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (A B : Type) (f : A -> B),
map f = bindd (η ∘ f ∘ extract)
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: A -> B
map f = bindd (η ∘ f ∘ extract)
    rewrite ctxset_map_to_mapd.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: A -> B
mapd (f ∘ extract) = bindd (η ∘ f ∘ extract)
    rewrite ctxset_mapd_to_bindd.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: A -> B
bindd (η ∘ (f ∘ extract)) = bindd (η ∘ f ∘ extract)
    reflexivity.
  Qed.

  Lemma ctxset_bind_spec: forall (A B: Type) (f: A -> ctxset W B),
      bind (T := ctxset W) f =
        bind (T := subset) (shift subset ∘ map (F := (W ×)) f).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (A B : Type) (f : A -> ctxset W B),
bind f = bind (shift subset ∘ map f)
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (A B : Type) (f : A -> ctxset W B),
bind f = bind (shift subset ∘ map f)
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: A -> ctxset W B
bind f = bind (shift subset ∘ map f)
    rewrite ctxset_bind_to_bindd.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: A -> ctxset W B
bindd (f ∘ extract) = bind (shift subset ∘ map f)
    rewrite ctxset_bindd_spec.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: A -> ctxset W B
bind (shift subset ∘ cobind (f ∘ extract)) =
bind (shift subset ∘ map f)
    rewrite map_to_cobind.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: A -> ctxset W B
bind (shift subset ∘ cobind (f ∘ extract)) =
bind (shift subset ∘ cobind (f ∘ extract))
    reflexivity.
  Qed.

  (** ** Compatibility Instances *)
  (********************************************************************)
  #[export] Instance Compat_Bind_Bindd_ctxset:
    Compat_Bind_Bindd W (ctxset W) (ctxset W).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Compat_Bind_Bindd W (ctxset W) (ctxset W)
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Compat_Bind_Bindd W (ctxset W) (ctxset W)
    reflexivity.
  Qed.

  #[export] Instance Compat_Map_Bindd_ctxset:
    Compat_Map_Bindd W (ctxset W) (ctxset W).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Compat_Map_Bindd W (ctxset W) (ctxset W)
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Compat_Map_Bindd W (ctxset W) (ctxset W)
    hnf.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Map_ctxset W =
DerivedOperations.Map_Bindd W (ctxset W) (ctxset W) ext A B f.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: A -> B
Map_ctxset W A B f =
DerivedOperations.Map_Bindd W (ctxset W) (ctxset W) A
  B f
    change_left (map f).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: A -> B
map f =
DerivedOperations.Map_Bindd W (ctxset W) (ctxset W) A
  B f
    rewrite ctxset_map_to_bindd.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: A -> B
bindd (η ∘ f ∘ extract) =
DerivedOperations.Map_Bindd W (ctxset W) (ctxset W) A
  B f
    reflexivity.
  Qed.

  #[export] Instance Compat_Mapd_Bindd_ctxset:
    Compat_Mapd_Bindd W (ctxset W) (ctxset W).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Compat_Mapd_Bindd W (ctxset W) (ctxset W)
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Compat_Mapd_Bindd W (ctxset W) (ctxset W)
    hnf.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
Mapd_ctxset W =
DerivedOperations.Mapd_Bindd W (ctxset W) (ctxset W) ext A B f.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
Mapd_ctxset W A B f =
DerivedOperations.Mapd_Bindd W (ctxset W) (ctxset W) A
  B f
    change_left (mapd f).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
mapd f =
DerivedOperations.Mapd_Bindd W (ctxset W) (ctxset W) A
  B f
    rewrite ctxset_mapd_to_bindd.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> B
bindd (η ∘ f) =
DerivedOperations.Mapd_Bindd W (ctxset W) (ctxset W) A
  B f
    reflexivity.
  Qed.

  (** ** Rewriting Laws *)
  (********************************************************************)
  Lemma bindd_ctxset_nil `{f: W * A -> ctxset W B}:
    bindd f (@subset_empty (W * A)) = @subset_empty (W * B).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
bindd f ∅ = ∅
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
bindd f ∅ = ∅
    ext [w b].
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
w: W
b: B
bindd f ∅ (w, b) = ∅ (w, b) cbn.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
w: W
b: B
(exists (wa : W) (a : A),
   ∅ (wa, a) /\
   (exists wb : W, f (wa, a) (wb, b) /\ w = wa ● wb)) =
∅ (w, b) propext.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
w: W
b: B
(exists (wa : W) (a : A),
   ∅ (wa, a) /\
   (exists wb : W, f (wa, a) (wb, b) /\ w = wa ● wb)) ->
∅ (w, b)
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
w: W
b: B
∅ (w, b) ->
exists (wa : W) (a : A),
  ∅ (wa, a) /\
  (exists wb : W, f (wa, a) (wb, b) /\ w = wa ● wb)
    -
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
w: W
b: B
(exists (wa : W) (a : A),
   ∅ (wa, a) /\
   (exists wb : W, f (wa, a) (wb, b) /\ w = wa ● wb)) ->
∅ (w, b) intros [wa [a [contra [w' [Hin Heq]]]]].
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
w: W
b: B
wa: W
a: A
contra: ∅ (wa, a)
w': W
Hin: f (wa, a) (w', b)
Heq: w = wa ● w'
∅ (w, b)
      inversion contra.
    -
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
w: W
b: B
∅ (w, b) ->
exists (wa : W) (a : A),
  ∅ (wa, a) /\
  (exists wb : W, f (wa, a) (wb, b) /\ w = wa ● wb) inversion 1.
  Qed.

  Lemma bindd_ctxset_one `{f: W * A -> ctxset W B} {w: W} {a: A}:
    bindd f {{ (w, a) }} = shift subset (w, f (w, a)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
w: W
a: A
bindd f {{(w, a)}} = shift subset (w, f (w, a))
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
w: W
a: A
bindd f {{(w, a)}} = shift subset (w, f (w, a))
    rewrite ctxset_bindd_spec.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
w: W
a: A
bind (shift subset ∘ cobind f) {{(w, a)}} =
shift subset (w, f (w, a))
    autorewrite with tea_set.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
w: W
a: A
(shift subset ∘ cobind f) (w, a) =
shift subset (w, f (w, a))
    reflexivity.
  Qed.

  Lemma bindd_ctxset_add `{f: W * A -> ctxset W B} {x y}:
      bindd f (x ∪ y: ctxset W A) = bindd f x ∪ bindd f y.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
x, y: W * A -> Prop
bindd f (x ∪ y : ctxset W A) = bindd f x ∪ bindd f y
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
x, y: W * A -> Prop
bindd f (x ∪ y : ctxset W A) = bindd f x ∪ bindd f y
    rewrite ctxset_bindd_spec.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
x, y: W * A -> Prop
bind (shift subset ∘ cobind f) (x ∪ y) =
bind (shift subset ∘ cobind f) x
∪ bind (shift subset ∘ cobind f) y
    now autorewrite with tea_set.
  Qed.

  #[local] Hint Rewrite
    @bindd_ctxset_nil @bindd_ctxset_one @bindd_ctxset_add
 : tea_set.

  (** ** Decorated Monad Laws *)
  (********************************************************************)
  Lemma ctxset_bindd0: forall (A B: Type) (f: W * A -> ctxset W B),
      bindd f ∘ ret = f ∘ pair Ƶ.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (A B : Type) (f : W * A -> ctxset W B),
bindd f ∘ η = f ∘ pair Ƶ
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (A B : Type) (f : W * A -> ctxset W B),
bindd f ∘ η = f ∘ pair Ƶ
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
bindd f ∘ η = f ∘ pair Ƶ ext a.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
a: A
(bindd f ∘ η) a = (f ∘ pair Ƶ) a
    rewrite ctxset_bindd_spec.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
a: A
(bind (shift subset ∘ cobind f) ∘ η) a =
(f ∘ pair Ƶ) a
    rewrite ctxset_ret_spec.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
a: A
(bind (shift subset ∘ cobind f) ∘ (η ∘ η)) a =
(f ∘ pair Ƶ) a
    unfold compose.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
a: A
bind (shift subset ○ cobind f) (η (η a)) = f (Ƶ, a)
    rewrite bind_set_one.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
a: A
shift subset (cobind f (η a)) = f (Ƶ, a)
    change (cobind f (η a)) with (Ƶ, f (Ƶ, a)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
a: A
shift subset (Ƶ, f (Ƶ, a)) = f (Ƶ, a)
    unfold ctxset. (* hidden *)
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
a: A
shift subset (Ƶ, f (Ƶ, a)) = f (Ƶ, a)
    rewrite (DecoratedMonad.shift_zero subset).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
a: A
f (Ƶ, a) = f (Ƶ, a)
    reflexivity.
  Qed.

  Lemma ctxset_bindd1: forall A: Type,
      bindd (T := ctxset W) (ret (T := ctxset W) ∘ extract) =
        @id (ctxset W A).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall A : Type, bindd (η ∘ extract) = id
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall A : Type, bindd (η ∘ extract) = id
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
bindd (η ∘ extract) = id
    rewrite ctxset_bindd_spec.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
bind (shift subset ∘ cobind (η ∘ extract)) = id
    rewrite <- map_to_cobind.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
bind (shift subset ∘ map (η)) = id
    replace (@id (ctxset W A))
      with (bind (U := subset) (T := subset) (@ret subset _ (W * A)))
      by (now rewrite kmon_bind1).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
bind (shift subset ∘ map (η)) = bind (η)
    fequal.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
shift subset ∘ map (η) = η unfold compose.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
shift subset ○ map (η) = η
    ext [w a].
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
w: W
a: A
shift subset (map (η) (w, a)) = η (w, a) cbn.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
w: W
a: A
shift subset (id w, η a) = η (w, a)
    change ((η ∘ extract) (w, a)) with (η a).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
w: W
a: A
shift subset (id w, η a) = η (w, a)
    rewrite ctxset_ret_spec.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
w: W
a: A
shift subset (id w, (η ∘ η) a) = η (w, a)
    change ((η ∘ η) a) with ({{ (Ƶ, a) }}).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
w: W
a: A
shift subset (id w, {{(Ƶ, a)}}) = η (w, a)
    unfold ctxset. (* hidden *)
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
w: W
a: A
shift subset (id w, {{(Ƶ, a)}}) = η (w, a)
    rewrite (DecoratedMonad.shift_spec subset).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
w: W
a: A
map (map_fst (fun m : W => id w ● m)) {{(Ƶ, a)}} =
η (w, a)
    autorewrite with tea_set.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
w: W
a: A
{{map_fst (fun m : W => id w ● m) (Ƶ, a)}} = η (w, a)
    cbn.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
w: W
a: A
{{(id w ● Ƶ, id a)}} = η (w, a) simpl_monoid.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
w: W
a: A
{{(id w, id a)}} = η (w, a)
    reflexivity.
  Qed.

  Lemma ctxset_bindd2_lemma:
    forall (A B C :Type) (g: W * B -> ctxset W C)
      (f: W * A -> ctxset W B),
      kc (T := subset) (shift subset ∘ cobind g)
        (shift subset ∘ cobind f) =
        shift subset ∘ cobind (g ⋆5 f).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (A B C : Type) (g : W * B -> ctxset W C)
  (f : W * A -> ctxset W B),
shift subset ∘ cobind g ⋆ shift subset ∘ cobind f =
shift subset ∘ cobind (g ⋆5 f)
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (A B C : Type) (g : W * B -> ctxset W C)
  (f : W * A -> ctxset W B),
shift subset ∘ cobind g ⋆ shift subset ∘ cobind f =
shift subset ∘ cobind (g ⋆5 f)
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
shift subset ∘ cobind g ⋆ shift subset ∘ cobind f =
shift subset ∘ cobind (g ⋆5 f) unfold kc, kc5.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
bind (shift subset ∘ cobind g)
∘ (shift subset ∘ cobind f) =
shift subset
∘ cobind (fun '(w, a) => bindd (g ⦿ w) (f (w, a)))
    ext [w a].
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
w: W
a: A
(bind (shift subset ∘ cobind g)
 ∘ (shift subset ∘ cobind f)) (w, a) =
(shift subset
 ∘ cobind (fun '(w, a) => bindd (g ⦿ w) (f (w, a))))
  (w, a)
    unfold compose at 1 3. (* LHS *)
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
w: W
a: A
bind (shift subset ∘ cobind g)
  (shift subset (cobind f (w, a))) =
(shift subset
 ∘ cobind (fun '(w, a) => bindd (g ⦿ w) (f (w, a))))
  (w, a)
    unfold compose at 2. (* RHS *)
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
w: W
a: A
bind (shift subset ∘ cobind g)
  (shift subset (cobind f (w, a))) =
shift subset
  (cobind (fun '(w, a) => bindd (g ⦿ w) (f (w, a)))
     (w, a))
    cbn.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
w: W
a: A
bind (shift subset ∘ cobind g)
  (shift subset (w, f (w, a))) =
shift subset (w, bindd (g ⦿ w) (f (w, a)))
    rewrite ctxset_bindd_spec.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
w: W
a: A
bind (shift subset ∘ cobind g)
  (shift subset (w, f (w, a))) =
shift subset
  (w, bind (shift subset ∘ cobind (g ⦿ w)) (f (w, a)))
    unfold ctxset.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
w: W
a: A
bind (shift subset ∘ cobind g)
  (shift subset (w, f (w, a))) =
shift subset
  (w, bind (shift subset ∘ cobind (g ⦿ w)) (f (w, a)))
    rewrite (DecoratedMonad.shift_spec subset).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
w: W
a: A
bind (shift subset ∘ cobind g)
  (map (map_fst (fun m : W => w ● m)) (f (w, a))) =
shift subset
  (w, bind (shift subset ∘ cobind (g ⦿ w)) (f (w, a)))
    rewrite (DecoratedMonad.shift_spec subset).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
w: W
a: A
bind (shift subset ∘ cobind g)
  (map (map_fst (fun m : W => w ● m)) (f (w, a))) =
map (map_fst (fun m : W => w ● m))
  (bind (shift subset ∘ cobind (g ⦿ w)) (f (w, a)))
    compose near (f (w, a)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
w: W
a: A
(bind (shift subset ∘ cobind g)
 ∘ map (map_fst (fun m : W => w ● m))) (f (w, a)) =
(map (map_fst (fun m : W => w ● m))
 ∘ bind (shift subset ∘ cobind (g ⦿ w))) (f (w, a))
    rewrite (bind_map (U := subset)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
w: W
a: A
bind
  (shift subset ∘ cobind g
   ∘ map_fst (fun m : W => w ● m)) (f (w, a)) =
(map (map_fst (fun m : W => w ● m))
 ∘ bind (shift subset ∘ cobind (g ⦿ w))) (f (w, a))
    rewrite (map_bind (U := subset)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
w: W
a: A
bind
  (shift subset ∘ cobind g
   ∘ map_fst (fun m : W => w ● m)) (f (w, a)) =
bind
  (map (map_fst (fun m : W => w ● m))
   ∘ (shift subset ∘ cobind (g ⦿ w))) (f (w, a))
    fequal.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
w: W
a: A
shift subset ∘ cobind g ∘ map_fst (fun m : W => w ● m) =
map (map_fst (fun m : W => w ● m))
∘ (shift subset ∘ cobind (g ⦿ w)) ext [w' b].
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
w: W
a: A
w': W
b: B
(shift subset ∘ cobind g
 ∘ map_fst (fun m : W => w ● m)) (w', b) =
(map (map_fst (fun m : W => w ● m))
 ∘ (shift subset ∘ cobind (g ⦿ w))) (w', b)
    unfold shift.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
w: W
a: A
w': W
b: B
(map (uncurry incr) ∘ strength ∘ cobind g
 ∘ map_fst (fun m : W => w ● m)) (w', b) =
(map (map_fst (fun m : W => w ● m))
 ∘ (map (uncurry incr) ∘ strength ∘ cobind (g ⦿ w)))
  (w', b)
    do 2 reassociate <- on right.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
w: W
a: A
w': W
b: B
(map (uncurry incr) ∘ strength ∘ cobind g
 ∘ map_fst (fun m : W => w ● m)) (w', b) =
(map (map_fst (fun m : W => w ● m))
 ∘ map (uncurry incr) ∘ strength ∘ cobind (g ⦿ w))
  (w', b)
    rewrite (fun_map_map (F:= subset)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
w: W
a: A
w': W
b: B
(map (uncurry incr) ∘ strength ∘ cobind g
 ∘ map_fst (fun m : W => w ● m)) (w', b) =
(map (map_fst (fun m : W => w ● m) ∘ uncurry incr)
 ∘ strength ∘ cobind (g ⦿ w)) (w', b)
    rewrite (map_strength_cobind_spec W B (G := subset)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
w: W
a: A
w': W
b: B
((fun '(e, a) =>
  map (uncurry incr ∘ pair e) (g (e, a)))
 ∘ map_fst (fun m : W => w ● m)) (w', b) =
(map (map_fst (fun m : W => w ● m) ∘ uncurry incr)
 ∘ strength ∘ cobind (g ⦿ w)) (w', b)
    rewrite (map_strength_cobind_spec W B (G := subset)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
w: W
a: A
w': W
b: B
((fun '(e, a) =>
  map (uncurry incr ∘ pair e) (g (e, a)))
 ∘ map_fst (fun m : W => w ● m)) (w', b) =
map
  (map_fst (fun m : W => w ● m) ∘ uncurry incr
   ∘ pair w') ((g ⦿ w) (w', b))
    unfold preincr, compose.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
w: W
a: A
w': W
b: B
(let
 '(e, a) := map_fst (fun m : W => w ● m) (w', b) in
  map (uncurry incr ○ pair e) (g (e, a))) =
map
  (fun a : W * C =>
   map_fst (fun m : W => w ● m) (uncurry incr (w', a)))
  (g (incr w (w', b))) cbn.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
w: W
a: A
w': W
b: B
map (fun a : W * C => incr (w ● w') a)
  (g (w ● w', id b)) =
map (map_fst (fun m : W => w ● m) ○ incr w')
  (g (w ● w', b))
    fequal.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
w: W
a: A
w': W
b: B
(fun a : W * C => incr (w ● w') a) =
map_fst (fun m : W => w ● m) ○ incr w' ext [w'' c].
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
w: W
a: A
w': W
b: B
w'': W
c: C
incr (w ● w') (w'', c) =
map_fst (fun m : W => w ● m) (incr w' (w'', c))
    cbn.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
w: W
a: A
w': W
b: B
w'': W
c: C
((w ● w') ● w'', c) = (w ● (w' ● w''), id c) simpl_monoid.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
w: W
a: A
w': W
b: B
w'': W
c: C
(w ● (w' ● w''), c) = (w ● (w' ● w''), id c)
    reflexivity.
  Qed.

  Lemma ctxset_bindd2:
    forall (A B C: Type)
      (g: W * B -> ctxset W C) (f: W * A -> ctxset W B),
      bindd g ∘ bindd f = bindd (g ⋆5 f).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (A B C : Type) (g : W * B -> ctxset W C)
  (f : W * A -> ctxset W B),
bindd g ∘ bindd f = bindd (g ⋆5 f)
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
forall (A B C : Type) (g : W * B -> ctxset W C)
  (f : W * A -> ctxset W B),
bindd g ∘ bindd f = bindd (g ⋆5 f)
    intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
bindd g ∘ bindd f = bindd (g ⋆5 f)
    do 3 rewrite ctxset_bindd_spec.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
bind (shift subset ∘ cobind g)
∘ bind (shift subset ∘ cobind f) =
bind (shift subset ∘ cobind (g ⋆5 f))
    unfold ctxset. (*hidden*)
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
bind (shift subset ∘ cobind g)
∘ bind (shift subset ∘ cobind f) =
bind (shift subset ∘ cobind (g ⋆5 f))
    rewrite (kmon_bind2 (T := subset)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
bind
  (shift subset ∘ cobind g ⋆ shift subset ∘ cobind f) =
bind (shift subset ∘ cobind (g ⋆5 f))
    rewrite ctxset_bindd2_lemma.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B, C: Type
g: W * B -> ctxset W C
f: W * A -> ctxset W B
bind (shift subset ∘ cobind (g ⋆5 f)) =
bind (shift subset ∘ cobind (g ⋆5 f))
    reflexivity.
  Qed.

  (** ** Typeclass Instances *)
  (********************************************************************)
  #[export] Instance DecoratedRightPreModule_ctxset:
    DecoratedRightPreModule W (ctxset W) (ctxset W) :=
    {| kdmod_bindd1 := ctxset_bindd1;
       kdmod_bindd2 := ctxset_bindd2;
    |}.

  #[export] Instance DecoratedMonad_ctxset:
    DecoratedMonad W (ctxset W) :=
    {| kdm_bindd0 := ctxset_bindd0;
    |}.

  #[export] Instance DecoratedRightModule_ctxset:
    DecoratedRightModule W (ctxset W) (ctxset W) :=
    {| kdmod_monad := _
    |}.

  (** ** <<bind>> is a Monoid Homomorphism *)
  (********************************************************************)
  #[export] Instance Monmor_ctxset_bindd {A B f}:
    Monoid_Morphism (ctxset W A) (ctxset W B) (bindd f).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
Monoid_Morphism (ctxset W A) (ctxset W B) (bindd f)
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
Monoid_Morphism (ctxset W A) (ctxset W B) (bindd f)
    constructor.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
Monoid (ctxset W A)
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
Monoid (ctxset W B)
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
bindd f Ƶ = Ƶ
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
forall a1 a2 : ctxset W A,
bindd f (a1 ● a2) = bindd f a1 ● bindd f a2
    -
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
Monoid (ctxset W A) typeclasses eauto.
    -
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
Monoid (ctxset W B) typeclasses eauto.
    -
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
bindd f Ƶ = Ƶ now rewrite bindd_ctxset_nil.
    -
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
forall a1 a2 : ctxset W A,
bindd f (a1 ● a2) = bindd f a1 ● bindd f a2 intros.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A, B: Type
f: W * A -> ctxset W B
a1, a2: ctxset W A
bindd f (a1 ● a2) = bindd f a1 ● bindd f a2 apply bindd_ctxset_add.
  Qed.

  (** ** Querying for an Element is a Monoid Homomorphism *)
  (********************************************************************)
  #[export] Instance Monmor_ctxset_evalAt {A: Type} (w: W) (a: A):
    @Monoid_Morphism (ctxset W A) Prop
      (@Monoid_op_subset (W * A))
      (@Monoid_unit_subset (W * A))
      (Monoid_op_or) (Monoid_unit_false)
      (evalAt (w, a)).
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
w: W
a: A
Monoid_Morphism (ctxset W A) Prop (evalAt (w, a))
  Proof.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
w: W
a: A
Monoid_Morphism (ctxset W A) Prop (evalAt (w, a))
    constructor.
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
w: W
a: A
Monoid (ctxset W A)
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
w: W
a: A
Monoid Prop
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
w: W
a: A
evalAt (w, a) Ƶ = Ƶ
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
w: W
a: A
forall a1 a2 : ctxset W A,
evalAt (w, a) (a1 ● a2) =
evalAt (w, a) a1 ● evalAt (w, a) a2
    -
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
w: W
a: A
Monoid (ctxset W A) typeclasses eauto.
    -
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
w: W
a: A
Monoid Prop typeclasses eauto.
    -
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
w: W
a: A
evalAt (w, a) Ƶ = Ƶ reflexivity.
    -
W: Type
op: Monoid_op W
unit0: Monoid_unit W
H: Monoid W
A: Type
w: W
a: A
forall a1 a2 : ctxset W A,
evalAt (w, a) (a1 ● a2) =
evalAt (w, a) a1 ● evalAt (w, a) a2 reflexivity.
  Qed.

End ctxset.