Tactics for comparing equivalent valuations

Stream: Is there code for X?

[Kenny Lau]

So in Lines 494-565 of PR #27437 I just found myself gradually proving more and more lemmas of the form:

import Mathlib.RingTheory.Valuation.Basic

variable {R Γ₀ Γ₀' : Type*} [Ring R]
  [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ₀']
  {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ₀'}
  (h : v₁.IsEquiv v₂) {x y z : R}
include h

#print Valuation.IsEquiv -- ∀ (r s : R), v₁ r ≤ v₁ s ↔ v₂ r ≤ v₂ s

theorem le_div_iff_lt_div : v₁ x < v₁ y / v₁ z ↔ v₂ x < v₂ y / v₂ z := by sorry
theorem lt_div_iff_le_div : v₁ x ≤ v₁ y / v₁ z ↔ v₂ x ≤ v₂ y / v₂ z := by sorry
theorem eq_div_iff_eq_div : v₁ x = v₁ y / v₁ z ↔ v₂ x = v₂ y / v₂ z := by sorry

(For your references, I have #printed out the definition of Valuation.IsEquiv: it says ∀ (r s : R), v₁ r ≤ v₁ s ↔ v₂ r ≤ v₂ s.)

Is there a tactic that can automatically prove all of these theorems? Because I just find myself wanting more and more and it isn't really scaling well, I can't just prove every single situation that I need. Maybe some sort of grw could be made to work?

[Kenny Lau]

I can just artifically create countably many cases by considering lemmas like:

v₁ x₁ * v₁ x₂ ≤ v₁ x₃ * v₁ x₄ * v₁ x₅ ↔ v₂ x₁ * v₂ x₂ ≤ v₂ x₃ * v₂ x₄ * v₂ x₅

which for this case you could solve by rw [← v₁.map_mul, ← v₂.map_mul, h.le_iff_le], but then generally the expressions would have symbols 0, 1, *, /, ⁻¹, min, max as well and the formulas can get more and more complex

[Kenny Lau]

so we have function symbols of arity 0, 0, 2, 2, 1, 2, 2; is there even any "normal form" that one can convert to?

[Kenny Lau]

I think I can very easily make a formal specification of what this tactic should do: there will be 4 relation symbols: ≤, <, =, ≠, each of arity 2, connecting terms that have the 7 function symbols above (and arbitrarily many free variables), where each free variable has to be in the form v₁ x on the left hand side, and v₂ x on the right hand side.

[Kenny Lau]

hmm maybe I can also allow for propositional logical operators like ∧ ∨ ¬ → ↔

[Kenny Lau]

ideally even the goal would just have the v1 expression, and then I would just do grw [h] and the goal would change each v1 to v2

[Aaron Liu]

I threw something together

import Mathlib.RingTheory.Valuation.Basic

variable {R Γ₀ Γ₀' : Type*} [Ring R]
  [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ₀']
  {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ₀'}
  {h : v₁.IsEquiv v₂} {x y z : R}
include h

#print Valuation.IsEquiv -- ∀ (r s : R), v₁ r ≤ v₁ s ↔ v₂ r ≤ v₂ s

set_option linter.unusedVariables false in
def Valuation.IsEquiv.Associated (h : v₁.IsEquiv v₂) (x : Γ₀) (y : Γ₀') : Prop :=
  ∃ z w, v₁ z / v₁ w = x ∧ v₂ z / v₂ w = y

theorem Valuation.IsEquiv.Associated.le_iff_le {x y : Γ₀} {z w : Γ₀'}
    (hxz : h.Associated x z) (hyw : h.Associated y w) :
    x ≤ y ↔ z ≤ w := by
  obtain ⟨g, k, rfl, rfl⟩ := hxz
  obtain ⟨c, l, rfl, rfl⟩ := hyw
  by_cases hk : v₁ k = v₁ 0
  · have hk' := h.val_eq.1 hk
    simp [hk, hk']
  have hk' := mt h.val_eq.2 hk
  simp only [v₁.map_zero, v₂.map_zero] at hk hk'
  by_cases hl : v₁ l = v₁ 0
  · have hl' := h.val_eq.1 hl
    simpa [hl, hl', hk, hk'] using (h.val_eq : v₁ g = v₁ 0 ↔ v₂ g = v₂ 0)
  have hl' := mt h.val_eq.2 hl
  simp only [v₁.map_zero, v₂.map_zero] at hl hl'
  rw [← ne_eq, ← zero_lt_iff] at hk hk' hl hl'
  rw [div_le_div_iff₀ hk hl, div_le_div_iff₀ hk' hl']
  simp [← map_mul, h (g * l) (c * k)]
theorem Valuation.IsEquiv.Associated.lt_iff_lt {x y : Γ₀} {z w : Γ₀'}
    (hxz : h.Associated x z) (hyw : h.Associated y w) :
    x < y ↔ z < w := by
  rw [← not_le, ← not_le, hyw.le_iff_le hxz]
theorem Valuation.IsEquiv.Associated.eq_iff_eq {x y : Γ₀} {z w : Γ₀'}
    (hxz : h.Associated x z) (hyw : h.Associated y w) :
    x = y ↔ z = w := by
  rw [le_antisymm_iff, le_antisymm_iff, hxz.le_iff_le hyw, hyw.le_iff_le hxz]

theorem Valuation.IsEquiv.Associated.zero : h.Associated 0 0 := ⟨0, 1, by simp, by simp⟩
theorem Valuation.IsEquiv.Associated.one : h.Associated 1 1 := ⟨1, 1, by simp, by simp⟩
theorem Valuation.IsEquiv.Associated.mul {x y : Γ₀} {z w : Γ₀'}
    (hxz : h.Associated x z) (hyw : h.Associated y w) :
    h.Associated (x * y) (z * w) := by
  obtain ⟨g, k, rfl, rfl⟩ := hxz
  obtain ⟨c, l, rfl, rfl⟩ := hyw
  exact ⟨g * c, k * l, by simp [mul_div_mul_comm], by simp [mul_div_mul_comm]⟩
theorem Valuation.IsEquiv.Associated.div {x y : Γ₀} {z w : Γ₀'}
    (hxz : h.Associated x z) (hyw : h.Associated y w) :
    h.Associated (x / y) (z / w) := by
  obtain ⟨g, k, rfl, rfl⟩ := hxz
  obtain ⟨c, l, rfl, rfl⟩ := hyw
  exact ⟨g * l, c * k,
    by simp [div_eq_mul_inv, mul_assoc, mul_left_comm],
    by simp [div_eq_mul_inv, mul_assoc, mul_left_comm]⟩
theorem Valuation.IsEquiv.Associated.inv {x : Γ₀} {z : Γ₀'}
    (hxz : h.Associated x z) :
    h.Associated x⁻¹ z⁻¹ := by
  obtain ⟨g, k, rfl, rfl⟩ := hxz
  exact ⟨k, g, by simp, by simp⟩
theorem Valuation.IsEquiv.Associated.min {x y : Γ₀} {z w : Γ₀'}
    (hxz : h.Associated x z) (hyw : h.Associated y w) :
    h.Associated (min x y) (min z w) := by
  by_cases hxy : x ≤ y
  · have hzw : z ≤ w := (hxz.le_iff_le hyw).1 hxy
    rwa [min_eq_left hxy, min_eq_left hzw]
  · have hzw : ¬z ≤ w := mt (hxz.le_iff_le hyw).2 hxy
    rwa [min_eq_right_of_lt (lt_of_not_ge hxy), min_eq_right_of_lt (lt_of_not_ge hzw)]
theorem Valuation.IsEquiv.Associated.max {x y : Γ₀} {z w : Γ₀'}
    (hxz : h.Associated x z) (hyw : h.Associated y w) :
    h.Associated (max x y) (max z w) := by
  by_cases hxy : x ≤ y
  · have hzw : z ≤ w := (hxz.le_iff_le hyw).1 hxy
    rwa [max_eq_right hxy, max_eq_right hzw]
  · have hzw : ¬z ≤ w := mt (hxz.le_iff_le hyw).2 hxy
    rwa [max_eq_left_of_lt (lt_of_not_ge hxy), max_eq_left_of_lt (lt_of_not_ge hzw)]
theorem Valuation.IsEquiv.Associated.value {x : R} : h.Associated (v₁ x) (v₂ x) :=
  ⟨x, 1, by simp, by simp⟩

macro "val_equiv_tac" h:term : tactic => `(tactic| focus
  first
  | refine Valuation.IsEquiv.Associated.le_iff_le (h := $h) ?_ ?_
  | refine Valuation.IsEquiv.Associated.lt_iff_lt (h := $h) ?_ ?_
  | refine Valuation.IsEquiv.Associated.eq_iff_eq (h := $h) ?_ ?_
  | fail "failed to recognize goal"
  repeat' first
    | exact Valuation.IsEquiv.Associated.zero
    | exact Valuation.IsEquiv.Associated.one
    | refine Valuation.IsEquiv.Associated.mul ?_ ?_
    | refine Valuation.IsEquiv.Associated.div ?_ ?_
    | refine Valuation.IsEquiv.Associated.inv ?_
    | refine Valuation.IsEquiv.Associated.min ?_ ?_
    | refine Valuation.IsEquiv.Associated.max ?_ ?_
    | exact Valuation.IsEquiv.Associated.value)

variable (h)

theorem le_div_iff_lt_div : v₁ x < v₁ y / v₁ z ↔ v₂ x < v₂ y / v₂ z := by val_equiv_tac h
theorem lt_div_iff_le_div : v₁ x ≤ v₁ y / v₁ z ↔ v₂ x ≤ v₂ y / v₂ z := by val_equiv_tac h
theorem eq_div_iff_eq_div : v₁ x = v₁ y / v₁ z ↔ v₂ x = v₂ y / v₂ z := by val_equiv_tac h

[Kenny Lau]

Thanks!

[Kenny Lau]

aha, that's a very nice approach

[Kenny Lau]

do you think we should make Associated inductive? (I don't think this is a significant change)

[Aaron Liu]

that could work

[Aaron Liu]

do you want to?

[Kenny Lau]

I'll try more stuff tomorrow

[Kenny Lau]

the main light bulb moment was seeing Associated

[Kenny Lau]

I don't think I would be able to progress at all without it

[Yakov Pechersky]

Is any of this in scope for grind? Does grind handle inequalities?

[Kenny Lau]

@Aaron Liu and I've made the rw version thanks to your code:

[Kenny Lau]

import Mathlib.RingTheory.Valuation.Basic

variable {R Γ₀ Γ₀' : Type*} [Ring R]
  [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ₀']
  {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ₀'}
  {h : v₁.IsEquiv v₂} {x y z : R}
include h

#print Valuation.IsEquiv -- ∀ (r s : R), v₁ r ≤ v₁ s ↔ v₂ r ≤ v₂ s

set_option linter.unusedVariables false in
def Valuation.IsEquiv.Associated (h : v₁.IsEquiv v₂) (x : Γ₀) (y : Γ₀') : Prop :=
  ∃ z w, v₁ z / v₁ w = x ∧ v₂ z / v₂ w = y

theorem Valuation.IsEquiv.Associated.le_iff_le {x y : Γ₀} {z w : Γ₀'}
    (hxz : h.Associated x z) (hyw : h.Associated y w) :
    x ≤ y ↔ z ≤ w := by
  obtain ⟨g, k, rfl, rfl⟩ := hxz
  obtain ⟨c, l, rfl, rfl⟩ := hyw
  by_cases hk : v₁ k = v₁ 0
  · have hk' := h.val_eq.1 hk
    simp [hk, hk']
  have hk' := mt h.val_eq.2 hk
  simp only [v₁.map_zero, v₂.map_zero] at hk hk'
  by_cases hl : v₁ l = v₁ 0
  · have hl' := h.val_eq.1 hl
    simpa [hl, hl', hk, hk'] using (h.val_eq : v₁ g = v₁ 0 ↔ v₂ g = v₂ 0)
  have hl' := mt h.val_eq.2 hl
  simp only [v₁.map_zero, v₂.map_zero] at hl hl'
  rw [← ne_eq, ← zero_lt_iff] at hk hk' hl hl'
  rw [div_le_div_iff₀ hk hl, div_le_div_iff₀ hk' hl']
  simp [← map_mul, h (g * l) (c * k)]
theorem Valuation.IsEquiv.Associated.lt_iff_lt {x y : Γ₀} {z w : Γ₀'}
    (hxz : h.Associated x z) (hyw : h.Associated y w) :
    x < y ↔ z < w := by
  rw [← not_le, ← not_le, hyw.le_iff_le hxz]
theorem Valuation.IsEquiv.Associated.eq_iff_eq {x y : Γ₀} {z w : Γ₀'}
    (hxz : h.Associated x z) (hyw : h.Associated y w) :
    x = y ↔ z = w := by
  rw [le_antisymm_iff, le_antisymm_iff, hxz.le_iff_le hyw, hyw.le_iff_le hxz]

theorem Valuation.IsEquiv.Associated.zero : h.Associated 0 0 := ⟨0, 1, by simp, by simp⟩
theorem Valuation.IsEquiv.Associated.one : h.Associated 1 1 := ⟨1, 1, by simp, by simp⟩
theorem Valuation.IsEquiv.Associated.mul {x y : Γ₀} {z w : Γ₀'}
    (hxz : h.Associated x z) (hyw : h.Associated y w) :
    h.Associated (x * y) (z * w) := by
  obtain ⟨g, k, rfl, rfl⟩ := hxz
  obtain ⟨c, l, rfl, rfl⟩ := hyw
  exact ⟨g * c, k * l, by simp [mul_div_mul_comm], by simp [mul_div_mul_comm]⟩
theorem Valuation.IsEquiv.Associated.div {x y : Γ₀} {z w : Γ₀'}
    (hxz : h.Associated x z) (hyw : h.Associated y w) :
    h.Associated (x / y) (z / w) := by
  obtain ⟨g, k, rfl, rfl⟩ := hxz
  obtain ⟨c, l, rfl, rfl⟩ := hyw
  exact ⟨g * l, c * k,
    by simp [div_eq_mul_inv, mul_assoc, mul_left_comm],
    by simp [div_eq_mul_inv, mul_assoc, mul_left_comm]⟩
theorem Valuation.IsEquiv.Associated.inv {x : Γ₀} {z : Γ₀'}
    (hxz : h.Associated x z) :
    h.Associated x⁻¹ z⁻¹ := by
  obtain ⟨g, k, rfl, rfl⟩ := hxz
  exact ⟨k, g, by simp, by simp⟩
theorem Valuation.IsEquiv.Associated.min {x y : Γ₀} {z w : Γ₀'}
    (hxz : h.Associated x z) (hyw : h.Associated y w) :
    h.Associated (min x y) (min z w) := by
  by_cases hxy : x ≤ y
  · have hzw : z ≤ w := (hxz.le_iff_le hyw).1 hxy
    rwa [min_eq_left hxy, min_eq_left hzw]
  · have hzw : ¬z ≤ w := mt (hxz.le_iff_le hyw).2 hxy
    rwa [min_eq_right_of_lt (lt_of_not_ge hxy), min_eq_right_of_lt (lt_of_not_ge hzw)]
theorem Valuation.IsEquiv.Associated.max {x y : Γ₀} {z w : Γ₀'}
    (hxz : h.Associated x z) (hyw : h.Associated y w) :
    h.Associated (max x y) (max z w) := by
  by_cases hxy : x ≤ y
  · have hzw : z ≤ w := (hxz.le_iff_le hyw).1 hxy
    rwa [max_eq_right hxy, max_eq_right hzw]
  · have hzw : ¬z ≤ w := mt (hxz.le_iff_le hyw).2 hxy
    rwa [max_eq_left_of_lt (lt_of_not_ge hxy), max_eq_left_of_lt (lt_of_not_ge hzw)]
theorem Valuation.IsEquiv.Associated.value {x : R} : h.Associated (v₁ x) (v₂ x) :=
  ⟨x, 1, by simp, by simp⟩

macro "val_equiv_tac" h:term : tactic => `(tactic| focus
  first
  | refine Valuation.IsEquiv.Associated.le_iff_le (h := $h) (z := ?_) (w := ?_) ?_ ?_
  | refine Valuation.IsEquiv.Associated.lt_iff_lt (h := $h) (z := ?_) (w := ?_) ?_ ?_
  | refine Valuation.IsEquiv.Associated.eq_iff_eq (h := $h) (z := ?_) (w := ?_) ?_ ?_
  | fail "failed to recognize goal"
  rotate_right 2
  repeat' first
    | exact Valuation.IsEquiv.Associated.zero
    | exact Valuation.IsEquiv.Associated.one
    | refine Valuation.IsEquiv.Associated.mul (h := $h) (z := ?_) (w := ?_) ?_ ?_; rotate_right 2
    | refine Valuation.IsEquiv.Associated.div (h := $h) (z := ?_) (w := ?_) ?_ ?_; rotate_right 2
    | refine Valuation.IsEquiv.Associated.inv (h := $h) (z := ?_) ?_; rotate_right 1
    | refine Valuation.IsEquiv.Associated.min (h := $h) (z := ?_) (w := ?_) ?_ ?_; rotate_right 2
    | refine Valuation.IsEquiv.Associated.max (h := $h) (z := ?_) (w := ?_) ?_ ?_; rotate_right 2
    | exact Valuation.IsEquiv.Associated.value (h := $h))

variable (h)

theorem le_div_iff_lt_div : v₁ x < v₁ y / v₁ z ↔ v₂ x < v₂ y / v₂ z := by val_equiv_tac h
theorem lt_div_iff_le_div : v₁ x ≤ v₁ y / v₁ z ↔ v₂ x ≤ v₂ y / v₂ z := by val_equiv_tac h
theorem eq_div_iff_eq_div : v₁ x = v₁ y / v₁ z ↔ v₂ x = v₂ y / v₂ z := by val_equiv_tac h

macro "rw_val_equiv" h:term : tactic => `(tactic| focus
  refine Iff.mpr (b := ?_) ?_ ?_
  rotate_left 1
  val_equiv_tac $h)

example : v₁ x < v₁ y / min (v₁ z) (v₁ y)⁻¹ := by
  rw_val_equiv h

[Kim Morrison]

Yakov Pechersky said:

Is any of this in scope for grind? Does grind handle inequalities?

grind handles linear equality in Int (and types that embed in Int) and it is soon to have parity with linarith (in fact, any totally ordered vector space, not just strict ordered rings), although right now it doesn't clear denominators.

[Yakov Pechersky]

Here, the type that's being operated on is a linear ordered commutative group with zero, not necessarily rank one. Apart from the underlying linarith module, do you foresee it being extensible to support something like the rule set developed above? It kinda looks like that whiteboard ruleset that the documentation describes. The tactic macro above seems similar to a cc or solve_by_elim approach. That's why I thought it could be relevant to a grind approach.

[Kenny Lau]

I have not written any tactics at all, how do I look at the first symbol of the goal and execute the corresponding theorem, instead of just blindly trying refine?

[Kenny Lau]

(and is there any actual performance boost?)

[Aaron Liu]

Kenny Lau said:

I have not written any tactics at all, how do I look at the first symbol of the goal and execute the corresponding theorem, instead of just blindly trying refine?

I would suggest Qq matching

[Kenny Lau]

is that still in macro land?

[Aaron Liu]

no

[Kenny Lau]

is there an example that I can learn from?

[Aaron Liu]

I'll see if I can find one

[Aaron Liu]

Kenny Lau said:

is there an example that I can learn from?

docs#Mathlib.Tactic.Order.collectFactsImp.processExpr

[Aaron Liu]

feel free to come to me with any question (or to ask on the Zulip)

[Kenny Lau]

that seems useful