feat(tactic/lint/misc): unused arguments checks for more sorry's (#10431

)

* The `unused_arguments` linter now checks whether `sorry` occurs in any of the `_proof_i` declarations and will not raise an error if this is the case
* Two minor changes: `open tactic` in all of `meta.expr` and fix a typo.
* I cannot add a test without adding a `sorry` to the test suite, but this succeeds without linter warning:
```lean
import tactic.lint

/-- dummy doc -/
def one (h : 0 < 1) : {n : ℕ // 0 < n} := ⟨1, sorry⟩

#lint
```





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

src/meta/expr.lean

@@ -17,6 +17,8 @@ This file is mostly for non-tactics. Tactics should generally be placed in `tact
 expr, name, declaration, level, environment, meta, metaprogramming, tactic
 -/
 
+open tactic
+
 attribute [derive has_reflect, derive decidable_eq] binder_info congr_arg_kind
 
 @[priority 100] meta instance has_reflect.has_to_pexpr {α} [has_reflect α] : has_to_pexpr α :=
@@ -274,7 +276,6 @@ protected meta def to_string (b : binder) : string :=
 let (l, r) := b.info.brackets in
 l ++ b.name.to_string ++ " : " ++ b.type.to_string ++ r
 
-open tactic
 meta instance : has_to_string binder := ⟨ binder.to_string ⟩
 meta instance : has_to_format binder := ⟨ λ b, b.to_string ⟩
 meta instance : has_to_tactic_format binder :=
@@ -374,7 +375,6 @@ end expr
 /-! ### Declarations about `expr` -/
 
 namespace expr
-open tactic
 
 /-- List of names removed by `clean`. All these names must resolve to functions defeq `id`. -/
 meta def clean_ids : list name :=
@@ -586,6 +586,7 @@ e.fold ff (λ e' _ b, if p (e'.const_name) then tt else b)
 
 /--
 Returns true if `e` contains a `sorry`.
+See also `name.contains_sorry`.
 -/
 meta def contains_sorry (e : expr) : bool :=
 e.fold ff (λ e' _ b, if (is_sorry e').is_some then tt else b)
@@ -974,8 +975,6 @@ end environment
 
 namespace expr
 
-open tactic
-
 /-- `is_eta_expansion_of args univs l` checks whether for all elements `(nm, pr)` in `l` we have
   `pr = nm.{univs} args`.
   Used in `is_eta_expansion`, where `l` consists of the projections and the fields of the value we
@@ -1036,7 +1035,6 @@ end expr
 /-! ### Declarations about `declaration` -/
 
 namespace declaration
-open tactic
 
 /--
 `declaration.update_with_fun f test tgt decl`

src/tactic/core.lean

@@ -43,9 +43,9 @@ meta def trans_conv (t₁ t₂ : expr → tactic (expr × expr)) (e : expr) :
   return (e₁, p₁)) <|> t₂ e
 
 end tactic
+open tactic
 
 namespace expr
-open tactic
 
 /-- Given an expr `α` representing a type with numeral structure,
 `of_nat α n` creates the `α`-valued numeral expression corresponding to `n`. -/
@@ -107,6 +107,26 @@ meta def kreplace (e old new : expr) (md := semireducible) (unify := tt)
 
 end expr
 
+namespace name
+
+/--
+`pre.contains_sorry_aux nm` checks whether `sorry` occurs in the value of the declaration `nm`
+or (recusively) in any declarations occurring in the value of `nm` with namespace `pre`.
+Auxiliary function for `name.contains_sorry`. -/
+meta def contains_sorry_aux (pre : name) : name → tactic bool | nm := do
+  env ← get_env,
+  decl ← get_decl nm,
+  ff ← return decl.value.contains_sorry | return tt,
+  (decl.value.list_names_with_prefix pre).mfold ff $
+    λ n b, if b then return tt else n.contains_sorry_aux
+
+/-- `nm.contains_sorry` checks whether `sorry` occurs in the value of the declaration `nm` or
+  in any declarations `nm._proof_i` (or to be more precise: any declaration in namespace `nm`).
+  See also `expr.contains_sorry`. -/
+meta def contains_sorry (nm : name) : tactic bool := nm.contains_sorry_aux nm
+
+end name
+
 namespace interaction_monad
 open result
 
@@ -1118,7 +1138,7 @@ and fail otherwise.
 meta def sorry_if_contains_sorry : tactic unit :=
 do
   g ← target,
-  guard g.contains_sorry <|> fail "goal does not contain `sorrry`",
+  guard g.contains_sorry <|> fail "goal does not contain `sorry`",
   tactic.admit
 
 /-- Fail if the target contains a metavariable. -/

src/tactic/lint/misc.lean

@@ -165,7 +165,7 @@ See also `check_unused_arguments`.
 This tactic additionally filters out all unused arguments of type `parse _`.
 We skip all declarations that contain `sorry` in their value. -/
 private meta def unused_arguments (d : declaration) : tactic (option string) := do
-  ff ← return d.value.contains_sorry | return none,
+  ff ← d.to_name.contains_sorry | return none,
   let ns := check_unused_arguments d,
   tt ← return ns.is_some | return none,
   let ns := ns.iget,