ring of injective

Stream: general

[Johan Commelin]

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]

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]

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]

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]

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

[Johan Commelin]

@Kenny Lau How would you prove this?

[Kenny Lau]

lemme see...

[Kenny Lau]

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

[Johan Commelin]

Huh? This should be provable, right?

[Kenny Lau]

like I can't prove it using tactics

[Johan Commelin]

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

[Kenny Lau]

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

[Johan Commelin]

What exactly is the elaboration issue?

[Kenny Lau]

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

[Kenny Lau]

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

[Johan Commelin]

Hmm, that's sad...

[Johan Commelin]

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

[Johan Commelin]

I guess I will just manually proof all the goals

[Andrew Ashworth]

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]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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]

The Lean proof should be

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

[Johan Commelin]

@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 },
    try {simp [mul_assoc, mul_add, add_mul] } },
    rw mul_comm,
end

[Kenny Lau]

so we should have esimp

[Reid Barton]

Sounds eslow

[Koundinya Vajjha]

I never could understand how erw is different from rw.

[Kenny Lau]

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 },
    simp [mul_assoc, mul_add, add_mul] },
  rw mul_comm
end

end

[Johan Commelin]

Yep, I also found that one.

[Johan Commelin]

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

[Johan Commelin]

But it works (-;

[Kenny Lau]

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 }, },
  exacts [add_assoc _ _ _, zero_add _, add_zero _, add_left_neg _, add_comm _ _,
    mul_assoc _ _ _, one_mul _, mul_one _, mul_add _ _ _, add_mul _ _ _, mul_comm _ _]
end

end

[Jesse Michael Han]

I never could understand how erw is different from rw.

The source is quite transparent about this:

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

meta def erewrite (q : parse rw_rules) (l : parse location) (cfg : rewrite_cfg := {md := semireducible}) : tactic unit :=
propagate_tags (rw_core q l cfg)

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.