Zulip Chat Archive

Stream: new members

Topic: arguing using by_cases


view this post on Zulip Aniruddh Agarwal (May 17 2020 at 16:35):

The setup is:

def is_zero_divisor [comm_ring α] (a : α) :=  b : α, b  0  a * b = 0
def is_nilpotent [comm_ring α] (a : α) :=  n : , n  0  a ^ n = 0

theorem nonzero_nilpotent_is_zerodivisor [comm_ring α] (a : α) (ha : is_nilpotent a) (ha' : a  0) : is_zero_divisor a
  := sorry

theorem zero_is_zero_divisor_in_nonzero_ring [nonzero_comm_ring α]
  : is_zero_divisor (0 : α) :=
exists.intro 1 one_ne_zero, by simp

I'm trying to prove

theorem nonzero_ring_nilpotent_is_zerodivisor [nonzero_comm_ring α] (a : α) (ha : is_nilpotent a)
  : is_zero_divisor a :=
classical.by_cases (assume h1  : a = 0, zero_is_zero_divisor_in_nonzero_ring)
                   (assume hnz : a  0, nonzero_nilpotent_is_zerodivisor a ha hnz)

but lean is complaining:

type mismatch at application
  classical.by_cases (λ (h1 : a = 0), zero_is_zero_divisor_in_nonzero_ring)
term
  λ (h1 : a = 0), zero_is_zero_divisor_in_nonzero_ring
has type
   (h1 : a = 0), is_zero_divisor 0
but is expected to have type
  a = 0  is_zero_divisor a

My guess is that lean isn't able to prove that is_zero_divisor 0 is the same as is_zero_divisor a in the first case. How can I fix this?

view this post on Zulip Kevin Buzzard (May 17 2020 at 17:06):

Can you post a #mwe ?

view this post on Zulip Aniruddh Agarwal (May 17 2020 at 17:20):

import algebra.associated

variables {α : Type*}

/- An element a of a ring α is a zero divisor if there exists a b ∈ α
   such that b ≠ 0 and ab = 0. -/
def is_zero_divisor [comm_ring α] (a : α) :=  b : α, b  0  a * b = 0

/- An element a of a ring α is nilpotent if there exists a n ∈ ℕ such
   that n ≠ 0 and a^n = 0 -/
def is_nilpotent [comm_ring α] (a : α) :=  n : , n  0  a ^ n = 0

theorem nonzero_nilpotent_is_zerodivisor [comm_ring α] (a : α) (ha : is_nilpotent a) (ha' : a  0) : is_zero_divisor a
  := sorry

theorem zero_is_zero_divisor_in_nonzero_ring [nonzero_comm_ring α]
  : is_zero_divisor (0 : α) :=
exists.intro 1 one_ne_zero, by simp

/- All nilpotents are zero divisors in a nonzero ring. -/
theorem nonzero_ring_nilpotent_is_zerodivisor [nonzero_comm_ring α] (a : α) (ha : is_nilpotent a)
  : is_zero_divisor a :=
classical.by_cases (assume hz  : a = 0, zero_is_zero_divisor_in_nonzero_ring)
                   (assume hnz : a  0, nonzero_nilpotent_is_zerodivisor a ha hnz)

view this post on Zulip Kevin Buzzard (May 17 2020 at 17:22):

is_zero_divisor 0 isn't the same as is_zero_divisor a, even if you have some hypothesis saying a = 0; you need to rewrite that hypothesis before the terms become equal.

view this post on Zulip Aniruddh Agarwal (May 17 2020 at 17:22):

Yeah, I'm just failing to see how to do that

view this post on Zulip Kevin Buzzard (May 17 2020 at 17:24):

theorem nonzero_ring_nilpotent_is_zerodivisor [nonzero_comm_ring α] (a : α) (ha : is_nilpotent a)
  : is_zero_divisor a :=
begin
  by_cases h : a = 0,
  { rw h,
    exact zero_is_zero_divisor_in_nonzero_ring},
  { exact nonzero_nilpotent_is_zerodivisor a ha h}
end

view this post on Zulip Aniruddh Agarwal (May 17 2020 at 17:25):

Ah, I was trying to avoid entering tactic mode

view this post on Zulip Kevin Buzzard (May 17 2020 at 17:25):

/- All nilpotents are zero divisors in a nonzero ring. -/
theorem nonzero_ring_nilpotent_is_zerodivisor [nonzero_comm_ring α] (a : α) (ha : is_nilpotent a)
  : is_zero_divisor a :=
classical.by_cases (assume hz  : a = 0, hz.symm  zero_is_zero_divisor_in_nonzero_ring)
                   (assume hnz : a  0, nonzero_nilpotent_is_zerodivisor a ha hnz)

view this post on Zulip Kevin Buzzard (May 17 2020 at 17:25):

The stupid triangle is a term mode version of rewrite.

view this post on Zulip Aniruddh Agarwal (May 17 2020 at 17:25):

Thank you!

view this post on Zulip Kevin Buzzard (May 17 2020 at 17:25):

But believe you me, it's nowhere near as powerful.

view this post on Zulip Kevin Buzzard (May 17 2020 at 17:26):

Oh -- I had to open_locale classical to get the tactic proof working by the way

view this post on Zulip Kevin Buzzard (May 17 2020 at 17:26):

Did you know that substitution is just induction on =?

view this post on Zulip Aniruddh Agarwal (May 17 2020 at 17:26):

What?

view this post on Zulip Kevin Buzzard (May 17 2020 at 17:27):

= isn't some inbuilt thing in Lean, it's just notation for some inductive type eq

view this post on Zulip Kevin Buzzard (May 17 2020 at 17:28):

eq x y has one constructor: eq.refl a has type eq a a and that's it.

view this post on Zulip Kevin Buzzard (May 17 2020 at 17:29):

And when you build the inductive type, Lean adds to its environment the new type, its constructor(s) and its eliminator (i.e. its recursor).

view this post on Zulip Kevin Buzzard (May 17 2020 at 17:29):

When you build the naturals using the standard functional definition (Peano's axioms), the recursor Lean generates is the standard principle of mathematical recursion.

view this post on Zulip Kevin Buzzard (May 17 2020 at 17:30):

When you make the eq inductive type, the recursor it generates is this:

eq.rec : Π {α : Sort u_3} {a : α} {C : α  Sort u_2}, C a  Π {a_1 : α}, a = a_1  C a_1

view this post on Zulip Kevin Buzzard (May 17 2020 at 17:30):

i.e. if you have a term of type C a, then for all b and for all proofs of a = b, you can get a term of type C b

view this post on Zulip Kevin Buzzard (May 17 2020 at 17:31):

In other words, a = b -> (C a -> C b)

view this post on Zulip Kevin Buzzard (May 17 2020 at 17:31):

which is rw

view this post on Zulip Kevin Buzzard (May 17 2020 at 17:33):

The stupid triangle (\t) is just notation for eq.subst (you can check this with #print notation ▸) and eq.subst is the Prop version of eq.rec: if a = b then P(a)    P(b)P(a)\implies P(b)

view this post on Zulip Kevin Buzzard (May 17 2020 at 17:33):

Did you know that "false implies PP" is just induction on false? ;-)

view this post on Zulip Kevin Buzzard (May 17 2020 at 17:34):

To give a map from false to anything, you just have to say where all its constructors go, but false has no constructors at all :laughing:

view this post on Zulip Bhavik Mehta (May 17 2020 at 17:39):

I sometimes use this when I can't convince rw to do what I want : if I have the hypothesis h : a = b and rw refuses to work for some reason I've done cases h which does!

view this post on Zulip Kevin Buzzard (May 17 2020 at 17:42):

I often use cases on an equality to mean "sub in everywhere".

view this post on Zulip Kevin Buzzard (May 17 2020 at 17:47):

@Aniruddh Agarwal you don't need n0n\not=0 in your definition of is_nilpotent.

view this post on Zulip Patrick Stevens (May 17 2020 at 17:47):

Kevin Buzzard said:

I often use cases on an equality to mean "sub in everywhere".

Isn't the subst tactic meant to do this? Is there a reason to use one or the other?

view this post on Zulip Mario Carneiro (May 17 2020 at 17:53):

Prefer the subst tactic when it applies (or rfl in an rcases/obtain pattern, which calls subst). It only works if one side of the equality is a variable, though, while cases can see through multiple layers of constructors. For example if h : (a, b) = (c, d) then cases h will replace c by a and d by b in the goal, while subst h will fail.

But cases will also often make a mess when trying to reduce things to a normal form, so the result of the substitution may not be optimal, for example if h : foo a = b then cases might unfold foo a before substitution, causing big expressions all through your goal. In these cases, you can use injection and subst to get a bit more control over unfolding.

view this post on Zulip Mario Carneiro (May 17 2020 at 17:54):

In an rcases pattern, rfl means subst and <> means cases


Last updated: May 10 2021 at 19:16 UTC