[Merged by Bors] - feat(data/sign): the sign function #12835

ericrbg · 2022-03-19T23:00:53Z

Mostly for discussion about how this should be done - what should the output type be? What should we require? What basic theorems would make a good part of the API?

vihdzp · 2022-03-20T00:07:49Z

Given that there's no clear canonical type for the sign function's output, maybe a new sign type should be made?

inductive sign : Type
| pos  : sign
| zero : sign
| neg  : sign

We could then define casts from sign into ℤ or into other rings, which would all be homomorphisms under multiplication.

As for theorems, I think the basic things should be enough, i.e. sign (a * b) = sign a * sign b and variants thereof.

ericrbg · 2022-03-20T11:10:56Z

this field would be isomorphic to zmod 3, whilst being a more suitable output type. interesting, I think that's a nice idea

Vierkantor

I agree with @vihdzp's suggestion of creating a new type. If we add a coercion of the form

instance [has_zero α] [has_one α] [has_neg α] : sign → α

then we can recover the original ℤ return value quite easily.

Vierkantor · 2022-03-28T07:47:51Z

src/data/sign.lean

+
+variables [preorder α] [decidable_rel ((<) : α → α → Prop)] {a b : α}
+
+@[simp] lemma sign_zero : sign (0 : α) = 0 := by simp [sign]


For completeness, could you add the sign of positive and negative values?

ericrbg · 2022-03-28T09:40:15Z

hmm, it could be a field but I feel like mathematically it's more of a group_with_zero; which instance should I add?

Vierkantor · 2022-03-28T09:41:39Z

Let's go for group_with_zero with a remark that it could be a field (but then we wouldn't get a nice order).

src/data/sign.lean

ericrbg · 2022-03-28T14:52:55Z

I'm also not sure how to bundle this; I want to bundle sign as a monoid_with_zero_hom, but there's no real ordered_comm_monoid_with_zero, just linear_ordered_comm_monoid_with_zero. should I do that? or ordered_semiring?

src/data/sign.lean

eric-wieser · 2022-03-28T22:37:02Z

I think I remember on zulip seeing some of the following suggested:

sign : R → with_zero (unitary R), which gives complex direction
sign : R → with_zero (units ℤ)

Were these ruled out as annoying, or just forgotten?

Co-authored-by: damiano <adomani@gmail.com>

ericrbg · 2022-03-28T22:52:28Z

the first one I thought may be a bit annoying. the second could work, too; I do quite like this custom type solution as we get to have a coercion to anything without needing to mess with smul and such like

ericrbg · 2022-03-30T11:46:43Z

I think this should be good for review again, I'm not sure what other obvious things are missing. There is a couple comments in the code - if people could figure out whether we really need ring for sign_hom that'd be nice!

src/data/sign.lean

Vierkantor

I think this is starting to look very good, thanks for the hard work!

src/data/sign.lean

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: damiano <adomani@gmail.com>

jcommelin · 2022-04-09T19:34:46Z

src/data/sign.lean

+
+@[simp] lemma zero_eq_zero   : zero = 0 := rfl
+@[simp] lemma neg_eq_neg_one : neg = -1 := rfl
+@[simp] lemma pos_eq_one     : pos = 1  := rfl


Do we get -0 = 0 and --1 = 1 via some other instance below?

I just added neg_zero' in another PR, and so it's fine because of the distrib neg. We have neg_neg as we have an involutive negation

jcommelin · 2022-04-11T04:57:45Z

src/data/sign.lean

+  { cases lt_irrefl 0 (h_1.trans $ h.trans_lt h_3) },
+  { cases h_2 (h_1.trans_le h) },
+  { cases h_2 (h.trans_lt h_4) }


This is referring to auto-generated names. Can you please rewrite?

done, but I think it made it a bit more messy

src/data/sign.lean

Co-authored-by: Johan Commelin <johan@commelin.net>

jcommelin

Thanks 🎉

bors merge

Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>

bors · 2022-04-11T20:58:12Z

Pull request successfully merged into master.

Build succeeded:

feat(data/sign): the sign function

9f61f6e

ericrbg added awaiting-review The author would like community review of the PR RFC Request for comment labels Mar 19, 2022

lintfix

4b75a80

Vierkantor reviewed Mar 28, 2022

View reviewed changes

Vierkantor added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Mar 28, 2022

Merge branch 'master' into sign

506be59

Vierkantor reviewed Mar 28, 2022

View reviewed changes

src/data/sign.lean Outdated Show resolved Hide resolved

some progress

db66169

adomani reviewed Mar 28, 2022

View reviewed changes

src/data/sign.lean Outdated Show resolved Hide resolved

wip

6c64422

bundle sign as a monoid_with_zero_hom

ed8db43

ericrbg added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Mar 28, 2022

Update src/data/sign.lean

ccc1463

Co-authored-by: damiano <adomani@gmail.com>

ericrbg added 4 commits March 29, 2022 19:46

various improvements

d0a07a5

fintype instance

4d667d6

Merge branch 'master' into sign

391d6a1

remove neg_zero

4550b5a

adomani reviewed Mar 30, 2022

View reviewed changes

src/data/sign.lean Outdated Show resolved Hide resolved

adomani reviewed Mar 30, 2022

View reviewed changes

src/data/sign.lean Outdated Show resolved Hide resolved

golf

1f0e3a5

Vierkantor reviewed Apr 8, 2022

View reviewed changes

src/data/sign.lean Outdated Show resolved Hide resolved

src/data/sign.lean Outdated Show resolved Hide resolved

src/data/sign.lean Outdated Show resolved Hide resolved

src/data/sign.lean Outdated Show resolved Hide resolved

Vierkantor added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Apr 8, 2022

ericrbg and others added 2 commits April 8, 2022 15:04

Apply suggestions from code review

f70b195

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: damiano <adomani@gmail.com>

reviewer suggestions

f281e92

ericrbg added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Apr 8, 2022

jcommelin reviewed Apr 9, 2022

View reviewed changes

jcommelin reviewed Apr 11, 2022

View reviewed changes

jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Apr 11, 2022

ericrbg and others added 2 commits April 11, 2022 09:24

don't use autogenerated names

234cabc

Update src/data/sign.lean

b4f62ef

Co-authored-by: Johan Commelin <johan@commelin.net>

ericrbg added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Apr 11, 2022

jcommelin approved these changes Apr 11, 2022

View reviewed changes

leanprover-community-bot-assistant 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 Apr 11, 2022

bors bot pushed a commit that referenced this pull request Apr 11, 2022

feat(data/sign): the sign function (#12835)

cea5e4b

Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>

bors bot changed the title ~~feat(data/sign): the sign function~~ [Merged by Bors] - feat(data/sign): the sign function Apr 11, 2022

bors bot closed this Apr 11, 2022

bors bot deleted the sign branch April 11, 2022 20:58

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(data/sign): the sign function #12835

[Merged by Bors] - feat(data/sign): the sign function #12835

ericrbg commented Mar 19, 2022

vihdzp commented Mar 20, 2022

ericrbg commented Mar 20, 2022

Vierkantor left a comment

Vierkantor Mar 28, 2022

ericrbg commented Mar 28, 2022

Vierkantor commented Mar 28, 2022

ericrbg commented Mar 28, 2022 •

edited

Loading

eric-wieser commented Mar 28, 2022 •

edited

Loading

ericrbg commented Mar 28, 2022

ericrbg commented Mar 30, 2022

Vierkantor left a comment

jcommelin Apr 9, 2022

ericrbg Apr 9, 2022

jcommelin Apr 11, 2022

ericrbg Apr 11, 2022

jcommelin left a comment

bors bot commented Apr 11, 2022


		variables [preorder α] [decidable_rel ((<) : α → α → Prop)] {a b : α}

		@[simp] lemma sign_zero : sign (0 : α) = 0 := by simp [sign]

[Merged by Bors] - feat(data/sign): the sign function #12835

[Merged by Bors] - feat(data/sign): the sign function #12835

Conversation

ericrbg commented Mar 19, 2022

vihdzp commented Mar 20, 2022

ericrbg commented Mar 20, 2022

Vierkantor left a comment

Choose a reason for hiding this comment

Vierkantor Mar 28, 2022

Choose a reason for hiding this comment

ericrbg commented Mar 28, 2022

Vierkantor commented Mar 28, 2022

ericrbg commented Mar 28, 2022 • edited Loading

eric-wieser commented Mar 28, 2022 • edited Loading

ericrbg commented Mar 28, 2022

ericrbg commented Mar 30, 2022

Vierkantor left a comment

Choose a reason for hiding this comment

jcommelin Apr 9, 2022

Choose a reason for hiding this comment

ericrbg Apr 9, 2022

Choose a reason for hiding this comment

jcommelin Apr 11, 2022

Choose a reason for hiding this comment

ericrbg Apr 11, 2022

Choose a reason for hiding this comment

jcommelin left a comment

Choose a reason for hiding this comment

bors bot commented Apr 11, 2022

ericrbg commented Mar 28, 2022 •

edited

Loading

eric-wieser commented Mar 28, 2022 •

edited

Loading