# Zulip Chat Archive

## 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_add R := ⟨R.add⟩
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
rw R.add
```

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_add.add,
unfold has_zero.zero,
rw R.add,
rw R.zero,
simp [int.zero_add]
end
theorem R.zero_add' (a : R): (0:R) + a = a :=
by ext; exact int.zero_add _
```

#### 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
⊢ has_add 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_add R := ⟨R.add⟩
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,
unfold has_add.add,
rw R.add,
simp [int.zero_add],
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,
unfold has_add.add,
rw R.add,
simp [int.zero_add],
end
theorem R.add_assoc (a b c : R): a + b + c = a + (b + c) :=
begin
cases a;
cases b;
cases c;
unfold has_add.add,
repeat { rw R.add },
finish,
end
theorem R.add_left_neg (a : R): -a + a = 0 :=
begin
cases a,
unfold has_neg.neg,
unfold has_add.add,
rw R.neg,
rw R.add,
finish,
end
theorem R.add_comm (a b : R): a + b = b + a :=
begin
cases a;
cases b;
unfold has_add.add,
repeat { rw R.add },
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,
unfold has_add.add,
repeat { rw R.add },
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,
unfold has_add.add,
repeat { rw R.add },
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_add R := ⟨R.add⟩
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,
unfold has_add.add,
rw R.add,
simp [int.zero_add],
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,
unfold has_add.add,
rw R.add,
simp [int.zero_add],
end
theorem R.add_assoc (a b c : R): a + b + c = a + (b + c) :=
begin
ext,
unfold has_add.add,
repeat { rw R.add },
finish,
end
theorem R.add_left_neg (a : R): -a + a = 0 :=
begin
ext,
unfold has_neg.neg,
unfold has_add.add,
rw R.neg,
rw R.add,
finish,
end
theorem R.add_comm (a b : R): a + b = b + a :=
begin
ext,
unfold has_add.add,
repeat { rw R.add },
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,
unfold has_add.add,
repeat { rw R.add },
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,
unfold has_add.add,
repeat { rw R.add },
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
```

and then you wouldn't need to write the lemmas about addition, only the ones about multiplication

Last updated: May 11 2021 at 00:31 UTC