feat(reduce_projections): add reduce_projections attribute (#1402)

* feat(reduce_projections): add attribute

This attribute automatically generates simp-lemmas for an instance of a structure stating what the projections of this instance are

* add tactic doc

* use lean code blocks

* missing `lemma`

* checkpoint

* recursively apply reduce_projections and eta-reduce structures

* reviewer comments, shorten name

new name is simps

* avoid name clashes

* remove recursive import

* fix eta-expansion bug

* typo

* apply whnf to type

* add test

* replace nm by decl_name

Author: fpvandoorn

docs/tactics.md

@@ -1208,3 +1208,27 @@ When possible, make `foo` non-private rather than using this feature.
 bug is often indicated by a message `nested exception message: tactic failed, there are no goals to be solved`,and solved by appending `using_well_founded wf_tacs` to the recursive definition.
 See also additional documentation of `using_well_founded` in
 [docs/extras/well_founded_recursion.md](extras/well_founded_recursion.md).
+
+### simps
+
+* The `@[simps]` attribute automatically derives lemmas specifying the projections of the declaration.
+* Example:
+  ```lean
+  @[simps] def refl (α) : α ≃ α := ⟨id, id, λ x, rfl, λ x, rfl⟩
+  ```
+  derives two simp-lemmas:
+  ```lean
+  @[simp] lemma refl_to_fun (α) : (refl α).to_fun = id
+  @[simp] lemma refl_inv_fun (α) : (refl α).inv_fun = id
+  ```
+* It does not derive simp-lemmas for the prop-valued projections.
+* It will automatically reduce newly created beta-redexes, but not unfold any definitions.
+* If one of the fields itself is a structure, this command will recursively create
+  simp-lemmas for all fields in that structure.
+* If one of the values is an eta-expanded structure, we will eta-reduce this structure.
+* You can use `@[simps lemmas_only]` to derive the lemmas, but not mark them
+  as simp-lemmas.
+* If one of the projections is marked as a coercion, the generated lemmas do *not* use this
+  coercion.
+* If one of the fields is a partially applied constructor, we will eta-expand it
+  (this likely never happens).

src/meta/expr.lean

@@ -233,6 +233,24 @@ meta def pi_arity_aux : ℕ → expr → ℕ
 meta def pi_arity : expr → ℕ :=
 pi_arity_aux 0
 
+/-- Get the names of the bound variables by a sequence of pis or lambdas. -/
+meta def binding_names : expr → list name
+| (pi n _ _ e)  := n :: e.binding_names
+| (lam n _ _ e) := n :: e.binding_names
+| e             := []
+
+/-- Instantiate lambdas in the second argument by expressions from the first. -/
+meta def instantiate_lambdas : list expr → expr → expr
+| (e'::es) (lam n bi t e) := instantiate_lambdas es (e.instantiate_var e')
+| _        e              := e
+
+/-- Instantiate lambdas in the second argument `e` by expressions from the first argument `es`.
+If the length of `es` is larger than the number of lambdas in `e`,
+then the term is applied to the remaining terms -/
+meta def instantiate_lambdas_or_apps : list expr → expr → expr
+| (e'::es) (lam n bi t e) := instantiate_lambdas_or_apps es (e.instantiate_var e')
+| es       e              := mk_app e es
+
 end expr
 
 namespace environment
@@ -264,6 +282,17 @@ option.is_some $ do
     (some di.type) | none,
   env.is_projection (n ++ x.deinternalize_field)
 
+/-- Get all projections of the structure `n`. Returns `none` if `n` is not structure-like.
+  If `n` is not a structure, but is structure-like, this does not check whether the names
+  are existing declarations. -/
+meta def get_projections (env : environment) (n : name) : option (list name) := do
+  (nparams, intro) ← env.is_structure_like n,
+  di ← (env.get intro).to_option,
+  tgt ← nparams.iterate
+    (λ e : option expr, do expr.pi _ _ _ body ← e | none, some body)
+    (some di.type) | none,
+  return $ tgt.binding_names.map (λ x, n ++ x.deinternalize_field)
+
 /-- For all declarations `d` where `f d = some x` this adds `x` to the returned list.  -/
 meta def decl_filter_map {α : Type} (e : environment) (f : declaration → option α) : list α :=
   e.fold [] $ λ d l, match f d with
@@ -303,6 +332,60 @@ s.is_prefix_of $ (e.decl_olean n).get_or_else ""
 
 end environment
 
+
+namespace expr
+/- In this section we define the tactic `is_eta_expansion` which checks whether an expression
+  is an eta-expansion of a structure. (not to be confused with eta-expanion for `λ`). -/
+open tactic
+
+/-- Checks whether for all elements `(nm, val)` in the list we have `val = nm.{univs} args` -/
+meta def is_eta_expansion_of (args : list expr) (univs : list level) (l : list (name × expr)) :
+  bool :=
+l.all $ λ⟨proj, val⟩, val = (const proj univs).mk_app args
+
+/-- Checks whether there is an expression `e` such that for all elements `(nm, val)` in the list
+  `val = nm ... e` where `...` denotes the same list of parameters for all applications.
+  Returns e if it exists. -/
+meta def is_eta_expansion_test : list (name × expr) → option expr
+| []              := none
+| (⟨proj, val⟩::l) :=
+  match val.get_app_fn with
+  | (const nm univs : expr) :=
+    if nm = proj then
+      let args := val.get_app_args in
+      let e := args.ilast in
+      if is_eta_expansion_of args univs l then some e else none
+    else
+      none
+  | _                       := none
+  end
+
+/-- Checks whether there is an expression `e` such that for all *non-propositional* elements
+  `(nm, val)` in the list `val = e ... nm` where `...` denotes the same list of parameters for all
+  applications. Also checks whether the resulting expression unifies with the given one -/
+meta def is_eta_expansion_aux (val : expr) (l : list (name × expr)) : tactic (option expr) :=
+do l' ← l.mfilter (λ⟨proj, val⟩, bnot <$> is_proof val),
+  match is_eta_expansion_test l' with
+  | some e := option.map (λ _, e) <$> try_core (unify e val)
+  | none   := return none
+  end
+
+/-- Checks whether there is an expression `e` such that `val` is the eta-expansion of `e`.
+  This assumes that `val` is a fully-applied application of the constructor of a structure.
+
+  This is useful to reduce expressions generated by the notation
+    `{ field_1 := _, ..other_structure }`
+  If `other_structure` is itself a field of the structure, then the elaborator will insert an
+  eta-expanded version of `other_structure`. -/
+meta def is_eta_expansion (val : expr) : tactic (option expr) := do
+  e ← get_env,
+  type ← infer_type val,
+  projs ← e.get_projections type.get_app_fn.const_name,
+  let args := (val.get_app_args).drop type.get_app_args.length,
+  is_eta_expansion_aux val (projs.zip args)
+
+end expr
+
 namespace declaration
 open tactic
 

src/tactic/basic.lean

@@ -18,6 +18,7 @@ import
   tactic.rewrite
   tactic.sanity_check
   tactic.simpa
+  tactic.simps
   tactic.split_ifs
   tactic.squeeze
   tactic.well_founded_tactics

src/tactic/core.lean

@@ -125,6 +125,16 @@ do e ← tactic.get_env,
              then s.insert d.to_name d else s),
    pure xs
 
+/-- If `{nm}_{n}` doesn't exist in the environment, returns that, otherwise tries `{nm}_{n+1}` -/
+meta def get_unused_decl_name_aux (e : environment) (nm : name) : ℕ → tactic name | n :=
+let nm' := nm.append_suffix ("_" ++ to_string n) in
+if e.contains nm' then get_unused_decl_name_aux (n+1) else return nm'
+
+/-- Return a name which doesn't already exist in the environment. If `nm` doesn't exist, it
+  returns that, otherwise it tries nm_2, nm_3, ... -/
+meta def get_unused_decl_name (nm : name) : tactic name :=
+get_env >>= λ e, if e.contains nm then get_unused_decl_name_aux e nm 2 else return nm
+
 /--
 Returns a pair (e, t), where `e ← mk_const d.to_name`, and `t = d.type`
 but with universe params updated to match the fresh universe metavariables in `e`.

src/tactic/default.lean

@@ -30,5 +30,4 @@ import
   tactic.wlog
   tactic.tfae
   tactic.apply_fun
-  tactic.localized
   tactic.apply

src/tactic/simps.lean

@@ -0,0 +1,111 @@
+/-
+Copyright (c) 2019 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+-/
+import tactic.core
+/-!
+  # simps attribute
+  This file defines the `@[simps]` attribute, to automatically generate simp-lemmas
+  reducing a definition when projections are applied to it.
+
+  ## Tags
+  structures, projections, simp, simplifier, generates declarations
+-/
+
+open tactic expr
+
+/-- Add a lemma with `nm` stating that `lhs = rhs`. `type` is the type of both `lhs` and `rhs`,
+  `args` is the list of local constants occurring, and `univs` is the list of universe variables.
+  If `add_simp` then we make the resulting lemma a simp-lemma. -/
+meta def add_projection (nm : name) (type lhs rhs : expr) (args : list expr)
+  (univs : list name) (add_simp : bool) : tactic unit := do
+  eq_ap ← mk_mapp `eq $ [type, lhs, rhs].map some,
+  refl_ap ← mk_app `eq.refl [type, lhs],
+  decl_name ← get_unused_decl_name nm,
+  let decl_type := eq_ap.pis args,
+  let decl_value := refl_ap.lambdas args,
+  let decl := declaration.thm decl_name univs decl_type (pure decl_value),
+  add_decl decl <|> fail format!"failed to add projection lemma {decl_name}.",
+  when add_simp $
+    set_basic_attribute `simp decl_name tt >> set_basic_attribute `_refl_lemma decl_name tt
+
+/-- Derive lemmas specifying the projections of the declaration. -/
+meta def add_projections : ∀(e : environment) (nm : name) (type lhs rhs : expr)
+  (args : list expr) (univs : list name) (add_simp must_be_str : bool), tactic unit
+  | e nm type lhs rhs args univs add_simp must_be_str := do
+  (type_args, tgt) ← mk_local_pis_whnf type,
+  tgt ← whnf tgt,
+  let new_args := args ++ type_args,
+  let lhs_ap := lhs.mk_app type_args,
+  let rhs_ap := rhs.instantiate_lambdas_or_apps type_args,
+  let str := tgt.get_app_fn.const_name,
+  if e.is_structure str then do
+    projs ← e.get_projections str,
+    [intro] ← return $ e.constructors_of str | fail "unreachable code (3)",
+    let params := get_app_args tgt, -- the parameters of the structure
+    if is_constant_of (get_app_fn rhs_ap) intro then do -- if the value is a constructor application
+      guard ((get_app_args rhs_ap).take params.length = params) <|> fail "unreachable code (1)",
+      let rhs_args := (get_app_args rhs_ap).drop params.length, -- the fields of the structure
+      guard (rhs_args.length = projs.length) <|> fail "unreachable code (2)",
+      let pairs := projs.zip rhs_args,
+      eta ← expr.is_eta_expansion_aux rhs_ap pairs,
+      match eta with
+      | none                 :=
+        pairs.mmap' $ λ ⟨proj, new_rhs⟩, do
+          new_type ← infer_type new_rhs,
+          b ← is_prop new_type,
+          when ¬ b $ do -- if this field is a proposition, we skip it
+            -- cannot use `mk_app` here, since the resulting application might still be a function.
+            new_lhs ← mk_mapp proj $ (params ++ [lhs_ap]).map some,
+            let new_nm := nm.append_suffix $ "_" ++ proj.last,
+            add_projections e new_nm new_type new_lhs new_rhs new_args univs add_simp ff
+      | (some eta_reduction) := add_projection nm tgt lhs_ap eta_reduction new_args univs add_simp
+      end
+    else (do
+      when must_be_str $
+        fail "Invalid `simps` attribute. Body is not a constructor application",
+      add_projection nm tgt lhs_ap rhs_ap new_args univs add_simp)
+  else
+    (do when must_be_str $
+      fail "Invalid `simps` attribute. Target is not a structure",
+    add_projection nm tgt lhs_ap rhs_ap new_args univs add_simp)
+
+/-- Derive lemmas specifying the projections of the declaration. -/
+meta def simps_tac (nm : name) (add_simp : bool) : tactic unit := do
+  e ← get_env,
+  d ← e.get nm,
+  let lhs : expr := const d.to_name (d.univ_params.map level.param),
+  add_projections e nm d.type lhs d.value [] d.univ_params add_simp tt
+
+reserve notation `lemmas_only`
+setup_tactic_parser
+
+/-- Automatically derive lemmas specifying the projections of this declaration.
+  Example: (note that the forward and reverse functions are specified differently!)
+  ```
+  @[simps] def refl (α) : α ≃ α := ⟨id, λ x, x, λ x, rfl, λ x, rfl⟩
+  ```
+  derives two simp-lemmas:
+  ```
+  @[simp] lemma refl_to_fun (α) (x : α) : (refl α).to_fun x = id x
+  @[simp] lemma refl_inv_fun (α) (x : α) : (refl α).inv_fun x = x
+  ```
+  * It does not derive simp-lemmas for the prop-valued projections.
+  * It will automatically reduce newly created beta-redexes, but not unfold any definitions.
+  * If one of the fields itself is a structure, this command will recursively create
+    simp-lemmas for all fields in that structure.
+  * If one of the values is an eta-expanded structure, we will eta-reduce this structure.
+  * You can use `@[simps lemmas_only]` to derive the lemmas, but not mark them
+    as simp-lemmas.
+  * If one of the projections is marked as a coercion, the generated lemmas do *not* use this
+    coercion.
+  * If one of the fields is a partially applied constructor, we will eta-expand it
+    (this likely never happens).
+  -/
+@[user_attribute] meta def simps_attr : user_attribute unit (option unit) :=
+{ name := `simps,
+  descr := "Automatically derive lemmas specifying the projections of this declaration.",
+  parser := optional (tk "lemmas_only"),
+  after_set := some $
+    λ n _ _, option.is_none <$> simps_attr.get_param n >>= simps_tac n }