Skip to content

Instantly share code, notes, and snippets.

@Lysxia
Last active Oct 27, 2021
Embed
What would you like to do?
There is no ZipList monad, proved in Coq; thread https://twitter.com/lysxia/status/1451202791796584454
(** 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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment