feat(tactic/linarith): better input syntax linarith only [...]

docs/tactics.md

@@ -555,10 +555,18 @@ 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 [t1, t2, t3]` will additionally use proof terms `t1, t2, t3`.
 
-`linarith using [t1, t2, t3]` will add `t1`, `t2`, `t3` to the local context and then run
-`linarith`.
+`linarith only [h1, h2, h3, t1, t2, t3]` will use only the goal (if relevant), local hypotheses
+h1, h2, h3, and proofs t1, t2, t3. It will ignore the rest of the local context.
+
+`linarith!` will use a stronger reducibility setting to try to identify atoms. For example,
+```lean
+example (x : ℚ) : id x ≥ x :=
+by linarith
+```
+will fail, because `linarith` will not identify `x` and `id x`. `linarith!` will.
+This can sometimes be expensive.
 
 `linarith {discharger := tac, restrict_type := tp, exfalso := ff}` takes a config object with three optional
 arguments.

src/analysis/complex/exponential.lean

@@ -175,7 +175,7 @@ lemma pi_div_two_pos : 0 < π / 2 :=
 half_pos pi_pos
 
 lemma two_pi_pos : 0 < 2 * π :=
-by linarith using [pi_pos]
+by linarith [pi_pos]
 
 @[simp] lemma sin_pi : sin π = 0 :=
 by rw [← mul_div_cancel_left pi (@two_ne_zero ℝ _), two_mul, add_div,
@@ -385,9 +385,9 @@ lemma cos_lt_cos_of_nonneg_of_le_pi {x y : ℝ} (hx₁ : 0 ≤ x) (hx₂ : x ≤
 match (le_total x (π / 2) : x ≤ π / 2 ∨ π / 2 ≤ x), le_total y (π / 2) with
 | or.inl hx, or.inl hy := cos_lt_cos_of_nonneg_of_le_pi_div_two hx₁ hx hy₁ hy hxy
 | or.inl hx, or.inr hy := (lt_or_eq_of_le hx).elim
-  (λ hx, calc cos y ≤ 0 : cos_nonpos_of_pi_div_two_le_of_le hy (by linarith using [pi_pos])
+  (λ hx, calc cos y ≤ 0 : cos_nonpos_of_pi_div_two_le_of_le hy (by linarith [pi_pos])
     ... < cos x : cos_pos_of_neg_pi_div_two_lt_of_lt_pi_div_two (by linarith) hx)
-  (λ hx, calc cos y < 0 : cos_neg_of_pi_div_two_lt_of_lt (by linarith) (by linarith using [pi_pos])
+  (λ hx, calc cos y < 0 : cos_neg_of_pi_div_two_lt_of_lt (by linarith) (by linarith [pi_pos])
     ... = cos x : by rw [hx, cos_pi_div_two])
 | or.inr hx, or.inl hy := by linarith
 | or.inr hx, or.inr hy := neg_lt_neg_iff.1 (by rw [← cos_pi_sub, ← cos_pi_sub];
@@ -590,7 +590,7 @@ sin_inj_of_le_of_le_pi_div_two
 sin_inj_of_le_of_le_pi_div_two
   (neg_pi_div_two_le_arcsin _)
   (arcsin_le_pi_div_two _)
-  (by linarith using [pi_pos])
+  (by linarith [pi_pos])
   (le_refl _)
   (by rw [sin_arcsin, sin_pi_div_two]; norm_num)
 
@@ -641,10 +641,10 @@ lemma arccos_eq_pi_div_two_sub_arcsin (x : ℝ) : arccos x = π / 2 - arcsin x :
 lemma arcsin_eq_pi_div_two_sub_arccos (x : ℝ) : arcsin x = π / 2 - arccos x := by simp [arccos]
 
 lemma arccos_le_pi (x : ℝ) : arccos x ≤ π :=
-by unfold arccos; linarith using [neg_pi_div_two_le_arcsin x]
+by unfold arccos; linarith [neg_pi_div_two_le_arcsin x]
 
 lemma arccos_nonneg (x : ℝ) : 0 ≤ arccos x :=
-by unfold arccos; linarith using [arcsin_le_pi_div_two x]
+by unfold arccos; linarith [arcsin_le_pi_div_two x]
 
 lemma cos_arccos {x : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) : cos (arccos x) = x :=
 by rw [arccos, cos_pi_div_two_sub, sin_arcsin hx₁ hx₂]
@@ -707,10 +707,10 @@ match lt_or_eq_of_le h0x, lt_or_eq_of_le hxp with
 end
 
 lemma tan_neg_of_neg_of_pi_div_two_lt {x : ℝ} (hx0 : x < 0) (hpx : -(π / 2) < x) : tan x < 0 :=
-neg_pos.1 (tan_neg x ▸ tan_pos_of_pos_of_lt_pi_div_two (by linarith) (by linarith using [pi_pos]))
+neg_pos.1 (tan_neg x ▸ tan_pos_of_pos_of_lt_pi_div_two (by linarith) (by linarith [pi_pos]))
 
 lemma tan_nonpos_of_nonpos_of_neg_pi_div_two_le {x : ℝ} (hx0 : x ≤ 0) (hpx : -(π / 2) ≤ x) : tan x ≤ 0 :=
-neg_nonneg.1 (tan_neg x ▸ tan_nonneg_of_nonneg_of_le_pi_div_two (by linarith) (by linarith using [pi_pos]))
+neg_nonneg.1 (tan_neg x ▸ tan_nonneg_of_nonneg_of_le_pi_div_two (by linarith) (by linarith [pi_pos]))
 
 lemma tan_lt_tan_of_nonneg_of_lt_pi_div_two {x y : ℝ} (hx₁ : 0 ≤ x) (hx₂ : x < π / 2) (hy₁ : 0 ≤ y)
   (hy₂ : y < π / 2) (hxy : x < y) : tan x < tan y :=
@@ -827,7 +827,7 @@ else
       exact real.arcsin_nonpos (by rw [neg_im, neg_div, neg_nonpos]; exact div_nonneg hx₂ (abs_pos.2 hx)))
   else by rw [arg, if_neg hx₁, if_neg hx₂];
       exact sub_le_iff_le_add.2 (le_trans (real.arcsin_le_pi_div_two _)
-        (by linarith using [real.pi_pos]))
+        (by linarith [real.pi_pos]))
 
 lemma neg_pi_lt_arg (x : ℂ) : -π < arg x :=
 if hx₁ : 0 ≤ x.re
@@ -838,7 +838,7 @@ else
   if hx₂ : 0 ≤ x.im
   then by rw [arg, if_neg hx₁, if_pos hx₂];
     exact sub_lt_iff_lt_add.1
-      (lt_of_lt_of_le (by linarith using [real.pi_pos]) (real.neg_pi_div_two_le_arcsin _))
+      (lt_of_lt_of_le (by linarith [real.pi_pos]) (real.neg_pi_div_two_le_arcsin _))
   else by rw [arg, if_neg hx₁, if_neg hx₂];
     exact lt_sub_iff_add_lt.2 (by rw neg_add_self;
       exact real.arcsin_pos (by rw [neg_im]; exact div_pos (neg_pos.2 (lt_of_not_ge hx₂))

src/data/complex/exponential.lean

@@ -836,7 +836,7 @@ calc x + 1 ≤ lim (⟨(λ n : ℕ, ((exp' x) n).re), is_cau_seq_re (exp' x)⟩
 ... = exp x : by rw [exp, complex.exp, ← cau_seq_re, lim_re]
 
 lemma one_le_exp {x : ℝ} (hx : 0 ≤ x) : 1 ≤ exp x :=
-by linarith using [add_one_le_exp_of_nonneg hx]
+by linarith [add_one_le_exp_of_nonneg hx]
 
 lemma exp_pos (x : ℝ) : 0 < exp x :=
 (le_total 0 x).elim (lt_of_lt_of_le zero_lt_one ∘ one_le_exp)

src/tactic/core.lean

@@ -626,9 +626,9 @@ do l ← local_context,
    r ← successes (l.reverse.map (λ h, cases h >> skip)),
    when (r.empty) failed
 
-meta def note_anon (e : expr) : tactic unit :=
+meta def note_anon (e : expr) : tactic expr :=
 do n ← get_unused_name "lh",
-   note n none e, skip
+   note n none e
 
 /-- `find_local t` returns a local constant with type t, or fails if none exists. -/
 meta def find_local (t : pexpr) : tactic expr :=

src/tactic/linarith.lean

@@ -286,21 +286,21 @@ meta def list.mfind {α} (tac : α → tactic unit) : list α → tactic α
 | [] := failed
 | (h::t) := tac h >> return h <|> list.mfind t
 
-meta def rb_map.find_defeq {v} (m : expr_map v) (e : expr) : tactic v :=
-prod.snd <$> list.mfind (λ p, is_def_eq e p.1) m.to_list
+meta def rb_map.find_defeq (red : transparency) {v} (m : expr_map v) (e : expr) : tactic v :=
+prod.snd <$> list.mfind (λ p, is_def_eq e p.1 red) m.to_list
 
 /--
   Turns an expression into a map from ℕ to ℤ, for use in a comp object.
     The expr_map ℕ argument identifies which expressions have already been assigned numbers.
     Returns a new map.
 -/
-meta def map_of_expr : expr_map ℕ → expr → tactic (expr_map ℕ × rb_map ℕ ℤ)
+meta def map_of_expr (red : transparency) : expr_map ℕ → expr → tactic (expr_map ℕ × rb_map ℕ ℤ)
 | m e@`(%%e1 * %%e2) :=
    (do (m', comp1) ← map_of_expr m e1,
       (m', comp2) ← map_of_expr m' e2,
       mp ← map_of_expr_mul_aux comp1 comp2,
       return (m', mp)) <|>
-   (do k ← rb_map.find_defeq m e, return (m, mk_rb_map.insert k 1)) <|>
+   (do k ← rb_map.find_defeq red m e, return (m, mk_rb_map.insert k 1)) <|>
    (let n := m.size + 1 in return (m.insert e n, mk_rb_map.insert n 1))
 | m `(%%e1 + %%e2) :=
    do (m', comp1) ← map_of_expr m e1,
@@ -316,7 +316,7 @@ meta def map_of_expr : expr_map ℕ → expr → tactic (expr_map ℕ × rb_map
   | some 0 := return ⟨m, mk_rb_map⟩
   | some z := return ⟨m, mk_rb_map.insert 0 z⟩
   | none :=
-    (do k ← rb_map.find_defeq m e, return (m, mk_rb_map.insert k 1)) <|>
+    (do k ← rb_map.find_defeq red m e, return (m, mk_rb_map.insert k 1)) <|>
     (let n := m.size + 1 in return (m.insert e n, mk_rb_map.insert n 1))
   end
 
@@ -326,16 +326,16 @@ meta def parse_into_comp_and_expr : expr → option (ineq × expr)
 | `(%%e = 0) := (ineq.eq, e)
 | _ := none
 
-meta def to_comp (e : expr) (m : expr_map ℕ) : tactic (comp × expr_map ℕ) :=
+meta def to_comp (red : transparency) (e : expr) (m : expr_map ℕ) : tactic (comp × expr_map ℕ) :=
 do (iq, e) ← parse_into_comp_and_expr e,
-   (m', comp') ← map_of_expr m e,
+   (m', comp') ← map_of_expr red m e,
    return ⟨⟨iq, comp'⟩, m'⟩
 
-meta def to_comp_fold : expr_map ℕ → list expr →
+meta def to_comp_fold (red : transparency) : expr_map ℕ → list expr →
       tactic (list (option comp) × expr_map ℕ)
 | m [] := return ([], m)
 | m (h::t) :=
-  (do (c, m') ← to_comp h m,
+  (do (c, m') ← to_comp red h m,
       (l, mp) ← to_comp_fold m' t,
       return (c::l, mp)) <|>
   (do (l, mp) ← to_comp_fold m t,
@@ -344,18 +344,18 @@ meta def to_comp_fold : expr_map ℕ → list expr →
 /--
   Takes a list of proofs of props of the form t {<, ≤, =} 0, and creates a linarith_structure.
 -/
-meta def mk_linarith_structure (l : list expr) : tactic (linarith_structure × rb_map ℕ (expr × expr)) :=
+meta def mk_linarith_structure (red : transparency) (l : list expr) : tactic (linarith_structure × rb_map ℕ (expr × expr)) :=
 do pftps ← l.mmap infer_type,
-  (l', map) ← to_comp_fold mk_rb_map pftps,
+  (l', map) ← to_comp_fold red mk_rb_map pftps,
   let lz := list.enum $ ((l.zip pftps).zip l').filter_map (λ ⟨a, b⟩, prod.mk a <$> b),
   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.succ,
   let pc : rb_set pcomp := rb_map.set_of_list $
     lz.map (λ ⟨n, x⟩, ⟨x.2, comp_source.assump n⟩),
   return (⟨vars, pc⟩, prmap)
 
-meta def linarith_monad.run {α} (tac : linarith_monad α) (l : list expr) : tactic ((pcomp ⊕ α) × rb_map ℕ (expr × expr)) :=
-do (struct, inputs) ← mk_linarith_structure l,
+meta def linarith_monad.run (red : transparency) {α} (tac : linarith_monad α) (l : list expr) : tactic ((pcomp ⊕ α) × rb_map ℕ (expr × expr)) :=
+do (struct, inputs) ← mk_linarith_structure red l,
 match (state_t.run (validate >> tac) struct).run with
 | (except.ok (a, _)) := return (sum.inr a, inputs)
 | (except.error contr) := return (sum.inl contr, inputs)
@@ -450,6 +450,7 @@ meta structure linarith_config :=
 (restrict_type : option Type := none)
 (restrict_type_reflect : reflected restrict_type . apply_instance)
 (exfalso : bool := tt)
+(transparency : transparency := reducible)
 
 meta def ineq_pf_tp (pf : expr) : tactic expr :=
 do (_, z) ← infer_type pf >>= get_rel_sides,
@@ -482,7 +483,7 @@ meta def prove_false_by_linarith1 (cfg : linarith_config) : list expr → tactic
 | l@(h::t) :=
   do l' ← add_neg_eq_pfs l,
      hz ← ineq_pf_tp h >>= mk_neg_one_lt_zero_pf,
-     (sum.inl contr, inputs) ← elim_all_vars.run (hz::l')
+     (sum.inl contr, inputs) ← elim_all_vars.run cfg.transparency (hz::l')
        | fail "linarith failed to find a contradiction",
      let coeffs := inputs.keys.map (λ k, (contr.src.flatten.ifind k)),
      let pfs : list expr := inputs.keys.map (λ k, (inputs.ifind k).1),
@@ -780,36 +781,63 @@ open lean lean.parser interactive tactic interactive.types
 local postfix `?`:9001 := optional
 local postfix *:9001 := many
 
-meta def linarith.interactive_aux (cfg : linarith_config) : option expr →
-     parse ident* → (parse (tk "using" *> pexpr_list)?) → tactic unit
-| pt l (some pe) := pe.mmap (λ p, i_to_expr p >>= note_anon) >> linarith.interactive_aux pt l none
-| pt [] none :=
-  do t ← target,
-     if t = `(false) then local_context >>= prove_false_by_linarith cfg pt
-     else match get_contr_lemma_name t with
-     | some nm := seq (applyc nm) (do t ← intro1 >>= ineq_pf_tp, linarith.interactive_aux (some t) [] none)
-     | none := if cfg.exfalso then exfalso >> linarith.interactive_aux pt [] none
-               else fail "linarith failed: target type is not an inequality."
-     end
-| pt ls none := (ls.mmap get_local) >>= prove_false_by_linarith cfg pt
+meta def linarith.elab_arg_list : option (list pexpr) → tactic (list expr)
+| none := return []
+| (some l) := l.mmap i_to_expr
+
+meta def linarith.preferred_type_of_goal : option expr → tactic (option expr)
+| none := return none
+| (some e) := some <$> ineq_pf_tp e
+
+/--
+linarith.interactive_aux cfg o_goal restrict_hyps args:
+ * cfg is a linarith_config object
+ * o_goal : option expr is the local constant corresponding to the former goal, if there was one
+ * restrict_hyps : bool is tt if `linarith only [...]` was used
+ * args : option (list pexpr) is the optional list of arguments in `linarith [...]`
+-/
+meta def linarith.interactive_aux (cfg : linarith_config) :
+  option expr → bool → option (list pexpr) → tactic unit
+| none tt none := fail "linarith only called with no arguments"
+| none tt (some l) := l.mmap i_to_expr >>= prove_false_by_linarith cfg none
+| (some e) tt l :=
+  do tp ← ineq_pf_tp e,
+     list.cons e <$> linarith.elab_arg_list l >>= prove_false_by_linarith cfg (some tp)
+| oe ff l :=
+  do otp ← linarith.preferred_type_of_goal oe,
+     list.append <$> local_context <*>
+      (list.filter (λ a, bnot $ expr.is_local_constant a) <$> linarith.elab_arg_list l) >>=
+     prove_false_by_linarith cfg otp
 
 /--
   Tries to prove a goal of `false` by linear arithmetic on hypotheses.
   If the goal is a linear (in)equality, tries to prove it by contradiction.
   If the goal is not `false` or an inequality, applies `exfalso` and tries linarith on the
   hypotheses.
   `linarith` will use all relevant hypotheses in the local context.
-  `linarith h1 h2 h3` will only use hypotheses h1, h2, h3.
-  `linarith using [t1, t2, t3]` will add proof terms t1, t2, t3 to the local context.
+  `linarith [t1, t2, t3]` will add proof terms t1, t2, t3 to the local context.
+  `linarith only [h1, h2, h3, t1, t2, t3]` will use only the goal (if relevant), local hypotheses
+    h1, h2, h3, and proofs t1, t2, t3. It will ignore the rest of the local context.
+  `linarith!` will use a stronger reducibility setting to identify atoms.
 
   Config options:
   `linarith {exfalso := ff}` will fail on a goal that is neither an inequality nor `false`
   `linarith {restrict_type := T}` will run only on hypotheses that are inequalities over `T`
   `linarith {discharger := tac}` will use `tac` instead of `ring` for normalization.
     Options: `ring2`, `ring SOP`, `simp`
 -/
-meta def tactic.interactive.linarith (ids : parse (many ident))
-     (using_hyps : parse (tk "using" *> pexpr_list)?) (cfg : linarith_config := {}) : tactic unit :=
-linarith.interactive_aux cfg none ids using_hyps
+meta def tactic.interactive.linarith (red : parse ((tk "!")?))
+  (restr : parse ((tk "only")?)) (hyps : parse pexpr_list?)
+  (cfg : linarith_config := {}) : tactic unit :=
+let cfg :=
+  if red.is_some then {cfg with transparency := semireducible, discharger := `[ring!]}
+  else cfg in
+do t ← target,
+   match get_contr_lemma_name t with
+   | some nm := seq (applyc nm) $
+     do t ← intro1, linarith.interactive_aux cfg (some t) restr.is_some hyps
+   | none := if cfg.exfalso then exfalso >> linarith.interactive_aux cfg none restr.is_some hyps
+             else fail "linarith failed: target type is not an inequality."
+   end
 
 end