1 mod 2 is in ℝ

Stream: new members

[Lars Ericson]

Lean isn't letting me say this:

#check (1:zmod 2) ∈ {x : ℝ | ∃ (y : zmod 2), x = ↑y}

the complaint is

failed to synthesize type class instance for
⊢ has_mem (zmod 2) (set ℝ)

Is there a way to make this work?

[Alex J. Best]

It's not clear what mathematically 1 mod 2 in R is. There are no ring homomorphisms from Z/2 to R or even additive homomorphisms.

[Adam Topaz]

@Lars Ericson I made some assumptions about what you're actually trying to do.

import data.real.basic

#check (1 % 2) ∈ {r : ℝ | ∃ y : fin 2, r = y}

[Damiano Testa]

For me, one of the hardest concepts to internalise of type theory is that terms have a unique type. When you write (1 : zmod 2), you are explicitly saying what the type of 1 is. Right after that, you are telling Lean that the term 1 has type \R. This cannot be, since terms have a unique type!

[Lars Ericson]

The context is that I am working on Exercise 7(a):
Screenshot-from-2021-01-21-00-28-17.png

I am trying to fill out this sketch:

import data.zmod.basic
import ring_theory.subring
import data.real.basic
import tactic
import tactic.slim_check

open real

abbreviation is_an_integral_domain {α : Type*} [ring α] (s : set α) := ∃ (sr : subring α) [integral_domain sr], s = sr  -- Eric Wieser

instance foo: has_mem (zmod 2) (set ℝ) := sorry

theorem A_one : (1:zmod 2) ∈ {x : ℝ | ∃ (y : zmod 2), x = ↑y} :=
begin
  sorry
end

def A : subring ℝ :=
{ carrier := {x : ℝ | ∃ (y : zmod 2), x = y},
  one_mem' := A_one,
  mul_mem' := sorry,
  zero_mem' := sorry,
  add_mem' := sorry,
  neg_mem' := sorry,
}

theorem ex7a : is_an_integral_domain {x : ℝ | ∃ (y : zmod 2), x = y} :=
⟨A, infer_instance, rfl⟩

In other words I think zmod 2 is an integral domain and I am trying to adapt a proof pattern used previously to prove it.

[Kyle Miller]

You could take that as a recipe to construct a new number system with symbols 0 and 1 that behave in the described way -- they don't have to literally be 0 and 1 in the real numbers.

Here's a start at creating that number system, call it R:

inductive R
| zero
| one

open R

def R.add : R → R → R
| zero zero := zero
| zero one := one
| one zero := one
| one one := zero

def R.mul : R → R → R
| zero zero := zero
| zero one := zero
| one zero := zero
| one one := one

instance : has_add R := ⟨R.add⟩
instance : has_mul R := ⟨R.mul⟩
instance : has_zero R := ⟨zero⟩
instance : has_one R := ⟨one⟩

[Kyle Miller]

Many proofs are trivial if you do them by cases:

lemma R_add_comm {a b : R} : a + b = b + a :=
begin
  cases a; cases b; refl
end

[Kyle Miller]

Another:

lemma R_mul_one {a : R} : a * 1 = a :=
by { cases a; refl }

[Kyle Miller]

(The downside of course is that you don't inherit any of the structure of another number system. Just showing it can be done this way.)

[Eric Wieser]

Can't you just use zmod2 directly, rather than embedding it to the reals?

[Lars Ericson]

Thanks I will work through both @Kyle Miller sketch and @Eric Wieser suggestion of proving

instance : integral_domain (zmod 2)

I am working through Kyle's sketch now. One interesting point, not clear in the exercise, but which is required by integral_domain, is to define neg. There are two ways to go, one is -0=0 and -1=1 which conforms to zmod 2. The other is -0=1 and -1=0 which corresponds to a Boolean algebra. I guess I'll try both and see if both negs give integral domains.

[Eric Wieser]

The proof amounts to "import the right files, remind mathlib that 2 is prime":

import data.nat.prime
import data.zmod.basic

instance : fact (nat.prime 2) := nat.prime_two

-- this is `@field.to_integral_domain _ (zmod.field 2)` under the hood
instance : integral_domain (zmod 2) := by apply_instance

I don't know if there's a more idiomatic way to introduce the fact.

If you actually want to know what the proof is, rather than just knowing that we already have it, check out src#zmod.field

[Adam Topaz]

When you import data.zmod.basic, I think you're automatically importing the ring structure on zmod n as well. If you want to do the exercise of defining the addition, multiplication, etc. from scratch, I suggest following Kyle's approach above.

[Mario Carneiro]

Lars Ericson said:

One interesting point, not clear in the exercise, but which is required by integral_domain, is to define neg. There are two ways to go, one is -0=0 and -1=1 which conforms to zmod 2. The other is -0=1 and -1=0 which corresponds to a Boolean algebra. I guess I'll try both and see if both negs give integral domains.

The axioms of an integral domain (an additive group, even) require that -0 = 0, so whatever element you decide to call zero has to be its own inverse. The complementation in a boolean algebra is not a valid group operation.

[Lars Ericson]

Done, following Kyle's approach:

import ring_theory.subring
import tactic
import tactic.slim_check
import data.zmod.basic

inductive R
| zero
| one

open R

def R.add : R → R → R
| zero zero := zero
| zero one := one
| one zero := one
| one one := zero

def R.mul : R → R → R
| zero zero := zero
| zero one := zero
| one zero := zero
| one one := one

def R.neg : R → R
| zero := zero
| one := one

instance : has_add R := ⟨R.add⟩
instance : has_mul R := ⟨R.mul⟩
instance : has_zero R := ⟨zero⟩
instance : has_one R := ⟨one⟩
instance : has_neg R := ⟨R.neg⟩

theorem R.exists_pair_ne : ∃ (x y : R), x ≠ y :=
begin
   use [R.zero, R.one],
end

theorem R.zero_add (a : R): 0 + a = a :=
begin
   cases a,
   repeat { exact rfl },
end

theorem R.add_zero (a : R): a + 0 = a :=
begin
   cases a,
   repeat { exact rfl },
end

theorem R.one_mul (a : R): 1 * a = a :=
begin
   cases a,
   repeat { exact rfl },
end

theorem R.mul_one (a : R): a * 1 = a :=
begin
   cases a,
   repeat { exact rfl },
end

theorem R.add_assoc (a b c : R): a + b + c = a + (b + c) :=
begin
   cases a,
   cases b,
   cases c,
   repeat { exact rfl },
   cases c,
   repeat { exact rfl },
   cases b,
   cases c,
   repeat { exact rfl },
   cases c,
   repeat { exact rfl },
end

theorem R.add_left_neg (a : R): -a + a = 0 :=
begin
   cases a,
   repeat { exact rfl },
end

theorem R.add_comm (a b : R): a + b = b + a :=
begin
   cases a,
   cases b,
   repeat { exact rfl },
   cases b,
   repeat { exact rfl },
end

theorem R.mul_assoc (a b c : R): a * b * c = a * (b * c) :=
begin
   cases a,
   cases b,
   cases c,
   repeat { exact rfl },
   cases c,
   repeat { exact rfl },
   cases b,
   cases c,
   repeat { exact rfl },
   cases c,
   repeat { exact rfl },
end


theorem R.left_distrib (a b c : R): a * (b + c) = a * b + a * c :=
begin
   cases a,
   cases b,
   cases c,
   repeat { exact rfl },
   cases c,
   repeat { exact rfl },
   cases b,
   cases c,
   repeat { exact rfl },
   cases c,
   repeat { exact rfl },
end

theorem R.right_distrib (a b c : R): (a + b) * c = a * c + b * c :=
begin
   cases a,
   cases b,
   cases c,
   repeat { exact rfl },
   cases c,
   repeat { exact rfl },
   cases b,
   cases c,
   repeat { exact rfl },
   cases c,
   repeat { exact rfl },
end

theorem R.mul_comm (a b : R): a * b = b * a :=
begin
   cases a,
   cases b,
   repeat { exact rfl },
   cases b,
   repeat { exact rfl },
end

theorem R.eq_zero_or_eq_zero_of_mul_eq_zero (a b : R) (h: a * b = 0): a = 0 ∨ b = 0:=
begin
   cases a,
   cases b,
   left,
   exact rfl,
   left,
   exact rfl,
   cases b,
   right,
   exact rfl,
   exfalso,
   finish,
end

instance ex7a_kyle_miller : integral_domain R :=
{
  zero := R.zero,
  one := R.one,
  add := R.add,
  mul := R.mul,
  add_assoc := R.add_assoc,
  zero_add := R.zero_add,
  add_zero := R.add_zero,
  neg := R.neg,
  add_left_neg := R.add_left_neg,
  add_comm := R.add_comm,
  one_mul := R.one_mul,
  mul_assoc := R.mul_assoc,
  mul_one := R.mul_one ,
  left_distrib := R.left_distrib,
  right_distrib := R.right_distrib,
  mul_comm := R.mul_comm,
  exists_pair_ne := R.exists_pair_ne,
  eq_zero_or_eq_zero_of_mul_eq_zero := R.eq_zero_or_eq_zero_of_mul_eq_zero,
}

[Yakov Pechersky]

exact rfl can also be refl

[Yakov Pechersky]

If you have a tactic you're applying repeatedly to complete, you can use the semicolon ; like so:

theorem R.add_assoc (a b c : R): a + b + c = a + (b + c) :=
begin
   cases a;
   cases b;
   cases c;
   refl
end

[Yakov Pechersky]

"For each a, for each b, for each c, refl".

[Lars Ericson]

Thanks Yakov!

The last one R.eq_zero_or_eq_zero_of_mul_eq_zero didn't follow as much of a pattern as the others.

[Yakov Pechersky]

theorem R.eq_zero_or_eq_zero_of_mul_eq_zero (a b : R) (h: a * b = 0): a = 0 ∨ b = 0:=
begin
  have h0 : 0 = zero := rfl,
  have h1 : 1 = one := rfl,
  rw h0 at *,
  have : one * one ≠ zero,
    { rw [←h1, R.one_mul, h1],
      simp },
  cases a;
  cases b;
  simpa [h] using this <|> simp
end

[Lars Ericson]

There is also an exercise 7b:
Screenshot-from-2021-01-21-19-14-03.png

I give this a passing grade:

import ring_theory.subring
import tactic
import tactic.slim_check
import data.zmod.basic

inductive R
| zero

open R

def R.add : R → R → R
| zero zero := zero

def R.mul : R → R → R
| zero zero := zero

def R.neg : R → R
| zero := zero

instance : has_add R := ⟨R.add⟩
instance : has_mul R := ⟨R.mul⟩
instance : has_zero R := ⟨zero⟩
instance : has_neg R := ⟨R.neg⟩

theorem R.not_exists_pair_ne : ¬ ∃ (x y : R), x ≠ y :=
begin
  intro h,
  cases h with a ha,
  cases ha with b hb,
  cases a,
  cases b,
  finish,
end

[Lars Ericson]

There is also a related 8A:
Screenshot-from-2021-01-21-19-21-37.png

I guess what they are asking is to prove that, if R has every property (including having 1 and the other properties above that involve 1) except 0 not equal to 1, then you can prove that R={0}. I'm not sure quite how to set that up in Lean, because among other things it requires that, other than providing 0 and 1, there may be any number of other elements in R, and then we have to prove that the only element in R is 0.

Which I guess gives me a way of expressing it in Lean: Assuming all properties hold and there are no two different elements, then every element must be the 0 element. Except that you can't even state the other properties that are not claimed to be missing, namely

  --one := R.one,
  --one_mul := R.one_mul,
  --mul_one := R.mul_one ,
  --exists_pair_ne := R.exists_pair_ne,

These can't be expressed at all, except if we assume that one is a synonym for zero. In terms of inductive structure definitions, I don't know how to make that claim, so I guess I have to declare an additional constant after declaring the structure.

[Kyle Miller]

Maybe this is a setup for the Lean version of these problems (using unit as a convenient singleton type):

import algebra.ring
import data.equiv.ring

universes u

def eq_zero_or_eq_zero_of_mul_eq_zero' (α : Type u) [ring α] : Prop :=
∀ a b : α, a * b = 0 → a = 0 ∨ b = 0

def is_zero_ring (α : Type u) [ring α] : Prop := ∀ (x : α), x = 0

instance : comm_ring unit :=
{ zero := (),
  one := (),
  add := λ _ _, (),
  mul := λ _ _, (),
  neg := λ _, (),
  add_assoc := by { intros, refl },
  add_comm := by { intros, refl },
  zero_add := by { rintro ⟨_⟩, refl },
  add_zero := by { rintro ⟨_⟩, refl },
  add_left_neg := by { rintro ⟨_⟩, refl },
  mul_assoc := by { intros, refl },
  mul_comm := by { intros, refl },
  one_mul := by { rintro ⟨_⟩, refl },
  mul_one := by { rintro ⟨_⟩, refl },
  left_distrib := by {intros, refl },
  right_distrib := by {intros, refl } }

lemma prob_7b : eq_zero_or_eq_zero_of_mul_eq_zero' unit :=
sorry

lemma prob_7b' : ¬nontrivial unit :=
sorry

lemma punit_is_zero_ring : is_zero_ring unit :=
sorry

/-- Every zero ring is isomorphic to the above ring. -/
def zero_ring_iso_punit (α : Type u) [ring α] (h : is_zero_ring α) :
  α ≃+* unit :=
{ to_fun := λ _, 0,
  inv_fun := λ _, 0,
  left_inv := λ x, (h x).symm,
  right_inv := by { rintro ⟨_⟩, refl },
  map_add' := by { intros, refl, },
  map_mul' := by { intros, refl, } }

lemma prob_8a (S : Type u) [comm_ring S]
  (h₁ : eq_zero_or_eq_zero_of_mul_eq_zero' S) (h₂ : ¬is_zero_ring S) :
  integral_domain S :=
sorry

[Eric Wieser]

Mathlib already has comm_ring unit as docs#punit.comm_ring

[Lars Ericson]

Thanks for these sketches. Please correct me if I'm wrong, but they both give an explicit carrier set.

I'm trying to wrap my head around the idea of showing that, if I have an arbitrary set of something arbitrary, and it has all the properties of integral_domain except eq_zero_or_eq_zero_of_mul_eq_zero, then the carrier set must be {0}. On paper it's elementary. Stating exactly that in exactly that way I'm not sure how to do in Lean, i.e., without constructing the set except to just set that it is set A for A: Type*. The problem with set A is that I then need to establish things like has_mem for A and I don't have those things, so it gets complicated.

[Eric Wieser]

Did you mean all properties of integral_domain except exists_pair_ne?

[Eric Wieser]

I think your theorem statement is:

import data.equiv.ring
import algebra.punit_instances

example {A : Type*} [comm_ring A] [no_zero_divisors A] (h : (0 : A) = 1) : A ≃+* unit := sorry

[Eric Wieser]

Which reads, if a ring has no zero divisors but has 0 = 1, then it must be isomorphic to the zero ring

[Eric Wieser]

The only interesting part of the proof is docs#subsingleton_of_zero_eq_one

[Eric Wieser]

I was hoping we had this, but we don't:

example {S R : Type*} [subsingleton S] [subsingleton R] [nonempty S] [nonempty R] : R ≃ S := by library_search
-- fails

[Mario Carneiro]

It needs inhabited

[Eric Wieser]

Even then, I can't find it. Is it missing, or am I just missing an import?

example {S R : Type*} [subsingleton S] [subsingleton R] [inhabited S] [inhabited R] : R ≃ S :=
{ to_fun := default _,
  inv_fun := default _,
  left_inv := λ _, subsingleton.elim _ _,
  right_inv := λ _, subsingleton.elim _ _}

[Mario Carneiro]

there might be a theorem saying that subsingleton + inhabited = unique, and an equiv between uniques

[Kyle Miller]

Lars Ericson said:

I'm trying to wrap my head around the idea of showing that, if I have an arbitrary set of something arbitrary, and it has all the properties of integral_domain except eq_zero_or_eq_zero_of_mul_eq_zero, then the carrier set must be {0}.

The only point of bringing in unit as a ring was to say that if every element equaled 0 (i.e., its carrier set is zero), then the ring is isomorphic to unit (see zero_ring_iso_punit) and hence the original ring has the structure described by the problem. You could also prove that if there is an isomorphism, then every element equals 0. You don't really need to talk about the carrier set itself, since the is_zero_ring predicate captures the notion.

But if for some reason you want to talk about carrier sets, you can use set.univ:

lemma zero_ring_carrier_eq_zero (α : Type u) [ring α] :
  is_zero_ring α ↔ (set.univ : set α) = {0} :=
begin
  split,
  { intro h, ext x, simp [h x], },
  { intros h x,
    have h' := set.mem_univ x,
    rw h at h',
    simpa using h', },
end

[Lars Ericson]

I'm trying to understand this. What your definition gives:

def  is_zero_ring (α : Type u) [ring α] : Prop := ∀ (x : α), x = 0

lemma zero_ring_carrier_eq_zero (α : Type u) [ring α] :
  is_zero_ring α ↔ (set.univ : set α) = {0} :=
begin
  split,
  { intro h, ext x, simp [h x], },
  { intros h x,
    have h' := set.mem_univ x,
    rw h at h',
    simpa using h', },
end

is a way of transferring a proof that every element of a type is 0 into a proof that every element of a set of that type equals 0. So it's a technical conversion of type equals {0} to set of type equals {0}.

What the exercise calls for is to prove that if I have a type R which is assumed to have all of the integral_domain properties but exists_pair_ne, then R={0}. The setup for this may or may not involve zero_ring_carrier_eq_zero to transfer from type argument to a set argument.

I think exercise 8A is the converse of 7B. 7B says "{0} → an integral domain except for exists_pair_ne". 8A says that " R is almost an integral domain except for exists_pair_ne → R={0}:
Screenshot-from-2021-01-23-13-42-54.png

[Lars Ericson]

Most importantly, the contents of R are not specified in advance as ∀ (x : α), x = 0. The contents of R are implicitly specified, without being constructed, by satisfying all of the integral_domain properties except exists_pair_ne. So there is no concrete specification of the type, inductive or otherwise. Only implicit specification through the properties.

[Kyle Miller]

I'm not familiar with what book you're following, but presumably it's in terms of set theory. Lean is based in type theory, and it usually takes a bit of translation to get the right idioms. What I was trying to say is "a way to write $S=\{0\}$ in type theory is is_zero_ring S, and if that's not convincing, then zero_ring_carrier_eq_zero shows that S as a set is indeed {0} (where 0 : S is the zero element of type S that ring S gives). This last piece of code is not meant to answer the full exercise -- it's just conceptual for sets vs types -- and it doesn't replace the prob_* lemmas from my earlier comment.

[Kyle Miller]

@Eric Wieser had another translation, too. Both of ours are using that $p \to (q \vee r)$ is $p \to \neg r \to q$ (but we chose a different thing to negate, basically) since the latter form can be more convenient, at least for the theorem statement and proof.

[Kyle Miller]

(I did this conversion because integral_domain S is not a Prop, so you can't $\vee$ it with is_zero_ring S. One way to say something "is" an integral domain is to give a full integral_domain S structure. This isn't exactly the best idea, though, since it doesn't guarantee that this structure has anything to do with the original ring structure on S...)

[Lars Ericson]

Thanks. The book is A survey of modern algebra, 4th edition, by Garret Birkhoff and Saunders Mac Lane. I am trying to start by specifying the list of properties assumed to hold. One problem is that with an abstract type R and hence no definition of 0, 1, plus and mul, I don't have the syntax to state the properties. I got this far:

import ring_theory.subring
import tactic
import tactic.slim_check

variable R: Type*

variable R.add : R → R → R
variable R.mul : R → R → R
variable R.neg : R → R
variable R.zero : R
variable R.one : R

theorem R.zero_add (a : R) (zero: R): zero + a = a := sorry

but I get errors of form

failed to synthesize type class instance for
R : Type u_1,
a zero : R
⊢ has_add R

[Lars Ericson]

I want to just say I have some R and it has these operations like mul : R → R → R and they have these properties:

variable R: Type*
variable R.add : R → R → R
variable R.mul : R → R → R
variable R.neg : R → R
variable R.zero : R
variable R.one : R
theorem R.zero_add (a : R) (zero: R): zero + a = a
theorem R.add_zero (a : R): a + 0 = a
theorem R.add_assoc (a b c : R): a + b + c = a + (b + c)
theorem R.add_left_neg (a : R): -a + a = 0
theorem R.add_comm (a b : R): a + b = b + a
theorem R.mul_assoc (a b c : R): a * b * c = a * (b * c)
theorem R.left_distrib (a b c : R): a * (b + c) = a * b + a * c
theorem R.right_distrib (a b c : R): (a + b) * c = a * c + b * c
theorem R.mul_comm (a b : R): a * b = b * a
theorem R.eq_zero_or_eq_zero_of_mul_eq_zero (a b : R) (h: a * b = 0): a = 0 ∨ b = 0
theorem R.one_mul (a : R): 1 * a = a
theorem R.mul_one (a : R): a * 1 = a
theorem R.not_exists_pair_ne : ¬ ∃ (x y : R), x ≠ y

and the only solution R for the logical system of equations consisting of that set of properties is {0}.

[Kyle Miller]

The idea of typeclasses is that they associate operations and axioms to a type. (α : Type u) [comm_ring α] gives you most of those, except eq_zero_or_eq_zero_of_mul_eq_zero and not_exists_pair_ne

[Kyle Miller]

and it's not specifying anything about α itself (in the sense of inductive definitions)

[Lars Ericson]

Thanks I will look at the source for comm_ring. Without relying on the hierarchy that is already in lean, I want to make a similar thing called almost_integral_domain_without_exists_pair_ne.

[Kyle Miller]

(typeclasses are how we implement "abuse of notation," also known as synecdoche: the α stands in for the commutative ring structure itself because Lean will locate the relevant typeclass instance, which is the commutative ring structure for the type.)

[Kyle Miller]

All an integral_domain is really is a comm_ring with these two additional axioms, so you can work with comm_ring and have these axioms as hypotheses or conclusions in your lemmas/theorems

[Kyle Miller]

though not_exists_pair_ne is implemented with the nontrivial typeclass

[Kyle Miller]

For example, this might be another rendering of problem 8(a):

lemma prob_8a (S : Type u) [comm_ring S] (h : eq_zero_or_eq_zero_of_mul_eq_zero S) :
  is_zero_ring S ∨ not_exists_pair_ne S :=
sorry

with the understanding that a comm_ring satisfying both eq_zero_or_eq_zero_of_mul_eq_zero and not_exists_pair_ne is an integral domain.

[Kyle Miller]

Or packaging up some of this, you could say

structure is_integral_domain (R : Type u) [comm_ring R] : Prop :=
(not_exists_pair_ne : ¬ ∃ (x y : R), x ≠ y)
(eq_zero_or_eq_zero_of_mul_eq_zero : ∀ (a b : R), a * b = 0 → a = 0 ∨ b = 0)

lemma prob_8a (S : Type u) [comm_ring S]
  (h : ∀ (a b : R), a * b = 0 → a = 0 ∨ b = 0) :
  is_zero_ring S ∨ is_integral_domain S :=
sorry

[Eric Wieser]

almost_integral_domain_without_... is just docs#no_zero_divisors, which is what I use I my solution above

[Eric Wieser]

Regarding "it's not a prop so you can't or it", you can use nonempty (integral_domain _) to make it a prop

[Kyle Miller]

Lars Ericson said:

but I get errors of form

failed to synthesize type class instance for
R : Type u_1,
a zero : R
⊢ has_add R

Answering this question, the issue is that you didn't introduce [has_add R] variables -- these are where the + notation comes from.

[Lars Ericson]

Thanks Kyle and Eric. is_integral_domain already exists, so the package becomes:

import ring_theory.subring
import tactic
import tactic.slim_check
import data.equiv.ring
import algebra.punit_instances

universe u

def is_zero_ring (α : Type u) [ring α] : Prop := ∀ (x : α), x = 0

lemma ex8a_kyle_miller (S : Type u) [comm_ring S]
  (h : ∀ (a b : S), a * b = 0 → a = 0 ∨ b = 0) :
  is_integral_domain S ∨ is_zero_ring S :=
sorry

lemma ex8a_eric_wieser {S: Type*} [comm_ring S] [no_zero_divisors S] (h : (0 : S) = 1) : S ≃+* unit :=
sorry

Kyle's version seems more evocative of the exact phrasing of the problem. The proposition

 is_integral_domain S  ∨ is_zero_ring S

directly reflects the problem statement "S is either an integral domain or the system consisting of 0 alone".

I will try to prove both versions. Thanks for the help!

[Eric Wieser]

Yes, I think Kyle's phrasing more directly matches the question

[Eric Wieser]

nonempty (S \equiv+* unit) is equivalent to is_zero_ring S, and the translation is uninteresting

[Kyle Miller]

Eric pointed out no_zero_divisors exists, so you could phrase it as

lemma ex8a_kyle_miller (S : Type u) [comm_ring S] [no_zero_divisors S] :
  is_integral_domain S ∨ is_zero_ring S :=
sorry

This gives hypothesis gives you eq_zero_or_eq_zero_of_mul_eq_zero. (no_zero_divisors is an example of using the typeclass system to provide certain kinds of basic properties of something automatically.)

[Lars Ericson]

Thanks, I will update ex8a_kyle_miller. For Eric's version I was able to prove it just by using the autopilot features on Lean, without really understanding what it says (for example I've never seen ≃+* before):

import ring_theory.subring
import tactic
import tactic.slim_check
import data.equiv.ring
import algebra.punit_instances

universe u

def is_zero_ring (α : Type u) [ring α] : Prop := ∀ (x : α), x = 0

lemma ex8a_eric_wieser {S: Type*} [CR: comm_ring S]
        [NZD: no_zero_divisors S] (h : (0 : S) = 1) : S ≃+* unit :=
begin
  refine ring_equiv.symm _,
  refine {to_fun := _, inv_fun := _, left_inv := _, right_inv := _, map_mul' := _, map_add' := _},
  intro h,
  exact ring.one,
  intro h1,
  exact (),
  rw function.left_inverse,
  intro x,
  exact unit.ext,
  rw function.right_inverse,
  rw function.left_inverse,
  intro x,
  exact eq_of_zero_eq_one h ring.one x,
  intro u1,
  intro u2,
  ring,
  exact eq_of_zero_eq_one h ring.one (ring.one * ring.one),
  intro u1,
  intro u2,
  exact eq_of_zero_eq_one h ring.one (ring.one + ring.one),
end

[Eric Wieser]

Proving Kyle's should be easy after by_cases h : (0 : R) = 1

[Lars Ericson]

Yes, thanks, here it is:

import ring_theory.subring
import tactic
import tactic.slim_check
import data.equiv.ring
import algebra.punit_instances

universe u

def is_zero_ring (α : Type u) [ring α] : Prop := ∀ (x : α), x = 0

lemma ex8a_kyle_miller (S : Type u) [comm_ring S] [no_zero_divisors S] :
  is_integral_domain S ∨ is_zero_ring S :=
begin
  by_cases h: (1:S) ≠ (0:S),
  fconstructor,
  refine {exists_pair_ne := _, mul_comm := _, eq_zero_or_eq_zero_of_mul_eq_zero := _},
  use [0,1],
  refine ne_comm.mp _,
  assumption,
  exact mul_comm,
  exact λ {a b : S}, mul_eq_zero.mp,
  refine or.inr _,
  rw is_zero_ring,
  refine eq_zero_of_zero_eq_one _,
  finish,
end

[Lars Ericson]

Exercise 8B is "Is 0≠1 used in proving Rules 1-9?". These rules are as follows, I think the answer is No (these are all provided from the definition of commutative ring):

import algebra.ring.basic

universe u

variables {α : Type u} [comm_ring α] {a b c d z x₁ x₂ :  α}

lemma rule_1 : (a+b)*c=a*c+b*c := add_mul _ _ _
lemma rule_2_plus : (0 + a = a) := zero_add _
lemma rule_2_times : (1 * a = a) := one_mul _

lemma rule_3 : (∀ (a : α), a + z = a) → z = 0 :=
begin
  intro h1,
  have h2 := h1 0,
  exact add_left_eq_self.mp (congr_arg (has_add.add z) (congr_arg (has_add.add z) (h1 z))),
end

lemma rule_4 : a + b = a + c → b = c := (add_right_inj a).mp

lemma rule_5 : a + x₁ = 0 → a + x₂ = 0 → x₁ = x₂ :=
begin
  intro h1,
  intro h2,
  exact neg_unique h1 h2,
end

lemma rule_6 : a + x₁ = b → a + x₂ = b → x₁ = x₂ :=
begin
  intro h1,
  intro h2,
  rw ← h1 at h2,
  exact rule_4 (eq.symm h2),
end

lemma rule_7a : a * 0 = 0 := mul_zero a
lemma rule_7b  : 0 * a = 0 := zero_mul a

lemma rule_8 : (∀ (a : α), a*z = a) → z = 1 :=
begin
  intro h1,
  exact (eq_one_iff_eq_one_of_mul_eq_one (h1 1)).mp rfl,
end

lemma rule_9 : (-a)*(-b) = a*b := neg_mul_neg _ _