## Stream: general

#### Yakov Pechersky (Mar 03 2022 at 20:06):

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_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


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)

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⟩

end

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

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

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 (Mar 03 2022 at 20:08):

try @not_lt_zero' nat in that simp only

#### Yakov Pechersky (Mar 03 2022 at 20:46):

Awesome! That worked. Very arcane.

Last updated: Dec 20 2023 at 11:08 UTC