feat(tactic/equiv_rw): incorporating equiv_functor (#2301)

* feat(tactic): rewriting along equivalences

* header

* minor

* type

* actually, rewriting the goal under functors is easy

* rewriting inside function types

* more

* way better

* improving comments

* fun

* feat(data/equiv): pi_congr

* various

* feat(data/equiv): sigma_congr

* docstrings

* change case for consistency

* tidying up

* minor

* minor

* switching names

* fixes

* add some tracing routines for convenience

* feat(tactic/core): trace_for

* typo

* oops

* oops

* various

* chore(tactic/solve_by_elim): cleanup

* cleanup

* what happened to my commit?

* fix

* fix

* rename to trace_if_enabled

* fixed?

* Tweak comments

* feat(tactic/solve_by_elim): add accept parameter to prune tree search

* when called with empty lemmas, use the same default set as the interactive tactic

* trace_state_if_enabled

* Update src/data/equiv/basic.lean

* implicit arguments

* stop cheating with [] ~ none

* indenting

* yay, working via solve_by_elim

* pretty good

* various

* various

* docstring

* fix docstrings

* more docs

* docs

* feat(data/equiv/functor): bifunctor.map_equiv

* bifunctors

* test rewriting under unique

* start

* sketch of equiv_functor

* rewriting in subtypes

* add documentation, and make the function an explicit argument

* documentation

* fix doc-strings

* typos

* minor

* adding demonstration of transporting semigroup

* update

* removing unimpressive inhabited example; easier later

* Update .vscode/settings.json

* err

* trying to transport through monoid

* err?

* much better

* improve documentation of accept, and add doc-string

* fix duplicated namespace

* improve docs

* feat(logic/basic): trivial transport lemmas

* try again with documentation

* update

* oops

* oops

* omit

* revert unnecessary change

* fix doc-string

* chore(data/equiv/basic): simp to_fun to coe

* feat(tactic/equiv_rw): incorporating equiv_functor

* rename adapt_equiv

* simplify the equivalence produced, and provide a tactic to access the equivalence

* add max_steps option

* add decl_name to add_tactic_doc

* fix add_tactic_doc

* satisfying linter

* fix names

* finish fix

* add defaults for cfg arguments

* remove simplify_term, which already existed as expr.simp

* remove duplicate functions that have been PRd separately

* no need for accept

* Update src/tactic/equiv_rw.lean

Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com>

* Update src/tactic/equiv_rw.lean

Co-Authored-By: Gabriel Ebner <gebner@gebner.org>

* replace max_steps with max_depth

* use solve_aux

* add missing simp lemmas about arrow_congr'

* fix failing test, by making sure we don't leave any ≃ goals on the table

* add comment

* comment out trace output

* fix fields

Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: 6 people

src/category/equiv_functor.lean

@@ -64,10 +64,4 @@ instance of_is_lawful_functor
   map_refl' := λ α, by { ext, apply is_lawful_functor.id_map, },
   map_trans' := λ α β γ k h, by { ext x, apply (is_lawful_functor.comp_map k h x), } }
 
--- TODO Include more examples here;
--- once `equiv_rw` is available these are hopefully easy to construct,
--- and in turn make `equiv_rw` more powerful.
-instance equiv_functor_unique : equiv_functor unique :=
-{ map := λ α β e, equiv.unique_congr e, }
-
 end equiv_functor

src/category/equiv_functor/instances.lean

@@ -0,0 +1,21 @@
+/-
+Copyright (c) 2020 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Scott Morrison
+-/
+import category.equiv_functor
+import tactic.equiv_rw
+
+/-!
+# `equiv_functor` instances
+
+We derive some `equiv_functor` instances, to enable `equiv_rw` to rewrite under these functions.
+-/
+
+open equiv
+
+instance equiv_functor_unique : equiv_functor unique :=
+{ map := λ α β e, equiv.unique_congr e, }
+
+instance equiv_functor_perm : equiv_functor perm :=
+{ map := λ α β e p, (e.symm.trans p).trans e }

src/tactic/equiv_rw.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import data.equiv.functor
+import category.equiv_functor
 
 /-!
 # The `equiv_rw` tactic transports goals or hypotheses along equivalences.
@@ -26,8 +26,7 @@ As an example, with `t = option α`, it will generate `functor.map_equiv option
 This is achieved by generating a new synthetic goal `%%t ≃ _`,
 and calling `solve_by_elim` with an appropriate set of congruence lemmas.
 To avoid having to specify the relevant congruence lemmas by hand,
-we mostly rely on `functor.map_equiv` and `bifunctor.map_equiv`
-(and, in a future PR, `equiv_functor.map_equiv`, see below),
+we mostly rely on `equiv_functor.map_equiv` and `bifunctor.map_equiv`
 along with some structural congruence lemmas such as
 * `equiv.arrow_congr'`,
 * `equiv.subtype_equiv_of_subtype'`,
@@ -42,21 +41,9 @@ revert this, and then attempt to `generalize`, replacing all occurrences of `e x
 before `intro`ing and `subst`ing `h`, and renaming `y` back to `x`.
 
 ## Future improvements
-While `equiv_rw` will rewrite under type-level functors (e.g. `option` and `list`),
-many constructions are only functorial with respect to equivalences
-(essentially, because of both positive and negative occurrences of the type being rewritten).
-At the moment, we only handle constructions of this form (e.g. `unique` or `ring`) by
-including explicit `equiv.*_congr` lemmas in the list provided to `solve_by_elim`.
-
-A (near) future PR will introduce `equiv_functor`,
-a typeclass for functions which are functorial with respect to equivalences,
-and use these instances rather than hard-coding the `congr` lemmas here.
-
-`equiv_functor` is not included in the initial implementation of `equiv_rw`, simply because
-the best way to construct an instance of `equiv_functor has_add` is to use `equiv_rw`!
-In fact, in a slightly more distant future PR I anticipate that
-`derive equiv_functor` should work on many examples, and
-we can incrementally bootstrap the strength of `equiv_rw`.
+In a future PR I anticipate that `derive equiv_functor` should work on many examples,
+(internally using `transport`, which is in turn based on `equiv_rw`)
+and we can incrementally bootstrap the strength of `equiv_rw`.
 
 An ambitious project might be to add `equiv_rw!`,
 a tactic which, when failing to find appropriate `equiv_functor` instances,
@@ -73,15 +60,10 @@ but this will wait for another subsequent PR.
 
 namespace tactic
 
-/-- A hard-coded list of names of lemmas used for constructing congruence equivalences. -/
+/-- A list of lemmas used for constructing congruence equivalences. -/
 
--- TODO: This should not be a hard-coded list.
--- We could accommodate the remaining "non-structural" lemmas using
--- `equiv_functor` instances.
--- Moreover, these instances can typically be `derive`d.
-
--- (Scott): I have not incorporated `equiv_functor` as part of this PR,
--- as the best way to construct instances, either by hand or using `derive`, is to use this tactic!
+-- Although this looks 'hard-coded', in fact the lemma `equiv_functor.map_equiv`
+-- allows us to extend `equiv_rw` simply by constructing new instance so `equiv_functor`.
 
 -- TODO: We should also use `category_theory.functorial` and `category_theory.hygienic` instances.
 -- (example goal: we could rewrite along an isomorphism of rings (either as `R ≅ S` or `R ≃+* S`)
@@ -91,10 +73,8 @@ meta def equiv_congr_lemmas : tactic (list expr) :=
 do exprs ←
   [
   `equiv.of_iff,
-  -- These are functorial w.r.t equiv,
-  -- and so will be subsumed by `equiv_functor.map_equiv` in a subsequent PR.
-  -- Many more could be added, but will wait for that framework.
-  `equiv.perm_congr, `equiv.equiv_congr, `equiv.unique_congr,
+  -- TODO decide what to do with this; it's an equiv_bifunctor?
+  `equiv.equiv_congr,
   -- The function arrow is technically a bifunctor `Typeᵒᵖ → Type → Type`,
   -- but the pattern matcher will never see this.
   `equiv.arrow_congr',
@@ -112,8 +92,8 @@ do exprs ←
    `equiv.Pi_congr_left',
   -- Handles `sum` and `prod`, and many others:
   `bifunctor.map_equiv,
-  -- Handles `list`, `option`, and many others:
-  `functor.map_equiv,
+  -- Handles `list`, `option`, `unique`, and many others:
+  `equiv_functor.map_equiv,
   -- We have to filter results to ensure we don't cheat and use exclusively `equiv.refl` and `iff.refl`!
   `equiv.refl,
   `iff.refl
@@ -254,9 +234,9 @@ with all occurrences of `h` in other hypotheses and the goal replaced with `e.sy
 `equiv_rw e` will attempt to transport the goal along an equivalence `e : α ≃ β`.
 In its minimal form it replaces the goal `⊢ α` with `⊢ β` by calling `apply e.inv_fun`.
 
-`equiv_rw` will also try rewriting under functors, so can turn
+`equiv_rw` will also try rewriting under (equiv_)functors, so can turn
 a hypothesis `h : list α` into `h : list β` or
-a goal `⊢ option α` into `⊢ option β`.
+a goal `⊢ unique α` into `⊢ unique β`.
 
 The maximum search depth for rewriting in subexpressions is controlled by
 `equiv_rw e {max_depth := n}`.

test/equiv_rw.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import tactic.equiv_rw
+import category.equiv_functor.instances -- these make equiv_rw more powerful!
 
 -- Uncomment this line to observe the steps of constructing appropriate equivalences.
 -- set_option trace.equiv_rw_type true
@@ -43,12 +44,20 @@ begin
   exact a,
 end
 
+-- Verify that `equiv_rw` will rewrite under `equiv_functor` instances.
 example {α β : Type} (u : unique α) (e : α ≃ β) : β :=
 begin
   equiv_rw e at u,
   apply inhabited.default,
 end
 
+example {α β : Type} (p : equiv.perm α) (e : α ≃ β) : equiv.perm β :=
+begin
+  equiv_rw e at p,
+  exact p,
+end
+
+
 -- We can rewrite the goal under functors.
 example {α β : Type} (e : α ≃ β) (b : β) : option α :=
 begin
@@ -203,11 +212,12 @@ begin
 end
 
 -- Demonstrate using `equiv_rw` to build new instances of `equiv_functor`
--- (which isn't yet in this PR, so we only define the fields without assembling them)
 -- Observe that the next three declarations could easily be implemented by a tactic.
 
 attribute [ext] semigroup
 
+-- This has been automated in the `transport` branch,
+-- so we won't attempt to write a deriver handler until we join with that.
 def semigroup.map {α β : Type} (e : α ≃ β) : semigroup α → semigroup β :=
 begin
   intro S, fconstructor,
@@ -217,20 +227,25 @@ begin
   { intros, dsimp, simp, apply S.mul_assoc, }
 end
 
--- Note this is purely formal, and will be provided by `equiv_functor` automatically.
-@[simps]
-def semigroup.map_equiv {α β : Type} (e : α ≃ β) : semigroup α ≃ semigroup β :=
-{ to_fun := semigroup.map e,
-  inv_fun := semigroup.map e.symm,
-  left_inv := by { intro x, funext, ext, dsimp [semigroup.map], simp, },
-  right_inv := by { intro x, funext, ext, dsimp [semigroup.map], simp, }, }
-
-lemma semigroup.map_id (α : Type) : semigroup.map_equiv (equiv.refl α) = equiv.refl (semigroup α) :=
+lemma semigroup.id_map (α : Type) : semigroup.map (equiv.refl α) = id :=
 by { ext, refl, }
 
-lemma semigroup.map_comp {α β γ : Type} (e : α ≃ β) (f : β ≃ γ) :
-  (semigroup.map_equiv e).trans (semigroup.map_equiv f) = semigroup.map_equiv (e.trans f) :=
-by { ext, dsimp [semigroup.map, semigroup.map_equiv], simp, }
+lemma semigroup.map_map {α β γ : Type} (e : α ≃ β) (f : β ≃ γ) :
+  semigroup.map (e.trans f) = (semigroup.map f) ∘ (semigroup.map e) :=
+by { ext, dsimp [semigroup.map], simp, }
+
+-- TODO (after joining the `transport` branch) create a derive handler for this
+instance : equiv_functor semigroup :=
+{ map := λ α β e, semigroup.map e,
+  map_refl' := semigroup.id_map,
+  map_trans' := λ α β γ e f, semigroup.map_map e f, }
+
+-- Verify that we can now use `equiv_rw` under `semigroup`:
+example {α : Type} [I : semigroup α] {β : Type} (e : α ≃ β) : semigroup β :=
+begin
+  equiv_rw e at I,
+  exact I,
+end
 
 -- Now we do `monoid`, to try out a structure with constants.
 attribute [ext] monoid