to_additive & exponents

Stream: general

[Eric Rodriguez]

I was trying to define this lemma (in group_theory/exponent):

--@[to_additive]
lemma exponent_eq_zero_iff : exponent G = 0 ↔ ¬ exponent_exists G :=
begin
  rw [monoid.exponent],
  split_ifs with h; simp [h]
end

however, when I try uncomment to_additive, it has an absolute fit. if i make the lemma by hand and say to_additive afterwards, it still completely breaks. I tried the troubleshooting steps and still am no closer to understanding what's up

[Eric Wieser]

Does it still fail if you replace the proof with sorry?

[Eric Rodriguez]

nope!

[Eric Rodriguez]

I'm really not sure why my autopilot brain decided that no translated to yes...

[Eric Wieser]

If it succeeds with sorry, that suggests one of the lemmas simp is finding is missing a to_additive or is tagged incorrectly

[Eric Rodriguez]

ok, this works:

@[to_additive]
lemma exponent_eq_zero_iff : exponent G = 0 ↔ ¬ exponent_exists G :=
begin
  rw [monoid.exponent],
  split_ifs with h,
  simp only [h, nat.find_eq_zero, not_true, @not_lt_zero' ℕ, false_and],--simp [h],
  simp only [h, eq_self_iff_true, not_false_iff],
end

[Eric Rodriguez]

this works... for some reason it wants to turn that not_lt_zero into something to do with the monoid, even though it's only used on ℕ

[Eric Rodriguez]

which I think may be because of its weird argument order; it's stated as {α} {x : α} [linear_ordered_comm_monoid α]

[Floris van Doorn]

Is this the error you got in the original example? I'll try to debug

type mismatch at application
  @linear_ordered_add_comm_monoid.to_linear_order α
    (@linear_ordered_comm_monoid_with_zero.to_linear_ordered_comm_monoid α _inst_1)
term
  @linear_ordered_comm_monoid_with_zero.to_linear_ordered_comm_monoid α _inst_1
has type
  linear_ordered_comm_monoid α
but is expected to have type
  linear_ordered_add_comm_monoid α

[Floris van Doorn]

Adding this line before fixes it:

attribute [to_additive] linear_ordered_comm_monoid_with_zero.to_linear_ordered_comm_monoid

I'll make a PR

[Floris van Doorn]

wait... but additivizing that declaration doesn't make sense...

[Floris van Doorn]

I think the problem is that the original proof works for the multiplicative case, but not for an additive one?

[Eric Rodriguez]

that lemma is only used for ℕ, if you see an alternative version that works

[Eric Rodriguez]

but I think the weird argument order means that to_additive's heuristic tries to additivize it in the proof

[Floris van Doorn]

"that lemma" = exponent_eq_zero_iff?

[Eric Rodriguez]

not_lt_zero'

[Eric Rodriguez]

used by simp in the proof

[Eric Rodriguez]

if I change the simp input to @not_lt_zero' ℕ it works fine

[Floris van Doorn]

I don't think @not_lt_zero' is the culprit. Also, the order of the arguments shouldn't matter, as long as α is the first argument.

[Floris van Doorn]

oh, maybe it does, the α threw me off...

[Eric Rodriguez]

image.png it looks like this in the final proof, which I think is what's tripping things up

[Floris van Doorn]

Yeah, I'm also looking at that right now. The problem is that simp generates the subterm

@(λ {α : Type} {a : α} [_inst_1 : linear_ordered_comm_monoid_with_zero α],
                                  @iff_false_intro (a < 0) (@not_lt_zero' α a _inst_1))
                                 ℕ
                                 0
                                 nat.linear_ordered_comm_monoid_with_zero)

This cannot be to_additive-ized correctly, since linear_ordered_comm_monoid_with_zero has no additive version, but linear_ordered_add_comm_monoid.to_linear_order (used as implicit argument) does.
If we would (beta) reduce the expression, we just get

@iff_false_intro (0 < 0) (@not_lt_zero' ℕ 0 nat.linear_ordered_comm_monoid_with_zero))

which will be additivized correctly. (that is, by changing nothing, since it is applied to ℕ)

[Floris van Doorn]

I'm not sure what the best solution is here, maybe just using the workaround by giving simp some extra information (simp [h, nat.not_lt_zero] and simp [h, -not_lt_zero'] both work)

[Floris van Doorn]

(though using @not_lt_zero' ℕ is better, since we might get rid of nat.not_lt_zero at some point)