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

source
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
source
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
source
theorem CancelDenoms.cancel_factors_eq_div {α : Type u_1} [Field α] {n e e' : α} (h : n * e = e') (h2 : n ≠ 0) :
e = e' / n
source
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
source
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
source
theorem CancelDenoms.neg_subst {α : Type u_1} [Ring α] {n e t : α} (h1 : n * e = t) :
n * -e = -t
source
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
source
theorem CancelDenoms.inv_subst {α : Type u_1} [Field α] {n k e : α} (h2 : e ≠ 0) (h3 : n * e = k) :
k * e⁻¹ = n
source
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'))
source
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'))
source
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'))
source
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 #

source
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`.

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

- One or more equations did not get rendered due to their size.

Instances For

source
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.

Instances For

source
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.

source
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.

Equations

- CancelDenoms.deriveThms = [`div_div_eq_mul_div, `div_neg]

Instances For

source
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`.

source
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`.

source
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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
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'`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
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

Equations

- One or more equations did not get rendered due to their size.

Instances For

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

- One or more equations did not get rendered due to their size.

Instances For

source
def cancelDenominatorsTarget :
Lean.Elab.Tactic.TacticM Unit
Equations

- One or more equations did not get rendered due to their size.

Instances For

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

- One or more equations did not get rendered due to their size.

Instances For

source
def tacticCancel_denoms_ :
Lean.ParserDescr
Equations

- One or more equations did not get rendered due to their size.

Instances For