## Stream: general

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

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

#### Reid Barton (Jun 03 2020 at 17:44):

This doesn't look true, since lists are finite

#### Reid Barton (Jun 03 2020 at 17:45):

or actually it just doesn't look true period

#### Reid Barton (Jun 03 2020 at 17:46):

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

#### Slavomir Kaslev (Jun 03 2020 at 17:46):

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

#### 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

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

#### Reid Barton (Jun 03 2020 at 18:13):

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

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

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

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

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

#### Reid Barton (Jun 03 2020 at 18:22):

Yes, just use this example above.

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

#### Reid Barton (Jun 03 2020 at 18:23):

But in Set, it's just false.

#### 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?

#### Reid Barton (Jun 03 2020 at 18:25):

Right, but where does that actually happen.

#### Reid Barton (Jun 03 2020 at 18:25):

Maybe in compact Hausdorff spaces for example.

#### Johan Commelin (Jun 03 2020 at 18:26):

Obligatory Hask is not a category link...

#### 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

#### Bhavik Mehta (Jun 03 2020 at 18:26):

Johan Commelin said:

Obligator Hask is not a cateogry link...

Hence the quotes around it!

#### Reid Barton (Jun 03 2020 at 18:27):

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

#### Reid Barton (Jun 03 2020 at 18:27):

but it's rather far from Set

#### 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


#### Bhavik Mehta (Jun 03 2020 at 18:36):

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

#### Bhavik Mehta (Jun 03 2020 at 18:40):

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

#### 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

#### Reid Barton (Jun 03 2020 at 19:03):

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

#### 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