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 cancel_factors.mul_subst {α : Type u_1} [comm_ring α] {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 cancel_factors.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 cancel_factors.cancel_factors_eq_div {α : Type u_1} [field α] {n e e' : α} (h : n * e = e') (h2 : n ≠ 0) :

e = e' / n

source

theorem cancel_factors.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 cancel_factors.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 cancel_factors.neg_subst {α : Type u_1} [ring α] {n e t : α} (h1 : n * e = t) :

n * -e = -t

source

theorem cancel_factors.cancel_factors_lt {α : Type u_1} [linear_ordered_field α] {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 cancel_factors.cancel_factors_le {α : Type u_1} [linear_ordered_field α] {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 cancel_factors.cancel_factors_eq {α : Type u_1} [linear_ordered_field α] {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')

Computing cancelation factors #

source

meta def cancel_factors.find_cancel_factor :

expr → ℕ × tree ℕ

find_cancel_factor 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

meta def cancel_factors.mk_prod_prf :

ℕ → tree ℕ → expr → tactic expr

mk_prod_prf n tr e produces a proof of n*e = e', where numeric denominators have been canceled in e', distributing n proportionally according to tr.

source

meta def cancel_factors.derive (e : expr) :

tactic (ℕ × 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.

source

meta def cancel_factors.derive_div (e : expr) :

tactic (ℕ × expr)

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

source

meta def cancel_factors.find_comp_lemma :

expr → option (expr × expr × name)

find_comp_lemma e arranges e in the form lhs R rhs, where R ∈ {<, ≤, =}, and returns lhs, rhs, and the cancel_factors lemma corresponding to R.

source

meta def cancel_factors.cancel_denominators_in_type (h : expr) :

tactic (expr × expr)

cancel_denominators_in_type 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'.

Interactive version #

source

meta def tactic.interactive.cancel_denoms (l : interactive.parse interactive.types.location) :

tactic unit

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

variables {α : Type} [linear_ordered_field α] (a b c : α)

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

example (h : a > 0) : a / 5 > 0 :=
begin
  cancel_denoms,
  exact h
end
```