arguing using by_cases

Stream: new members

[Aniruddh Agarwal]

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]

Can you post a #mwe ?

[Aniruddh Agarwal]

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]

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]

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

[Kevin Buzzard]

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]

Ah, I was trying to avoid entering tactic mode

[Kevin Buzzard]

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

The stupid triangle is a term mode version of rewrite.

[Aniruddh Agarwal]

Thank you!

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Did you know that substitution is just induction on =?

[Aniruddh Agarwal]

What?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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]

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

[Kevin Buzzard]

which is rw

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

[Patrick Stevens]

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]

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]

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