A tactic for canceling numeric denominators

This file defines tactics that cancel numeric denominators from field Expressions.

As an example, we want to transform a comparison 5*(a/3 + b/4) < c/3 into the equivalent 5*(4*a + 3*b) < 4*c.

Implementation notes

The tooling here was originally written for linarith, not intended as an interactive tactic. The interactive version has been split off because it is sometimes convenient to use on its own. There are likely some rough edges to it.

Improving this tactic would be a good project for someone interested in learning tactic programming.

Lemmas used in the procedure

theorem CancelDenoms.mul_subst {α : Type u_1} [CommRing α] {n1 n2 k e1 e2 t1 t2 : α} (h1 : n1 * e1 = t1) (h2 : n2 * e2 = t2) (h3 : n1 * n2 = k) : k * (e1 * e2) = t1 * t2

theorem CancelDenoms.div_subst {α : Type u_1} [Field α] {n1 n2 k e1 e2 t1 : α} (h1 : n1 * e1 = t1) (h2 : n2 / e2 = 1) (h3 : n1 * n2 = k) : k * (e1 / e2) = t1

theorem CancelDenoms.cancel_factors_eq_div {α : Type u_1} [Field α] {n e e' : α} (h : n * e = e') (h2 : n ≠ 0) : e = e' / n

theorem CancelDenoms.add_subst {α : Type u_1} [Ring α] {n e1 e2 t1 t2 : α} (h1 : n * e1 = t1) (h2 : n * e2 = t2) : n * (e1 + e2) = t1 + t2

theorem CancelDenoms.sub_subst {α : Type u_1} [Ring α] {n e1 e2 t1 t2 : α} (h1 : n * e1 = t1) (h2 : n * e2 = t2) : n * (e1 - e2) = t1 - t2

theorem CancelDenoms.neg_subst {α : Type u_1} [Ring α] {n e t : α} (h1 : n * e = t) : n * -e = -t

theorem CancelDenoms.pow_subst {α : Type u_1} [CommRing α] {n e1 t1 k l : α} {e2 : ℕ} (h1 : n * e1 = t1) (h2 : l * n ^ e2 = k) : k * e1 ^ e2 = l * t1 ^ e2

theorem CancelDenoms.inv_subst {α : Type u_1} [Field α] {n k e : α} (h2 : e ≠ 0) (h3 : n * e = k) : k * e⁻¹ = n

theorem CancelDenoms.cancel_factors_lt {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b ad bd a' b' gcd : α} (ha : ad * a = a') (hb : bd * b = b') (had : 0 < ad) (hbd : 0 < bd) (hgcd : 0 < gcd) : (a < b) = (1 / gcd * (bd * a') < 1 / gcd * (ad * b'))

theorem CancelDenoms.cancel_factors_le {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a b ad bd a' b' gcd : α} (ha : ad * a = a') (hb : bd * b = b') (had : 0 < ad) (hbd : 0 < bd) (hgcd : 0 < gcd) : (a ≤ b) = (1 / gcd * (bd * a') ≤ 1 / gcd * (ad * b'))

theorem CancelDenoms.cancel_factors_eq {α : Type u_1} [Field α] {a b ad bd a' b' gcd : α} (ha : ad * a = a') (hb : bd * b = b') (had : ad ≠ 0) (hbd : bd ≠ 0) (hgcd : gcd ≠ 0) : (a = b) = (1 / gcd * (bd * a') = 1 / gcd * (ad * b'))

theorem CancelDenoms.cancel_factors_ne {α : Type u_1} [Field α] {a b ad bd a' b' gcd : α} (ha : ad * a = a') (hb : bd * b = b') (had : ad ≠ 0) (hbd : bd ≠ 0) (hgcd : gcd ≠ 0) : (a ≠ b) = (1 / gcd * (bd * a') ≠ 1 / gcd * (ad * b'))

Computing cancellation factors

partial def CancelDenoms.findCancelFactor (e : Lean.Expr) : ℕ × Tree ℕ

findCancelFactor e produces a natural number n, such that multiplying e by n will be able to cancel all the numeric denominators in e. The returned Tree describes how to distribute the value n over products inside e.

def CancelDenoms.synthesizeUsingNormNum (type : Q(Prop)) : Lean.MetaM Q(«$type»)

structure CancelDenoms.CancelResult {u : Lean.Level} {α : Q(Type u)} (mα : Q(Mul «$α»)) (e v : Q(«$α»)) : Type

CancelResult mα e v' provides a value for v * e where the denominators have been cancelled.

• cancelled : Q(«$α»)

  An expression with denominators cancelled.

• pf : Q(«$v» * «$e» = unknown_1)

  The proof that cancelled is valid.

partial def CancelDenoms.mkProdPrf {u : Lean.Level} (α : Q(Type u)) (sα : Q(Field «$α»)) (v : ℕ) (v' : Q(«$α»)) (t : Tree ℕ) (e : Q(«$α»)) : Lean.MetaM (CancelResult q(inferInstance) e v')

mkProdPrf α sα v v' tr e produces a proof of v'*e = e', where numeric denominators have been canceled in e', distributing v proportionally according to the tree tr computed by findCancelFactor.

The v' argument is a numeral expression corresponding to v, which we need in order to state the return type accurately.

def CancelDenoms.deriveThms : List Lean.Name

Theorems to get expression into a form that findCancelFactor and mkProdPrf can more easily handle. These are important for dividing by rationals and negative integers.

theorem CancelDenoms.derive_trans {α : Type u_1} [Mul α] {a b c d : α} (h : a = b) (h' : c * b = d) : c * a = d

Helper lemma to chain together a simp proof and the result of mkProdPrf.

theorem CancelDenoms.derive_trans₂ {α : Type u_1} [Mul α] {a b c d e : α} (h : a = b) (h' : b = c) (h'' : d * c = e) : d * a = e

Helper lemma to chain together two simp proofs and the result of mkProdPrf.

def CancelDenoms.derive (e : Lean.Expr) : Lean.MetaM (ℕ × Lean.Expr)

Given e, a term with rational division, produces a natural number n and a proof of n*e = e', where e' has no division. Assumes "well-behaved" division.

def CancelDenoms.findCompLemma (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Name × Bool))

findCompLemma e arranges e in the form lhs R rhs, where R ∈ {<, ≤, =, ≠}, and returns lhs, rhs, the cancel_factors lemma corresponding to R, and a boolean indicating whether R involves the order (i.e. < and ≤) or not (i.e. = and ≠). In the case of LT, LE, GE, and GT an order on the type is needed, in the last case it is not, the final component of the return value tracks this.

def CancelDenoms.cancelDenominatorsInType (h : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr)

cancelDenominatorsInType h assumes that h is of the form lhs R rhs, where R ∈ {<, ≤, =, ≠, ≥, >}. It produces an Expression h' of the form lhs' R rhs' and a proof that h = h'. Numeric denominators have been canceled in lhs' and rhs'.

def cancelDenoms : Lean.ParserDescr

cancel_denoms attempts to remove numerals from the denominators of fractions. It works on propositions that are field-valued inequalities.

variable [LinearOrderedField α] (a b c : α)

example (h : a / 5 + b / 4 < c) : 4*a + 5*b < 20*c := by
  cancel_denoms at h
  exact h

example (h : a > 0) : a / 5 > 0 := by
  cancel_denoms
  exact h

def cancelDenominatorsAt (fvar : Lean.FVarId) : Lean.Elab.Tactic.TacticM Unit

def cancelDenominatorsTarget : Lean.Elab.Tactic.TacticM Unit

def cancelDenominators (loc : Lean.Elab.Tactic.Location) : Lean.Elab.Tactic.TacticM Unit

def tacticCancel_denoms_ : Lean.ParserDescr