sorryful_lemma?

Stream: PhysLean

[Joseph Tooby-Smith]

So Physlean all the lemmas and definitions are sorry free, and I don't think we should change this.

However, I think it would be nice to allow to have a certain types of lemmas and definitions which do allow sorry, e.g. sorryful_lemma and sorryful_def.

I think this can be achieved with some type of linter which

• fails if a lemma or def or theorem contains the sorry axiom,
• fails if a sorryful_lemma or sorryful_def does not contain a sorry axiom.

Ideally the sorryful_lemma and sorryful_def should also appear in the TODO list.

I'm open to different names instead of sorryful_lemma and sorryful_def, and any thoughts on whether this is a good idea or not. But also, does anyone know the best way this could be implemented?

[Joseph Tooby-Smith]

I think this #lean4 > Silent sorry could form part of a solution

[ZhiKai Pong]

what's the difference between this and semiformal_result?

[Joseph Tooby-Smith]

This can be viewed as a more general version of semiformal_result.

This is because semiformal_result does not accept any proof, whilst sorryful_lemma would accept a partial proof which contains sorry. For example, you may know how to do most of a proof but not one or two steps etc.

Also you should be able to use sorryful_lemma and sorryful_def results to prove and define further sorryful_lemma and sorryful_def results which is not currently possible with semiformal_result.

[Tomas Skrivan]

I think this should effectively subsume semiformal_result. It would help with labor division as someone experienced can quickly churnout a good API with sorries and then others can fill in the blanks and also already use it somewhere else.

[Joseph Tooby-Smith]

Agreed, after this is implemented semiformal_result should be removed.

A draft PR is here PR627.
The idea is to have sorryful_lemma and sorryful_def as synonymous of lemma and def, and have a linter which picks up the presence of the sorry axiom in all declarations execpt sorryful_lemma and sorryful_def, where it's inclusion is enforced.

I currently have the linter (just for sorryful_lemma for now), but can't work out how to turn it on globally, or make it run when using lake exe runlinter.

[Joseph Tooby-Smith]

I've now finished PR627. Ended up going down a different route to sorryful_lemma and sorryful_def, which is to create an attribute @[sorryful] and a linter noSorry.

The linter noSorry enforces the condition that the declaration depnds on thesorryAx axiom if and only if that it has the sorryful attribute. With the vscode extension TODO Highlight the sorryful attribute will appear in red.

An example is:

@[sorryful]
lemma toElectricMagneticField_equivariant (d : ℕ)
    (g : LorentzGroup 3) (E : ElectricField) (B : MagneticField)
    (x : SpaceTime) :
    (toElectricMagneticField.symm (lorentzAction.smul g (E, B))).1 x=
    (realLorentzTensor.F.obj _).ρ g ((toElectricMagneticField.symm (E, B)).1 x) := by
  sorry

One downside of this is that Linting now takes a bit longer due to the extra noSorry lint. The @[sorryful] attribute also helps with adding these lemmas to the TODO list of the project.

If anyone one would like to review that PR that would be great :).

[Joseph Tooby-Smith]

I'm planning on modifying this noSorry linter to include another attribute on top of sorryful, called pseudo (happy to hear suggestions for other names).

The idea is that the linter will enforce the condition that a definition or theorem depends on the axiom Lean.ofReduceBool if and only if it also has the attribute pseudo. This will be part of the same linter so should not take any more time to enforce.

The axiom Lean.ofReduceBool gets added when using the tactic native_decide which can be much much faster then decide. The catch is, that with Lean.ofReduceBool it is possible to prove false is true, and therefore prove anything (although from what I understand you have to be trying to get this to happen). Hence why i think having an attribute is a nice way to enforce the labelling of such results. This is described nicely in the docstring of native_decide:

This should be used with care because it adds the entire lean compiler to the trusted part, and the axiom Lean.ofReduceBool will show up in #print axioms for theorems using this method or anything that transitively depends on them. Nevertheless, because it is compiled, this can be significantly more efficient than using decide, and for very large computations this is one way to run external programs and trust the result.

[Shaopeng]

@Joseph Tooby-Smith would you mind confirming if the TODO list on the Physlean website (https://physlean.com/TODOList) is up to date? Thank you!

[Joseph Tooby-Smith]

Hi @Shaopeng. Yep, the TODO list is up to date. It is actually automatically generated from the Lean code itself rather than made independently - so should always be up-to date in this respect. This doesn't mean someone isn't already working on those TODO items (but in the vast majority of cases no one is), and looking at the open PR's is a good way of seeing this.

[Joseph Tooby-Smith]

In particular the only once I know which are been tackled by someone are the once related to the Harmonic Oscillator in classical mechanics, which are being discussed here: #PhysLean > Mini projects, and the once related to the Space file which are been discussed here: #PhysLean > Space, Time and SpaceTime API .

[Shaopeng]

Thank you for clarifying this and for the tips, @Joseph Tooby-Smith . I truly appreciate it!!