-
Notifications
You must be signed in to change notification settings - Fork 298
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.
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
chore(logic/hydra): instance well_founded.cut_expand
#18757
base: master
Are you sure you want to change the base?
Conversation
vihdzp
commented
Apr 7, 2023
theorem _root_.well_founded.cut_expand (hr : well_founded r) : well_founded (cut_expand r) := | ||
⟨by { letI h := hr.is_irrefl, exact λ s, acc_of_singleton $ λ a _, (hr.apply a).cut_expand }⟩ | ||
instance _root_.is_well_founded.cut_expand [is_well_founded α r] : | ||
is_well_founded _ (cut_expand r) := | ||
⟨⟨λ s, acc_of_singleton $ λ a _, (is_well_founded.apply r a).cut_expand⟩⟩ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The instance is good but I don't see why you'd like to remove the theorem.
It's also tempting to add a has_well_founded
instance but when I look into the surreal multiplication proof I see we're using (trans_gen $ cut_expand is_option)
as the well-founded relation ...
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The has_well_founded
instance is not needed, as there already exists an instance is_well_founded α (has_well_founded α).r
.
As for removing the theorem, I guess this is a matter of code style. It seems like the pattern throughout Mathlib is to prefer bundled predicates like these, e.g. using is_irrefl
instead of irreflexive
, etc. We get many convenient instances this way - for instance, is_well_founded _ (trans_gen $ cut_expand is_option)
could be inferred entirely automatically. So I don't see the need for having both the theorem and the instance.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's telling that we're using well_founded.is_irrefl
, which turns the non-instance well_founded
into an instance is_well_founded
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should we change well_founded.trans_gen to instance at the same time? Anyway it looks like you can't have any PRs merged before you port all your PRs ...