idea: `native_decide +no_implementedBy`

Stream: lean4

[Alex Meiburg]

A few mathematicians (like Kevin Buzzard and Terence Tao afaik - quiet tags there) have a policy, I know, of not accepting native_decide proofs. While I understand the reasoning, I also think it's a bit unfortunate because I think it's a very nice feature.

But: my understanding is that it isn't to do with the substantially larger trusted codebase, but rather it's about the implemented_by attribute. It's easy to throw that attribute on anything and get ridiculous behavior. It's necessary to the language of course, but usually not to mathematical theorem proving; when performance is a big concern, csimp covers it quite well.

How hard would it be to have an option on native_decide that says "I don't want any implemented_by or extern functions used"? To be clear, I'm not suggesting a flag that stops them from being in the compiler -- that would be a big change -- just a flag that, at the end of compilation, checks if any were used, and if so, throws an error on the native_decide tactic instead of closing the proof out. But, @csimp should be allowed in.

I think this would then make it "hard enough to prove False" that this would get wider acceptance among mathematicians.

Ideally there would also be a different axiom to differentiate between a native_decide call that used impl/extern functions, and one that didn't, so that at the end of very a long proof repo it's easy to check by the axioms whether all native_decide calls were of the correct setting.

[Eric Wieser]

Note that removing implementedBy would prevent you adding natural numbers

[Shreyas Srinivas]

I don’t think making this change will result in people trusting native_decide any more than at present. And then there is the fact that you might not get the performance benefits of native_decide if you remove those implemented_bys

[Shreyas Srinivas]

Also, at least in equational theories, the objection to native_decide came from me since it wouldn’t pass lean4checker

[Shreyas Srinivas]

And I was not too keen to turn off that checker and wanted to fix the code instead. There is some thread in that channel where Mario explores some alternatives

[Shreyas Srinivas]

Also back in ICFP, I asked Joachim about the idea of having two kernels, one which is more efficient and less trusted but doesn’t include the whole compiler, and another which is slower and more trusted. I don’t recall how far that discussion went. This would make native_decide potentially less necessary

[Alex Meiburg]

Eric Wieser said:

Note that removing implementedBy would prevent you adding natural numbers

Fair point - but, actually those are all externs. For an all-Lean codebase, I could see allowing extern's to be ok, and it's really just the implementedBy that's the problem. I tried looking around and the only functions with implBy that I could reasonably see cropping up in a theorem were (List/Vector/Array).attachWith and (List/Array).mapMonoM -- and Nat.repr, but that should really be changed to a csimp.

[Eric Wieser]

implementedBy can be hacked around with extern + export

[Alex Meiburg]

Ahh shoot! True :sweat:

[Alex Meiburg]

Well, I'm all for other ideas, I'm sure there is some reasonable version of this that captures "I trust the Lean compiler + core, but not any of my own code" well

[Kevin Buzzard]

It might be worth adding that I cannot immediately see any situation where native_decide would help me prove FLT (the proof is conceptual, not calculational), so my announcing "I won't have it in my repo" is very cheap for me.

[Mario Carneiro]

I think what you actually want here is just a way to track what externs and implementedBys are used in a native_decide execution, in the style of #print axioms. All the ones involved in the definition of Nat can be whitelisted

[Eric Wieser]

Alex Meiburg said:

But, @csimp should be allowed in.

csimp is unsafe too

[Kim Morrison]

This seems pretty fixable, and shouldn't get in the way of someone thinking about Mario's suggestion above.

But at the moment this seems pretty low priority to me.

[Eric Wieser]

If fixing this is low priority (which is reasonable), I think we should throw csimp in with the warnings in docstrings about implemented_by and extern.

[Mario Carneiro]

Note that unlike #print axioms, it's not possible to implement #print axioms_and_extern_and_implemented_by externally because the compiler can use simp rules during compilation, which have no trace in the cstage1 or cstage2 definitions, so post hoc by looking at the environment there is no way to know the dependencies (including proof dependencies) of a native decide proof.

For me this came up as a problem when I contemplated what it would take to implement (a sound version of) native_decide in lean4lean: even if I had a model of the whole lean IR semantics, the equivalence proof between the IR and the original def depends on unknown axioms which have been forgotten.

[Mario Carneiro]

I think the most likely implementation route for this is to do something like the simp? implementation: track usage of csimp lemmas during compilation and write them down in some kind of permanent export object like an internal def