Skip to content

[Merged by Bors] - chore: uncomment cons_injective and cons_inj in Data/List/Basic.lean#372

Closed
dwrensha wants to merge 3 commits intoleanprover-community:masterfrom
dwrensha:list-basic
Closed

[Merged by Bors] - chore: uncomment cons_injective and cons_inj in Data/List/Basic.lean#372
dwrensha wants to merge 3 commits intoleanprover-community:masterfrom
dwrensha:list-basic

Conversation

@dwrensha
Copy link
Copy Markdown
Member

@dwrensha dwrensha commented Aug 19, 2022 •
edited
Loading

@digama0
Copy link
Copy Markdown
Member

digama0 commented Aug 19, 2022

nolints are almost never the right thing to do in response to a linter warning. In this case the issue is that injective is reducible, I don't think it was in lean 3. (The reason it was omitted from #22 is because injective didn't exist at the time.)

@dwrensha
Copy link
Copy Markdown
Member Author

dwrensha commented Aug 19, 2022

Should we remove the @[reducible] attribute from injective?

@gebner
Copy link
Copy Markdown
Member

gebner commented Aug 22, 2022

Yes, injective should not be reducible. See also leanprover-community/mathport#118

@gebner
Copy link
Copy Markdown
Member

gebner commented Aug 22, 2022

Please also follow the commit message guidelines and title this PR chore: uncomment cons_injective and cons_inj

@dwrensha
Copy link
Copy Markdown
Member Author

dwrensha commented Aug 22, 2022

(link to commit message guidelines: https://github.com/leanprover-community/lean/blob/master/doc/commit_convention.md )

@gebner
Copy link
Copy Markdown
Member

gebner commented Aug 22, 2022

New guidelines: https://github.com/leanprover/lean4/blob/3a20b6be8a570eb2027675aee1ca2206c7b73b8a/doc/dev/commit_convention.md

@dwrensha dwrensha changed the title [Data/List/Basic] uncomment some cons_injective and cons_inj chore(Data/List/Basic): uncomment cons_injective and cons_inj Aug 22, 2022
@dwrensha
Copy link
Copy Markdown
Member Author

dwrensha commented Aug 22, 2022

Updated the PR title (subject) and summary (body) to conform with the conventions.

@gebner
Copy link
Copy Markdown
Member

gebner commented Aug 22, 2022

Can you please remove the @[reducible] from injective instead?

@gebner
Copy link
Copy Markdown
Member

gebner commented Aug 22, 2022

And please follow the new conventions. (Which no longer have the (Data/List/Basic) part.)

@gebner gebner added the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 22, 2022
@dwrensha
Copy link
Copy Markdown
Member Author

dwrensha commented Aug 22, 2022

Removing @[reducible] from Function.injective causes these errors:

./././Mathlib/Order/Basic.lean:317:2: error: @[ext] attribute only applies to structures or lemmas proving x = y, got injective (@toLE ?α)
./././Mathlib/Order/Basic.lean:339:2: error: @[ext] attribute only applies to structures or lemmas proving x = y, got injective (@toPreorder ?α)
./././Mathlib/Order/Basic.lean:347:2: error: @[ext] attribute only applies to structures or lemmas proving x = y, got injective (@toPartialOrder ?α)
./././Mathlib/Order/Basic.lean:361:2: error: tactic 'introN' failed, insufficient number of binders
α✝ : Type u
β : Type v
γ : Type w
r : α✝ → α✝ → Prop
α : Type u_1
A B : Preorder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B
./././Mathlib/Order/Basic.lean:366:2: error: tactic 'introN' failed, insufficient number of binders
α✝ : Type u
β : Type v
γ : Type w
r : α✝ → α✝ → Prop
α : Type u_1
A B : PartialOrder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B
./././Mathlib/Order/Basic.lean:372:2: error: tactic 'introN' failed, insufficient number of binders
α✝ : Type u
β : Type v
γ : Type w
r : α✝ → α✝ → Prop
α : Type u_1
A B : LinearOrder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B

These didn't look trivial to fix, so I thought it would it would make sense to land this with the comment instead.
I'll look into fixing them...

@dwrensha dwrensha changed the title chore(Data/List/Basic): uncomment cons_injective and cons_inj chore: uncomment cons_injective and cons_inj in Data/List/Basic.lean Aug 22, 2022
@dwrensha dwrensha mentioned this pull request Aug 22, 2022
Closed
bors bot pushed a commit that referenced this pull request Aug 22, 2022
@dwrensha
fix: remove @[reducible] attribute from Function.injective (#375)
6c88b50 
In mathlib3, [`function.injective`](https://github.com/leanprover-community/lean/blob/4b58f26becf336a50cf037c3e2894b6f2938956e/library/init/function.lean#L73) is not reducible, so `Function.injective` should not be reducible here either.

To avoid errors in `Order/Basic` ("@[ext] attribute only applies to structures or lemmas proving x = y"), we need to adjust `extAttribute` too.

Fixes some problems seen in #372.
@gebner
Copy link
Copy Markdown
Member

gebner commented Aug 22, 2022

bors r+

bors bot pushed a commit that referenced this pull request Aug 22, 2022
@dwrensha
chore: uncomment cons_injective and cons_inj in Data/List/Basic.lean (#…
d211150 
…372)

Uncomment two theorems that were added in commented form in #22.

You may compare to the mathlib3 versions here: https://github.com/leanprover-community/mathlib/blob/aaf7dc2c34831dbd92a21b9e37c1f63017d35f45/src/data/list/basic.lean#L50-L54
@bors
Copy link
Copy Markdown

bors bot commented Aug 22, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore: uncomment cons_injective and cons_inj in Data/List/Basic.lean [Merged by Bors] - chore: uncomment cons_injective and cons_inj in Data/List/Basic.lean Aug 22, 2022
@bors bors bot closed this Aug 22, 2022
@dwrensha dwrensha deleted the list-basic branch August 22, 2022 17:27
@gebner gebner mentioned this pull request Jun 15, 2023
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

awaiting-author A reviewer has asked the author a question or requested changes.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@dwrensha @digama0 @gebner