to_additive conjures with_zero

Stream: general

[Yakov Pechersky]

Here is a somewhat mwe of a weird to_additive issue I am hitting. Why is it erroring with:

type mismatch at application
  @linear_ordered_add_comm_monoid.to_ordered_add_comm_monoid α
    (@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 α

My proofs don't even mention any α, nor does the sorried proof below talk about any order on S itself...

import algebra.order.with_zero

variables {S : Type*}

section

variables [has_mul S] (x : S) (p : ℕ+) (n : ℕ)

-- use `x * pnpow_rec n x` and not `pnpow_rec n x * x` in the definition to make sure that
-- definitional unfolding of `pnpow_rec` is blocked, to avoid deep recursion issues.
/-- The fundamental power operation in a monoid. `pnpow_rec n a = a*a*...*a` n times.
Use instead `a ^ n`,  which has better definitional behavior. -/
def pnpow_rec {S : Type*} [has_mul S] : ℕ+ → S → S :=
λ n, pnat.rec_on n id (λ _ f x, x * f x)

/-- The fundamental scalar multiplication in an additive monoid. `pnsmul_rec n a = a+a+...+a` n
times. Use instead `n • a`, which has better definitional behavior. -/
def pnsmul_rec {S : Type*} [has_add S] : ℕ+ → S → S :=
λ n, pnat.rec_on n id (λ _ f x, x + f x)

attribute [to_additive pnsmul_rec] pnpow_rec

instance has_mul.has_pow {M : Type*} [has_mul M] : has_pow M ℕ+ := ⟨λ x n, pnpow_rec n x⟩

instance has_add.has_scalar_pnat {M : Type*} [has_add M] : has_scalar ℕ+ M :=
⟨pnsmul_rec⟩

attribute [to_additive has_add.has_scalar_pnat] has_mul.has_pow
end

@[to_additive is_infinite_add_order]

def is_infinite_order [has_mul S] (x : S) : Prop :=
∀ (i j : ℕ+) (h : i ≠ j), x ^ i ≠ x ^ j

@[to_additive quasi_add_idempotent]
def quasi_idempotent [has_mul S] (x : S) : Prop :=
∃ (n' : ℕ) (n : ℕ+), n' = n ∧ set.inj_on (λ k : ℕ+, x ^ k) (set.Iic n) ∧
  ∀ (k : ℕ+), n ≤ k → x ^ k = x ^ n

@[to_additive is_infinite_add_order_or_quasi_add_idempotent]
lemma is_infinite_order_or_quasi_idempotent {S : Type*} [semigroup S] (x : S) :
  is_infinite_order x ∨ quasi_idempotent x :=
begin
  refine or_iff_not_imp_left.mpr (λ h, _),
  rw is_infinite_order at h,
  push_neg at h,
  have h' : ∃ (i : ℕ), 0 < i ∧ ∃ (j : ℕ), 0 < j ∧ i ≠ j ∧ x ^ i.to_pnat' = x ^ j.to_pnat',
  { obtain ⟨⟨i, hi⟩, ⟨j, hj⟩, hne, h⟩ := h,
    refine ⟨i, hi, j, hj, _, _⟩,
    { simpa using hne },
    { convert h;
      simp [subtype.ext_iff, hi, hj] } },
  classical,
  set i : ℕ := nat.find h' with hi,
  have h'' := nat.find_spec h',
  have hs : set.inj_on (λ (k : ℕ+), x ^ k) (set.Iic i.to_pnat'),
  { rintros ⟨m, hm'⟩ hm ⟨n, hn'⟩ hn hmn,
    obtain ⟨k, rfl⟩ := nat.exists_eq_succ_of_ne_zero hm'.ne',
    obtain ⟨l, rfl⟩ := nat.exists_eq_succ_of_ne_zero hn'.ne',
    simp only [set.mem_Iic, ←pnat.coe_le_coe, pnat.mk_coe, nat.le_find_iff, ne.def, not_exists,
               not_and, nat.to_pnat'_coe, nat.find_pos, not_lt_zero', false_and, exists_false,
               not_false_iff, if_true, exists_and_distrib_left] at hm hn hmn,
    rcases lt_trichotomy k l with H|rfl|H,
    { refine absurd hmn _,
      exact hn k.succ (nat.succ_lt_succ H) k.succ_pos l.succ l.succ_pos (nat.succ_lt_succ H).ne },
    { refl },
    { refine absurd hmn.symm _,
      exact hm l.succ (nat.succ_lt_succ H) l.succ_pos k.succ k.succ_pos (nat.succ_lt_succ H).ne } },
  refine ⟨i, i.to_pnat', _, hs, _⟩,
  sorry,
  sorry,
  -- { simp },
  -- sorry,
  -- intros k hk,
  -- rw ←hi at h'',
  -- obtain ⟨hi', j, hj, hne, hij⟩ := h'',
  -- cases positive_or_negative x with hx hx;
  -- { refine hx.pnpow_eq_of_eq hij _ _ hk,
  --   simp [subtype.ext_iff, hj, hne] }
end

[Eric Rodriguez]

try @not_lt_zero' nat in that simp only

[Eric Rodriguez]

c.f. https://github.com/leanprover-community/mathlib/blob/16d48d7ed350fea30a1e072db9013c72534fd119/src/group_theory/exponent.lean#L71

[Yakov Pechersky]

Awesome! That worked. Very arcane.