Zulip Chat Archive

Stream: new members

Topic: Sum type cancellation


view this post on Zulip Grayson Burton (Mar 02 2020 at 01:28):

Hello. This is my first time posting here (or on Zulip at all) so if I should've put this somewhere else or done this differently, my bad.
I've been fairly stuck trying to prove this theorem that I believe is correct. I really want to stick to computable proofs as well, but I'm happy to bend that if need be.

-- Type isomorphism. Classically is equivalent to bijection but this allows me to use the inverse function `g` while staying computable.
def type_iso (α β : Type) : Prop :=  (f : α  β) (g : β  α),
  function.left_inverse f g  function.right_inverse f g

theorem sum_cancel {α β γ : Type} (hsum : type_iso (α  β) (α  γ)) : type_iso β γ :=
begin
  cases hsum with fs gshfs,
  cases gshfs with gs hfs,
  let f : β  γ := λ x, sum.cases_on (fs $ sum.inr x)
    (λ a, sorry)
    id,
  let g : γ  β := λ x, sum.cases_on (gs $ sum.inr x)
    (λ a, sorry)
    id,
  existsi f,
  existsi g,
  split,
  begin
    intro x,
    sorry
  end,
  begin
    intro x,
    sorry
  end
end

(I could've used rintros for sum_cancel but am using the Lean web editor to draft this)
Can someone point me in the right direction? Thanks!

view this post on Zulip Mario Carneiro (Mar 02 2020 at 01:51):

The theorem is false. nat ⊕ empty is isomorphic to nat ⊕ nat

view this post on Zulip Mario Carneiro (Mar 02 2020 at 01:52):

By the way, the computable version of bijection is called equiv and there is a sizeable mathlib file about it

view this post on Zulip Bryan Gin-ge Chen (Mar 02 2020 at 01:54):

(You can use rintros in the community web editor if you import tactic.)

view this post on Zulip Grayson Burton (Mar 02 2020 at 02:01):

Oh cool. Thanks! @Mario Carneiro @Bryan Gin-ge Chen

view this post on Zulip Mario Carneiro (Mar 02 2020 at 02:02):

The theorem is true for cancelling option, or more generally if α is finite, but I don't think it is computable

view this post on Zulip Mario Carneiro (Mar 02 2020 at 02:06):

Actually, I think it might be computable. If f : option A -> option B has an inverse g, and you want to construct a function A -> B, you check if f (some a) = some b so you are done, or f (some a) = none in which case f none = some b. (f none cannot be none in this case since f is injective.)

view this post on Zulip Grayson Burton (Mar 02 2020 at 02:11):

I'll have to see about using data.equiv, it seems to have gotten most of the boilerplate out of the way (like proving type isomorphism an equivalence relation).

view this post on Zulip Grayson Burton (Mar 02 2020 at 06:49):

Product types aren't cancellative either. :( There go my dreams of embedding the commutative semiring of types in a signed type commutative ring

view this post on Zulip Reid Barton (Mar 02 2020 at 16:21):

https://ncatlab.org/nlab/show/Eilenberg+swindle


Last updated: May 09 2021 at 19:11 UTC