[Merged by Bors] - feat(tactic/protect_proj): protect_proj attribute for structures #2855

ChrisHughes24 · 2020-05-29T08:38:11Z

This attribute protect the projections of a structure that is being defined.

There were some errors in Euclidean domain caused by rw using euclidean_domain.mul_assoc instead of mul_assoc because the euclidean_domain namespace was open. This fixes this problem, and makes the group and ring etc. namespaces more usable.

robertylewis

It's not needed now, but soon enough, someone will ask if they can protect only some of the fields of a structure. What about taking an optional list of identifiers? If it's not given, the behavior should be as it is now (protect all fields). If it's given, protect only those.

robertylewis · 2020-05-29T08:43:40Z

src/tactic/protect_proj.lean

+-/
+import meta.expr
+/-!
+# protect_proj user attribute


Suggested change

# protect_proj user attribute

# `protect_proj` user attribute

robertylewis · 2020-05-29T08:47:05Z

src/tactic/protect_proj.lean

+namespace tactic
+
+/-- Tactic that is executed when a structure is marked with the `protect_proj` attribute -/
+meta def protect_proj_tac (n : name) (env : environment) : tactic environment :=


I feel like I've noticed this before, do we still not have tactic.mk_protected? This seems like a big oversight.

I'd add this function to tactic.core and implement protect_proj_tac : name -> tactic unit that fails (with your current error message) if the name is not a structure. (There's environment.is_structure to test this.)

robertylewis · 2020-05-29T08:47:54Z

src/tactic/protect_proj.lean

+    all of the projections become projected, meaning they must always be referred to by
+    their full name `foo.bar`, even when the `foo` namespace is open.",
+  after_set := some (λ n _ _, get_env >>= protect_proj_tac n >>= set_env) }
+


protect_proj should have an add_tactic_doc.

ChrisHughes24 · 2020-05-29T09:55:36Z

It's not needed now, but soon enough, someone will ask if they can protect only some of the fields of a structure. What about taking an optional list of identifiers? If it's not given, the behavior should be as it is now (protect all fields). If it's given, protect only those.

I can't work out how to do this. I give it the type user_attribute unit (list name) right? and then set parser := lean.parser.list_include_var_names. This didn't seem to work. The trouble is there are several meta constants of type lean.parser (list name), none of which are documented.

…of identifiers

ChrisHughes24 · 2020-05-29T10:19:37Z

It's not needed now, but soon enough, someone will ask if they can protect only some of the fields of a structure. What about taking an optional list of identifiers? If it's not given, the behavior should be as it is now (protect all fields). If it's given, protect only those.

I can't work out how to do this. I give it the type user_attribute unit (list name) right? and then set parser := lean.parser.list_include_var_names. This didn't seem to work. The trouble is there are several meta constants of type lean.parser (list name), none of which are documented.

I worked this out. It takes a list of identifiers that shouldn't be protected, rather than a list that should, as this is usually a shorter list. I also added a protected user attribute, and the tactic you suggested, so if the protected list is shorter, you can just use this attribute.

kckennylau · 2020-05-29T10:47:17Z

Also see discussion in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/old_structure_cmd

…y/mathlib into protect_proj

src/tactic/protected.lean

robertylewis · 2020-05-29T11:17:26Z

It would also be nice to add a few tests for these functions!

Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

…y/mathlib into protect_proj

robertylewis · 2020-05-29T16:10:42Z

Thanks Chris, this looks great.

bors merge

This attribute protect the projections of a structure that is being defined. There were some errors in Euclidean domain caused by `rw` using `euclidean_domain.mul_assoc` instead of `mul_assoc` because the `euclidean_domain` namespace was open. This fixes this problem, and makes the `group` and `ring` etc. namespaces more usable. Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com> Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>

bors · 2020-05-29T18:08:16Z

Pull request successfully merged into master.

Build succeeded:

This uses the recent `protect_proj` attribute (#2855).

…nprover-community#2855) This attribute protect the projections of a structure that is being defined. There were some errors in Euclidean domain caused by `rw` using `euclidean_domain.mul_assoc` instead of `mul_assoc` because the `euclidean_domain` namespace was open. This fixes this problem, and makes the `group` and `ring` etc. namespaces more usable. Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com> Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>

…community#2867) This uses the recent `protect_proj` attribute (leanprover-community#2855).

ChrisHughes24 added 6 commits May 29, 2020 09:32

feat(tactic/protect_proj): protect_proj attribute for structures

cf3fd7c

mark various structures with protect_proj

abe8acc

delete mess

1e3e967

finish deleting mess

5173b4f

whitespace

1dc64c9

delete attribute for nonneg_add_comm_group

c9c97e3

robertylewis reviewed May 29, 2020

View reviewed changes

ChrisHughes24 added 2 commits May 29, 2020 09:55

spelling mistakes

cc8eff6

fix euclidean_domain

850bb49

ChrisHughes24 added 3 commits May 29, 2020 11:13

mk_protected tactic, and protected attribute, and add a without list …

10c7d0d

…of identifiers

forgot to save

2d419fa

fix build

72afd1b

undo unrelated changes to euclidean domain

53e9b32

ChrisHughes24 added the awaiting-review The author would like community review of the PR label May 29, 2020

ChrisHughes24 added 2 commits May 29, 2020 11:31

make the tactic fail on non-structures

926f856

big fix

cc09e34

robertylewis and others added 5 commits May 29, 2020 12:48

Delete padic_norm.olean.lock

5751e93

fix euclidean_domain

732bb23

Merge branch 'protect_proj' of https://github.com/leanprover-communit…

fc07b8f

…y/mathlib into protect_proj

fix import of tactic.protected

a2c954e

Merge remote-tracking branch 'origin/master' into protect_proj

fd4892a

robertylewis reviewed May 29, 2020

View reviewed changes

ChrisHughes24 and others added 4 commits May 29, 2020 12:32

fix group_theory/subgroup

657780d

Update src/tactic/protected.lean

acad434

Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

Update src/tactic/protected.lean

534dc27

Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

examples

023c814

ChrisHughes24 and others added 6 commits May 29, 2020 12:42

Update src/tactic/protected.lean

6913354

Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

Merge branch 'protect_proj' of https://github.com/leanprover-communit…

5ec4871

…y/mathlib into protect_proj

fix example

db16306

add test

00c8dfe

strengthen tests

69ef16a

doc changes

5f67156

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels May 29, 2020

bors bot changed the title ~~feat(tactic/protect_proj): protect_proj attribute for structures~~ [Merged by Bors] - feat(tactic/protect_proj): protect_proj attribute for structures May 29, 2020

bors bot closed this May 29, 2020

bors bot deleted the protect_proj branch May 29, 2020 18:08

rwbarton added a commit that referenced this pull request May 30, 2020

chore(topology): make topological_space fields protected

d076ce2

This uses the recent `protect_proj` attribute (#2855).

rwbarton mentioned this pull request May 30, 2020

[Merged by Bors] - chore(topology): make topological_space fields protected #2867

Closed

bors bot pushed a commit that referenced this pull request May 30, 2020

chore(topology): make topological_space fields protected (#2867)

b40ac2a

This uses the recent `protect_proj` attribute (#2855).

cipher1024 pushed a commit to cipher1024/mathlib that referenced this pull request Mar 15, 2022

chore(topology): make topological_space fields protected (leanprover-…

206bfae

…community#2867) This uses the recent `protect_proj` attribute (leanprover-community#2855).

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(tactic/protect_proj): protect_proj attribute for structures #2855

[Merged by Bors] - feat(tactic/protect_proj): protect_proj attribute for structures #2855

ChrisHughes24 commented May 29, 2020

robertylewis left a comment

robertylewis May 29, 2020

robertylewis May 29, 2020

robertylewis May 29, 2020

ChrisHughes24 commented May 29, 2020

ChrisHughes24 commented May 29, 2020

kckennylau commented May 29, 2020

robertylewis commented May 29, 2020

robertylewis commented May 29, 2020

bors bot commented May 29, 2020

	# protect_proj user attribute
	# `protect_proj` user attribute

[Merged by Bors] - feat(tactic/protect_proj): protect_proj attribute for structures #2855

[Merged by Bors] - feat(tactic/protect_proj): protect_proj attribute for structures #2855

Conversation

ChrisHughes24 commented May 29, 2020

robertylewis left a comment

Choose a reason for hiding this comment

robertylewis May 29, 2020

Choose a reason for hiding this comment

robertylewis May 29, 2020

Choose a reason for hiding this comment

robertylewis May 29, 2020

Choose a reason for hiding this comment

ChrisHughes24 commented May 29, 2020

ChrisHughes24 commented May 29, 2020

kckennylau commented May 29, 2020

robertylewis commented May 29, 2020

robertylewis commented May 29, 2020

bors bot commented May 29, 2020