chore(logic/hydra): instance well_founded.cut_expand
#18757
Conversation
vihdzp
commented
Apr 7, 2023
vihdzp
commented
vihdzp
added
the
modifies-synchronized-file
| 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.
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.
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.
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.
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 ...
YaelDillies
added
awaiting-author
