## Stream: general

### Topic: ring of injective

#### Johan Commelin (Jun 14 2019 at 08:36):

How do I prove this in a one-liner:

section
open function
variables {α : Type*} [has_zero α] [has_one α] [has_add α] [has_mul α] [has_neg α]
variables {β : Type*} [comm_ring β]

def comm_ring_of_injective (f : α → β) (inj : injective f)
(zero : f 0 = 0) (one : f 1 = 1) (add : ∀ {x y}, f (x + y) = f x + f y)
(mul : ∀ {x y}, f (x * y) = f x * f y) (neg : ∀ {x}, f (-x) = - f x) :
comm_ring α :=
begin
refine_struct { ..‹has_zero α›, ..‹has_one α›, ..‹has_add α›, ..‹has_mul α›, ..‹has_neg α› },
all_goals {sorry}
end

end


#### Johan Commelin (Jun 14 2019 at 09:00):

I was hoping that all_goals { intros, apply inj, simp [zero, one, mul, add, neg] }, would close most of the goals. But it doesn't...

#### Kevin Buzzard (Jun 14 2019 at 09:04):

I guess we have some instance that says that a subgroup of a group is a group. Maybe there is some analogous instance that a subring of a ring is a ring. So you could just use this instance and then transfer the structure over to alpha via the canonical bijection.

#### Johan Commelin (Jun 14 2019 at 09:13):

I was hoping there would be a 1-line tactic proof that works with the current state of mathlib... transfer doesn't currently work.

#### Kevin Buzzard (Jun 14 2019 at 09:14):

Oh well, stick it on the list at https://github.com/leanprover-community/mathlib/issues/408

#### Johan Commelin (Jun 14 2019 at 15:38):

@Kenny Lau How would you prove this?

lemme see...

#### Kenny Lau (Jun 14 2019 at 16:41):

I can't prove it. It's because of + being elaborated differently in the two different contexts.

#### Johan Commelin (Jun 14 2019 at 17:04):

Huh? This should be provable, right?

#### Kenny Lau (Jun 14 2019 at 17:07):

like I can't prove it using tactics

#### Johan Commelin (Jun 14 2019 at 17:14):

Any proof is fine... but I expected/hoped that a tactic proof would be way shorter than a term-mode proof

#### Kenny Lau (Jun 14 2019 at 17:14):

as in I can't prove it using a few lines

#### Johan Commelin (Jun 14 2019 at 17:16):

What exactly is the elaboration issue?

#### Kenny Lau (Jun 14 2019 at 17:21):

in add, the + is @has_add.add \a _inst_3 or something like that

#### Kenny Lau (Jun 14 2019 at 17:21):

but in the goals it is @has_add.add \a (semigroup.to_has_add ...) etc

#### Johan Commelin (Jun 14 2019 at 17:26):

I also need the dual version, with a surjective map...

#### Johan Commelin (Jun 14 2019 at 17:26):

I guess I will just manually proof all the goals

#### Andrew Ashworth (Jun 14 2019 at 17:39):

I'm just now sort of getting an inkling of why everyone wants a beefed up transfer, since I rarely deal in very abstract types. But I'm unsure of why people think a 1-line proof is possible. For any map between two types equipped with a ring instance you will always have to prove that it is a ring homomorphism, right? Isn't isomorphism in the context of rings an equivalence relation, so you could use the same machinery to reason about them? (sorry if this observation sounds incredibly stupid to those who have spent much more time thinking about this sort of thing)

#### Kevin Buzzard (Jun 14 2019 at 17:42):

Mathematicians look at the question and cannot see what the issue is.

#### Kevin Buzzard (Jun 14 2019 at 17:43):

alpha is a subset of beta closed under all the operations and it will inherit all of the axioms automatically -- of course it's a ring. What frustrates us is that apparently this is not obvious to computer scientists.

#### Kevin Buzzard (Jun 14 2019 at 17:44):

Johan's assumptions identify alpha with a subtype of beta in a way which preserves everything of interest, so whatever is there left to check?

#### Kevin Buzzard (Jun 14 2019 at 17:45):

Mathematicians have a zero-line proof that alpha is a ring. In a maths lecture you would just deduce it immediately.

#### Kevin Buzzard (Jun 14 2019 at 17:47):

For example f (x + y) = f x + f y and injectivity of f immediately imply associativity of alpha's + because we imagine alpha as literally being a subset of beta with the induced +.

#### Johan Commelin (Jun 14 2019 at 17:55):

Here is the one-line maths proof:
"All the data is there, and f is structure preserving. The ring axioms are universal formulas in the language of rings. Since f is injective this means we are done."

#### Johan Commelin (Jun 14 2019 at 17:56):

The Lean proof should be

all_goals { intros, apply inj, simp [*] }


#### Johan Commelin (Jun 14 2019 at 18:21):

@Kenny Lau erw helps. This is what I've got for the surjective variant:

def comm_ring_of_surjective (f : β → α') (sur : surjective f)
(zero : f 0 = 0) (one : f 1 = 1) (add : ∀ {x y}, f (x + y) = f x + f y)
(mul : ∀ {x y}, f (x * y) = f x * f y) (neg : ∀ {x}, f (-x) = - f x) :
comm_ring α' :=
begin
refine_struct { ..‹has_zero α'›, ..‹has_one α'›, ..‹has_add α'›, ..‹has_mul α'›, ..‹has_neg α'› },
all_goals {
try { intro a, rcases sur a with ⟨a, rfl⟩ },
try { intro b, rcases sur b with ⟨b, rfl⟩ },
try { intro c, rcases sur c with ⟨c, rfl⟩ },
repeat { erw ← zero <|> erw ← one <|> erw ← add <|> erw ← mul <|> erw ← neg },
rw mul_comm,
end


#### Kenny Lau (Jun 14 2019 at 19:19):

so we should have esimp

Sounds eslow

#### Koundinya Vajjha (Jun 14 2019 at 19:31):

I never could understand how erw is different from rw.

#### Kenny Lau (Jun 14 2019 at 20:51):

import tactic.interactive

section
open function
variables {α : Type*} [has_zero α] [has_one α] [has_add α] [has_mul α] [has_neg α]
variables {β : Type*} [comm_ring β]

def comm_ring_of_injective (f : α → β) (inj : injective f)
(zero : f 0 = 0) (one : f 1 = 1) (add : ∀ {x y}, f (x + y) = f x + f y)
(mul : ∀ {x y}, f (x * y) = f x * f y) (neg : ∀ {x}, f (-x) = - f x) :
comm_ring α :=
begin
refine_struct { ..‹has_zero α›, ..‹has_one α›, ..‹has_add α›, ..‹has_mul α›, ..‹has_neg α› },
all_goals { intros, apply inj, repeat { erw zero <|> erw one <|> erw add <|> erw mul <|> erw neg },
rw mul_comm
end

end


#### Johan Commelin (Jun 14 2019 at 20:54):

Yep, I also found that one.

#### Johan Commelin (Jun 14 2019 at 20:54):

It's sad that it seems a bit slow...

But it works (-;

#### Kenny Lau (Jun 14 2019 at 20:58):

import tactic.interactive

section
open function
variables {α : Type*} [has_zero α] [has_one α] [has_add α] [has_mul α] [has_neg α]
variables {β : Type*} [comm_ring β]

set_option profiler true
-- elaboration of comm_ring_of_injective took 493ms
def comm_ring_of_injective (f : α → β) (inj : injective f)
(zero : f 0 = 0) (one : f 1 = 1) (add : ∀ {x y}, f (x + y) = f x + f y)
(mul : ∀ {x y}, f (x * y) = f x * f y) (neg : ∀ {x}, f (-x) = - f x) :
comm_ring α :=
begin
refine_struct { ..‹has_zero α›, ..‹has_one α›, ..‹has_add α›, ..‹has_mul α›, ..‹has_neg α› },
all_goals { intros, apply inj,
repeat { erw mul }, repeat { erw add }, repeat { erw mul },
try { erw neg }, try { erw zero }, try { erw one }, },
mul_assoc _ _ _, one_mul _, mul_one _, mul_add _ _ _, add_mul _ _ _, mul_comm _ _]
end

end


#### Jesse Michael Han (Jun 15 2019 at 04:48):

I never could understand how erw is different from rw.

meta def rewrite (q : parse rw_rules) (l : parse location) (cfg : rewrite_cfg := {}) : tactic unit :=

The difference is that rewrite_core is allowed to peek into semireducible definitions, where reducible is the default. This means you need to do less explicit unfolding for your rewrites to succeed, but because more definitions are exposed and unification is expensive, erw can be an order of magnitude slower.