Zulip Chat Archive

Stream: general

Topic: Proving γ ≃ α ⊕ β × γ ⇒ γ ≃ α × list β


view this post on Zulip Slavomir Kaslev (Jun 03 2020 at 17:42):

I'm trying to formalize[1] some ideas from analytic combinatorics[2] and got stuck on trying to prove the following isomorphism:

structure {u v} iso (α : Sort u) (β : Sort v) :=
(f : α  β) (g : β  α) (gf : Π x, g (f x) = x) (fg : Π x, f (g x) = x)

def linear {α β γ : Type} (i : iso γ (α  β × γ)) : iso γ (α × list β) :=
⟨λ x, sum.rec (λ y, (y, [])) (λ y, (sorry, y.1 :: sorry)) (i.f x),
 λ x, list.rec (i.g (sum.inl x.1)) (λ y ys ih, i.g (sum.inr (y, ih))) x.2,
 λ x, sorry,
 λ x, sorry

This is how I would do it in Haskell:

data Iso a b = Iso { to :: a->b, from :: b->a }

lin_iso_to :: Iso c (Either a (b, c)) -> c -> (a, [b])
lin_iso_to i c = case to i c of
  Left a -> (a, [])
  Right (b, c) -> let (a, bs) = lin_iso_to i c in (a, b : bs)

lin_iso_from :: Iso c (Either a (b, c)) -> (a, [b]) -> c
lin_iso_from i (a, []) = from i $ Left a
lin_iso_from i (a, b:bs) = from i $ Right (b, lin_iso_from i (a, bs))

-- c = a + b c   =>   c = a (list b)
lin_iso :: Iso c (Either a (b, c)) -> Iso c (a, [b])
lin_iso i = Iso {to = lin_iso_to i, from = lin_iso_from i}

but I can't figure out how to do the recursive call in lin_iso_to.

I haven't used the well-founded machinery in Lean so far and I guess that's the missing piece for the above definition.

[1] https://github.com/skaslev/papers/blob/master/analytic_functor.lean
[2] http://algo.inria.fr/flajolet/Publications/book.pdf

view this post on Zulip Reid Barton (Jun 03 2020 at 17:44):

This doesn't look true, since lists are finite

view this post on Zulip Reid Barton (Jun 03 2020 at 17:45):

or actually it just doesn't look true period

view this post on Zulip Reid Barton (Jun 03 2020 at 17:46):

Aren't potentially infinite streams another solution to γ ≃ α ⊕ β × γ?

view this post on Zulip Slavomir Kaslev (Jun 03 2020 at 17:46):

Lists are potentially infinite in Haskell but always finite in Lean, if I understand correctly.

view this post on Zulip Reid Barton (Jun 03 2020 at 17:47):

In Lean α × list β is the initial algebra for α ⊕ β × - so you could build a map from α × list β to γ, but you can't necessarily go back

view this post on Zulip Slavomir Kaslev (Jun 03 2020 at 18:11):

The Haskell version works correctly though. What's missing imo is given iso γ (α ⊕ β × γ) to be able to do a recursive call over the γ on the rhs (since it should be "smaller" than the γ on the lhs and thus should terminate) but my well-founded-fu is nonexistent.

view this post on Zulip Reid Barton (Jun 03 2020 at 18:13):

It's not missing, though, because it's not true!

view this post on Zulip Reid Barton (Jun 03 2020 at 18:13):

Lean's semantics correspond to ordinary math, and the statement you are trying to prove is false in ordinary math.

view this post on Zulip Reid Barton (Jun 03 2020 at 18:14):

Haskell's semantics don't correspond to ordinary math so it's not surprising that you can "prove" it there.

view this post on Zulip Reid Barton (Jun 03 2020 at 18:15):

Here is a counterexample, take γ = α × list β ⊕ ℕ → β. Then there is still an isomorphism γ ≃ α ⊕ β × γ, but there isn't an isomorphism γ ≃ α × list β (in general; for example, take α empty).

view this post on Zulip Slavomir Kaslev (Jun 03 2020 at 18:15):

Can it be formally proved false in Lean then?

I've been using this isomorphism for a while and I haven't be able to come up with contradiction or any surprises so far.

view this post on Zulip Reid Barton (Jun 03 2020 at 18:22):

Yes, just use this example above.

view this post on Zulip Reid Barton (Jun 03 2020 at 18:23):

It's tempting to think that there should be some extra structure one can impose on top of bare sets to rule out examples like this one, but I don't know what it is.

view this post on Zulip Reid Barton (Jun 03 2020 at 18:23):

But in Set, it's just false.

view this post on Zulip Bhavik Mehta (Jun 03 2020 at 18:24):

Reid Barton said:

It's tempting to think that there should be some extra structure one can impose on top of bare sets to rule out examples like this one, but I don't know what it is.

Maybe that initial algebras and final coalgebras coincide?

view this post on Zulip Reid Barton (Jun 03 2020 at 18:25):

Right, but where does that actually happen.

view this post on Zulip Reid Barton (Jun 03 2020 at 18:25):

Maybe in compact Hausdorff spaces for example.

view this post on Zulip Bhavik Mehta (Jun 03 2020 at 18:25):

In 'Hask' :P

view this post on Zulip Johan Commelin (Jun 03 2020 at 18:26):

Obligatory Hask is not a category link...

view this post on Zulip Bhavik Mehta (Jun 03 2020 at 18:26):

I vaguely remember something about that happening in the category of CPOs with bottom, but might be misremembering

view this post on Zulip Bhavik Mehta (Jun 03 2020 at 18:26):

Johan Commelin said:

Obligator Hask is not a cateogry link...

Hence the quotes around it!

view this post on Zulip Reid Barton (Jun 03 2020 at 18:27):

right, and this is one place where you can say Haskell has its semantics I think

view this post on Zulip Reid Barton (Jun 03 2020 at 18:27):

but it's rather far from Set

view this post on Zulip Chris Hughes (Jun 03 2020 at 18:28):

Here's a disproof

example (h :  α β γ, γ  α  β × γ  γ  α × list β) : false :=
have unit  empty  unit × unit,
from { to_fun := λ _, sum.inr ((),()),
        inv_fun := λ _, (),
        left_inv := λ x, by cases x; refl,
        right_inv := λ x, begin cases x, cases x, cases x, cases x_fst, cases x_snd, refl end },
(h empty unit unit this ()).1.elim

view this post on Zulip Bhavik Mehta (Jun 03 2020 at 18:36):

The same idea lets you construct a term of type Void in Haskell

view this post on Zulip Bhavik Mehta (Jun 03 2020 at 18:40):

What's the actual bit of maths you wanted this result for?

view this post on Zulip Slavomir Kaslev (Jun 03 2020 at 18:58):

For constructing other isomorphisms (iso.linear is the offending propositionγ ≃ α ⊕ β × γ ⇒ γ ≃ α × list β) such as
https://github.com/skaslev/papers/blob/3d42174fa43cd71680a89c5cc14924b21d0b57de/analytic_functor.lean#L596-L607
https://github.com/skaslev/papers/blob/3d42174fa43cd71680a89c5cc14924b21d0b57de/analytic_functor.lean#L701-L716

view this post on Zulip Reid Barton (Jun 03 2020 at 19:03):

Well, those are all fine; you could construct the isomorphisms directly.

view this post on Zulip Slavomir Kaslev (Jun 03 2020 at 19:45):

This last use was giving me grief last time I tried to prove it directly :cold_sweat:

https://github.com/skaslev/papers/blob/3d42174fa43cd71680a89c5cc14924b21d0b57de/analytic_functor.lean#L774-L776


Last updated: May 17 2021 at 21:12 UTC