fix(tactic/linarith): elaborate and insert arguments before destructing hypotheses (#5501)

closes #5480

Arguments to `linarith` can depend on hypotheses (e.g. conjunctions) that get destructed during preprocessing, after which the arguments will no longer elaborate or typecheck. This just moves the elaboration earlier and adds these arguments as hypotheses themselves.



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

Author: robertylewis

src/tactic/linarith/frontend.lean

@@ -242,7 +242,8 @@ do t ← target,
 if t.is_eq.is_some then
   linarith_trace "target is an equality: splitting" >>
     seq' (applyc ``eq_of_not_lt_of_not_gt) tactic.linarith else
-do when cfg.split_hypotheses (linarith_trace "trying to split hypotheses" >> try auto.split_hyps),
+do hyps ← hyps.mmap $ λ e, i_to_expr e >>= note_anon none,
+   when cfg.split_hypotheses (linarith_trace "trying to split hypotheses" >> try auto.split_hyps),
 /- If we are proving a comparison goal (and not just `false`), we consider the type of the
    elements in the comparison to be the "preferred" type. That is, if we find comparison
    hypotheses in multiple types, we will run `linarith` on the goal type first.
@@ -255,7 +256,6 @@ do when cfg.split_hypotheses (linarith_trace "trying to split hypotheses" >> try
    let cfg := cfg.update_reducibility reduce_semi,
    let (pref_type, new_var) := pref_type_and_new_var_from_tgt.elim (none, none) (λ ⟨a, b⟩, (some a, some b)),
    -- set up the list of hypotheses, considering the `only_on` and `restrict_type` options
-   hyps ← hyps.mmap i_to_expr,
    hyps ← if only_on then return (new_var.elim [] singleton ++ hyps) else (++ hyps) <$> local_context,
    hyps ← (do t ← get_restrict_type cfg.restrict_type_reflect, filter_hyps_to_type t hyps) <|> return hyps,
    linarith_trace_proofs "linarith is running on the following hypotheses:" hyps,

test/linarith.lean

@@ -392,3 +392,6 @@ by linarith {split_ne := tt}
 example (x y : ℚ) (h₁ : 0 ≤ y) (h₂ : y ≤ x) : y * x ≤ x * x := by nlinarith
 
 example (x y : ℚ) (h₁ : 0 ≤ y) (h₂ : y ≤ x) : y * x ≤ x ^ 2 := by nlinarith
+
+axiom foo {x : int} : 1 ≤ x → 1 ≤ x*x
+lemma bar (x y: int)(h : 0 ≤ y ∧ 1 ≤ x) : 1 ≤ y + x*x := by linarith [foo h.2]