tactic for calculations in `ℤₘ₀`

Stream: mathlib4

[Kevin Buzzard]

Finite adeles need some love. Along the way to proving that the finite adeles of K are a K-algebra (K the field of fractions of a DVR), I was faced with this:

import Mathlib--.RingTheory.Valuation.Basic

open scoped DiscreteValuation

#check ℤₘ₀ -- Notation for WithZero (Multiplicative ℤ)

example (k d n : ℤₘ₀) (h1 : 1 < k) (h2 : k * d = n) (h3 : n ≤ 1) : d < 1 := by sorry

This turned out to be trickier than I'd expected. Here's my current solution:

import Mathlib--.RingTheory.Valuation.Basic

open scoped DiscreteValuation

#check ℤₘ₀ -- Notation for WithZero (Multiplicative ℤ)

example (k d n : ℤₘ₀) (h1 : 1 < k) (h2 : k * d = n) (h3 : n ≤ 1) : d < 1 := by sorry


open Multiplicative in
theorem foo (x : ℤₘ₀) : x = 0 ∨ ∃ (n : ℤ), x = (↑(ofAdd n)) := by
  cases x
  · left; aesop
  · right; aesop

open Multiplicative in
theorem bar {x : ℤₘ₀} (hx : 0 < x) : ∃ (n : ℤ), x = (↑(ofAdd n)) := by
  cases foo x <;> aesop

-- this makes `mul_lt_mul_left`, `mul_pos` etc work on `ℤₘ₀`
open Multiplicative in
instance : PosMulStrictMono ℤₘ₀ where
  elim := by
    intro ⟨x, hx⟩ a b (h : a < b)
    rcases bar hx with ⟨x, rfl⟩
    dsimp
    rcases foo a with (rfl | ⟨a, rfl⟩)
    · rw [mul_zero]
      rcases bar h with ⟨b, rfl⟩
      exact WithZero.zero_lt_coe _
    · have hoo : (0 : ℤₘ₀) < b := by
        refine lt_trans ?_ h
        exact WithZero.zero_lt_coe (ofAdd a)
      rcases bar hoo with ⟨b, rfl⟩
      norm_cast at h ⊢
      change x + a < x + b
      change a < b at h
      linarith

example (k d n : ℤₘ₀) (h1 : 1 < k) (h2 : k * d = n) (h3 : n ≤ 1) : d < 1 := by
  cases' eq_bot_or_bot_lt d
  · case inl h => exact h ▸ zero_lt_one
  · case inr h => change (0 < d) at h; calc
    d = d * 1 := by simp
    _ < d * k := by rwa [mul_lt_mul_left h]
    _ = k * d := mul_comm _ _
    _ = n     := h2
    _ ≤ 1     := h3

Do we want some of this in mathlib? What should foo and bar be called?

[Kevin Buzzard]

I was also wondering whether it would be possible to make some kind of tactic for working with ℤₘ₀ of the form "I will turn one question about this into a finite number of questions about integers, obtained by doing a case split

[Alex J. Best]

In the past I implemented a tactic very much like this (for very much the same application), the value group/monoid of a valuation is something that is mostly like the linear theory of integers / naturals (hence decidable) together with infinity (zero in the multiplicative case). This theory is also decidable. A decision procedure for the universally quantified problems is basically just "do cases then linarith" though by now you could probably use omega to get much further: https://github.com/KisaraBlue/ec-tate-lean/blob/master/ECTate/Tactic/ELinarith.lean . In your case you'l have to throw in some simp lemmas that converts multiplicative to additive I guess

[Kevin Buzzard]

Yeah my proof is supposed to be "cases for 0 and then reduce to a question about integers otherwise"

[Kevin Buzzard]

#13090 seems to help (there's some hideous defeq abuse happening behind the scenes but I figured people probably wouldn't notice)