There is no ZipList monad, proved in Coq; thread https://twitter.com/lysxia/status/1451202791796584454

NoZipListMonad.v

(** Coq proof that there is no monad compatible with the ZipList applicative functor. *)
(** Based on the original proof by Koji Miyazato https://gist.github.com/viercc/38853067c893f7ad9e0894abb543178b *)

(** Main theorem: [No_LawfulJoin : forall join, ~(LawfulJoin join)]
    where [~] means "not" and [LawfulJoin] is the conjunction of the following properties (monad laws):
 
    1. [join] is associative:
         join (join xs) = join (map join xs)]
 
    2. [join] is compatible with ZipList's applicative (i.e., [zip_with]):
         zip_with f xs ys = join (map (fun x => map (f x) ys) xs))%colist
 
    3. [join] preserves the canonical relations between its inputs and outputs:
         RColist (RColist r) xs ys -> RColist r (join xs) (join ys)
 
    Requirement (1) is one of the core monad laws.
    (2) corresponds to the monad law [(<*>) = ap] relating Monad and Applicative in Haskell.
    In other words, [m1 <*> m2 = m1 >>= (fun x1 -> m2 >>= (fun x2 -> return (x1 x2)))]
    where [return] is [repeat]
    (https://hackage.haskell.org/package/base-4.15.0.0/docs/Control-Monad.html#t:Monad).
    It implies the identity laws (as proved in [join_repeat] and [join_map_repeat], kinda).
    (3) is the parametricity assumption (so it holds for free for all values of join's type;
    or if you don't trust parametricity, you can just say that it's an extra monad law
    that should be satisfied by implementors).
 
    N.B.: The ZipList applicative functor consists of [zip_with] (as [liftA2]) and [repeat]
    (as [pure]).
*)

(** Core definitions

    - The type of coinductive lists: [Colist].

    - Main functions: [map], [zip_with], [repeat], [nats]

    - Membership: [In x xs] ("[x] is in the list [xs]")

    - Equivalence: [RColist], parameterized by an equivalence relation on
      elements (typically [eq] for simple elements, or [RColist _] for nested
      lists).

    - Minimal definition of a monad compatible with [zip_with]/[repeat]: [LawfulJoin]
*)

(** Proof, main steps
    See also the original for more details: https://gist.github.com/viercc/38853067c893f7ad9e0894abb543178b

    - We define a certain family of list of lists of lists
      [ex n : Colist (Colist (Colist (nat * nat)))]
      whose rows are given by a common function [q : nat -> Colist (Colist (nat * nat))].
      (All [ex n] are simple translations of [ex 0].)
    - The goal is to show the following contradictory facts:
        1. [join (join (tail (ex 0))]) is empty ([fact1]).
        2. [join (map join (tail (ex 0)))] is non-empty ([fact2]).
    - (1) follows by straightforward calculations.
    - It's (2) that's the hard part.
      + For all i, [join (join (ex i))] is an infinite list (the diagonal of [ex i]). ([map_join_ex])
      + From that we deduce that [join (q i)] is an infinite list, for all [i].
        * That step crucially relies on parametricity, which specifically implies: for all [xs],
          any element of [join xs] is an element of [xs]. ([In_join_inv])
        * We go through three characterizations of infinite lists ([l := join (q i)]):
          -- There is an infinite family of elements [f : nat -> x] all in the list [l] ([f := fun i => (i, i+m)]) ([fact0])
          -- The list [l] has no [Nil] ([Neverending_join_q])
          -- The list [l] is a [map] on [nats] ([map_lookupNE_join_q])
      + (2) then follows from that by equational reasoning.
 *)

From Coq Require Import Arith Setoid Morphisms Lia.

Set Primitive Projections.
Set Implicit Arguments.
Set Maximal Implicit Insertion.
Set Contextual Implicit.

Inductive ColistF (a : Type) (x : Type) :=
| Nil : ColistF a x
| Cons : a -> x -> ColistF a x
.

CoInductive Colist (a : Type) : Type :=
  Delay { force : ColistF a (Colist a) }.

Add Printing Constructor Colist.

Declare Scope colist_scope.
Delimit Scope colist_scope with colist.
Local Open Scope colist_scope.

Notation "'[' ']'" := Nil : colist_scope.
Notation "x :: xs" := (Cons x xs) : colist_scope.

CoFixpoint map {a b} (f : a -> b) (xs : Colist a) : Colist b := Delay
  match force xs with
  | [] => []
  | x :: xs => f x :: map f xs
  end.

CoFixpoint zip_with {a b c} (f : a -> b -> c) (xs : Colist a) (ys : Colist b) : Colist c := Delay
  match force xs, force ys with
  | x :: xs, y :: ys => f x y :: zip_with f xs ys
  | _, _ => []
  end.

CoFixpoint repeat {a} (x : a) : Colist a := Delay (x :: repeat x).

CoFixpoint nats_from (n : nat) : Colist nat := Delay
  (n :: nats_from (S n)).

Definition nats := nats_from 0.

Unset Elimination Schemes.

Inductive In {a : Type} (x : a) (xs : Colist a) : Prop :=
| In_split y ys : force xs = Cons y ys -> x = y \/ In x ys -> In x xs
.

Lemma In_ind (a : Type) (x : a) (P : Colist a -> Prop)
    (H : forall xs (y : a) (ys : Colist a),
         force xs = y :: ys -> x = y \/ (In x ys /\ P ys) -> P xs)
  : forall xs, In x xs -> P xs.
Proof.
  fix SELF 2; intros xs [].
  eapply H; eauto.
  destruct H1; [ left | right ]; auto.
Qed.

Lemma not_In_nil {a} (x : a) : ~ In x (Delay []).
Proof.
  intros []; discriminate.
Qed.
#[global] Hint Resolve not_In_nil : core.

Lemma not_In_nil_ {a} (x : a) xs : force xs = [] -> In x xs -> False.
Proof.
  intros ? []; congruence.
Qed.
#[global] Hint Resolve not_In_nil_ : core.

Inductive RColistF {a b} (r : a -> b -> Prop) xa xb (rx : xa -> xb -> Prop) : ColistF a xa -> ColistF b xb -> Prop :=
| RColist_Nil : RColistF r rx [] []
| RColist_Cons x xs y ys : r x y -> rx xs ys -> RColistF r rx (Cons x xs) (Cons y ys)
.

(* Note: Coinductive Props are dangerous if you're not familiar with Coq's termination checking rules,
   as you can get stuck with some incomprehensible errors.
   I live dangerously, but the paco library provides a safer framework if you're interested in doing
   similar things.
 *)
CoInductive RColist {a b} (r : a -> b -> Prop) (xs : Colist a) (ys : Colist b) : Prop :=
| RColist_force : RColistF r (RColist r) (force xs) (force ys) -> RColist r xs ys
.

Notation "x = y" := (RColist eq x y) : colist_scope.

Lemma RColist_nil {a b} (r : a -> b -> Prop) : RColist r (Delay []) (Delay []).
Proof.
  constructor; constructor 1; auto.
Qed.
#[global] Hint Resolve RColist_nil : core.

Lemma RColist_mon {a b} (r r' : a -> b -> Prop)
  : (forall x y, r x y -> r' x y) ->
    forall xs ys, RColist r xs ys -> RColist r' xs ys.
Proof.
  intros H; cofix SELF; intros ? ? [HH]; constructor; destruct HH; constructor; auto.
Qed.

Instance Equivalence_RColist {a} (r : a -> a -> Prop) `{!Equivalence r}
  : Equivalence (RColist r).
Proof.
  constructor.
  - red; cofix SELF; intros x; constructor; destruct (force x) eqn:Eforce; econstructor; [ reflexivity | auto ].
  - red; cofix SELF; intros ? ? [H]; constructor; destruct H; constructor; [ symmetry; auto | auto ].
  - red; cofix SELF; intros ? ? ? [H1] [H2]; constructor; destruct H1; inversion H2; constructor; [ etransitivity; eauto | eauto ].
Qed.

Notation pr := (pointwise_relation _).

Instance RColist_map {a b} (r : b -> b -> Prop)
  : Proper (pr r ==> RColist eq ==> RColist r) (map (a := a) (b := b)).
Proof.
  unfold Proper, respectful, pr. cofix SELF.
  intros f g Hf ? ? [H]; constructor; cbn; destruct H; constructor; subst; auto.
Qed.

Lemma RColist_repeat {a b} (r : a -> b -> Prop) x y
  : r x y -> RColist r (repeat x) (repeat y).
Proof.
  cofix SELF; constructor; cbn; constructor; auto.
Qed.

Instance RColist_repeat_ {a} (r : a -> a -> Prop) : Proper (r ==> RColist r) (repeat (a := a)).
Proof.
  unfold Proper, respectful. apply RColist_repeat.
Qed.

Lemma map_id {a} : forall (xs : Colist a), (map (fun x => x) xs = xs)%colist.
Proof.
  cofix SELF; intros xs; constructor; cbn; destruct (force _); constructor; auto.
Qed.

Lemma repeat_map {a} (x : a) : (repeat x = map (fun _ => x) nats)%colist.
Proof.
  unfold nats; generalize 0.
  cofix SELF; constructor; cbn; constructor; auto.
Qed.

Lemma zip_with_const {a c} (f : a -> c) (xs : Colist a)
  : (zip_with (fun x _ => f x) xs nats = map f xs)%colist.
Proof.
  unfold nats; generalize 0; revert xs; cofix SELF; constructor; cbn; destruct (force _); constructor; auto.
Qed.

Lemma zip_with_const_l {b c} (f : b -> c) (xs : Colist b)
  : (zip_with (fun _ y =>  f y) nats xs = map f xs)%colist.
Proof.
  unfold nats; generalize 0; revert xs; cofix SELF; constructor; cbn; destruct (force _); constructor; auto.
Qed.

Lemma zip_with_diag {a b} (f : a -> a -> b) (xs : Colist a)
  : (zip_with f xs xs = map (fun i => f i i) xs)%colist.
Proof.
  revert xs; cofix SELF; constructor; cbn; destruct (force _); constructor; auto.
Qed.

Lemma map_In {a b} (f : a -> b) x : forall xs, In x xs -> In (f x) (map f xs).
Proof.
  induction 1. destruct H0 as [ | []]; subst; econstructor; cbn; eauto.
  all: rewrite H; eauto.
Qed.

Lemma In_map {a b} (f : a -> b) y xs : In y (map f xs) -> exists x, y = f x /\ In x xs.
Proof.
  remember (map f xs) as ys eqn:Eys. intros H. revert xs Eys.
  induction H; intros ? ->; cbn in H. destruct H0 as [ | []]; subst.
  - destruct (force _) eqn:Eforce in H; try discriminate; inversion H.
    eexists; split; eauto. econstructor; eauto.
  - destruct (force _) eqn:Eforce in H; try discriminate.
    inversion H; subst; clear H.
    edestruct H1 as [? []]; eauto.
    eexists; split; eauto. econstructor; eauto.
Qed.

Lemma In_repeat {a} (x y : a) : In x (repeat y) -> x = y.
Proof.
  remember (repeat y) as ys; intros H; revert Heqys; induction H; intros ->; cbn in *; auto.
  destruct H0 as [ | []]. { inversion H; auto. } { inversion H; subst; auto. }
Qed.

Lemma In_nats_from i j : In (j + i) (nats_from j).
Proof.
  revert j; induction i; econstructor; cbn; eauto.
  right; rewrite Nat.add_succ_r. apply (IHi (S _)).
Qed.

Lemma In_nats i : In i nats.
Proof.
  apply (In_nats_from i 0).
Qed.

Lemma map_map {a b c} (f : a -> b) (g : b -> c) xs
  : (map g (map f xs) = map (fun i => g (f i)) xs)%colist.
Proof.
  revert xs; cofix SELF; intros; constructor; cbn; destruct (force _); constructor; auto.
Qed.

Instance eq_Colist_In {a}
  : Proper (eq ==> RColist eq ==> Basics.impl) (In (a := a)).
Proof.
  unfold Proper, respectful, Basics.impl; intros; subst.
  revert y0 H0. induction H1.
  intros ? []. inversion H1; try congruence; subst.
  destruct H0 as [ | [] ].
  - subst. rewrite H in H2; inversion H2; subst. econstructor; eauto.
  - econstructor; eauto. right; apply H4. congruence. 
Qed.

Class LawfulJoin (join : forall {a}, Colist (Colist a) -> Colist a) : Prop :=
  { join_join : forall a (xs : Colist (Colist (Colist a))), join (join xs) = join (map join xs)
  ; join_as_zip_with : forall {a b c} (f : a -> b -> c) (xs : Colist a) (ys : Colist b),
      (zip_with f xs ys = join (map (fun x => map (f x) ys) xs))%colist

    (* Should hold by parametricity *)
  ; RColist_join : forall a b (r : a -> b -> Prop) xs ys,
      RColist (RColist r) xs ys -> RColist r (join xs) (join ys)
  }.

(* Proof *)

Section Work.

Context join {LJ : LawfulJoin join}. 

Instance eq_Colist_join a : Proper (RColist eq ==> RColist eq) (join (a := a)).
Proof.
  unfold Proper, respectful.
  intros ? ? H. apply RColist_join. revert H; apply RColist_mon.
  intros ? ? []; reflexivity.
Qed.

Lemma In_join_inv {a} (x : a) : forall (xs : Colist (Colist a)),
  (In x (join xs) -> exists ys, In x ys /\ In ys xs)%colist.
Proof.
  intros xs.
  assert (H := RColist_join (r := fun x _ => exists ys, In x ys /\ In ys xs) (xs := xs) (ys := xs)).
  assert (J : forall zs, (forall x, In x zs -> In x xs) -> RColist (RColist (fun x _ => exists ys, In x ys /\ In ys xs)) zs zs).
  { cofix SELF; intros; constructor; destruct (force _) eqn:Hforce; constructor.
    - clear SELF.
      assert (JJ : forall us, (forall x, In x us -> In x c) -> RColist (fun x _ => exists ys, In x ys /\ In ys xs) us us).
      { cofix SELF; intros; constructor; destruct (force us) eqn:HHforce; constructor.
        + exists c. split; [ apply H1 | apply H0 ].
          { econstructor; eauto. }
          { econstructor; eauto. }
        + cbn; apply SELF; intros; apply H1; econstructor; eauto. }
      apply JJ. auto.
    - cbn; apply SELF; intros; apply H0; econstructor; eauto. }
  evar (p : Prop); assert (Wp : p); [ | specialize (H Wp) ]; subst p.
  { apply J; auto. }
  clear J Wp.
  intros H1. revert H; induction H1. destruct H0 as [<- | []].
  - intros []. rewrite H in H0. inversion H0; auto.
  - intros []. rewrite H in H2. inversion H2; auto.
Qed.

Lemma join_repeat {a} (xs : Colist a)
  : (join (repeat xs) = xs)%colist.
Proof.
  assert (RColist (RColist eq) (repeat xs) (map (fun _ => map (fun x => x) xs) nats)).
  { etransitivity; [ | eapply RColist_mon; [ intros ? _ <-; reflexivity | apply repeat_map ] ].
    rewrite map_id. reflexivity. }
  etransitivity; [ eapply RColist_join, H | ].
  rewrite <- join_as_zip_with, zip_with_const_l, map_id.
  reflexivity.
Qed.

Lemma join_diag {a b} (f : a -> a -> b) (xs : Colist a)
  : (join (map (fun i => map (f i) xs) xs) = map (fun i => f i i) xs)%colist.
Proof.
  rewrite <- join_as_zip_with. apply zip_with_diag.
Qed.

Lemma join_map_repeat {a b} (f : a -> b) (xs : Colist a)
  : (join (map (fun i => repeat (f i)) xs) = map f xs)%colist.
Proof.
  etransitivity.
  - eapply RColist_join.
    eapply RColist_map; [ | reflexivity ].
    intros ?. apply repeat_map.
  - rewrite <- join_as_zip_with.
    apply zip_with_const.
Qed.

Definition q (i : nat) : Colist (Colist (nat * nat)) :=
  map (fun j => if j <? i then Delay [] else repeat (i, j)) nats.

Definition ex m : Colist (Colist (Colist (nat * nat))) :=
  map (fun i => q (i - m)) nats.

Lemma join_join_ex m
  : (join (join (ex m)) = map (fun i => (i - m, i)) nats)%colist.
Proof.
  unfold ex, q. rewrite join_diag.
  assert (E : pr eq (fun i => if i <? i - m then Delay [] else repeat (i - m, i)) (fun i => repeat (i - m, i))).
  { intros i; rewrite (proj2 (Nat.ltb_ge _ _)); [ reflexivity | apply Nat.le_sub_l ]. }
  rewrite E. apply join_map_repeat.
Qed.

Lemma map_join_ex m
  : (map join (ex m) = map (fun i => join (q (i - m))) nats)%colist.
Proof.
  apply map_map.
Qed.

Lemma fact0_ i m : In (i-m, i) (join (q (i - m))).
Proof.
  assert (H := @In_nats i).
  apply map_In with (f := fun i => (i - m, i)) in H.
  rewrite <- join_join_ex, join_join, map_join_ex in H.
  apply In_join_inv in H.
  destruct H as [ys [Hi Hy]].
  apply In_map in Hy.
  destruct Hy as [j [-> _]].
  enough (HH : j - m = i - m).
  { rewrite HH in Hi; auto. }
  apply In_join_inv in Hi.
  destruct Hi as [zs [Hi Hz]].
  unfold q in Hz.
  apply In_map in Hz.
  destruct Hz as [jj [-> _]].
  destruct (Nat.ltb_spec jj (j - m)).
  - exfalso; revert Hi; apply not_In_nil.
  - apply In_repeat in Hi. injection Hi; auto. 
Qed.

Lemma fact0 i m : In (i, i+m) (join (q i)).
Proof.
  assert (H := @fact0_ (i+m) m).
  rewrite Nat.add_sub in H.
  apply H.
Qed.

CoInductive Neverending {a} (xs : Colist a) : Prop :=
| Neverending_Cons x ys : force xs = Cons x ys -> Neverending ys -> Neverending xs
.

Lemma Neverending_join_q_ i : forall n xs, (forall m, n <= m -> In (i, i+m) xs) -> Neverending xs.
Proof.
  cofix SELF; intros n xs H. destruct (force xs) as [ | [i' im] xs'] eqn:Eforce.
  - exfalso. eauto. 
  - econstructor; [ eassumption | ].
    apply SELF with (n := max n (im - i + 1)).
    clear SELF.
    intros.
    specialize (H m).
    destruct H.
    + revert H0; apply Nat.max_lub_l.
    + rewrite Eforce in H; inversion H; subst. destruct H1.
      * exfalso. subst. inversion H1; subst. lia.
      * assumption.
Qed.

Lemma Neverending_join_q i : Neverending (join (q i)).
Proof.
  eapply (Neverending_join_q_ (n := 0)).
  intros; apply fact0.
Qed.

Definition force_dep {a} (xs : Colist a)
  : { x & { xs' | (force xs = Cons x xs')%type } } + { force xs = [ ] }.
Proof.
  destruct (force xs).
  - right; constructor.
  - left; eauto.
Qed.

Fixpoint lookupNE {a} (xs : Colist a) (_ : Neverending xs) (i : nat) {struct i} : a.
Proof.
  destruct (force_dep xs) as [ [ x [ xs' Hforce ] ] | Hforce ].
  - destruct i as [ | i].
    + assumption.
    + apply (fun H => lookupNE _ xs' H i). clear lookupNE.
      destruct H. rewrite H in Hforce; inversion Hforce; subst. assumption.
  - exfalso; destruct H; congruence.
Defined.

Lemma lookupNE_irrel {a} i
  : forall (xs : Colist a) (Hxs Hxs' : Neverending xs), lookupNE Hxs i = lookupNE Hxs' i.
Proof.
  induction i; intros xs ? ?; cbn;
    (destruct force_dep as [ [ x [ xs' Hforce ] ] | Hforce ]; [ | destruct Hxs; congruence ]); auto.
Qed.

Lemma map_lookupNE_ {a}
  : forall (xs : Colist a) (Hxs : Neverending xs) f n,
    (forall i, lookupNE Hxs i = f (n + i)) ->
    (xs = map f (nats_from n))%colist.
Proof.
  cofix SELF.
  constructor.
  assert (H0 := H 0). cbn in H0.
  destruct force_dep as [ [ x' [ xs' Hforce ] ] | Hforce ] eqn:Hfd in H0; [ | destruct Hxs; congruence ].
  rewrite Hforce, H0. cbn.
  constructor.
  { auto. }
  assert (NE: Neverending xs').
  { clear Hfd. destruct Hxs.  rewrite e in Hforce; inversion Hforce; subst; auto. }
  apply (SELF _ NE). clear SELF.
  intros i. specialize (H (S i)).
  rewrite Nat.add_succ_r in H. cbn; rewrite <- H; cbn.
  rewrite Hfd. 
  apply lookupNE_irrel.
Qed.

Lemma map_lookupNE {a} (xs : Colist a) (Hxs : Neverending xs)
  : (xs = map (lookupNE Hxs) nats)%colist.
Proof.
  unfold nats.
  apply (@map_lookupNE_ a xs Hxs _ 0).
  reflexivity.
Qed.

Definition g i := lookupNE (Neverending_join_q i).

Lemma map_lookupNE_join_q i : (join (q i) = map (g i) nats)%colist.
Proof.
  apply map_lookupNE.
Qed.

Lemma fact1 : (join (join (map (fun i => q (S i)) nats)) = Delay [])%colist.
Proof.
  unfold q. rewrite join_diag.
  etransitivity.
  - eapply RColist_join. eapply (RColist_map (y := fun _ => Delay [])); [ | reflexivity ].
    intros i. rewrite (proj2 (Nat.ltb_lt i (S i))); [ reflexivity | constructor ].
  - rewrite <- repeat_map. apply join_repeat.
Qed.

Lemma fact2 : (join (map join (map (fun i => q (S i)) nats)) = map (fun i => g (S i) i) nats)%colist.
Proof.
  rewrite map_map.
  assert (H : pr (RColist eq) (fun i => join (q (S i))) (fun i => map (g (S i)) nats)).
  { intros i; apply map_lookupNE_join_q. }
  etransitivity.
  - eapply RColist_join. eapply RColist_map. { eapply H. } { reflexivity. }
  - apply join_diag.
Qed.

Lemma bad : (map (fun i => g (S i) i) nats = Delay [])%colist.
Proof.
  rewrite <- fact2, <- fact1, join_join. reflexivity.
Qed.

Theorem contra : False.
Proof.
  assert (H := bad).
  destruct H; inversion H.
Qed.

End Work.

Theorem no_LawfulJoin : forall join, ~(LawfulJoin join).
Proof.
  exact @contra.
Qed.