Zulip Chat Archive

Stream: maths

Topic: annoying proof challenge


view this post on Zulip Chris Hughes (Dec 01 2018 at 21:49):

Is there a nice way to prove this?

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

view this post on Zulip Kenny Lau (Dec 01 2018 at 21:58):

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 

view this post on Zulip Kenny Lau (Dec 01 2018 at 21:58):

@Chris Hughes

view this post on Zulip Kevin Buzzard (Dec 01 2018 at 22:01):

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

view this post on Zulip Chris Hughes (Dec 01 2018 at 22:03):

Maybe it's some super duper eta reduction.

view this post on Zulip Kenny Lau (Dec 01 2018 at 22:04):

oops it's supposed to end in rfl

view this post on Zulip Kenny Lau (Dec 01 2018 at 22:04):

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

view this post on Zulip Kevin Buzzard (Dec 01 2018 at 22:05):

oh that works better :-)

view this post on Zulip Kevin Buzzard (Dec 01 2018 at 22:06):

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

view this post on Zulip Kenny Lau (Dec 01 2018 at 22:07):

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

view this post on Zulip Kenny Lau (Dec 01 2018 at 22:07):

it does option.no_confusion

view this post on Zulip Kevin Buzzard (Dec 01 2018 at 22:09):

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


Last updated: May 06 2021 at 18:20 UTC