Fix one Lean misformalisation #217
Conversation
The hypotheses were contradictory without the missing positivity guard as the following succeeds without the change included here: ``` exfalso have : IsQualifying S := hS.1 rw [IsQualifying_def] at this obtain ⟨h₁, h₂, h₃, h₄⟩ := this have : -7 ∈ S := h₃ (-7) (h₄ 2 h₂) replace this : 0 < -7 := h₁ _ this linarith ``` This was previously "fixed" in c4512ca but unfortunately an error remained.
|
I've just realised that I presumably have to add the informal statements for the four new problems also. I'll come back to this tomorrow. |
|
To clarify, these are "missing" in the sense that we never formalized them, right? I don't believe we've formalized these in any of the other languages either. Presumably there was a barrier in our understanding or in the naturality of the formalization. |
Yes, exactly.
Agreed.
I can't comment here but they are definitely slightly awkward to state. |
|
Thanks for taking this on! Do you think you will be adding more new formalizations? I might need to add other team members to assist with reviewing, and also possibly to add corresponding Isabelle formalizations, if this is the case. |
|
Perhaps in that case the fixed formalization should be split to a separate PR from the new ones? |
ocfnash
changed the title
Agreed, done. The new statements now exist in this branch and I will create a PR if / when George indicates he is open to this (as well as after I have had a chance to add the informal statements). |
I'm not sure, for now I have other priorities but things may change. Sorry not to have a better answer.
Totally understandable. For now I'll assume you are not open to adding new statements but I might ask you again in the near future to see if that changes (no problem if not!). |
|
For emphasis: this PR now has just one commit with a small fix. |
By default I am definitely open to contributions to the benchmark! Please feel free to contribute new statements as you please, I'll handle on our end coordinating who on the team can assist with reviews in the case that effort required is such that I alone cannot make the review process speedy and effective while balancing other priorities. |
No description provided.