Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - chore(data/fintype): drop a decidable_pred assumption #14971

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - chore(data/fintype): drop a decidable_pred assumption #14971

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions src/data/fintype/basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1006,8 +1006,9 @@ begin
end

/-- If the subtype of all-but-one elements is a `fintype` then the type itself is a `fintype`. -/
def fintype_of_fintype_ne (a : α) [decidable_pred (= a)] (h : fintype {b // b ≠ a}) : fintype α :=
fintype.of_equiv _ $ equiv.sum_compl (= a)
def fintype_of_fintype_ne (a : α) (h : fintype {b // b ≠ a}) : fintype α :=
fintype.of_bijective (sum.elim (coe : {b // b = a} → α) (coe : {b // b ≠ a} → α)) $
by { classical, exact (equiv.sum_compl (= a)).bijective }
Comment on lines +1010 to +1011
Copy link
Collaborator

@vihdzp vihdzp Jun 26, 2022 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is this new proof so much longer than the old one? Can't you just do?

Suggested change
fintype.of_bijective (sum.elim (coe : {b // b = a} → α) (coe : {b // b ≠ a} → α)) $
by { classical, exact (equiv.sum_compl (= a)).bijective }
by { classical, exact fintype.of_equiv _ (equiv.sum_compl (= a)) }

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

With my proof, it is clear that the "data" part of the definition does not depend on classical.choice. I don't know if your definition is computable.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is just the old proof with classical slapped on top, so the data part should be computable as well.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Your definition is noncomputable. My definition still compiles if I remove type annotations from coe but I'm not sure how much this will affect readability.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here is a bit more straightforward of an algorithm data-wise, but it still depends on classical.choice -- the goal is equivalent to x = a ∨ ¬x = a, and I wouldn't be surprised if LEM could be proved from this definition.

Suggested change
fintype.of_bijective (sum.elim (coe : {b // b = a} → α) (coe : {b // b ≠ a} → α)) $
by { classical, exact (equiv.sum_compl (= a)).bijective }
⟨((finset.univ : finset {b // b ≠ a}).map (function.embedding.subtype _)).cons a (by simp),
λ x, by { cases eq_or_ne x a; simp [*] }⟩

@vihdzp The reason it's not computable when you put classical at the beginning is that the generated term is of the form let I := foo in bar where foo is the noncomputable classical decidability instance.


section finset

Expand Down