perf(tactic/linarith): implement redundancy test to reduce number of comparisons (#3079)

This implements a redundancy check in `linarith` which can drastically reduce the size of the sets of comparisons that the tactic needs to deal with.

`linarith` iteratively transforms sets of inequalities to equisatisfiable sets by eliminating a single variable. If there are `n` comparisons in the set, we expect `O(n^2)` comparisons after one elimination step. Many of these comparisons are redundant, i.e. removing them from the set does not change its satisfiability.

Deciding redundancy is expensive, but there are cheap approximations that are very useful in practice. This PR tests comparisons for non-minimal history (http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.51.493&rep=rep1&type=pdf p.13, theorem 7). Non-minimal history implies redundancy.



Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>

Author: robertylewis

src/analysis/special_functions/trigonometric.lean

@@ -766,23 +766,23 @@ lemma cos_le_cos_of_nonneg_of_le_pi {x y : ℝ} (hx₁ : 0 ≤ x) (hx₂ : x ≤
   (le_of_lt ∘ cos_lt_cos_of_nonneg_of_le_pi hx₁ hx₂ hy₁ hy₂)
   (λ h, h ▸ le_refl _)
 
-lemma sin_lt_sin_of_le_of_le_pi_div_two {x y : ℝ} (hx₁ : -(π / 2) ≤ x) (hx₂ : x ≤ π / 2) (hy₁ : -(π / 2) ≤ y)
+lemma sin_lt_sin_of_le_of_le_pi_div_two {x y : ℝ} (hx₁ : -(π / 2) ≤ x)
   (hy₂ : y ≤ π / 2) (hxy : x < y) : sin x < sin y :=
 by rw [← cos_sub_pi_div_two, ← cos_sub_pi_div_two, ← cos_neg (x - _), ← cos_neg (y - _)];
   apply cos_lt_cos_of_nonneg_of_le_pi; linarith
 
-lemma sin_le_sin_of_le_of_le_pi_div_two {x y : ℝ} (hx₁ : -(π / 2) ≤ x) (hx₂ : x ≤ π / 2) (hy₁ : -(π / 2) ≤ y)
+lemma sin_le_sin_of_le_of_le_pi_div_two {x y : ℝ} (hx₁ : -(π / 2) ≤ x)
   (hy₂ : y ≤ π / 2) (hxy : x ≤ y) : sin x ≤ sin y :=
 (lt_or_eq_of_le hxy).elim
-  (le_of_lt ∘ sin_lt_sin_of_le_of_le_pi_div_two hx₁ hx₂ hy₁ hy₂)
+  (le_of_lt ∘ sin_lt_sin_of_le_of_le_pi_div_two hx₁ hy₂)
   (λ h, h ▸ le_refl _)
 
 lemma sin_inj_of_le_of_le_pi_div_two {x y : ℝ} (hx₁ : -(π / 2) ≤ x) (hx₂ : x ≤ π / 2) (hy₁ : -(π / 2) ≤ y)
   (hy₂ : y ≤ π / 2) (hxy : sin x = sin y) : x = y :=
 match lt_trichotomy x y with
-| or.inl h          := absurd (sin_lt_sin_of_le_of_le_pi_div_two hx₁ hx₂ hy₁ hy₂ h) (by rw hxy; exact lt_irrefl _)
+| or.inl h          := absurd (sin_lt_sin_of_le_of_le_pi_div_two hx₁ hy₂ h) (by rw hxy; exact lt_irrefl _)
 | or.inr (or.inl h) := h
-| or.inr (or.inr h) := absurd (sin_lt_sin_of_le_of_le_pi_div_two hy₁ hy₂ hx₁ hx₂ h) (by rw hxy; exact lt_irrefl _)
+| or.inr (or.inr h) := absurd (sin_lt_sin_of_le_of_le_pi_div_two hy₁ hx₂ h) (by rw hxy; exact lt_irrefl _)
 end
 
 lemma cos_inj_of_nonneg_of_le_pi {x y : ℝ} (hx₁ : 0 ≤ x) (hx₂ : x ≤ π) (hy₁ : 0 ≤ y) (hy₂ : y ≤ π)
@@ -986,8 +986,7 @@ lemma arcsin_nonneg {x : ℝ} (hx : 0 ≤ x) : 0 ≤ arcsin x :=
 if hx₁ : x ≤ 1 then
 not_lt.1 (λ h, not_lt.2 hx begin
   have := sin_lt_sin_of_le_of_le_pi_div_two
-    (neg_pi_div_two_le_arcsin _) (arcsin_le_pi_div_two _)
-    (neg_nonpos.2 (le_of_lt pi_div_two_pos)) (le_of_lt pi_div_two_pos) h,
+    (neg_pi_div_two_le_arcsin _) (le_of_lt pi_div_two_pos) h,
   rw [real.sin_arcsin, sin_zero] at this; linarith
 end)
 else by rw [arcsin, dif_neg]; simp [hx₁]
@@ -1091,8 +1090,7 @@ lemma tan_lt_tan_of_nonneg_of_lt_pi_div_two {x y : ℝ} (hx₁ : 0 ≤ x) (hx₂
 begin
   rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos],
   exact div_lt_div
-    (sin_lt_sin_of_le_of_le_pi_div_two (by linarith) (le_of_lt hx₂)
-      (by linarith) (le_of_lt hy₂) hxy)
+    (sin_lt_sin_of_le_of_le_pi_div_two (by linarith) (le_of_lt hy₂) hxy)
     (cos_le_cos_of_nonneg_of_le_pi hx₁ (by linarith) hy₁ (by linarith) (le_of_lt hxy))
     (sin_nonneg_of_nonneg_of_le_pi hy₁ (by linarith))
     (cos_pos_of_neg_pi_div_two_lt_of_lt_pi_div_two (by linarith) hy₂)

src/meta/rb_map.lean

@@ -45,6 +45,22 @@ meta def of_list_core {key} (base : native.rb_set key) : list key → native.rb_
 | []      := base
 | (x::xs) := native.rb_set.insert (of_list_core xs) x
 
+/--
+`of_list l` transforms a list `l : list key` into an `rb_set`,
+inferring an order on the type `key`.
+-/
+meta def of_list {key} [has_lt key] [decidable_rel ((<) : key → key → Prop)] :
+  list key → rb_set key :=
+of_list_core mk_rb_set
+
+/--
+`sdiff s1 s2` returns the set of elements that are in `s1` but not in `s2`.
+It does so by folding over `s2`. If `s1` is significantly smaller than `s2`,
+it may be worth it to reverse the fold.
+-/
+meta def sdiff {α} (s1 s2 : rb_set α) : rb_set α :=
+s2.fold s1 $ λ v s, s.erase v
+
 end rb_set
 
 namespace rb_map

src/tactic/linarith.lean

@@ -23,7 +23,9 @@ meta def nat.to_pexpr : ℕ → pexpr
 | 1 := ``(1)
 | n := if n % 2 = 0 then ``(bit0 %%(nat.to_pexpr (n/2))) else ``(bit1 %%(nat.to_pexpr (n/2)))
 
+
 open native
+
 namespace linarith
 
 section lemmas
@@ -177,6 +179,10 @@ def cmp : linexp → linexp → ordering
   else if z2 < z1 then ordering.gt
   else cmp t1 t2
 
+/-- `l.vars` returns the list of variables that occur in `l`. -/
+def vars (l : linexp) : list ℕ :=
+l.map prod.fst
+
 end linexp
 
 section datatypes
@@ -216,11 +222,16 @@ The represented term is `coeffs.sum (λ ⟨k, v⟩, v * Var[k])`.
 str determines the direction of the comparison -- is it < 0, ≤ 0, or = 0?
 -/
 @[derive inhabited]
-meta structure comp : Type :=
+structure comp : Type :=
 (str : ineq)
 (coeffs : linexp)
 
-meta inductive comp_source : Type
+/-- `c.vars` returns the list of variables that appear in the linear expression contained in `c`. -/
+def comp.vars : comp → list ℕ :=
+linexp.vars ∘ comp.coeffs
+
+@[derive inhabited]
+inductive comp_source : Type
 | assump : ℕ → comp_source
 | add : comp_source → comp_source → comp_source
 | scale : ℕ → comp_source → comp_source
@@ -230,17 +241,76 @@ meta def comp_source.flatten : comp_source → rb_map ℕ ℕ
 | (comp_source.add c1 c2) := (comp_source.flatten c1).add (comp_source.flatten c2)
 | (comp_source.scale n c) := (comp_source.flatten c).map (λ v, v * n)
 
-meta def comp_source.to_string : comp_source → string
+def comp_source.to_string : comp_source → string
 | (comp_source.assump e) := to_string e
 | (comp_source.add c1 c2) := comp_source.to_string c1 ++ " + " ++ comp_source.to_string c2
 | (comp_source.scale n c) := to_string n ++ " * " ++ comp_source.to_string c
 
 meta instance comp_source.has_to_format : has_to_format comp_source :=
 ⟨λ a, comp_source.to_string a⟩
 
-meta structure pcomp :=
+/--
+A `pcomp` stores a linear comparison `Σ cᵢ*xᵢ R 0`,
+along with information about how this comparison was derived.
+
+The original expressions fed into `linarith` are each assigned a unique natural number label.
+The *historical set* `pcomp.history` stores the labels of expressions
+that were used in deriving the current `pcomp`.
+
+Variables are also indexed by natural numbers. The sets `pcomp.effective`, `pcomp.implicit`,
+and `pcomp.vars` contain variable indices.
+
+* `pcomp.vars` contains the variables that appear in `pcomp.c`. We store them in `pcomp` to
+  avoid recomputing the set, which requires folding over a list. (TODO: is this really needed?)
+* `pcomp.effective` contains the variables that have been effectively eliminated from `pcomp`.
+  A variable `n` is said to be *effectively eliminated* in `pcomp` if the elimination of `n`
+  produced at least one of the ancestors of `pcomp`.
+* `pcomp.implicit` contains the variables that have been implicitly eliminated from `pcomp`.
+  A variable `n` is said to be *implicitly eliminated* in `pcomp` if it satisfies the following
+  properties:
+  - There is some `ancestor` of `pcomp` such that `n` appears in `ancestor.vars`.
+  - `n` does not appear in `pcomp.vars`.
+  - `n` was not effectively eliminated.
+
+We track these sets in order to compute whether the history of a `pcomp` is *minimal*.
+Checking this directly is expensive, but effective approximations can be defined in terms of these
+sets. During the variable elimination process, a `pcomp` with non-minimal history can be discarded.
+-/
+meta structure pcomp : Type :=
 (c : comp)
 (src : comp_source)
+(history : rb_set ℕ)
+(effective : rb_set ℕ)
+(implicit : rb_set ℕ)
+(vars : rb_set ℕ)
+
+/--
+Any comparison whose history is not minimal is redundant,
+and need not be included in the new set of comparisons.
+
+`elimed_ge : ℕ` is a natural number such that all variables with index ≥ `elimed_ge` have been
+removed from the system.
+
+This test is an overapproximation to minimality. It gives necessary but not sufficient conditions.
+If the history of `c` is minimal, then `c.maybe_minimal` is true,
+but `c.maybe_minimal` may also be true for some `c` with minimal history.
+Thus, if `c.maybe_minimal` is false, `c` is known not to be minimal and must be redundant.
+
+See http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.51.493&rep=rep1&type=pdf p.13
+(Theorem 7).
+
+The condition described there considers only implicitly eliminated variables that have been
+officially eliminated from the system. This is not the case for every implicitly eliminated variable.
+Consider eliminating `z` from `{x + y + z < 0, x - y - z < 0}`. The result is the set
+`{2*x < 0}`; `y` is implicitly but not officially eliminated.
+
+This implementation of Fourier-Motzkin elimination processes variables in decreasing order of
+indices. Immediately after a step that eliminates variable `k`, variable `k'` has been eliminated
+iff `k' ≥ k`. Thus we can compute the intersection of officially and implicitly eliminated variables
+by taking the set of implicitly eliminated variables with indices ≥ `elimed_ge`.
+-/
+meta def pcomp.maybe_minimal (c : pcomp) (elimed_ge : ℕ) : bool :=
+c.history.size ≤ 1 + ((c.implicit.filter (≥ elimed_ge)).union c.effective).size
 
 /-- `comp` has a lex order. First the `ineq`s are compared, then the `coeff`s. -/
 meta def comp.cmp : comp → comp → ordering
@@ -268,10 +338,47 @@ meta def comp.add (c1 c2 : comp) : comp :=
 ⟨c1.str.max c2.str, c1.coeffs.add c2.coeffs⟩
 
 meta def pcomp.scale (c : pcomp) (n : ℕ) : pcomp :=
-⟨c.c.scale n, comp_source.scale n c.src⟩
+{c with c := c.c.scale n, src := c.src.scale n}
 
-meta def pcomp.add (c1 c2 : pcomp) : pcomp :=
-⟨c1.c.add c2.c, comp_source.add c1.src c2.src⟩
+/--
+`pcomp.add c1 c2 elim_var` creates the result of summing the linear comparisons `c1` and `c2`,
+during the process of eliminating the variable `elim_var`.
+The computation assumes, but does not enforce, that `elim_var` appears in both `c1` and `c2`
+and does not appear in the sum.
+
+Computing the sum of the two comparisons is easy; the complicated details lie in tracking the
+additional fields of `pcomp`.
+
+* The historical set `pcomp.history` of `c1 + c2` is the union of the two historical sets.
+* We recompute the variables that appear in `c1 + c2` from the newly created `linexp`,
+  since some may have been implicitly eliminated.
+* The effectively eliminated variables of `c1 + c2` are the union of the two effective sets,
+  with `elim_var` inserted.
+* The implicitly eliminated variables of `c1 + c2` are those that appear in at least one of
+  `c1.vars` and `c2.vars` but not in `(c1 + c2).vars`, excluding `elim_var`.
+-/
+meta def pcomp.add (c1 c2 : pcomp) (elim_var : ℕ) : pcomp :=
+let c := c1.c.add c2.c,
+    src := c1.src.add c2.src,
+    history := c1.history.union c2.history,
+    vars := native.rb_set.of_list c.vars,
+    effective := (c1.effective.union c2.effective).insert elim_var,
+    implicit := ((c1.vars.union c2.vars).sdiff vars).erase elim_var in
+⟨c, src, history, effective, implicit, vars⟩
+
+/--
+`pcomp.assump c n` creates a `pcomp` whose comparison is `c` and whose source is
+`comp_source.assump n`, that is, `c` is derived from the `n`th hypothesis.
+The history is the singleton set `{n}`.
+No variables have been eliminated (effectively or implicitly).
+-/
+meta def pcomp.assump (c : comp) (n : ℕ) : pcomp :=
+{ c := c,
+  src := comp_source.assump n,
+  history := mk_rb_set.insert n,
+  effective := mk_rb_set,
+  implicit := mk_rb_set,
+  vars := rb_set.of_list c.vars }
 
 meta instance pcomp.to_format : has_to_format pcomp :=
 ⟨λ p, to_fmt p.c.coeffs ++ to_string p.c.str ++ "0"⟩
@@ -288,42 +395,36 @@ end datatypes
 section fm_elim
 
 /-- If `c1` and `c2` both contain variable `a` with opposite coefficients,
-produces `v1`, `v2`, and `c` such that `a` has been cancelled in `c := v1*c1 + v2*c2`. -/
-meta def elim_var (c1 c2 : comp) (a : ℕ) : option (ℕ × ℕ × comp) :=
+produces `v1`, `v2` such that `a` has been cancelled in `v1*c1 + v2*c2`. -/
+meta def elim_var (c1 c2 : comp) (a : ℕ) : option (ℕ × ℕ) :=
 let v1 := c1.coeff_of a,
     v2 := c2.coeff_of a in
 if v1 * v2 < 0 then
   let vlcm :=  nat.lcm v1.nat_abs v2.nat_abs,
       v1' := vlcm / v1.nat_abs,
       v2' := vlcm / v2.nat_abs in
-  some ⟨v1', v2', comp.add (c1.scale v1') (c2.scale v2')⟩
+  some ⟨v1', v2'⟩
 else none
 
 meta def pelim_var (p1 p2 : pcomp) (a : ℕ) : option pcomp :=
-do (n1, n2, c) ← elim_var p1.c p2.c a,
-   return ⟨c, comp_source.add (p1.src.scale n1) (p2.src.scale n2)⟩
+do (n1, n2) ← elim_var p1.c p2.c a,
+   return $ (p1.scale n1).add (p2.scale n2) a
 
 meta def comp.is_contr (c : comp) : bool := c.coeffs.empty ∧ c.str = ineq.lt
 
 meta def pcomp.is_contr (p : pcomp) : bool := p.c.is_contr
 
 meta def elim_with_set (a : ℕ) (p : pcomp) (comps : rb_set pcomp) : rb_set pcomp :=
-if ¬ p.c.coeffs.contains a then mk_pcomp_set.insert p else
 comps.fold mk_pcomp_set $ λ pc s,
 match pelim_var p pc a with
-| some pc := s.insert pc
+| some pc := if pc.maybe_minimal a then s.insert pc else s
 | none := s
 end
 
 /--
 The state for the elimination monad.
 * `vars`: the set of variables present in `comps`
 * `comps`: a set of comparisons
-* `inputs`: a set of pairs of exprs `(t, pf)`, where `t` is a term and `pf` is a proof that
-  `t {<, ≤, =} 0`, indexed by `ℕ`.
-* `has_false`: stores a `pcomp` of `0 < 0` if one has been found
-
-TODO: is it more efficient to store comps as a list, to avoid comparisons?
 -/
 meta structure linarith_structure :=
 (vars : rb_set ℕ)
@@ -351,13 +452,34 @@ end
 meta def update (vars : rb_set ℕ) (comps : rb_set pcomp) : linarith_monad unit :=
 state_t.put ⟨vars, comps⟩ >> validate
 
+/--
+`split_set_by_var_sign a comps` partitions the set `comps` into three parts.
+* `pos` contains the elements of `comps` in which `a` has a positive coefficient.
+* `neg` contains the elements of `comps` in which `a` has a negative coefficient.
+* `not_present` contains the elements of `comps` in which `a` has coefficient 0.
+
+Returns `(pos, neg, not_present)`.
+-/
+meta def split_set_by_var_sign (a : ℕ) (comps : rb_set pcomp) :
+  rb_set pcomp × rb_set pcomp × rb_set pcomp :=
+comps.fold ⟨mk_pcomp_set, mk_pcomp_set, mk_pcomp_set⟩ $ λ pc ⟨pos, neg, not_present⟩,
+  let n := pc.c.coeff_of a in
+  if n > 0 then ⟨pos.insert pc, neg, not_present⟩
+  else if n < 0 then ⟨pos, neg.insert pc, not_present⟩
+  else ⟨pos, neg, not_present.insert pc⟩
+
+/--
+`monad.elim_var a` performs one round of Fourier-Motzkin elimination, eliminating the variable `a`
+from the `linarith` state.
+-/
 meta def monad.elim_var (a : ℕ) : linarith_monad unit :=
 do vs ← get_vars,
    when (vs.contains a) $
-do comps ← get_comps,
-   let cs' := comps.fold mk_pcomp_set (λ p s, s.union (elim_with_set a p comps)),
+do ⟨pos, neg, not_present⟩ ← split_set_by_var_sign a <$> get_comps,
+   let cs' := pos.fold not_present (λ p s, s.union (elim_with_set a p neg)),
    update (vs.erase a) cs'
 
+
 meta def elim_all_vars : linarith_monad unit :=
 get_var_list >>= list.mmap' monad.elim_var
 
@@ -516,8 +638,8 @@ do pftps ← l.mmap infer_type,
   let prmap := rb_map.of_list $ lz.map (λ ⟨n, x⟩, (n, x.1)),
   let vars : rb_set ℕ := rb_map.set_of_list $ list.range map.size,
   let pc : rb_set pcomp :=
-    rb_set.of_list_core mk_pcomp_set $ lz.map (λ ⟨n, x⟩, ⟨x.2, comp_source.assump n⟩),
-  return (⟨vars, pc⟩, prmap)
+    rb_set.of_list_core mk_pcomp_set $ lz.map (λ ⟨n, x⟩, pcomp.assump x.2 n),
+  return ({vars := vars, comps := pc}, prmap)
 
 meta def linarith_monad.run (red : transparency) {α} (tac : linarith_monad α) (l : list expr) :
   tactic ((pcomp ⊕ α) × rb_map ℕ (expr × expr)) :=