refactor(tactic/linarith): big refactor and docs (#3113)

This PR:
* Splits `linarith` into multiple files for organizational purposes
* Uses the general `zify` and `cancel_denom` tactics instead of weaker custom versions
* Refactors many components of `linarith`, in particular,
* Modularizes `linarith` preprocessing, so that users can insert custom steps
* Implements `nlinarith` preprocessing as such a custom step, so it happens at the correct point of the preprocessing stage
* Better encapsulates the FM elimination module, to make it easier to plug in alternate oracles if/when they exist
* Docs, docs, docs

The change to zification means that some goals which involved multiplication of natural numbers will no longer be solved. However, others are now in scope. `nlinarith` is a possible drop-in replacement; otherwise, generalize the product of naturals to a single natural, and `linarith` should still succeed.



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

archive/imo1988_q6.lean

@@ -212,7 +212,7 @@ begin
     apply ne_of_lt,
     calc x*x + x*x = x*x * 2       : by rw mul_two
                ... ≤ x*x * k       : nat.mul_le_mul_left (x*x) k_lt_one
-               ... < (x*x + 1) * k : by apply mul_lt_mul; linarith },
+               ... < (x*x + 1) * k : by linarith },
   { -- Show the descent step.
     intros x y hx x_lt_y hxky h z h_root hV₁ hV₀,
     split,

src/data/list/defs.lean

@@ -166,6 +166,10 @@ def find (p : α → Prop) [decidable_pred p] : list α → option α
 | []     := none
 | (a::l) := if p a then some a else find l
 
+/-- `mfind tac l` returns the first element of `l` on which `tac` succeeds, and fails otherwise. -/
+def mfind {α} {m : Type → Type u} [monad m] [alternative m] (tac : α → m unit) : list α → m α :=
+list.mfirst $ λ a, tac a $> a
+
 def find_indexes_aux (p : α → Prop) [decidable_pred p] : list α → nat → list nat
 | []     n := []
 | (a::l) n := let t := find_indexes_aux l (succ n) in if p a then n :: t else t
@@ -525,7 +529,19 @@ def mmap_filter {m : Type → Type v} [monad m] {α β} (f : α → m (option β
   match b with none := t' | (some x) := x::t' end
 
 /--
-`mmap'_diag f l` calls `f` on all elements in the "upper diagonal" of `l × l`.
+`mmap_upper_triangle f l` calls `f` on all elements in the upper triangular part of `l × l`.
+That is, for each `e ∈ l`, it will run `f e e` and then `f e e'`
+for each `e'` that appears after `e` in `l`.
+
+Example: suppose `l = [1, 2, 3]`. `mmap_upper_triangle f l` will produce the list
+`[f 1 1, f 1 2, f 1 3, f 2 2, f 2 3, f 3 3]`.
+-/
+def mmap_upper_triangle {m} [monad m] {α β : Type u} (f : α → α → m β) : list α → m (list β)
+| [] := return []
+| (h::t) := do v ← f h h, l ← t.mmap (f h), t ← t.mmap_upper_triangle, return $ (v::l) ++ t
+
+/--
+`mmap'_diag f l` calls `f` on all elements in the upper triangular part of `l × l`.
 That is, for each `e ∈ l`, it will run `f e e` and then `f e e'`
 for each `e'` that appears after `e` in `l`.
 

src/meta/expr.lean

@@ -231,6 +231,15 @@ meta def int.mk_numeral (type has_zero has_one has_add has_neg : expr) : ℤ →
 | -[1+n] := let ne := (n+1).mk_numeral type has_zero has_one has_add in
             `(@has_neg.neg.{0} %%type %%has_neg %%ne)
 
+/--
+`nat.to_pexpr n` creates a `pexpr` that will evaluate to `n`.
+The `pexpr` does not hold any typing information:
+`to_expr ``((%%(nat.to_pexpr 5) : ℤ))` will create a native integer numeral `(5 : ℤ)`.
+-/
+meta def nat.to_pexpr : ℕ → pexpr
+| 0 := ``(0)
+| 1 := ``(1)
+| n := if n % 2 = 0 then ``(bit0 %%(nat.to_pexpr (n/2))) else ``(bit1 %%(nat.to_pexpr (n/2)))
 namespace expr
 
 /--
@@ -354,6 +363,15 @@ e.fold mk_name_set $ λ e' _ l,
 meta def contains_constant (e : expr) (p : name → Prop) [decidable_pred p] : bool :=
 e.fold ff (λ e' _ b, if p (e'.const_name) then tt else b)
 
+/--
+`app_symbol_in e l` returns true iff `e` is an application of a constant whose name is in `l`.
+-/
+meta def app_symbol_in (e : expr) (l : list name) : bool :=
+match e.get_app_fn with
+| (expr.const n _) := n ∈ l
+| _ := ff
+end
+
 /-- `get_simp_args e` returns the arguments of `e` that simp can reach via congruence lemmas. -/
 meta def get_simp_args (e : expr) : tactic (list expr) :=
 -- `mk_specialized_congr_lemma_simp` throws an assertion violation if its argument is not an app
@@ -727,10 +745,10 @@ end expr
 namespace declaration
 open tactic
 
-/-- 
-`declaration.update_with_fun f tgt decl` 
+/--
+`declaration.update_with_fun f tgt decl`
 sets the name of the given `decl : declaration` to `tgt`, and applies `f` to the names
-of all `expr.const`s which appear in the value or type of `decl`. 
+of all `expr.const`s which appear in the value or type of `decl`.
 -/
 protected meta def update_with_fun (f : name → name) (tgt : name) (decl : declaration) :
   declaration :=

src/meta/rb_map.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Robert Y. Lewis
 -/
 import data.option.defs
+import data.list.defs
 
 /-!
 # rb_map
@@ -14,6 +15,8 @@ and are generally the most efficient dictionary structures to use for pure metap
 -/
 
 namespace native
+
+/-! ### Declarations about `rb_set` -/
 namespace rb_set
 
 meta instance {key} [has_lt key] [decidable_rel ((<) : key → key → Prop)] :
@@ -41,9 +44,9 @@ It takes a user_provided `rb_set` to use for the base case.
 This can be used to pre-seed the set with additional elements,
 and/or to use a custom comparison operator.
 -/
-meta def of_list_core {key} (base : native.rb_set key) : list key → native.rb_map key unit
+meta def of_list_core {key} (base : rb_set key) : list key → rb_map key unit
 | []      := base
-| (x::xs) := native.rb_set.insert (of_list_core xs) x
+| (x::xs) := rb_set.insert (of_list_core xs) x
 
 /--
 `of_list l` transforms a list `l : list key` into an `rb_set`,
@@ -63,6 +66,8 @@ s2.fold s1 $ λ v s, s.erase v
 
 end rb_set
 
+/-! ### Declarations about `rb_map` -/
+
 namespace rb_map
 
 meta instance {key data : Type} [has_lt key] [decidable_rel ((<) : key → key → Prop)] :
@@ -126,6 +131,8 @@ end
 
 end rb_map
 
+/-! ### Declarations about `rb_lmap` -/
+
 namespace rb_lmap
 
 meta instance (key : Type) [has_lt key] [decidable_rel ((<) : key → key → Prop)] (data : Type) :
@@ -145,6 +152,8 @@ m.fold [] (λ _, (++))
 end rb_lmap
 end native
 
+/-! ### Declarations about `name_set` -/
+
 namespace name_set
 
 meta instance : inhabited name_set := ⟨mk_name_set⟩
@@ -177,6 +186,8 @@ l.foldr (λ n s', s'.insert n) s
 
 end name_set
 
+/-! ### Declarations about `name_map` -/
+
 namespace name_map
 
 meta instance {data : Type} : inhabited (name_map data) :=

src/tactic/cancel_denoms.lean

@@ -17,11 +17,6 @@ This file defines tactics that cancel numeric denominators from field expression
 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`.
 
-See also the `field_simp` tactic, which tries to do a similar simplification for field expressions.
-The tactics are not related: `field_simp` handles non-numeral denominators, but has limited support
-for numerals; `field_simp` does not multiply by new terms to cancel denominators, it just
-produces an equal expression.
-
 ## Implementation notes
 
 The tooling here was originally written for `linarith`, not intended as an interactive tactic.
@@ -232,11 +227,6 @@ begin
   exact h
 end
 ```
-
-See also the `field_simp` tactic, which tries to do a similar simplification for field expressions.
-The tactics are not related: `field_simp` handles non-numeral denominators, but has limited support
-for numerals; `field_simp` does not multiply by new terms to cancel denominators, it just
-produces an equal expression.
 -/
 meta def tactic.interactive.cancel_denoms (l : parse location) : tactic unit :=
 do locs ← l.get_locals,

src/tactic/core.lean

@@ -2114,3 +2114,12 @@ add_tactic_doc
   tags                     := ["simplification"] }
 
 end tactic
+
+/--
+`find_defeq red m e` looks for a key in `m` that is defeq to `e` (up to transparency `red`),
+and returns the value associated with this key if it exists.
+Otherwise, it fails.
+-/
+meta def list.find_defeq (red : tactic.transparency) {v} (m : list (expr × v)) (e : expr) :
+  tactic (expr × v) :=
+m.mfind $ λ ⟨e', val⟩, tactic.is_def_eq e e' red