From 58d83ed5268d96bd37757ac03062a4d69e5aa435 Mon Sep 17 00:00:00 2001
From: Arthur Paulino <arthurleonardo.ap@gmail.com>
Date: Fri, 6 May 2022 16:39:40 +0000
Subject: [PATCH] feat(tactic/lint/misc): adding a linter that flags iffs with
 explicit variables on both sides (#11606)

---
 src/tactic/lint/default.lean |  7 +++--
 src/tactic/lint/misc.lean    | 53 +++++++++++++++++++++++++++++++++++-
 2 files changed, 56 insertions(+), 4 deletions(-)

diff --git a/src/tactic/lint/default.lean b/src/tactic/lint/default.lean
index b3a03b928d748..2db842856f084 100644
--- a/src/tactic/lint/default.lean
+++ b/src/tactic/lint/default.lean
@@ -63,10 +63,11 @@ The following linters are run by default:
 21. `syn_taut` checks that declarations are not syntactic tautologies.
 22. `check_reducibility` checks whether non-instances with a class as type are reducible.
 23. `unprintable_interactive` checks that interactive tactics have parser documentation.
-24. `to_additive_doc` checks if additive versions of lemmas have documentation
+24. `to_additive_doc` checks if additive versions of lemmas have documentation.
 
-Another linter, `doc_blame_thm`, checks for missing doc strings on lemmas and theorems.
-This is not run by default.
+The following linters are not run by default:
+1. `doc_blame_thm`, checks for missing doc strings on lemmas and theorems.
+2. `explicit_vars_of_iff` checks if there are explicit variables used on both sides of an iff.
 
 The command `#list_linters` prints a list of the names of all available linters.
 
diff --git a/src/tactic/lint/misc.lean b/src/tactic/lint/misc.lean
index 58550d77ed4bc..78ddc7dc12693 100644
--- a/src/tactic/lint/misc.lean
+++ b/src/tactic/lint/misc.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Floris van Doorn, Robert Y. Lewis
+Authors: Floris van Doorn, Robert Y. Lewis, Arthur Paulino
 -/
 import data.bool.basic
 import meta.rb_map
@@ -449,6 +449,7 @@ meta def linter.unused_haves_suffices : linter :=
 "proofs appear as if they are used. ",
   is_fast := ff }
 
+
 /-!
 ## Linter for unprintable interactive tactics
 -/
@@ -481,3 +482,53 @@ meta def linter.unprintable_interactive : linter :=
 "like `?` `*>` `<*` `<*>` `<|>` and `<$>` (but not `>>=` or `do` blocks) " ++
 "that automatically generate a description.",
   is_fast := tt }
+
+
+/-!
+## Linter for iff's
+-/
+
+open binder_info
+
+/--
+Recursively consumes a Pi expression while accumulating names and the complement of de-Bruijn
+indexes of explicit variables, ultimately obtaining the remaining non-Pi expression as well.
+-/
+meta def unravel_explicits_of_pi :
+  expr → ℕ → list name → list ℕ → (list name) × (list ℕ) × expr
+| (pi n default _ e) i ln li := unravel_explicits_of_pi e (i + 1) (n :: ln) (i :: li)
+| (pi n _ _ e)       i ln li := unravel_explicits_of_pi e (i + 1) ln        li
+| e                  _ ln li := (ln, li, e)
+
+/--
+This function works as follows:
+1. Call `unravel_explicits_of_pi` to obtain the names, complements of de-Bruijn indexes and the
+remaining non-Pi expression;
+2. Check if the remaining non-Pi expression is an iff, already obtaining the respective left and
+right expressions if this is the case. Returns `none` otherwise;
+3. Filter the explicit variables that appear on the left *and* right side of the iff;
+4. If no variable satisfies the condition above, return `none`;
+5. Return a message mentioning the variables that do, otherwise.
+-/
+meta def explicit_vars_of_iff (d : declaration) :
+    tactic (option string) := do
+  let (ln, li, e) := unravel_explicits_of_pi d.type 0 [] [],
+  match e.is_iff with
+  | none          := return none
+  | some (el, er) := do
+    let li := li.map (λ i, d.type.pi_arity - i - 1), -- fixing for the actual de-Bruijn indexes
+    let l := (ln.zip li).filter (λ t, (el.has_var_idx t.2) && (er.has_var_idx t.2)),
+    if l = [] then return none
+    else return $ "The following variables are used on both sides of an iff and ".append $
+      "should be made implicit: ".append $ ", ".intercalate (l.map (λ t, to_string t.1))
+  end
+
+/--
+A linter for checking if variables appearing on both sides of an iff are explicit. Ideally, such
+variables should be implicit instead.
+-/
+meta def linter.explicit_vars_of_iff : linter :=
+{ test := explicit_vars_of_iff,
+  auto_decls := ff,
+  no_errors_found := "No explicit variables on both sides of iff",
+  errors_found := "EXPLICIT VARIABLES ON BOTH SIDES OF IFF" }