Skip to content
{{ message }}

Instantly share code, notes, and snippets.

# Lysxia/NoZipListMonad.v

Last active Oct 27, 2021
There is no ZipList monad, proved in Coq; thread https://twitter.com/lysxia/status/1451202791796584454
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 (** 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 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 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.
to join this conversation on GitHub. Already have an account? Sign in to comment