diff --git a/src/algebra/big_operators/basic.lean b/src/algebra/big_operators/basic.lean index 410a55c04a59d..d599a0b842b06 100644 --- a/src/algebra/big_operators/basic.lean +++ b/src/algebra/big_operators/basic.lean @@ -273,7 +273,7 @@ calc (∏ x in s.sigma t, f x) = ∏ x in s.bind (λa, (t a).map (function.embedding.sigma_mk a)), f x : by rw sigma_eq_bind ... = ∏ a in s, ∏ x in (t a).map (function.embedding.sigma_mk a), f x : prod_bind $ assume a₁ ha a₂ ha₂ h x hx, - by { simp only [inf_eq_inter, mem_inter, mem_map, function.embedding.sigma_mk_to_fun] at hx, + by { simp only [inf_eq_inter, mem_inter, mem_map, function.embedding.sigma_mk_apply] at hx, rcases hx with ⟨⟨y, hy, rfl⟩, ⟨z, hz, hz'⟩⟩, cc } ... = ∏ a in s, ∏ s in t a, f ⟨a, s⟩ : prod_congr rfl $ λ _ _, prod_map _ _ _ diff --git a/src/field_theory/fixed.lean b/src/field_theory/fixed.lean index bacf16a712f39..4b9986375a4d5 100644 --- a/src/field_theory/fixed.lean +++ b/src/field_theory/fixed.lean @@ -239,14 +239,14 @@ fintype_card_le_findim_of_linear_independent $ linear_independent_to_linear_map namespace fixed_points /-- Embedding produced from a faithful action. -/ -@[simps to_fun {fully_applied := ff}] +@[simps apply {fully_applied := ff}] def to_alg_hom (G : Type u) (F : Type v) [group G] [field F] [faithful_mul_semiring_action G F] : G ↪ (F →ₐ[fixed_points G F] F) := { to_fun := λ g, { commutes' := λ x, x.2 g, .. mul_semiring_action.to_semiring_hom G F g }, inj' := λ g₁ g₂ hg, injective_to_semiring_hom G F $ ring_hom.ext $ λ x, alg_hom.ext_iff.1 hg x, } -lemma to_alg_hom_apply {G : Type u} {F : Type v} [group G] [field F] +lemma to_alg_hom_apply_apply {G : Type u} {F : Type v} [group G] [field F] [faithful_mul_semiring_action G F] (g : G) (x : F) : to_alg_hom G F g x = g • x := rfl diff --git a/src/logic/embedding.lean b/src/logic/embedding.lean index 621429bc48dde..f5d07be7ad2a3 100644 --- a/src/logic/embedding.lean +++ b/src/logic/embedding.lean @@ -24,6 +24,8 @@ infixr ` ↪ `:25 := embedding instance {α : Sort u} {β : Sort v} : has_coe_to_fun (α ↪ β) := ⟨_, embedding.to_fun⟩ +initialize_simps_projections embedding (to_fun → apply) + end function /-- Convert an `α ≃ β` to `α ↪ β`. -/ @@ -164,12 +166,12 @@ section sigma variables {α α' : Type*} {β : α → Type*} {β' : α' → Type*} /-- `sigma.mk` as an `function.embedding`. -/ -@[simps to_fun] def sigma_mk (a : α) : β a ↪ Σ x, β x := +@[simps apply] def sigma_mk (a : α) : β a ↪ Σ x, β x := ⟨sigma.mk a, sigma_mk_injective⟩ /-- If `f : α ↪ α'` is an embedding and `g : Π a, β α ↪ β' (f α)` is a family of embeddings, then `sigma.map f g` is an embedding. -/ -@[simps to_fun] def sigma_map (f : α ↪ α') (g : Π a, β a ↪ β' (f a)) : +@[simps apply] def sigma_map (f : α ↪ α') (g : Π a, β a ↪ β' (f a)) : (Σ a, β a) ↪ Σ a', β' a' := ⟨sigma.map f (λ a, g a), f.injective.sigma_map (λ a, (g a).injective)⟩ @@ -199,7 +201,7 @@ protected def subtype_map {α β} {p : α → Prop} {q : β → Prop} (f : α open set /-- `set.image` as an embedding `set α ↪ set β`. -/ -@[simps to_fun] protected def image {α β} (f : α ↪ β) : set α ↪ set β := +@[simps apply] protected def image {α β} (f : α ↪ β) : set α ↪ set β := ⟨image f, f.2.image_injective⟩ end embedding @@ -219,7 +221,7 @@ end equiv namespace set /-- The injection map is an embedding between subsets. -/ -@[simps to_fun] def embedding_of_subset {α} (s t : set α) (h : s ⊆ t) : s ↪ t := +@[simps apply] def embedding_of_subset {α} (s t : set α) (h : s ⊆ t) : s ↪ t := ⟨λ x, ⟨x.1, h x.2⟩, λ ⟨x, hx⟩ ⟨y, hy⟩ h, by { congr, injection h }⟩ end set diff --git a/src/measure_theory/haar_measure.lean b/src/measure_theory/haar_measure.lean index d5885da14df3a..3db2eb7edaa1d 100644 --- a/src/measure_theory/haar_measure.lean +++ b/src/measure_theory/haar_measure.lean @@ -208,7 +208,7 @@ begin { simp only [mem_set_of_eq], refine subset.trans (image_subset _ h1s) _, rintro _ ⟨g₁, ⟨_, ⟨g₂, rfl⟩, ⟨_, ⟨hg₂, rfl⟩, hg₁⟩⟩, rfl⟩, simp only [mem_preimage] at hg₁, simp only [exists_prop, mem_Union, finset.mem_map, - equiv.coe_mul_right, exists_exists_and_eq_and, mem_preimage, equiv.to_embedding_to_fun], + equiv.coe_mul_right, exists_exists_and_eq_and, mem_preimage, equiv.to_embedding_apply], refine ⟨_, hg₂, _⟩, simp only [mul_assoc, hg₁, inv_mul_cancel_left] } end diff --git a/src/tactic/simps.lean b/src/tactic/simps.lean index 0b5b111e44711..7bc9c66bf215e 100644 --- a/src/tactic/simps.lean +++ b/src/tactic/simps.lean @@ -45,10 +45,13 @@ used by the `@[simps]` attribute. - To change the default value, see Note [custom simps projection]. - You are strongly discouraged to add this attribute manually. - The first argument is the list of names of the universe variables used in the structure -- The second argument is the expressions that correspond to the projections of the structure - (these can contain the universe parameters specified in the first argument). +- The second argument is a list that consists of + - a custom name for each projection of the structure + - an expressions for each projections of the structure (definitionally equal to the + corresponding projection). These expressions can contain the universe parameters specified + in the first argument). -/ -@[user_attribute] meta def simps_str_attr : user_attribute unit (list name × list expr) := +@[user_attribute] meta def simps_str_attr : user_attribute unit (list name × list (name × expr)) := { name := `_simps_str, descr := "An attribute specifying the projection of the given structure.", parser := do e ← texpr, eval_pexpr _ e } @@ -77,6 +80,11 @@ attribute [notation_class* coe_fn] has_coe_to_fun Get the projections used by `simps` associated to a given structure `str`. The second component is the list of projections, and the first component the (shared) list of universe levels used by the projections. + + The returned information is also stored in a parameter of the attribute `@[_simps_str]`, which + is given to `str`. If `str` already has this attribute, the information is read from this + attribute instead. + The returned universe levels are the universe levels of the structure. For the projections there are three cases * If the declaration `{structure_name}.simps.{projection_name}` has been declared, then the value @@ -102,15 +110,31 @@ attribute [notation_class* coe_fn] has_coe_to_fun ``` def equiv.simps.inv_fun {α β} (e : α ≃ β) : β → α := e.symm ``` + + Optionally, this command accepts two optional arguments + * If `trace_if_exists` the command will always generate a trace message when the structure already + has the attribute `@[_simps_str]`. + * The `name_changes` argument accepts a list of pairs `(old_name, new_name)`. This is used to + change the projection name `old_name` to the custom projection name `new_name`. Example: + for the structure `equiv` the projection `to_fun` could be renamed `apply`. This name will be + used for parsing and generating projection names. This argument is ignored if the structure + already has an existing attribute. -/ -- if performance becomes a problem, possible heuristic: use the names of the projections to -- skip all classes that don't have the corresponding field. -meta def simps_get_raw_projections (e : environment) (str : name) : - tactic (list name × list expr) := do +meta def simps_get_raw_projections (e : environment) (str : name) (trace_if_exists : bool := ff) + (name_changes : list (name × name) := []) : tactic (list name × list (name × expr)) := do has_attr ← has_attribute' `_simps_str str, if has_attr then do - when_tracing `simps.verbose trace!"[simps] > found projection information for structure {str}", - simps_str_attr.get_param str + data ← simps_str_attr.get_param str, + to_print ← data.2.mmap $ λ s, to_string <$> pformat!"Projection {s.1}: {s.2}", + let to_print := string.join $ to_print.intersperse "\n > ", + -- We always trace this when called by `initialize_simps_projections`, + -- because this doesn't do anything extra (so should not occur in mathlib). + -- It can be useful to find the projection names. + when (is_trace_enabled_for `simps.verbose || trace_if_exists) trace! + "[simps] > Already found projection information for structure {str}:\n > {to_print}", + return data else do when_tracing `simps.verbose trace! "[simps] > generating projection information for structure {str}:", @@ -172,10 +196,17 @@ Expected type:\n {raw_expr_type}" }, when_tracing `simps.verbose trace! " > using {proj_nm} instead of the default projection {relevant_proj.last}.", return $ raw_exprs.update_nth pos lambda_raw_expr) <|> return raw_exprs) raw_exprs, - when_tracing `simps.verbose trace! - "[simps] > generated projections for {str}:\n > {raw_exprs}", - simps_str_attr.set str (raw_univs, raw_exprs) tt, - return (raw_univs, raw_exprs) + proj_names ← e.structure_fields str, + -- if we find the name in name_changes, change the name + let proj_names : list name := proj_names.map $ + λ nm, (name_changes.find $ λ p : _ × _, p.1 = nm).elim nm prod.snd, + let projs := proj_names.zip raw_exprs, + when_tracing `simps.verbose $ do { + to_print ← projs.mmap $ λ s, to_string <$> pformat!"Projection {s.1}: {s.2}", + let to_print := string.join $ to_print.intersperse "\n > ", + trace!"[simps] > generated projections for {str}:\n > {to_print}" }, + simps_str_attr.set str (raw_univs, projs) tt, + return (raw_univs, projs) /-- You can specify custom projections for the `@[simps]` attribute. @@ -194,39 +225,65 @@ Expected type:\n {raw_expr_type}" }, library_note "custom simps projection" /-- Specify simps projections, see Note [custom simps projection]. - Set `trace.simps.verbose` to true to see the generated projections. -/ + You can specify custom names by writing e.g. + `initialize_simps_projections equiv (to_fun → apply, inv_fun → symm_apply)`. + Set `trace.simps.verbose` to true to see the generated projections. + If the projections were already specified before, you can call `initialize_simps_projections` + again to see the generated projections. -/ @[user_command] meta def initialize_simps_projections_cmd (_ : parse $ tk "initialize_simps_projections") : parser unit := do env ← get_env, - ns ← many ident, - ns.mmap' $ λ nm, do nm ← resolve_constant nm, simps_get_raw_projections env nm + ns ← (prod.mk <$> ident <*> (tk "(" >> + sep_by (tk ",") (prod.mk <$> ident <*> (tk "->" >> ident)) <* tk ")")?)*, + ns.mmap' $ λ data, do + nm ← resolve_constant data.1, + simps_get_raw_projections env nm tt $ data.2.get_or_else [] /-- Get the projections of a structure used by `@[simps]` applied to the appropriate arguments. - Returns a list of triples (projection expression, projection name, corresponding right-hand-side), - one for each projection. + Returns a list of quadruples + (projection expression, given projection name, original (full) projection name, + corresponding right-hand-side), + one for each projection. The given projection name is the name for the projection used by the user + used to generate (and parse) projection names. The original projection name is the actual + projection name in the structure, which is only used to check whether the expression is an + eta-expansion of some other expression. For example, in the structure + + Example 1: ``simps_get_projection_exprs env `(α × β) `(⟨x, y⟩)`` will give the output + ``` + [(`(@prod.fst.{u v} α β), `fst, `prod.fst, `(x)), + (`(@prod.snd.{u v} α β), `snd, `prod.snd, `(y))] + ``` - Example: ``simps_get_projection_exprs env `(α × β) `(⟨x, y⟩)`` will give the output + Example 2: ``simps_get_projection_exprs env `(α ≃ α) `(⟨id, id, λ _, rfl, λ _, rfl⟩)`` + will give the output ``` - [(`(@prod.fst.{u v} α β), `prod.fst, `(x)), (`(@prod.snd.{u v} α β), `prod.snd, `(y))] + [(`(@equiv.to_fun.{u u} α α), `apply, `equiv.to_fun, `(id)), + (`(@equiv.inv_fun.{u u} α α), `symm_apply, `equiv.inv_fun, `(id)), + ..., + ...] ``` + The last two fields of the list correspond to the propositional fields of the structure, + and are rarely/never used. -/ -- This function does not use `tactic.mk_app` or `tactic.mk_mapp`, because the the given arguments -- might not uniquely specify the universe levels yet. meta def simps_get_projection_exprs (e : environment) (tgt : expr) - (rhs : expr) : tactic $ list $ expr × name × expr := do + (rhs : expr) : tactic $ list $ expr × name × name × expr := do let params := get_app_args tgt, -- the parameters of the structure (params.zip $ (get_app_args rhs).take params.length).mmap' (λ ⟨a, b⟩, is_def_eq a b) <|> fail "unreachable code (1)", let str := tgt.get_app_fn.const_name, - projs ← e.structure_fields_full str, let rhs_args := (get_app_args rhs).drop params.length, -- the fields of the object - guard (rhs_args.length = projs.length) <|> fail "unreachable code (2)", - (raw_univs, raw_exprs) ← simps_get_raw_projections e str, + (raw_univs, projs_and_raw_exprs) ← simps_get_raw_projections e str, + guard (rhs_args.length = projs_and_raw_exprs.length) <|> fail "unreachable code (2)", let univs := raw_univs.zip tgt.get_app_fn.univ_levels, + let projs := projs_and_raw_exprs.map $ prod.fst, + original_projection_names ← e.structure_fields_full str, + let raw_exprs := projs_and_raw_exprs.map $ prod.snd, let proj_exprs := raw_exprs.map $ λ raw_expr, (raw_expr.instantiate_univ_params univs).instantiate_lambdas_or_apps params, - return $ proj_exprs.zip $ projs.zip rhs_args + return $ proj_exprs.zip $ projs.zip $ original_projection_names.zip rhs_args /-- Configuration options for the `@[simps]` attribute. @@ -316,8 +373,8 @@ meta def simps_add_projections : ∀(e : environment) (nm : name) (suffix : stri if is_constant_of (get_app_fn rhs_ap) intro then do -- if the value is a constructor application tuples ← simps_get_projection_exprs e tgt rhs_ap, let projs := tuples.map $ λ x, x.2.1, - let pairs := tuples.map $ λ x, x.2, - eta ← expr.is_eta_expansion_aux rhs_ap pairs, -- check whether `rhs_ap` is an eta-expansion + let pairs := tuples.map $ λ x, x.2.2, + eta ← rhs_ap.is_eta_expansion_aux pairs, -- check whether `rhs_ap` is an eta-expansion let rhs_ap := eta.lhoare rhs_ap, -- eta-reduce `rhs_ap` /- As a special case, we want to automatically generate the current projection if `rhs_ap` was an eta-expansion. Also, when this was a desired projection, we need to generate the @@ -335,8 +392,14 @@ meta def simps_add_projections : ∀(e : environment) (nm : name) (suffix : stri let x := (todo.find $ λ x, projs.all $ λ proj, ¬ ("_" ++ proj.last).is_prefix_of x).iget, simp_lemma := nm.append_suffix $ suffix ++ x, needed_proj := (x.split_on '_').tail.head in - fail!"Invalid simp-lemma {simp_lemma}. Projection {needed_proj} doesn't exist.", - tuples.mmap' $ λ ⟨proj_expr, proj, new_rhs⟩, do + fail! +"Invalid simp-lemma {simp_lemma}. Structure {str} does not have projection {needed_proj}. +The known projections are: + {projs} +You can also see this information by running + `initialize_simps_projections {str}`. +Note: the projection names used by @[simps] might not correspond to the projection names in the structure.", + tuples.mmap' $ λ ⟨proj_expr, proj, _, new_rhs⟩, do new_type ← infer_type new_rhs, let new_todo := todo.filter_map $ λ x, string.get_rest x $ "_" ++ proj.last, b ← is_prop new_type, @@ -380,7 +443,7 @@ meta def simps_tac (nm : name) (cfg : simps_cfg := {}) (todo : list string := [] /-- The parser for the `@[simps]` attribute. -/ meta def simps_parser : parser (list string × simps_cfg) := do -/- note: we currently don't check whether the user has written a nonsense namespace as arguments. -/ +/- note: we don't check whether the user has written a nonsense namespace in an argument. -/ prod.mk <$> many (name.last <$> ident) <*> (do some e ← parser.pexpr? | return {}, eval_pexpr simps_cfg e) @@ -420,10 +483,14 @@ derives two simp-lemmas: ⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a ``` +* You can specify custom projection names, by specifying the new projection names using + `initialize_simps_projections`. + Example: `initialize_simps_projections equiv (to_fun → apply, inv_fun → symm_apply)`. + * If one of the fields itself is a structure, this command will recursively create simp-lemmas for all fields in that structure. * Exception: by default it will not recursively create simp-lemmas for fields in the structures - `prod` and `pprod`. Give explicit projection names to override this. + `prod` and `pprod`. Give explicit projection names to override this behavior. Example: ```lean @@ -432,7 +499,7 @@ derives two simp-lemmas: ``` generates ```lean - @[simp] lemma foo_fst : foo.fst = (1, 2) + @[simp] lemma foo_fst : foo.fst = (1, 2) @[simp] lemma foo_snd_fst : foo.snd.fst = 3 @[simp] lemma foo_snd_snd : foo.snd.snd = 4 ``` diff --git a/test/simps.lean b/test/simps.lean index fdb220f510401..f265805594106 100644 --- a/test/simps.lean +++ b/test/simps.lean @@ -237,9 +237,19 @@ run_cmd do "Invalid simp-lemma specify.specify1_fst_fst. Projection fst doesn't exist, because target is not a structure.", success_if_fail_with_msg (simps_tac `specify.specify1 {} ["foo_fst"]) - "Invalid simp-lemma specify.specify1_foo_fst. Projection foo doesn't exist.", + "Invalid simp-lemma specify.specify1_foo_fst. Structure prod does not have projection foo. +The known projections are: + [fst, snd] +You can also see this information by running + `initialize_simps_projections prod`. +Note: the projection names used by @[simps] might not correspond to the projection names in the structure.", success_if_fail_with_msg (simps_tac `specify.specify1 {} ["snd_bar"]) - "Invalid simp-lemma specify.specify1_snd_bar. Projection bar doesn't exist.", + "Invalid simp-lemma specify.specify1_snd_bar. Structure prod does not have projection bar. +The known projections are: + [fst, snd] +You can also see this information by running + `initialize_simps_projections prod`. +Note: the projection names used by @[simps] might not correspond to the projection names in the structure.", success_if_fail_with_msg (simps_tac `specify.specify5 {} ["snd_snd"]) "Invalid simp-lemma specify.specify5_snd_snd. The given definition is not a constructor application: @@ -586,6 +596,48 @@ initialize_simps_projections equiv end manual_universes +namespace manual_projection_names + +structure equiv (α : Sort*) (β : Sort*) := +(to_fun : α → β) +(inv_fun : β → α) + +local infix ` ≃ `:25 := manual_projection_names.equiv + +variables {α β γ : Sort*} + +instance : has_coe_to_fun $ α ≃ β := ⟨_, equiv.to_fun⟩ + +def equiv.symm (e : α ≃ β) : β ≃ α := ⟨e.inv_fun, e.to_fun⟩ + +/-- See Note [custom simps projection] -/ +def equiv.simps.inv_fun (e : α ≃ β) : β → α := e.symm + +initialize_simps_projections equiv (to_fun → apply, inv_fun → symm_apply) + +run_cmd do + e ← get_env, + data ← simps_get_raw_projections e `manual_projection_names.equiv, + guard $ data.2.map prod.fst = [`apply, `symm_apply] + +@[simps {simp_rhs := tt}] protected def equiv.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ := +⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩ + +example (e₁ : α ≃ β) (e₂ : β ≃ γ) (x : α) : (e₁.trans e₂) x = e₂ (e₁ x) := +by simp only [equiv.trans_apply] + +example (e₁ : α ≃ β) (e₂ : β ≃ γ) (x : γ) : (e₁.trans e₂).symm x = e₁.symm (e₂.symm x) := +by simp only [equiv.trans_symm_apply] + +-- the new projection names are parsed correctly (the old projection names won't work anymore) +@[simps apply symm_apply] protected def equiv.trans2 (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ := +⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩ + +-- initialize_simps_projections equiv + +end manual_projection_names + + -- test transparency setting structure set_plus (α : Type) := (s : set α)