From Tealeaves Require Export
  Classes.Monoid
  Classes.Categorical.Applicative
  Tactics.Debug.

Import Monoid.Notations.

#[local] Generalizable Variables W M N ϕ.

#[local] Arguments map F%function_scope {Map}
  {A B}%type_scope f%function_scope _.

(** * Inductive Definition of the Constant Functor *)
(**********************************************************************)
Inductive Const V (tag: Type): Type :=
| mkConst: V -> Const V tag.

Arguments mkConst {V tag}%type_scope v: rename.

Definition unconst {V tag}: Const V tag -> V :=
  fun '(mkConst c) => c.

Lemma unconst_mkConst {V A}:
  forall (v: V), unconst (mkConst (tag := A) v) = v.
V, A: Type
forall v : V, unconst (mkConst v) = v
Proof.
V, A: Type
forall v : V, unconst (mkConst v) = v
  now intros.
Qed.

Lemma mkConst_unconst {V A}:
  forall (x: @Const V A), mkConst (unconst x) = x.
V, A: Type
forall x : Const V A, mkConst (unconst x) = x
Proof.
V, A: Type
forall x : Const V A, mkConst (unconst x) = x
  now intros [?].
Qed.

Definition retag {V A B}: Const V A -> Const V B :=
  mkConst ∘ unconst.

#[global] Instance Map_Const {V}: Map (Const V) :=
  fun A B f x => mkConst (unconst x).

#[global, program] Instance End_Const {V}: Functor (Const V).

Solve All Obligations with
  (intros; now ext [?]).

#[local] Hint Immediate unconst_mkConst mkConst_unconst: tea_applicative.

#[global] Hint Rewrite (@unconst_mkConst)
  (@mkConst_unconst): tea_applicative.

Lemma map_Const_1: forall V (A B: Type) (f: A -> B) (x: Const V A),
    unconst (map (Const V) f x) = unconst x.
forall (V A B : Type) (f : A -> B) (x : Const V A),
unconst (map (Const V) f x) = unconst x
Proof.
forall (V A B : Type) (f : A -> B) (x : Const V A),
unconst (map (Const V) f x) = unconst x
  introv.
V, A, B: Type
f: A -> B
x: Const V A
unconst (map (Const V) f x) = unconst x now destruct x.
Qed.

Definition mapConst {A B} (f: A -> B) {C}: Const A C -> Const B C :=
  fun '(mkConst a) => mkConst (f a).

Theorem mapConst_1 {A B} (f: A -> B) {C} (x: Const A C):
  f (unconst x) = unconst (mapConst f x).
A, B: Type
f: A -> B
C: Type
x: Const A C
f (unconst x) = unconst (mapConst f x)
Proof.
A, B: Type
f: A -> B
C: Type
x: Const A C
f (unconst x) = unconst (mapConst f x)
  destruct x; cbn.
A, B: Type
f: A -> B
C: Type
a: A
f a = f a reflexivity.
Qed.

Theorem mapConst_2 {A B} (f: A -> B) {C}:
  f ∘ unconst (tag := C) = unconst ∘ mapConst f.
A, B: Type
f: A -> B
C: Type
f ∘ unconst = unconst ∘ mapConst f
Proof.
A, B: Type
f: A -> B
C: Type
f ∘ unconst = unconst ∘ mapConst f
  ext [?].
A, B: Type
f: A -> B
C: Type
a: A
(f ∘ unconst) (mkConst a) =
(unconst ∘ mapConst f) (mkConst a) cbn.
A, B: Type
f: A -> B
C: Type
a: A
(f ∘ unconst) (mkConst a) = f a apply mapConst_1.
Qed.

(** ** Monoids as Constant Applicative Functors *)
(**********************************************************************)
Section const_ops.

  Context
    `{Monoid M}.

  #[global] Instance Pure_Const: Pure (Const M) :=
    fun (A: Type) (a: A) => mkConst (tag := A) Ƶ.

  #[global] Instance Mult_Const: Mult (Const M) :=
    fun A B (p: Const M A * Const M B) =>
      mkConst (tag := A * B) (unconst (fst p) ● unconst (snd p)).

  #[global, program] Instance Applicative_Const `{Monoid M}:
    Applicative (Const M).

  Solve Obligations with
    (intros; unfold transparent tcs in *; cbn; simpl_monoid;
     now auto with tea_applicative).

End const_ops.

#[global] Instance ApplicativeMorphism_Monoid_Morphism
  `(f: M1 -> M2) `{Monoid M1} `{Monoid M2} `{! Monoid_Morphism M1 M2 f}:
  ApplicativeMorphism (Const M1) (Const M2) (@mapConst M1 M2 f).
M1, M2: Type
f: M1 -> M2
op: Monoid_op M1
unit0: Monoid_unit M1
H: Monoid M1
op0: Monoid_op M2
unit1: Monoid_unit M2
H0: Monoid M2
Monoid_Morphism0: Monoid_Morphism M1 M2 f
ApplicativeMorphism (Const M1) (Const M2)
  (@mapConst M1 M2 f)
Proof.
M1, M2: Type
f: M1 -> M2
op: Monoid_op M1
unit0: Monoid_unit M1
H: Monoid M1
op0: Monoid_op M2
unit1: Monoid_unit M2
H0: Monoid M2
Monoid_Morphism0: Monoid_Morphism M1 M2 f
ApplicativeMorphism (Const M1) (Const M2)
  (@mapConst M1 M2 f)
  match goal with H: Monoid_Morphism _ _ f |- _ => inversion H end.
M1, M2: Type
f: M1 -> M2
op: Monoid_op M1
unit0: Monoid_unit M1
H: Monoid M1
op0: Monoid_op M2
unit1: Monoid_unit M2
H0: Monoid M2
Monoid_Morphism0: Monoid_Morphism M1 M2 f
monmor_src: Monoid M1
monmor_tgt: Monoid M2
monmor_unit: f Ƶ = Ƶ
monmor_op: forall a1 a2 : M1,
f (a1 ● a2) = f a1 ● f a2
ApplicativeMorphism (Const M1) (Const M2)
  (@mapConst M1 M2 f)
  constructor; try typeclasses eauto.
M1, M2: Type
f: M1 -> M2
op: Monoid_op M1
unit0: Monoid_unit M1
H: Monoid M1
op0: Monoid_op M2
unit1: Monoid_unit M2
H0: Monoid M2
Monoid_Morphism0: Monoid_Morphism M1 M2 f
monmor_src: Monoid M1
monmor_tgt: Monoid M2
monmor_unit: f Ƶ = Ƶ
monmor_op: forall a1 a2 : M1,
f (a1 ● a2) = f a1 ● f a2
forall (A B : Type) (f0 : A -> B) (x : Const M1 A),
mapConst f (map (Const M1) f0 x) =
map (Const M2) f0 (mapConst f x)
M1, M2: Type
f: M1 -> M2
op: Monoid_op M1
unit0: Monoid_unit M1
H: Monoid M1
op0: Monoid_op M2
unit1: Monoid_unit M2
H0: Monoid M2
Monoid_Morphism0: Monoid_Morphism M1 M2 f
monmor_src: Monoid M1
monmor_tgt: Monoid M2
monmor_unit: f Ƶ = Ƶ
monmor_op: forall a1 a2 : M1,
f (a1 ● a2) = f a1 ● f a2
forall (A : Type) (a : A),
mapConst f (pure a) = pure a
M1, M2: Type
f: M1 -> M2
op: Monoid_op M1
unit0: Monoid_unit M1
H: Monoid M1
op0: Monoid_op M2
unit1: Monoid_unit M2
H0: Monoid M2
Monoid_Morphism0: Monoid_Morphism M1 M2 f
monmor_src: Monoid M1
monmor_tgt: Monoid M2
monmor_unit: f Ƶ = Ƶ
monmor_op: forall a1 a2 : M1,
f (a1 ● a2) = f a1 ● f a2
forall (A B : Type) (x : Const M1 A) (y : Const M1 B),
mapConst f (mult (x, y)) =
mult (mapConst f x, mapConst f y)
  -
M1, M2: Type
f: M1 -> M2
op: Monoid_op M1
unit0: Monoid_unit M1
H: Monoid M1
op0: Monoid_op M2
unit1: Monoid_unit M2
H0: Monoid M2
Monoid_Morphism0: Monoid_Morphism M1 M2 f
monmor_src: Monoid M1
monmor_tgt: Monoid M2
monmor_unit: f Ƶ = Ƶ
monmor_op: forall a1 a2 : M1,
f (a1 ● a2) = f a1 ● f a2
forall (A B : Type) (f0 : A -> B) (x : Const M1 A),
mapConst f (map (Const M1) f0 x) =
map (Const M2) f0 (mapConst f x) introv.
M1, M2: Type
f: M1 -> M2
op: Monoid_op M1
unit0: Monoid_unit M1
H: Monoid M1
op0: Monoid_op M2
unit1: Monoid_unit M2
H0: Monoid M2
Monoid_Morphism0: Monoid_Morphism M1 M2 f
monmor_src: Monoid M1
monmor_tgt: Monoid M2
monmor_unit: f Ƶ = Ƶ
monmor_op: forall a1 a2 : M1,
f (a1 ● a2) = f a1 ● f a2
A, B: Type
f0: A -> B
x: Const M1 A
mapConst f (map (Const M1) f0 x) =
map (Const M2) f0 (mapConst f x) destruct x.
M1, M2: Type
f: M1 -> M2
op: Monoid_op M1
unit0: Monoid_unit M1
H: Monoid M1
op0: Monoid_op M2
unit1: Monoid_unit M2
H0: Monoid M2
Monoid_Morphism0: Monoid_Morphism M1 M2 f
monmor_src: Monoid M1
monmor_tgt: Monoid M2
monmor_unit: f Ƶ = Ƶ
monmor_op: forall a1 a2 : M1,
f (a1 ● a2) = f a1 ● f a2
A, B: Type
f0: A -> B
m: M1
mapConst f (map (Const M1) f0 (mkConst m)) =
map (Const M2) f0 (mapConst f (mkConst m)) reflexivity.
  -
M1, M2: Type
f: M1 -> M2
op: Monoid_op M1
unit0: Monoid_unit M1
H: Monoid M1
op0: Monoid_op M2
unit1: Monoid_unit M2
H0: Monoid M2
Monoid_Morphism0: Monoid_Morphism M1 M2 f
monmor_src: Monoid M1
monmor_tgt: Monoid M2
monmor_unit: f Ƶ = Ƶ
monmor_op: forall a1 a2 : M1,
f (a1 ● a2) = f a1 ● f a2
forall (A : Type) (a : A),
mapConst f (pure a) = pure a intros.
M1, M2: Type
f: M1 -> M2
op: Monoid_op M1
unit0: Monoid_unit M1
H: Monoid M1
op0: Monoid_op M2
unit1: Monoid_unit M2
H0: Monoid M2
Monoid_Morphism0: Monoid_Morphism M1 M2 f
monmor_src: Monoid M1
monmor_tgt: Monoid M2
monmor_unit: f Ƶ = Ƶ
monmor_op: forall a1 a2 : M1,
f (a1 ● a2) = f a1 ● f a2
A: Type
a: A
mapConst f (pure a) = pure a cbn.
M1, M2: Type
f: M1 -> M2
op: Monoid_op M1
unit0: Monoid_unit M1
H: Monoid M1
op0: Monoid_op M2
unit1: Monoid_unit M2
H0: Monoid M2
Monoid_Morphism0: Monoid_Morphism M1 M2 f
monmor_src: Monoid M1
monmor_tgt: Monoid M2
monmor_unit: f Ƶ = Ƶ
monmor_op: forall a1 a2 : M1,
f (a1 ● a2) = f a1 ● f a2
A: Type
a: A
mkConst (f Ƶ) = pure a rewrite monmor_unit.
M1, M2: Type
f: M1 -> M2
op: Monoid_op M1
unit0: Monoid_unit M1
H: Monoid M1
op0: Monoid_op M2
unit1: Monoid_unit M2
H0: Monoid M2
Monoid_Morphism0: Monoid_Morphism M1 M2 f
monmor_src: Monoid M1
monmor_tgt: Monoid M2
monmor_unit: f Ƶ = Ƶ
monmor_op: forall a1 a2 : M1,
f (a1 ● a2) = f a1 ● f a2
A: Type
a: A
mkConst Ƶ = pure a reflexivity.
  -
M1, M2: Type
f: M1 -> M2
op: Monoid_op M1
unit0: Monoid_unit M1
H: Monoid M1
op0: Monoid_op M2
unit1: Monoid_unit M2
H0: Monoid M2
Monoid_Morphism0: Monoid_Morphism M1 M2 f
monmor_src: Monoid M1
monmor_tgt: Monoid M2
monmor_unit: f Ƶ = Ƶ
monmor_op: forall a1 a2 : M1,
f (a1 ● a2) = f a1 ● f a2
forall (A B : Type) (x : Const M1 A) (y : Const M1 B),
mapConst f (mult (x, y)) =
mult (mapConst f x, mapConst f y) intros.
M1, M2: Type
f: M1 -> M2
op: Monoid_op M1
unit0: Monoid_unit M1
H: Monoid M1
op0: Monoid_op M2
unit1: Monoid_unit M2
H0: Monoid M2
Monoid_Morphism0: Monoid_Morphism M1 M2 f
monmor_src: Monoid M1
monmor_tgt: Monoid M2
monmor_unit: f Ƶ = Ƶ
monmor_op: forall a1 a2 : M1,
f (a1 ● a2) = f a1 ● f a2
A, B: Type
x: Const M1 A
y: Const M1 B
mapConst f (mult (x, y)) =
mult (mapConst f x, mapConst f y) destruct x, y.
M1, M2: Type
f: M1 -> M2
op: Monoid_op M1
unit0: Monoid_unit M1
H: Monoid M1
op0: Monoid_op M2
unit1: Monoid_unit M2
H0: Monoid M2
Monoid_Morphism0: Monoid_Morphism M1 M2 f
monmor_src: Monoid M1
monmor_tgt: Monoid M2
monmor_unit: f Ƶ = Ƶ
monmor_op: forall a1 a2 : M1,
f (a1 ● a2) = f a1 ● f a2
A, B: Type
m, m0: M1
mapConst f (mult (mkConst m, mkConst m0)) =
mult (mapConst f (mkConst m), mapConst f (mkConst m0)) cbn.
M1, M2: Type
f: M1 -> M2
op: Monoid_op M1
unit0: Monoid_unit M1
H: Monoid M1
op0: Monoid_op M2
unit1: Monoid_unit M2
H0: Monoid M2
Monoid_Morphism0: Monoid_Morphism M1 M2 f
monmor_src: Monoid M1
monmor_tgt: Monoid M2
monmor_unit: f Ƶ = Ƶ
monmor_op: forall a1 a2 : M1,
f (a1 ● a2) = f a1 ● f a2
A, B: Type
m, m0: M1
mkConst (f (m ● m0)) =
mult (mkConst (f m), mkConst (f m0)) rewrite monmor_op.
M1, M2: Type
f: M1 -> M2
op: Monoid_op M1
unit0: Monoid_unit M1
H: Monoid M1
op0: Monoid_op M2
unit1: Monoid_unit M2
H0: Monoid M2
Monoid_Morphism0: Monoid_Morphism M1 M2 f
monmor_src: Monoid M1
monmor_tgt: Monoid M2
monmor_unit: f Ƶ = Ƶ
monmor_op: forall a1 a2 : M1,
f (a1 ● a2) = f a1 ● f a2
A, B: Type
m, m0: M1
mkConst (f m ● f m0) =
mult (mkConst (f m), mkConst (f m0)) reflexivity.
Qed.

(** * Computational Definition of the Constant Functor *)
(**********************************************************************)
Section constant_functor.

  Definition retag_const {A X Y: Type}:
    const A X -> const A Y := @id A.

  (** First we establish that (const M) is an applicative functor. *)
  Section with_monoid.

    Context
      `{Monoid M}.

    #[global] Instance Map_const: Map (const M) :=
      fun X Y f t => t.

    Theorem map_const_spec: forall {X Y: Type} (f: X -> Y),
        map (const M) f = id.
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall (X Y : Type) (f : X -> Y), map (const M) f = id
    Proof.
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
forall (X Y : Type) (f : X -> Y), map (const M) f = id
      reflexivity.
    Qed.

    (** ** Monoids as Constant Applicative Functors *)
    (******************************************************************)
    #[global] Instance Pure_const: Pure (const M) :=
      fun X x => Ƶ.

    #[global] Instance Mult_const: Mult (const M) :=
      fun X Y '(x, y) => x ● y.

    #[global] Instance Applicative_const:
      Applicative (const M).
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
Applicative (const M)
    Proof.
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
Applicative (const M)
      constructor; intros; try reflexivity.
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
Functor (const M)
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A, B, C: Type
x: const M A
y: const M B
z: const M C
map (const M) associator (mult (mult (x, y), z)) =
mult (x, mult (y, z))
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
x: const M A
map (const M) left_unitor (mult (pure tt, x)) = x
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
x: const M A
map (const M) right_unitor (mult (x, pure tt)) = x
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A, B: Type
a: A
b: B
mult (pure a, pure b) = pure (a, b)
      -
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
Functor (const M) constructor; reflexivity.
      -
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A, B, C: Type
x: const M A
y: const M B
z: const M C
map (const M) associator (mult (mult (x, y), z)) =
mult (x, mult (y, z)) cbn.
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A, B, C: Type
x: const M A
y: const M B
z: const M C
(x ● y) ● z = x ● (y ● z) now Monoid.simpl_monoid.
      -
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
x: const M A
map (const M) left_unitor (mult (pure tt, x)) = x cbn.
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
x: const M A
pure tt ● x = x unfold_ops @Pure_const.
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
x: const M A
Ƶ ● x = x now Monoid.simpl_monoid.
      -
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
x: const M A
map (const M) right_unitor (mult (x, pure tt)) = x cbn.
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
x: const M A
x ● pure tt = x unfold_ops @Pure_const.
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A: Type
x: const M A
x ● Ƶ = x now Monoid.simpl_monoid.
      -
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A, B: Type
a: A
b: B
mult (pure a, pure b) = pure (a, b) cbn.
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A, B: Type
a: A
b: B
pure a ● pure b = pure (a, b) unfold_ops @Pure_const.
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
A, B: Type
a: A
b: B
Ƶ ● Ƶ = Ƶ now Monoid.simpl_monoid.
    Qed.

    #[global] Instance ApplicativeMorphism_unconst:
      ApplicativeMorphism (Const M) (const M)
        (fun X => unconst).
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
ApplicativeMorphism (Const M) (const M)
  (fun X : Type => unconst)
    Proof.
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
ApplicativeMorphism (Const M) (const M)
  (fun X : Type => unconst)
      constructor; try typeclasses eauto; reflexivity.
    Qed.

  End with_monoid.

  #[global] Instance ApplicativeMorphism_monoid_morphism
    `{Monoid M} `{Monoid N}
    `{hom: ! Monoid_Morphism M N ϕ }:
    ApplicativeMorphism (const M) (const N) (const ϕ).
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
N: Type
op0: Monoid_op N
unit1: Monoid_unit N
H0: Monoid N
ϕ: M -> N
hom: Monoid_Morphism M N ϕ
ApplicativeMorphism (const M) (const N) (const ϕ)
  Proof.
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
N: Type
op0: Monoid_op N
unit1: Monoid_unit N
H0: Monoid N
ϕ: M -> N
hom: Monoid_Morphism M N ϕ
ApplicativeMorphism (const M) (const N) (const ϕ)
    inversion hom.
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H: Monoid M
N: Type
op0: Monoid_op N
unit1: Monoid_unit N
H0: Monoid N
ϕ: M -> N
hom: Monoid_Morphism M N ϕ
monmor_src: Monoid M
monmor_tgt: Monoid N
monmor_unit: ϕ Ƶ = Ƶ
monmor_op: forall a1 a2 : M,
ϕ (a1 ● a2) = ϕ a1 ● ϕ a2
ApplicativeMorphism (const M) (const N) (const ϕ)
    constructor; now try typeclasses eauto.
  Qed.


  Lemma map_compose_const {F} `{Functor F} `{M: Type}:
    @Map_compose F (const M) _ _ = @Map_const (F M).
F: Type -> Type
Map_F: Map F
H: Functor F
M: Type
Map_compose F (const M) = Map_const
  Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
M: Type
Map_compose F (const M) = Map_const
    ext A' B' f' t.
F: Type -> Type
Map_F: Map F
H: Functor F
M, A', B': Type
f': A' -> B'
t: (F ∘ const M) A'
Map_compose F (const M) A' B' f' t =
Map_const A' B' f' t
    unfold_ops @Map_compose @Map_const.
F: Type -> Type
Map_F: Map F
H: Functor F
M, A', B': Type
f': A' -> B'
t: (F ∘ const M) A'
map F (fun t : const M A' => t) t = t
    rewrite fun_map_id.
F: Type -> Type
Map_F: Map F
H: Functor F
M, A', B': Type
f': A' -> B'
t: (F ∘ const M) A'
id t = t
    reflexivity.
  Qed.

  Lemma mult_compose_const {G} `{Applicative G} `{Monoid M}:
    @Mult_compose G (const M) _ _ _ =
      @Mult_const (G M) (Monoid_op_applicative G M).
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
Mult_compose G (const M) = Mult_const
  Proof.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
Mult_compose G (const M) = Mult_const
    ext A' B' [m1 m2].
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
M: Type
op: Monoid_op M
unit0: Monoid_unit M
H0: Monoid M
A', B': Type
m1: (G ∘ const M) A'
m2: (G ∘ const M) B'
Mult_compose G (const M) A' B' (m1, m2) =
Mult_const A' B' (m1, m2)
    reflexivity.
  Qed.

End constant_functor.


(** * Simplification Support *)
(**********************************************************************)

Lemma pure_const_rw: forall {A} {a:A} {M} {unit: Monoid_unit M},
    pure (F := const M) (Pure := @Pure_const _ unit) a = @monoid_unit M unit.
forall (A : Type) (a : A) (M : Type)
  (unit : Monoid_unit M), pure a = Ƶ
Proof.
forall (A : Type) (a : A) (M : Type)
  (unit : Monoid_unit M), pure a = Ƶ
  reflexivity.
Qed.

Lemma ap_const_rw:
  forall {M} `{op: Monoid_op M} {A B} (x: const M (A -> B)) (y: const M A),
    ap (const M) x y = (@monoid_op M op x y).
forall (M : Type) (op : Monoid_op M) (A B : Type)
  (x : const M (A -> B)) (y : const M A),
ap (const M) x y = x ● y
Proof.
forall (M : Type) (op : Monoid_op M) (A B : Type)
  (x : const M (A -> B)) (y : const M A),
ap (const M) x y = x ● y
  Set Printing All.
forall (M : Type) (op : Monoid_op M) (A B : Type)
  (x : @const Type Type M (forall _ : A, B))
  (y : @const Type Type M A),
@eq (@const Type Type M B)
  (@ap (@const Type Type M) (@Map_const M)
     (@Mult_const M op) A B x y) (@monoid_op M op x y)
  intros.
M: Type
op: Monoid_op M
A, B: Type
x: @const Type Type M (forall _ : A, B)
y: @const Type Type M A
@eq (@const Type Type M B)
  (@ap (@const Type Type M) (@Map_const M)
     (@Mult_const M op) A B x y) (@monoid_op M op x y)
  reflexivity.
Qed.

Lemma map_const_rw: forall A B (f: A -> B) X,
    map (const X) f = @id X.
forall (A B : Type) (f : forall _ : A, B) (X : Type),
@eq
  (forall _ : @const Type Type X A,
   @const Type Type X B)
  (@map (@const Type Type X) (@Map_const X) A B f)
  (@id X)
Proof.
forall (A B : Type) (f : forall _ : A, B) (X : Type),
@eq
  (forall _ : @const Type Type X A,
   @const Type Type X B)
  (@map (@const Type Type X) (@Map_const X) A B f)
  (@id X)
  reflexivity.
Qed.


(** ** Constant applicatives *)
(**********************************************************************)
Ltac simplify_applicative_const :=
  ltac_trace "simplify_applicative_const";
  match goal with
  | |- context [pure (F := const ?W) ?x] =>
      rewrite pure_const_rw
  | |- context[(ap (const ?W) ?x ?y)] =>
      rewrite ap_const_rw
  end.

Ltac simplify_applicative_const_in :=
  match goal with
  | H: context [pure (F := const ?W) ?x] |- _ =>
      rewrite pure_const_rw in H
  | H: context[(ap (const ?W) ?x ?y)] |- _ =>
      rewrite ap_const_rw in H
  end.

(** ** Constant maps *)
(**********************************************************************)
Ltac simplify_map_const :=
  ltac_trace "simplify_map_const";
  match goal with
  | |- context[map (const ?X) ?f] =>
      rewrite map_const_rw
  end.

Ltac simplify_map_const_in :=
  match goal with
  | H: context[map (const ?X) ?f] |- _ =>
      rewrite map_const_rw in H
  end.