feat(tactic/mk_iff_of_inductive_prop): mk_iff attribute (#4863)

This attribute should make `mk_iff_of_inductive_prop` easier to use.

archive/imo/imo1981_q3.lean

@@ -27,7 +27,7 @@ open int nat set
 section
 variable (N : ℕ) -- N = 1981
 
-structure problem_predicate (m n : ℤ) : Prop :=
+@[mk_iff] structure problem_predicate (m n : ℤ) : Prop :=
 (m_range : m ∈ Ioc 0 (N : ℤ))
 (n_range : n ∈ Ioc 0 (N : ℤ))
 (eq_one : (n ^ 2 - m * n - m ^ 2) ^ 2 = 1)
@@ -43,10 +43,6 @@ except for the base case of `(1, 1)`.
 namespace problem_predicate
 variable {N}
 
-/- This creates a lemma `problem_predicate.iff` that allows `problem_predicate`
-to be unfolded in `norm_num`. -/
-mk_iff_of_inductive_prop problem_predicate problem_predicate.iff
-
 lemma m_le_n {m n : ℤ} (h1 : problem_predicate N m n) : m ≤ n :=
 begin
   by_contradiction h2,
@@ -204,5 +200,5 @@ begin
   have := λ h, @solution_greatest 1981 16 h 3524578,
   simp only [show fib (16:ℕ) = 987 ∧ fib (16+1:ℕ) = 1597,
     by norm_num [fib_succ_succ]] at this,
-  apply_mod_cast this; norm_num [problem_predicate.iff],
+  apply_mod_cast this; norm_num [problem_predicate_iff],
 end

src/data/multiset/basic.lean

@@ -1803,12 +1803,10 @@ section rel
 
 /-- `rel r s t` -- lift the relation `r` between two elements to a relation between `s` and `t`,
 s.t. there is a one-to-one mapping betweem elements in `s` and `t` following `r`. -/
-inductive rel (r : α → β → Prop) : multiset α → multiset β → Prop
+@[mk_iff] inductive rel (r : α → β → Prop) : multiset α → multiset β → Prop
 | zero : rel 0 0
 | cons {a b as bs} : r a b → rel as bs → rel (a ::ₘ as) (b ::ₘ bs)
 
-mk_iff_of_inductive_prop multiset.rel multiset.rel_iff
-
 variables {δ : Type*} {r : α → β → Prop} {p : γ → δ → Prop}
 
 private lemma rel_flip_aux {s t} (h : rel r s t) : rel (flip r) t s :=

src/field_theory/perfect_closure.lean

@@ -84,11 +84,9 @@ section
 variables (K : Type u) [comm_ring K] (p : ℕ) [fact p.prime] [char_p K p]
 
 /-- `perfect_closure K p` is the quotient by this relation. -/
-inductive perfect_closure.r : (ℕ × K) → (ℕ × K) → Prop
+@[mk_iff] inductive perfect_closure.r : (ℕ × K) → (ℕ × K) → Prop
 | intro : ∀ n x, perfect_closure.r (n, x) (n+1, frobenius K p x)
 
-mk_iff_of_inductive_prop perfect_closure.r perfect_closure.r_iff
-
 /-- The perfect closure is the smallest extension that makes frobenius surjective. -/
 def perfect_closure : Type u := quot (perfect_closure.r K p)
 

src/logic/relation.lean

@@ -71,28 +71,23 @@ protected def map (r : α → β → Prop) (f : α → γ) (g : β → δ) : γ
 variables {r : α → α → Prop} {a b c d : α}
 
 /-- `refl_trans_gen r`: reflexive transitive closure of `r` -/
+@[mk_iff relation.refl_trans_gen.cases_tail_iff]
 inductive refl_trans_gen (r : α → α → Prop) (a : α) : α → Prop
 | refl : refl_trans_gen a
 | tail {b c} : refl_trans_gen b → r b c → refl_trans_gen c
 
 attribute [refl] refl_trans_gen.refl
 
-mk_iff_of_inductive_prop relation.refl_trans_gen relation.refl_trans_gen.cases_tail_iff
-
 /-- `refl_gen r`: reflexive closure of `r` -/
-inductive refl_gen (r : α → α → Prop) (a : α) : α → Prop
+@[mk_iff] inductive refl_gen (r : α → α → Prop) (a : α) : α → Prop
 | refl : refl_gen a
 | single {b} : r a b → refl_gen b
 
-mk_iff_of_inductive_prop relation.refl_gen relation.refl_gen_iff
-
 /-- `trans_gen r`: transitive closure of `r` -/
-inductive trans_gen (r : α → α → Prop) (a : α) : α → Prop
+@[mk_iff] inductive trans_gen (r : α → α → Prop) (a : α) : α → Prop
 | single {b} : r a b → trans_gen b
 | tail {b c} : trans_gen b → r b c → trans_gen c
 
-mk_iff_of_inductive_prop relation.trans_gen relation.trans_gen_iff
-
 attribute [refl] refl_gen.refl
 
 lemma refl_gen.to_refl_trans_gen : ∀{a b}, refl_gen r a b → refl_trans_gen r a b

src/tactic/core.lean

@@ -1639,6 +1639,9 @@ meta def mk_comp (v : expr) : expr → tactic expr
      t ← infer_type e,
      mk_mapp ``id [t]
 
+/-- Given two expressions `e₀` and `e₁`, return the expression `` `(%%e₀ ↔ %%e₁)``. -/
+meta def mk_iff (e₀ : expr) (e₁ : expr) : expr := `(%%e₀ ↔ %%e₁)
+
 /--
 From a lemma of the shape `∀ x, f (g x) = h x`
 derive an auxiliary lemma of the form `f ∘ g = h`

src/tactic/mk_iff_of_inductive_prop.lean

@@ -2,50 +2,61 @@
 Copyright (c) 2018 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
+-/
+import tactic.core
+import tactic.lint
+/-!
+# mk_iff_of_inductive_prop
 
-Generation function for iff rules for inductives, like for `list.chain`:
+This file defines a tactic `tactic.mk_iff_of_inductive_prop` that generates `iff` rules for
+inductive `Prop`s. For example, when applied to `list.chain`, it creates a declaration with
+the following type:
 
-    ∀{α : Type*} (R : α → α → Prop) (a : α) (l : list α),
-      chain R a l ↔ l = [] ∨ ∃{b : α} {l' : list α}, R a b ∧ chain R b l ∧ l = b :: l'
+```lean
+∀{α : Type*} (R : α → α → Prop) (a : α) (l : list α),
+  chain R a l ↔ l = [] ∨ ∃{b : α} {l' : list α}, R a b ∧ chain R b l ∧ l = b :: l'
+```
 
+This tactic can be called using either the `mk_iff_of_inductive_prop` user command or
+the `mk_iff` attribute.
 -/
-import tactic.core
-
-namespace tactic
 
 open tactic expr
+namespace mk_iff
 
-meta def mk_iff (e₀ : expr) (e₁ : expr) : expr := `(%%e₀ ↔ %%e₁)
-
+/-- `select m n` runs `tactic.right` `m` times, and then `tactic.left` `(n-m)` times.
+Fails if `n < m`. -/
 meta def select : ℕ → ℕ → tactic unit
 | 0 0             := skip
 | 0 (n + 1)       := left >> skip
 | (m + 1) (n + 1) := right >> select m n
 | (n + 1) 0       := failure
 
 /-- `compact_relation bs as_ps`: Produce a relation of the form:
-  R as := ∃ bs, Λ_i a_i = p_i[bs]
-This relation is user visible, so we compact it by removing each `b_j` where a `p_i = b_j`, and
+```lean
+R as := ∃ bs, Λ_i a_i = p_i[bs]
+```
+This relation is user-visible, so we compact it by removing each `b_j` where a `p_i = b_j`, and
 hence `a_i = b_j`. We need to take care when there are `p_i` and `p_j` with `p_i = p_j = b_k`.
 
-TODO: this is copied from Lean's `coinductive_predicates.lean`, export it there.
- -/
-private meta def compact_relation :
+TODO: this is a variant of `compact_relation` in `coinductive_predicates.lean`, export it there.
+-/
+meta def compact_relation :
   list expr → list (expr × expr) → list (option expr) × list (expr × expr)
 | []        ps := ([], ps)
 | (b :: bs) ps :=
   match ps.span (λap:expr × expr, ¬ ap.2 =ₐ b) with
-    | (_, [])           := let (bs, ps) := compact_relation bs ps in (b::bs, ps)
-    | (ps₁, list.cons (a, _) ps₂) :=
-      let
-        i := a.instantiate_local b.local_uniq_name,
+    | (_, [])              := let (bs, ps) := compact_relation bs ps in (b::bs, ps)
+    | (ps₁, (a, _) :: ps₂) :=
+      let i := a.instantiate_local b.local_uniq_name,
         (bs, ps) := compact_relation (bs.map i) ((ps₁ ++ ps₂).map (λ⟨a, p⟩, (a, i p)))
       in (none :: bs, ps)
   end
 
+@[nolint doc_blame] -- TODO: document
 meta def constr_to_prop (univs : list level) (g : list expr) (idxs : list expr) (c : name) :
-  tactic ((list (option expr) × (expr ⊕ ℕ)) × expr) := do
-  e ← get_env,
+  tactic ((list (option expr) × (expr ⊕ ℕ)) × expr) :=
+do e ← get_env,
   decl ← get_decl c,
   some type' ← return $ decl.instantiate_type_univ_params univs,
   type ← drop_pis g type',
@@ -76,8 +87,9 @@ meta def constr_to_prop (univs : list level) (g : list expr) (idxs : list expr)
   end,
   return ((bs, n), r)
 
-private meta def to_cases (s : list $ list (option expr) × (expr ⊕ ℕ)) : tactic unit := do
-  h ← intro1,
+@[nolint doc_blame] -- TODO: document
+meta def to_cases (s : list $ list (option expr) × (expr ⊕ ℕ)) : tactic unit :=
+do h ← intro1,
   i ← induction h,
   focus ((s.zip i).enum.map $ λ⟨p, (shape, t), _, vars, _⟩, do
     let si := (shape.zip vars).filter_map (λ⟨c, v⟩, c >>= λ _, some v),
@@ -94,13 +106,24 @@ private meta def to_cases (s : list $ list (option expr) × (expr ⊕ ℕ)) : ta
     done),
   done
 
-private def list_option_merge {α : Type*} {β : Type*} : list (option α) → list β → list (option β)
+/--
+Iterate over two lists, if the first element of the first list is `none`, insert `none` into the
+result and continue with the tail of first list. Otherwise, wrap the first element of the second
+list with `some` and continue with the tails of both lists. Return when either list is empty.
+
+Example:
+```
+list_option_merge [none, some (), none, some ()] [0, 1, 2, 3, 4] = [none, (some 0), none, (some 1)]
+```
+-/
+def list_option_merge {α : Type*} {β : Type*} : list (option α) → list β → list (option β)
 | [] _ := []
 | (none :: xs) ys := none :: list_option_merge xs ys
-| (some a :: xs) (y :: ys) := some y :: list_option_merge xs ys
-| (some a :: xs) [] := []
+| (some _ :: xs) (y :: ys) := some y :: list_option_merge xs ys
+| (some _ :: xs) [] := []
 
-private meta def to_inductive
+@[nolint doc_blame] -- TODO: document
+meta def to_inductive
   (cs : list name) (gs : list expr) (s : list (list (option expr) × (expr ⊕ ℕ))) (h : expr) :
   tactic unit :=
 match s.length with
@@ -118,9 +141,9 @@ match s.length with
       (hs, h, _) ← elim_gen_prod n h [] [],
       (es, eq, _) ← elim_gen_prod e h [] [],
       let es := es ++ [eq],
-      /- `es.mmap' subst`: fails when we have dependent equalities (heq). `subst will change the
-        dependent hypotheses, so that the uniq local names in `es` are wrong afterwards. Instead
-        we revert them and pull them out one by one -/
+      /- `es.mmap' subst`: fails when we have dependent equalities (`heq`). `subst` will change the
+        dependent hypotheses, so that the `uniq` local names in `es` are wrong afterwards. Instead
+        we revert them and pull them out one-by-one. -/
       revert_lst es,
       es.mmap' (λ_, intro1 >>= subst)
     end,
@@ -135,36 +158,45 @@ match s.length with
   done
 end
 
+end mk_iff
+
+namespace tactic
+open mk_iff
+
 /--
-`mk_iff_of_inductive_prop i r` makes an iff rule for the inductively defined proposition `i`.
+`mk_iff_of_inductive_prop i r` makes an `iff` rule for the inductively-defined proposition `i`.
 The new rule `r` has the shape `∀ps is, i as ↔ ⋁_j, ∃cs, is = cs`, where `ps` are the type
 parameters, `is` are the indices, `j` ranges over all possible constructors, the `cs` are the
-parameters for each constructors, the equalities `is = cs` are the instantiations for each
-constructor for each of the indices to the inductive type `i`.
+parameters for each of the constructors, and the equalities `is = cs` are the instantiations for
+each constructor for each of the indices to the inductive type `i`.
 
 In each case, we remove constructor parameters (i.e. `cs`) when the corresponding equality would
 be just `c = i` for some index `i`.
 
-For example: `mk_iff_of_inductive_prop` on `list.chain` produces:
+For example, `mk_iff_of_inductive_prop` on `list.chain` produces:
 
 ```lean
 ∀ {α : Type*} (R : α → α → Prop) (a : α) (l : list α),
   chain R a l ↔ l = [] ∨ ∃{b : α} {l' : list α}, R a b ∧ chain R b l ∧ l = b :: l'
 ```
 -/
-meta def mk_iff_of_inductive_prop (i : name) (r : name) : tactic unit := do
-  e ← get_env,
+meta def mk_iff_of_inductive_prop (i : name) (r : name) : tactic unit :=
+do e ← get_env,
   guard (e.is_inductive i),
   let constrs := e.constructors_of i,
   let params := e.inductive_num_params i,
   let indices := e.inductive_num_indices i,
-  let rec := match e.recursor_of i with some rec := rec | none := i.append `rec end,
+  let rec := match e.recursor_of i with
+    | some rec := rec
+    | none := i.append `rec
+    end,
   decl ← get_decl i,
   let type := decl.type,
 
   let univ_names := decl.univ_params,
   let univs := univ_names.map level.param,
-    /- we use these names for our universe parameters, maybe we should construct a copy of them using uniq_name -/
+    /- we use these names for our universe parameters, maybe we should construct a copy of them
+    using `uniq_name` -/
 
   (g, `(Prop)) ← open_pis type | fail "Inductive type is not a proposition",
   let lhs := (const i univs).mk_app g,
@@ -183,21 +215,23 @@ section
 setup_tactic_parser
 
 /--
-`mk_iff_of_inductive_prop i r` makes an iff rule for the inductively defined proposition `i`.
+`mk_iff_of_inductive_prop i r` makes an `iff` rule for the inductively-defined proposition `i`.
 The new rule `r` has the shape `∀ps is, i as ↔ ⋁_j, ∃cs, is = cs`, where `ps` are the type
 parameters, `is` are the indices, `j` ranges over all possible constructors, the `cs` are the
-parameters for each constructors, the equalities `is = cs` are the instantiations for each
-constructor for each of the indices to the inductive type `i`.
+parameters for each of the constructors, and the equalities `is = cs` are the instantiations for
+each constructor for each of the indices to the inductive type `i`.
 
 In each case, we remove constructor parameters (i.e. `cs`) when the corresponding equality would
 be just `c = i` for some index `i`.
 
-For example: `mk_iff_of_inductive_prop` on `list.chain` produces:
+For example, `mk_iff_of_inductive_prop` on `list.chain` produces:
 
 ```lean
 ∀ {α : Type*} (R : α → α → Prop) (a : α) (l : list α),
   chain R a l ↔ l = [] ∨ ∃{b : α} {l' : list α}, R a b ∧ chain R b l ∧ l = b :: l'
 ```
+
+See also the `mk_iff` user attribute.
 -/
 @[user_command] meta def mk_iff_of_inductive_prop_cmd (_ : parse (tk "mk_iff_of_inductive_prop")) :
   parser unit :=
@@ -208,4 +242,56 @@ add_tactic_doc
   category    := doc_category.cmd,
   decl_names  := [``mk_iff_of_inductive_prop_cmd],
   tags        := ["logic", "environment"] }
+
+/--
+Applying the `mk_iff` attribute to an inductively-defined proposition `mk_iff` makes an `iff` rule
+`r` with the shape `∀ps is, i as ↔ ⋁_j, ∃cs, is = cs`, where `ps` are the type parameters, `is` are
+the indices, `j` ranges over all possible constructors, the `cs` are the parameters for each of the
+constructors, and the equalities `is = cs` are the instantiations for each constructor for each of
+the indices to the inductive type `i`.
+
+In each case, we remove constructor parameters (i.e. `cs`) when the corresponding equality would
+be just `c = i` for some index `i`.
+
+For example, if we try the following:
+```lean
+@[mk_iff] structure foo (m n : ℕ) : Prop :=
+(equal : m = n)
+(sum_eq_two : m + n = 2)
+```
+
+Then `#check foo_iff` returns:
+```lean
+foo_iff : ∀ (m n : ℕ), foo m n ↔ m = n ∧ m + n = 2
+```
+
+You can add an optional string after `mk_iff` to change the name of the generated lemma.
+For example, if we try the following:
+```lean
+@[mk_iff bar] structure foo (m n : ℕ) : Prop :=
+(equal : m = n)
+(sum_eq_two : m + n = 2)
+```
+
+Then `#check bar` returns:
+```lean
+bar : ∀ (m n : ℕ), foo m n ↔ m = n ∧ m + n = 2
+```
+
+See also the user command `mk_iff_of_inductive_prop`.
+-/
+@[user_attribute] meta def mk_iff_attr : user_attribute unit (option name) :=
+{ name := `mk_iff,
+  descr := "Generate an `iff` lemma for an inductive `Prop`.",
+  parser := ident?,
+  after_set := some $ λ n _ _, do
+    tgt ← mk_iff_attr.get_param n,
+    tactic.mk_iff_of_inductive_prop n (tgt.get_or_else (n.append_suffix "_iff")) }
+
+add_tactic_doc
+{ name        := "mk_iff",
+  category    := doc_category.attr,
+  decl_names  := [`mk_iff_attr],
+  tags        := ["logic", "environment"] }
+
 end

test/mk_iff_of_inductive.lean

@@ -26,3 +26,15 @@ inductive test.is_true (p : Prop) : Prop
 | triviality : p → test.is_true
 
 mk_iff_of_inductive_prop test.is_true test.is_true_iff
+
+@[mk_iff] structure foo (m n : ℕ) : Prop :=
+(equal : m = n)
+(sum_eq_two : m + n = 2)
+
+example (m n : ℕ) : foo m n ↔ m = n ∧ m + n = 2 := foo_iff m n
+
+@[mk_iff bar] structure foo2 (m n : ℕ) : Prop :=
+(equal : m = n)
+(sum_eq_two : m + n = 2)
+
+example (m n : ℕ) : foo2 m n ↔ m = n ∧ m + n = 2 := bar m n