## Stream: new members

### Topic: arguing using by_cases

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

#### Kevin Buzzard (May 17 2020 at 17:06):

Can you post a #mwe ?

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


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

#### Aniruddh Agarwal (May 17 2020 at 17:22):

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

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


#### Aniruddh Agarwal (May 17 2020 at 17:25):

Ah, I was trying to avoid entering tactic mode

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


#### Kevin Buzzard (May 17 2020 at 17:25):

The stupid triangle is a term mode version of rewrite.

Thank you!

#### Kevin Buzzard (May 17 2020 at 17:25):

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

#### Kevin Buzzard (May 17 2020 at 17:26):

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

#### Kevin Buzzard (May 17 2020 at 17:26):

Did you know that substitution is just induction on =?

What?

#### Kevin Buzzard (May 17 2020 at 17:27):

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

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

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

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

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


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

#### Kevin Buzzard (May 17 2020 at 17:31):

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

#### Kevin Buzzard (May 17 2020 at 17:31):

which is rw

#### 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)\implies P(b)$

#### Kevin Buzzard (May 17 2020 at 17:33):

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

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

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

#### Kevin Buzzard (May 17 2020 at 17:42):

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

#### Kevin Buzzard (May 17 2020 at 17:47):

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

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

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

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