fail_if_success vs success_if_fail

Stream: general

[Bolton Bailey]

I notice these tactics do the same thing. Their docstrings are even exactly the same, and the only difference is that the error messages says "fail_if _success" in one and "success_if_fail" in the other. Autocomplete suggests there may have been a previous thread about this, but I can't get Zulip to show me that thread. Should this be fixed?

[Eric Rodriguez]

I don't think they're the same?

[Bolton Bailey]

Hmm, maybe I just have an old lean version, let me check

[Mario Carneiro]

I think they are the same

[Mario Carneiro]

What do you mean by "fixed"?

[Bolton Bailey]

Here is the line https://github.com/leanprover-community/lean/blob/98a113f41ddcc750ba0d780c7b46976339d2a325/library/init/meta/tactic.lean#L170

[Bolton Bailey]

Well, by "fixed" I mean "changed so that only one of these exists".

[Bolton Bailey]

Or at least, redefined so that one is an alias for the other

[Eric Rodriguez]

hmm, I didn't experiment with plugging in a success to success if fail. to me, it seems that success_if_fail {x} should do nothing on a success instead of thrwoing

[Mario Carneiro]

that's called try

[Mario Carneiro]

They can't be aliases if they have different error messages

[Bolton Bailey]

Eric Rodriguez said:

hmm, I didn't experiment with plugging in a success to success if fail. to me, it seems that success_if_fail {x} should do nothing on a success instead of thrwoing

Going off the names I'm not sure I would expect one of fail_if_success/success_if_fail to behave differently from the other. I just don't expect to see both.

[Mario Carneiro]

FWIW only failIfSuccess exists in lean 4

[Bolton Bailey]

I guess backwards compatibility is an issue, since this is actually in lean and not mathlib. Is it a backwards compatibility problem if one of them starts printing out the error message that the other prints now? Maybe it's best to just leave it.

[Mario Carneiro]

There are 48 uses of fail_if_success and 11 uses of success_if_fail in lean core, and 11 uses of fail_if_success and 194 uses of success_if_fail in mathlib

[Mario Carneiro]

backwards compatibility is a non-goal

[Bolton Bailey]

Ok, then maybe better to just leave it?

[Mario Carneiro]

we would just cut another version of lean if we wanted to change this

[Mario Carneiro]

I'm not sure I would be able to reliably guess which one exists, if only one does

[Bolton Bailey]

I was going off the heuristic of "you shouldn't have two pieces of code to do one thing" but honestly, this is maybe only ~20s of confusion for those who encounter it and use "go to definition" in vscode to see what's going on.

[Mario Carneiro]

there is also success_if_fail_with_msg but no fail_if_success_with_msg in mathlib

[Mario Carneiro]

I like that the coq version of this tactic is just called Fail

[Mario Carneiro]

so I don't have to think about this ordering

[Mario Carneiro]

Even better, you can (and people do) use Fail Fail to write the equivalent of example in lean, to test that a definition works without actually doing it

[Eric Rodriguez]

Fail is way nicer, though; gives a lot nicer output for Alectryon to use ;b

[Mario Carneiro]

can you elaborate?

[Eric Rodriguez]

Fail says something like:

Command `xyz` did indeed fail, with error message:
------------
ActualOutputErrorMessage

whilst success_if_fail just said tactic did indeed fail owtte; if you're explaining why typechecking fails or something subtle it's cool to have the OG error message

[Eric Rodriguez]

I'm not sure if this changd in Lean4

[Mario Carneiro]

Oh, yeah that makes sense, since lean tactics that succeed aren't supposed to produce any output

[Mario Carneiro]

I suppose there could be a success_if_fail? that prints the error message

[Mario Carneiro]

maybe it should be called trace_if_fail

[Johan Commelin]

But then there should also be a fail_if_trace :rofl:

[Kevin Buzzard]

I just see a bunch of computer scientists arguing about whether $X\implies Y$ and $Y\implies X$ are the same thing here, and apparently they are

[Kevin Buzzard]

Maybe it should be called success_iff_fail

[Eric Wieser]

(deleted)

[Mario Carneiro]

I think this is something like the use of "if" in making definitions. If I say that tactic X fails if Y succeeds, it leaves undetermined whether it also fails in other cases, but it is a violation of linguistic convention to do not say the most precise statement so the "if" gets promoted to "iff".

In other words, blame english, not computer science

[Kevin Buzzard]

"if you don't get down from that tree, I'm calling the police". Sounds like it implies "if you do get down from that tree, I'm not calling the police" but not if you read the small print

[David Wärn]

I think "if" is used this way in maths definitions too, as in "we say a function f is analytic if bla". You can think of it as an inductive prop!