diff --git a/library/init/algebra.lean b/library/init/algebra.lean index 13e97c8cd8..211dd93343 100644 --- a/library/init/algebra.lean +++ b/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 diff --git a/library/init/meta/decl_cmds.lean b/library/init/meta/decl_cmds.lean new file mode 100644 index 0000000000..881737ebf5 --- /dev/null +++ b/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 () diff --git a/library/init/meta/declaration.lean b/library/init/meta/declaration.lean index 1ceb89ee3a..bc28bce744 100644 --- a/library/init/meta/declaration.lean +++ b/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 diff --git a/library/init/meta/environment.lean b/library/init/meta/environment.lean index a68df05314..f7fc2a647d 100644 --- a/library/init/meta/environment.lean +++ b/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 → diff --git a/library/init/meta/exceptional.lean b/library/init/meta/exceptional.lean index 96203d5495..9a03e1f071 100644 --- a/library/init/meta/exceptional.lean +++ b/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