annoying proof challenge

Stream: maths

[Chris Hughes]

Is there a nice way to prove this?

example {a b : with_bot ℕ} (h : a + b = 1) : a = 0 ∨ b = 0

[Kenny Lau]

import algebra.ordered_group data.nat.basic

example : ∀ {a b : with_bot ℕ}, a + b = 1 → a = 0 ∨ b = 0
| (some a) (some 0) H := or.inr rfl
| (some a) (some (b+1)) H := or.inl $ (add_eq_zero_iff.1 (nat.succ_inj $ option.some.inj H)).1.symm ▸

[Kenny Lau]

@Chris Hughes

[Kevin Buzzard]

Didn't your mother tell you never to end a sentence with a ▸?

[Chris Hughes]

Maybe it's some super duper eta reduction.

[Kenny Lau]

oops it's supposed to end in rfl

[Kenny Lau]

import algebra.ordered_group data.nat.basic

example : ∀ {a b : with_bot ℕ}, a + b = 1 → a = 0 ∨ b = 0
| (some a) (some 0) H := or.inr rfl
| (some a) (some (b+1)) H := or.inl $ (add_eq_zero_iff.1 (nat.succ_inj $ option.some.inj H)).1.symm ▸ rfl

[Kevin Buzzard]

oh that works better :-)

[Kevin Buzzard]

What does the equation compiler actually do to decide that it can ignore the none cases? I mean, what does it try?

[Kenny Lau]

import algebra.ordered_group data.nat.basic

theorem test : ∀ {a b : with_bot ℕ}, a + b = 1 → a = 0 ∨ b = 0
| (some a) (some 0) H := or.inr rfl
| (some a) (some (b+1)) H := or.inl $ (add_eq_zero_iff.1 (nat.succ_inj $ option.some.inj H)).1.symm ▸ rfl

#print test
/-
theorem test : ∀ {a b : with_bot ℕ}, a + b = 1 → a = 0 ∨ b = 0 :=
λ {a b : with_bot ℕ} (a_1 : a + b = 1),
  option.cases_on a
    (λ (a : none + b = 1),
       option.cases_on b
         (λ (a : none + none = 1),
            eq.dcases_on a (λ (a_1 : some 1 = none), option.no_confusion a_1) (eq.refl 1) (heq.refl a))
         (λ (b : ℕ) (a : none + some b = 1),
            eq.dcases_on a (λ (a_1 : some 1 = none), option.no_confusion a_1) (eq.refl 1) (heq.refl a))
         a)
    (λ (a : ℕ) (a_1 : some a + b = 1),
       option.cases_on b
         (λ (a_1 : some a + none = 1),
            eq.dcases_on a_1 (λ (a_2 : some 1 = none), option.no_confusion a_2) (eq.refl 1) (heq.refl a_1))
         (λ (b : ℕ) (a_1 : some a + some b = 1),
            nat.cases_on b (λ (a_1 : some a + some 0 = 1), id_rhs (some a = 0 ∨ some 0 = 0) (or.inr rfl))
              (λ (b : ℕ) (a_1 : some a + some (nat.succ b) = 1),
                 id_rhs (some a = 0 ∨ some (b + 1) = 0)
                   (or.inl (eq.symm ((add_eq_zero_iff.mp (nat.succ_inj (option.some.inj a_1))).left) ▸ rfl)))
              a_1)
         a_1)
    a_1
-/

[Kenny Lau]

it does option.no_confusion

[Kevin Buzzard]

option.no_confusion is such a great name for a function. I might get it on a t-shirt.