Zulip Chat Archive

Stream: general

Topic: putting algebra in mathlib


view this post on Zulip Johan Commelin (May 16 2020 at 09:21):

I'm trying to put the algebra from core back into mathlib.
I'm hitting an error in data/int/basic:

1 goal
α : Type u_1,
_inst_1 : ring α,
cast_mul :  (m n : ), (m * n) = m * n,
m n : 
 -((m + 1) * n) = -(m + 1) * n
basic.lean:1193:5: error
rewrite tactic failed, did not find instance of the pattern in the target expression
  -(?m_1 * ?m_2)
state:
α : Type u_1,
_inst_1 : ring α,
cast_mul :  (m n : ), (m * n) = m * n,
m n : 
 -((m + 1) * n) = -(m + 1) * n

view this post on Zulip Johan Commelin (May 16 2020 at 09:22):

@[simp, norm_cast] theorem cast_mul [ring α] :  m n, ((m * n : ) : α) = m * n
| (m : ) (n : ) := nat.cast_mul _ _
| (m : ) -[1+ n] := (cast_neg_of_nat _).trans $
  show (-(m * (n + 1) : ) : α) = m * -(n + 1),
  by rw [nat.cast_mul, nat.cast_add_one, neg_mul_eq_mul_neg]
| -[1+ m] (n : ) := (cast_neg_of_nat _).trans $
  show (-((m + 1) * n : ) : α) = -(m + 1) * n,
  by rw [nat.cast_mul, nat.cast_add_one, neg_mul_eq_neg_mul]
  -- ^ error is here
| -[1+ m] -[1+ n] := show (((m + 1) * (n + 1) : ) : α) = -(m + 1) * -(n + 1),
  by rw [nat.cast_mul, nat.cast_add_one, nat.cast_add_one, neg_mul_neg]

view this post on Zulip Johan Commelin (May 16 2020 at 09:22):

Of course I can fix it. But I'm trying to understand where the error came from in the first place. I would rather fix the root issue.

view this post on Zulip Johan Commelin (May 16 2020 at 09:24):

Ooh, never mind... that line has neg_mul_eq_neg_mul :face_palm:
which is not the same as neg_mul_eq_mul_neg

view this post on Zulip Johan Commelin (May 16 2020 at 09:24):

So I need to make more things protected. (-;

view this post on Zulip Johan Commelin (May 16 2020 at 09:24):

Thanks for rubberducking!

view this post on Zulip Johan Commelin (May 16 2020 at 10:04):

#2697 puts algebra back in mathlib (this depends on a new lean release). Currently the branch builds number_theory/quadratic_reciprocity without errors.

view this post on Zulip Johan Commelin (May 16 2020 at 10:05):

There are some errors in category_theory, but I think this is due to other changes in the newest version of lean.

view this post on Zulip Yury G. Kudryashov (May 16 2020 at 10:08):

Is there some nightly/hourly/whatever version of lean that we can put into leanpkg.toml instead of local?

view this post on Zulip Sebastien Gouezel (May 16 2020 at 10:08):

This means we will be able to remove the simp attribute on one_div_eq_inv, among many many other things. Thanks so much!

view this post on Zulip Johan Commelin (May 16 2020 at 10:42):

A second iteration of this might also move the order hierarchy out of core. I didn't do that now, because I don't really have a need for it. And I wanted to keep this "small" (-;
Yes, I'm excited about all the tiny little fixes that we can now start making.

view this post on Zulip Yury G. Kudryashov (May 16 2020 at 11:38):

We still have

/-- this is needed for compatibility between Lean 3.4.2 and Lean 3.5.1c -/
def has_div_of_division_ring [division_ring α] : has_div α := division_ring_has_div

in algebra/ring

view this post on Zulip Johan Commelin (May 16 2020 at 13:44):

@Yury G. Kudryashov Sorry, I'm slow. What is your point? I've moved everything out of core, right? So this is stuff that we can now leisurely fix.

view this post on Zulip Johan Commelin (May 16 2020 at 13:45):

Or am I missing something?


Last updated: May 18 2021 at 17:44 UTC