## Stream: new members

### Topic: How to expand 0 and structure defs

#### Lars Ericson (Jan 24 2021 at 00:09):

I am working with a structure with an unusual multiplication operation:

import tactic

structure R := mk :: (x : ℤ)

open R

def R.add (a b : R) := mk (a.x + b.x)
def R.mul (a b : R) := mk 0
def R.neg (a : R) := mk (-a.x)
def R.zero : R := mk 0
def R.one : R := mk 1

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

theorem R.zero_add (a : R): (0:R) + a = a :=
begin
sorry
end


I want to start proving theorems about the structure, for example zero_add. At the point of the sorry, the tactic state is:

a: R
⊢ 0 + a = a


In the goal, is there a way to reduce 0 to {x := int.of_nat 0} and a to {x := int.of_nat a}? I tried the following without success:

rw R.zero
rw R


These had no effect. I also tried:

ring,
simp,
ext,
substs,
library_search,
hint,
suggest,


and didn't get anywhere.

#### Yakov Pechersky (Jan 24 2021 at 00:18):

cases a will destruct a into its constituents.

#### Lars Ericson (Jan 24 2021 at 00:49):

Thanks Yakov! What about the 0? cases a gets me here:

a: ℤ
⊢ 0 + {x := a} = {x := a}


for

theorem R.zero_add (a : R): (0:R) + a = a :=
begin
cases a,
sorry,
end


and doing these doesn't help:

rw R.zero
unfold 0
ext
refl


doesn't expand. If I do

#reduce (0:R)


I get

{x := int.of_nat 0}


which is what I'm hoping for.

#### Yakov Pechersky (Jan 24 2021 at 01:05):

@[ext] lemma ext (a b : R) : a.x = b.x → a = b :=
by cases a; cases b; simp

theorem R.zero_add (a : R): (0:R) + a = a :=
begin
ext,
unfold has_zero.zero,
rw R.zero,
end

theorem R.zero_add' (a : R): (0:R) + a = a :=


#### Yakov Pechersky (Jan 24 2021 at 01:05):

I'm abusing definitional equality in the second proof.

#### Yakov Pechersky (Jan 24 2021 at 01:06):

For your structure, you'll want some very basic API lemmas that say that 0 = R.zero, a + b = R.add a b, etc.

#### Yakov Pechersky (Jan 24 2021 at 01:06):

So you can avoid unfold

#### Lars Ericson (Jan 24 2021 at 01:14):

Thanks! The lesson learned is that to expand 0 or + I need to do an unfold of the has_X and then an rw of the op.

The problem I am working on is 9:
Screenshot-from-2021-01-23-20-11-54.png

I did this setup:

structure R := mk :: (x : ℤ)

open R

def R.mul (a b : R) := mk 0


To get integers but with multiplication altered. I don't know if there is a more approved way to do this kind of temporary structure modfication to explore the consequence of a variation in the rules.

#### Kyle Miller (Jan 24 2021 at 01:16):

Probably the two main ways are using a structure like you did, or using a def like

def R := ℤ


since typeclass resolution won't look at the definition of R to try to, for example, find a ring structure, so you're safe defining a new one.

#### Lars Ericson (Jan 24 2021 at 01:20):

I think I need to stick with structure because if I try this:

import tactic

def R := ℤ

def R.add (a b : R) := a+b


I can't take integer plus for granted, it complains:

failed to synthesize type class instance for
a b : R
foo24.lean:8:4


It seems easier to build the small structure because it fits into the rest of the mathlib framework better.

#### Kyle Miller (Jan 24 2021 at 01:20):

def R.add (a b : R) := (a+b : ℤ)


#### Kyle Miller (Jan 24 2021 at 01:22):

The rule I hear repeated is that typeclass resolution goes "outside-in". Here, the ℤ ends up being a hint to Lean that you want the addition for ℤ rather than R, and since R = ℤ, there are no type errors.

#### Lars Ericson (Jan 24 2021 at 01:54):

And so that finishes Exercise 9:

import tactic

namespace ex9

structure R := mk :: (x : ℤ)

open R

def R.add (a b : R) := mk (a.x + b.x)
def R.mul (a b : R) := mk 0
def R.neg (a : R) := mk (-a.x)
def R.zero : R := mk 0
def R.one : R := mk 1

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

@[ext] lemma ext (a b : R) : a.x = b.x → a = b := -- Yakov Pechersky
by cases a; cases b; simp

theorem R.zero_add (a : R): (0:R) + a = a :=
begin
ext,
cases a,
unfold has_zero.zero,
rw R.zero,
end

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

theorem R.add_zero (a : R): a + 0 = a :=
begin
ext,
cases a,
unfold has_zero.zero,
rw R.zero,
end

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

theorem R.add_left_neg (a : R): -a + a = 0 :=
begin
cases a,
unfold has_neg.neg,
rw R.neg,
finish,
end

theorem R.add_comm (a b : R): a + b = b + a :=
begin
cases a;
cases b;
finish,
end

theorem R.mul_assoc (a b c : R): a * b * c = a * (b * c) :=
begin
cases a;
cases b;
cases c;
unfold has_mul.mul,
repeat { rw R.mul },
end

theorem R.left_distrib (a b c : R): a * (b + c) = a * b + a * c :=
begin
cases a;
cases b;
cases c;
unfold has_mul.mul,
repeat { rw R.mul },
finish,
end

theorem R.right_distrib (a b c : R): (a + b) * c = a * c + b * c :=
begin
cases a;
cases b;
cases c;
unfold has_mul.mul,
repeat { rw R.mul },
finish,
end

theorem R.mul_comm (a b : R): a * b = b * a :=
begin
cases a;
cases b;
unfold has_mul.mul,
repeat { rw R.mul },
end

lemma R.not_one_mul_or_mul_one: (1:R) * (1:R) ≠ (1:R):=
begin
unfold has_one.one,
unfold has_mul.mul,
rw R.one,
rw R.mul,
finish,
end

lemma R.not_eq_zero_or_eq_zero_of_mul_eq_zero : ¬∀ (a b : R), a * b = (0:R) → (a = (0:R) ∨ b = (0:R)) :=
begin
unfold has_mul.mul,
unfold has_zero.zero,
rw R.zero,
simp at *,
use (1:R),
use (1:R),
rw R.mul,
split,
simp,
intro h,
simp at *,
unfold has_one.one at h,
rw R.one at h,
simp at h,
assumption,
end

end ex9


#### Yakov Pechersky (Jan 24 2021 at 02:00):

I think if you're doing ext, you won't have to do cases a.

#### Lars Ericson (Jan 24 2021 at 02:04):

Thanks, no more cases:

import tactic

namespace ex9

structure R := mk :: (x : ℤ)

open R

def R.add (a b : R) := mk (a.x + b.x)
def R.mul (a b : R) := mk 0
def R.neg (a : R) := mk (-a.x)
def R.zero : R := mk 0
def R.one : R := mk 1

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

@[ext] lemma ext (a b : R) : a.x = b.x → a = b := -- Yakov Pechersky
by cases a; cases b; simp

theorem R.zero_add (a : R): (0:R) + a = a :=
begin
ext,
unfold has_zero.zero,
rw R.zero,
end

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

theorem R.add_zero (a : R): a + 0 = a :=
begin
ext,
unfold has_zero.zero,
rw R.zero,
end

theorem R.add_assoc (a b c : R): a + b + c = a + (b + c) :=
begin
ext,
finish,
end

theorem R.add_left_neg (a : R): -a + a = 0 :=
begin
ext,
unfold has_neg.neg,
rw R.neg,
finish,
end

theorem R.add_comm (a b : R): a + b = b + a :=
begin
ext,
finish,
end

theorem R.mul_assoc (a b c : R): a * b * c = a * (b * c) :=
begin
ext,
unfold has_mul.mul,
repeat { rw R.mul },
end

theorem R.left_distrib (a b c : R): a * (b + c) = a * b + a * c :=
begin
ext,
unfold has_mul.mul,
repeat { rw R.mul },
finish,
end

theorem R.right_distrib (a b c : R): (a + b) * c = a * c + b * c :=
begin
ext,
unfold has_mul.mul,
repeat { rw R.mul },
finish,
end

theorem R.mul_comm (a b : R): a * b = b * a :=
begin
ext,
unfold has_mul.mul,
repeat { rw R.mul },
end

lemma R.not_one_mul_or_mul_one: (1:R) * (1:R) ≠ (1:R):=
begin
unfold has_one.one,
unfold has_mul.mul,
rw R.one,
rw R.mul,
finish,
end

lemma R.not_eq_zero_or_eq_zero_of_mul_eq_zero : ¬∀ (a b : R), a * b = (0:R) → (a = (0:R) ∨ b = (0:R)) :=
begin
unfold has_mul.mul,
unfold has_zero.zero,
rw R.zero,
simp at *,
use (1:R),
use (1:R),
rw R.mul,
split,
simp,
intro h,
simp at *,
unfold has_one.one at h,
rw R.one at h,
simp at h,
assumption,
end

end ex9


#### Eric Wieser (Jan 24 2021 at 08:31):

You could use

@[derive add_comm_group]
def R := \Z