Zulip Chat Archive

Stream: general

Topic: ring of injective


view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 14 2019 at 09:14):

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

view this post on Zulip Johan Commelin (Jun 14 2019 at 15:38):

@Kenny Lau How would you prove this?

view this post on Zulip Kenny Lau (Jun 14 2019 at 16:12):

lemme see...

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 14 2019 at 17:04):

Huh? This should be provable, right?

view this post on Zulip Kenny Lau (Jun 14 2019 at 17:07):

like I can't prove it using tactics

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 14 2019 at 17:14):

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

view this post on Zulip Johan Commelin (Jun 14 2019 at 17:16):

What exactly is the elaboration issue?

view this post on Zulip Kenny Lau (Jun 14 2019 at 17:21):

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

view this post on Zulip Kenny Lau (Jun 14 2019 at 17:21):

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

view this post on Zulip Johan Commelin (Jun 14 2019 at 17:25):

Hmm, that's sad...

view this post on Zulip Johan Commelin (Jun 14 2019 at 17:26):

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

view this post on Zulip Johan Commelin (Jun 14 2019 at 17:26):

I guess I will just manually proof all the goals

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Jun 14 2019 at 17:42):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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 +.

view this post on Zulip 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."

view this post on Zulip Johan Commelin (Jun 14 2019 at 17:56):

The Lean proof should be

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

view this post on Zulip 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 },
    try {simp [mul_assoc, mul_add, add_mul] } },
    rw mul_comm,
end

view this post on Zulip Kenny Lau (Jun 14 2019 at 19:19):

so we should have esimp

view this post on Zulip Reid Barton (Jun 14 2019 at 19:24):

Sounds eslow

view this post on Zulip Koundinya Vajjha (Jun 14 2019 at 19:31):

I never could understand how erw is different from rw.

view this post on Zulip 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 },
    simp [mul_assoc, mul_add, add_mul] },
  rw mul_comm
end

end

view this post on Zulip Johan Commelin (Jun 14 2019 at 20:54):

Yep, I also found that one.

view this post on Zulip Johan Commelin (Jun 14 2019 at 20:54):

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

view this post on Zulip Johan Commelin (Jun 14 2019 at 20:54):

But it works (-;

view this post on Zulip 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 }, },
  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

view this post on Zulip Jesse Michael Han (Jun 15 2019 at 04:48):

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.


Last updated: May 15 2021 at 00:39 UTC