# Zulip Chat Archive

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

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

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 `=`

?

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

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: Dec 20 2023 at 11:08 UTC