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

Stream: general

[Slavomir Kaslev]

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

[Reid Barton]

This doesn't look true, since lists are finite

[Reid Barton]

or actually it just doesn't look true period

[Reid Barton]

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

[Slavomir Kaslev]

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

[Reid Barton]

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

[Slavomir Kaslev]

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.

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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).

[Slavomir Kaslev]

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.

[Reid Barton]

Yes, just use this example above.

[Reid Barton]

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.

[Reid Barton]

But in Set, it's just false.

[Bhavik Mehta]

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?

[Reid Barton]

Right, but where does that actually happen.

[Reid Barton]

Maybe in compact Hausdorff spaces for example.

[Bhavik Mehta]

In 'Hask' :P

[Johan Commelin]

Obligatory Hask is not a category link...

[Bhavik Mehta]

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

[Bhavik Mehta]

Johan Commelin said:

Obligator Hask is not a cateogry link...

Hence the quotes around it!

[Reid Barton]

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

[Reid Barton]

but it's rather far from Set

[Chris Hughes]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Slavomir Kaslev]

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

[Reid Barton]

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

[Slavomir Kaslev]

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