Checking disproofs with comparator

Stream: lean4

[Mirek Olšák]

Let's say there is a challenge problem which cannot be solved simply because it is possible to prove its negation (as long as we believe in Lean's consistency). Then claiming such challenge as False should be in a way officially accepted answer.

• Do I understand correctly that Comparator doesn't have a way of checking for disproofs so far?
• If it doesn't, how hard would be to add such feature? Is there an intention to have it in the future?

I was also thinking of a two possible workarounds:

• (a) Write a meta-code in the challenge file which automatically adds a new theorem theorem challenge_disproof : ... (original type ... -> False := sorry disproof-challenges as new theorems to be proven. Downside: it would not be possible to properly negate universe arguments.
• (b) Write another meta-code which adds a new axiom axiom challenge_axiom : ... (original type) ..., and then asks to prove False under this new axiom. Downside: needs tinkering with both the challenge and the proposed disproof solution.

[James E Hanson]

Mirek Olšák said:

• Do I understand correctly that Comparator doesn't have a way of checking for disproofs so far?

What do you mean by a 'disproof' in the context of Lean specifically?

[Mirek Olšák]

I think by workaround (b) defines it quite precisely from the logical standpoint. As something that can be easily checked, a theorem of type definitionally equal to challenge_statement -> False with arbitrarily set universe metavariables.

[Mirek Olšák]

(arbitrarily set by the disproof)

[James E Hanson]

Ah, okay I see. This is equivalent to asking for the ability to check whether something is a proof of a given proposition with some solver-chosen substitution of universe levels. This would be pretty easy to add to Comparator if you really wanted to.

[Mirek Olšák]

So you would propose: (1) add lmvar unification as an option to comparator, (2) with a meta-code, add a theorem negation to the challenge file.

[James E Hanson]

Yes that would be one way to do it.

[Mirek Olšák]

Note that it is not that I would see a strong practical need for the lmvar unification, it just feels more logically precise.

[James E Hanson]

I believe you would only need to change the behavior of this line for (1).

[Mirek Olšák]

I found this line too but I don't understand exactly comparator's inner working. As far as I understand, this compares two constants that happened to be equal by some previous merging.

[Mirek Olšák]

In MetaM, I would know what to do but this seems more low-level.

[James E Hanson]

Mirek Olšák said:

I found this line too but I don't understand exactly comparator's inner working. As far as I understand, this compares two constants that happened to be equal by some previous merging.

Right now it's checking for literal syntactic identity of the ConstantVal of the two theorems, which means it's checking that the name, level parameters, and type expressions are literally identical (although the name check is redundant at that point, since it's used to grab the constants).

[Henrik Böving]

Just as a heads up: I will not be accepting option PRs to comparator unless there is a really really really good reason. It's supposed to be a tool that you give the constants to compare, you say the axioms that can be used and then it says yes or no and it is perfectly clear what that yes or no means. The fact that nanoda is currently an option is just transient until it stabilizes again.

[Mirek Olšák]

So it is meant to be minimalistic, rather than a general judge tool for different purposes?
What would you propose if someone wants to be able checking for disproofs then? Use only the Comparator's sandboxing, and write a custom (perhaps a clone) script to check the solution?

In general, you could want to check if a solution provides a constant satisfying given properties, not necessarily being exactly equal to something.

[Henrik Böving]

What would you propose if someone wants to be able checking for disproofs then?

Well, just write out the challenge with a not in front of it I would say?

[Aaron Liu]

that doesn't always work :(

[Eric Wieser]

I think we should have a non_theorem keyword that does that transformation automatically in the elaborator

[Eric Wieser]

From the comparator side this would amount to the logic being something like

if isExactlySameType orig new then
  ok
else if isExactlySameType orig (mkNot new) then
  exit 2
else
  exit 1

[Mirek Olšák]

Henrik Böving said:

What would you propose if someone wants to be able checking for disproofs then?

Well, just write out the challenge with a not in front of it I would say?

That is my proposed (a) workaround which expects an extra line of meta-command in the challenge (fair), and doesn't negate universe parameters properly. I am fine with it as a temporary solution but I would not consider it fully principled.

[Mirek Olšák]

I understand if extending Comparator only with negation sounds unprincipled. What about having a way for the user to write his own comparator check in MetaM for some of the constants instead of comparing via direct type equality? Another (pseudocode) example could be something like

def answer : Nat := sorry
#comparator_check isLiteral answer

[Henrik Böving]

We do not want to make it extensible in this manner (or any manner really). That way some people on twitter or w/e will just say "oh look the Lean people still didn't get a fool proof way to check whether you got something right, you can just put a trivial comparison check here and it eats it".

[Henrik Böving]

If you want to write your own tool and maybe even base it off comparator that is okay but please make sure to not call it comparator or anything that is reminiscent of it. While comparator fulfills a technical role it also very much fulfills a marketing role for the Lean project.

[Mirek Olšák]

I would like to make a distinction between setting up challenge, and writing a solution. If the challenge is "You must prove this." then it should not expect anything else. But I would also expect more flexibility for what a challenge could be.

[Mirek Olšák]

In Lean Together, I have heard that the developers are preparing tools for defining what a challenge is. Then it feels a little unsatisfactory if you say "Checking exactly equal types is all we offer." But ok, if you say the developers are not interested in building more flexible verification tools, I might think of a custom one.

[Henrik Böving]

In Lean Together, I have heard that the developers are preparing tools for defining what a challenge is.

Where have you heard that? I am "the developers" and I'm not working on this

[Henrik Böving]

Oh maybe you overheard people talking about making it easier to set up a comparator environment, that's certainly on the list somewhere. But comparator as it exists is essentially feature complete by definition, modulo maybe adding more kernels as they come around.

[Mirek Olšák]

I recall something like that from some of the big talks, I would need to rewatch, maybe Leo, maybe the introduction... but fine, I understand comparator is not the tool.