How to expand 0 and structure defs

Stream: new members

[Lars Ericson]

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]

cases a will destruct a into its constituents.

[Lars Ericson]

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]

@[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]

I'm abusing definitional equality in the second proof.

[Yakov Pechersky]

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]

So you can avoid unfold

[Lars Ericson]

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]

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]

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]

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

[Kyle Miller]

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]

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]

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

[Lars Ericson]

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]

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