feat(library/init/algebra): tactics for copying multiplicative structures into additive ones

library/init/algebra.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.logic init.binary init.combinator init.meta.interactive
+import init.logic init.binary init.combinator init.meta.interactive init.meta.decl_cmds
 
 universe variable u
 
@@ -55,3 +55,83 @@ class group (A : Type u) extends monoid A, has_inv A :=
 group.mul_left_inv
 
 class comm_group (A : Type u) extends group A, comm_monoid A
+
+/- Additive "sister" structures.
+   Example, add_semigroup mirrors semigroup.
+   These structures exist just to help automation.
+   In an alternative design, we could have the binary operation as an
+   extra argument for semigroup, monoid, group, etc. However, the lemmas
+   would be hard to index since they would not contain any constant.
+   For example, mul_assoc would be
+
+   lemma mul_assoc {A : Type u} {op : A → A → A} [semigroup A op] :
+                   ∀ a b c : A, op (op a b) c = op a (op b c) :=
+    semigroup.mul_assoc
+
+   The simplifier cannot effectively use this lemma since the pattern for
+   the left-hand-side would be
+
+        ?op (?op ?a ?b) ?c
+
+   Remark: we use a tactic for transporting theorems from the multiplicative fragment
+   to the additive one.
+-/
+
+@[class] def add_semigroup      := semigroup
+@[class] def add_monoid         := monoid
+@[class] def add_group          := group
+@[class] def add_comm_semigroup := comm_semigroup
+@[class] def add_comm_monoid    := comm_monoid
+@[class] def add_comm_group     := comm_group
+
+instance add_semigroup.to_has_add {A : Type u} [s : add_semigroup A] : has_add A :=
+⟨@mul A (@semigroup.to_has_mul A s)⟩
+instance add_monoid.to_has_zero {A : Type u} [s : add_monoid A] : has_zero A :=
+⟨@one A (@monoid.to_has_one A s)⟩
+instance add_group.to_has_neg {A : Type u} [s : add_group A] : has_neg A :=
+⟨@inv A (@group.to_has_inv A s)⟩
+
+meta def multiplicative_to_additive : name_map name :=
+rb_map.of_list $
+  [/- map operations -/
+   (`mul, `add), (`one, `zero), (`inv, `neg),
+   /- map structures -/
+   (`semigroup, `add_semigroup),
+   (`monoid, `add_monoid),
+   (`group, `add_group),
+   (`comm_semigroup, `add_comm_semigroup),
+   (`comm_monoid, `add_comm_monoid),
+   (`comm_group, `add_comm_group),
+   /- map instances -/
+   (`semigroup.to_has_mul, `add_semigroup.to_has_add),
+   (`monoid.to_has_one, `add_monoid.to_has_zero),
+   (`group.to_has_inv, `add_group.to_has_neg),
+   (`comm_semigroup.to_semigroup, `add_comm_semigroup.to_add_semigroup),
+   (`monoid.to_semigroup, `add_monoid.to_add_semigroup),
+   (`comm_monoid.to_monoid, `add_comm_monoid.to_add_monoid),
+   (`comm_monoid.to_comm_semigroup, `add_comm_monoid.to_add_comm_semigroup),
+   (`group.to_monoid, `add_group.to_add_monoid),
+   (`comm_group.to_group, `add_comm_group.to_add_group),
+   (`comm_group.to_comm_monoid, `add_comm_group.to_add_comm_monoid)
+ ]
+
+meta def transport_to_additive : name → name → command :=
+copy_decl_updating_type multiplicative_to_additive
+
+open tactic
+
+/- Make sure all constants at multiplicative_to_additive are declared -/
+meta def init_multiplicative_to_additive : command :=
+multiplicative_to_additive^.fold skip (λ s t tac, do
+  env ← get_env,
+  if (env^.get t)^.to_bool = ff
+  then tac >> transport_to_additive s t
+  else tac)
+
+run_command init_multiplicative_to_additive
+run_command transport_to_additive `mul_assoc `add_assoc
+run_command transport_to_additive `mul_comm  `add_comm
+run_command transport_to_additive `mul_left_comm `add_left_comm
+run_command transport_to_additive `one_mul `zero_add
+run_command transport_to_additive `mul_one `add_zero
+run_command transport_to_additive `mul_left_inv `add_left_neg

library/init/meta/decl_cmds.lean

@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.meta.tactic init.meta.rb_map
+open tactic
+
+/- Given a set of constant renamings `replacements` and a declaration name `src_decl_name`, create a new
+   declaration called `new_decl_name` s.t. its type is the type of `src_decl_name` after applying the
+   given constant replacement.
+
+   Remark: the new type must be definitionally equal to the type of `src_decl_name`.
+
+   Example:
+   Assume the environment contains
+        def f : nat -> nat  := ...
+        def g : nat -> nat  := f
+        lemma f_lemma : forall a, f a > 0 := ...
+
+   Moreover, assume we have a mapping M containing `f -> `g
+   Then, the command
+        run_command copy_decl_updating_type M `f_lemma `g_lemma
+   creates the declaration
+        lemma g_lemma : forall a, g a > 0 := ...
+-/
+meta def copy_decl_updating_type (replacements : name_map name) (src_decl_name : name) (new_decl_name : name) : command :=
+do env      ← get_env,
+   decl     ← returnex $ env^.get src_decl_name,
+   new_type ← return $ decl^.type^.replace (λ e d,
+              match e with
+              | expr.const n ls :=
+                match replacements^.find n with
+                | some new_n := some (expr.const new_n ls)
+                | none       := none
+                end
+              | _ := none
+              end),
+   new_value ← return $ expr.const src_decl_name (decl^.univ_params^.for level.param),
+   add_decl (((decl^.update_type new_type)^.update_name new_decl_name)^.update_value new_value),
+   return ()

library/init/meta/declaration.lean

@@ -72,6 +72,23 @@ meta def declaration.type : declaration → expr
 | (declaration.cnst n ls t tr) := t
 | (declaration.ax n ls t) := t
 
+meta def declaration.update_type : declaration → expr → declaration
+| (declaration.defn n ls t v h tr) new_t := declaration.defn n ls new_t v h tr
+| (declaration.thm n ls t v)       new_t := declaration.thm n ls new_t v
+| (declaration.cnst n ls t tr)     new_t := declaration.cnst n ls new_t tr
+| (declaration.ax n ls t)          new_t := declaration.ax n ls new_t
+
+meta def declaration.update_name : declaration → name → declaration
+| (declaration.defn n ls t v h tr) new_n := declaration.defn new_n ls t v h tr
+| (declaration.thm n ls t v)       new_n := declaration.thm new_n ls t v
+| (declaration.cnst n ls t tr)     new_n := declaration.cnst new_n ls t tr
+| (declaration.ax n ls t)          new_n := declaration.ax new_n ls t
+
+meta def declaration.update_value : declaration → expr → declaration
+| (declaration.defn n ls t v h tr) new_v := declaration.defn n ls t new_v h tr
+| (declaration.thm n ls t v)       new_v := declaration.thm n ls t new_v
+| d                                new_v := d
+
 /- Instantiate a universe polymorphic declaration type with the given universes. -/
 meta constant declaration.instantiate_type_univ_params : declaration → list level → option expr
 

library/init/meta/environment.lean

@@ -17,6 +17,11 @@ meta constant trust_lvl       : environment → nat
 meta constant add             : environment → declaration → exceptional environment
 /- Retrieve a declaration from the environment -/
 meta constant get             : environment → name → exceptional declaration
+meta def      contains (env : environment) (d : name) : bool :=
+match env^.get d with
+| exceptional.success _      := tt
+| exceptional.exception ._ _ := ff
+end
 /- Add a new inductive datatype to the environment
    name, universe parameters, number of parameters, type, constructors (name and type), is_meta -/
 meta constant add_inductive   : environment → name → list name → nat → expr → list (name × expr) → bool →

library/init/meta/exceptional.lean

@@ -29,6 +29,14 @@ end
 namespace exceptional
 variables {A B : Type}
 
+protected meta definition to_bool : exceptional A → bool
+| (success _)      := tt
+| (exception .A _) := ff
+
+protected meta definition to_option : exceptional A → option A
+| (success a)      := some a
+| (exception .A _) := none
+
 attribute [inline]
 protected meta definition fmap (f : A → B) (e : exceptional A) : exceptional B :=
 exceptional.cases_on e