feat(tactic): add linear arithmetic tactic (#301)

* feat(data/list, tactic): small helper functions

* feat(meta/rb_map): extra operations on native rb_maps

* feat(tactic/linarith): add tactic for solving linear arithmetic goals

* doc(tactic/linarith): add documentation and tests

* chore(tactic/linarith): add copyright

* feat(tactic/linarith): allow products of coefficients

* feat(tactic/linarith): cut off search early if contradiction is found

* feat(tests/linarith_tests): add test

* doc(doc/tactics): update doc

* feat(tactic/linarith): add config options

* feat(tactic/linarith): support equality goals

* chore(tactic/linarith): move non-tactic code out of tactic monad

* feat(tactic/linarith): support rational coefficients

* doc(tactic/linarith): update doc

* feat(tactic/linarith): fix obvious inefficiency in canceling denoms

* feat(tactic/linarith): efficiency improvements

* fix(tactic/linarith): remove unnecessary import and dead code

* fix(data/list/basic, meta/rb_map): shorter proofs

Author: robertylewis

data/list/basic.lean

@@ -686,7 +686,8 @@ index_of_cons_eq _ rfl
 @[simp] theorem index_of_cons_ne {a b : α} (l : list α) : a ≠ b → index_of a (b::l) = succ (index_of a l) :=
 assume n, if_neg n
 
-theorem index_of_eq_length {a : α} {l : list α} : index_of a l = length l ↔ a ∉ l :=
+theorem index_of_eq_length {a : α} {l : list α} : index_of a l = length l ↔ a ∉ l 
+:=
 begin
   induction l with b l ih; simp [-add_comm],
   by_cases h : a = b; simp [h, -add_comm],
@@ -3831,6 +3832,9 @@ theorem reverse_range' : ∀ s n : ℕ,
   map prod.fst (enum l) = range l.length :=
 by simp [enum, range_eq_range']
 
+def reduce_option {α} : list (option α) → list α :=
+list.filter_map id
+
 def map_head {α} (f : α → α) : list α → list α
 | [] := []
 | (x :: xs) := f x :: xs

docs/tactics.md

@@ -312,4 +312,29 @@ end
 The default list of tactics can be found by looking up the definition of 
 [`default_tidy_tactics`](https://github.com/leanprover/mathlib/blob/master/tactic/tidy.lean).
 
-This list can be overriden using `tidy { tactics :=  ... }`. (The list must be a list of `tactic string`.)
+This list can be overriden using `tidy { tactics :=  ... }`. (The list must be a list of `tactic string`.)
+
+## linarith
+
+`linarith` attempts to find a contradiction between hypotheses that are linear (in)equalities.
+Equivalently, it can prove a linear inequality by assuming its negation and proving `false`. 
+This tactic is currently work in progress, and has various limitations. In particular, 
+it will not work on `nat`. The tactic can be made much more efficient.
+
+An example: 
+```
+example (x y z : ℚ) (h1 : 2*x  < 3*y) (h2 : -4*x + 2*z < 0) 
+        (h3 : 12*y - 4* z < 0)  : false :=
+by linarith
+```
+
+`linarith` will use all appropriate hypotheses and the negation of the goal, if applicable.
+`linarith h1 h2 h3` will ohly use the local hypotheses `h1`, `h2`, `h3`.
+`linarith using [t1, t2, t3] will add `t1`, `t2`, `t3` to the local context and then run 
+`linarith`.
+`linarith {discharger := tac, restrict_type := tp}` takes a config object with two optional 
+arguments. `discharger` specifies a tactic to be used for reducing an algebraic equation in the
+proof stage. The default is `ring`. Other options currently include `ring SOP` or `simp` for basic
+problems. `restrict_type` will only use hypotheses that are inequalities over `tp`. This is useful
+if you have e.g. both integer and rational valued inequalities in the local context, which can
+sometimes confuse the tactic.

meta/rb_map.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2018 Robert Y. Lewis. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Robert Y. Lewis
+
+Additional operations on native rb_maps and rb_sets.
+-/
+import data.option
+
+namespace native
+namespace rb_set 
+
+meta def filter {key} (s : rb_set key) (P : key → bool) : rb_set key :=
+s.fold s (λ a m, if P a then m else m.erase a)
+
+meta def union {key} (s t : rb_set key) : rb_set key :=
+s.fold t (λ a t, t.insert a)
+
+end rb_set 
+
+namespace rb_map 
+
+meta def ifind {α β} [inhabited β] (m : rb_map α β) (a : α) : β :=
+(m.find a).iget
+
+meta def zfind {α β} [has_zero β] (m : rb_map α β) (a : α) : β :=
+(m.find a).get_or_else 0
+
+meta def add {α β} [has_add β] [has_zero β] [decidable_eq β] (m1 m2 : rb_map α β) : rb_map α β :=
+m1.fold m2 
+  (λ n v m, 
+   let nv := v + m2.zfind n in
+   if nv = 0 then m.erase n else m.insert n nv)
+
+meta def scale {α β} [has_lt α] [decidable_rel ((<) : α → α → Prop)] [has_mul β] (b : β) (m : rb_map α β) : rb_map α β :=
+m.map ((*) b)
+
+end rb_map 
+end native

tactic/basic.lean

@@ -509,7 +509,12 @@ do l ← local_context,
 
 run_cmd add_interactive [`injections_and_clear]
 
+meta def note_anon (e : expr) : tactic unit :=
+do n ← get_unused_name "lh",
+   note n none e, skip 
+
 meta def find_local (t : pexpr) : tactic expr :=
 do t' ← to_expr t,
    prod.snd <$> solve_aux t' assumption
-end tactic
+
+end tactic