unsafe customizations

Stream: lean4

[Arthur Adjedj]

Is there any set_option that lets one turn off the positivity checker for inductive types ? I know that non-strictly-positive inductives are allowed with unsafe, but I'm wondering if Lean 4 has an option to allow you to bypass this restriction outside of unsafe.

[Notification Bot]

This topic was moved here from #lean4 > possibly unsafe customizations ? by Arthur Adjedj.

[Kevin Buzzard]

Surely no set_option will enable a possible proof of false, and presumably the point of the positivity checker is to make sure you're not going to be able to prove false.

[Jason Rute]

@Arthur Adjedj It might be helpful to give you #xy here. I think the Lean developers don't want it to be easy to having an inconsistent kernel with just a simple option setting.

[Henrik Böving]

Note that this is not just an issue with consistency in the kernel, it is also a run time issue. As soon as the strong positivity checker is disabled you can start building cyclic data structures which of course our reference counting approach to memory cannot deal with.

[Arthur Adjedj]

Henrik Böving said:

Note that this is not just an issue with consistency in the kernel, it is also a run time issue. As soon as the strong positivity checker is disabled you can start building cyclic data structures which of course our reference counting approach to memory cannot deal with.

While this is true, there also exist some datatypes that are both acyclic and sound, but which are not accepted by the positivity checker. Such an example would be :

inductive Foo : Type _:=
    |  foo : HashMap Nat Foo → Foo

which doesn't get accepted, even though

inductive Foo : Type _:=
    |  foo : (Nat→ Foo) →  Foo

does.
Jason Rute said:

Arthur Adjedj It might be helpful to give you #xy here. I think the Lean developers don't want it to be easy to having an inconsistent kernel with just a simple option setting.

I agree that being able to cause unsoundness shouldn't be accessible, but there already are accessible sources of unsoundness, such as implemented_by, and it would be nice to allow the user to define a non-positive inductive type as a "safe" type if he knows that this wouldn't cause unsoundness.

[Kevin Buzzard]

Can you show me a proof of false using implemented_by?

[Arthur Adjedj]

(This is orthogonal to this discussion, but it would also be preferable IMO for native_compute and native_decide(which are unsound) to be hidden behind an option as well)

[Adam Topaz]

def foo : Nat := 0

@[implemented_by foo]
def bar : Nat := 1

example : False := by
  have : 1 = 0 := by
    show bar = foo
    native_decide
  simp at this

[Adam Topaz]

Is native_decide supposed to be disallowed?

[Arthur Adjedj]

I don't believe so, but as said previously, it should perhaps be preferable for things that can prove False to not be too easily accessible

[Adam Topaz]

yeah, I agree

[Adam Topaz]

Or there should at least be an option for "safe" implemented_by that takes a proof that the terms are equal (even if the proof is a sorry), and to only allow native_decide to evaluate using safe implementations.

[Arthur Adjedj]

Allowing possibly unsafe features to be hidden behind options (which could perhaps give warning during type-checking) feels like a safe trade-off to me, and that's probably why such options are already available in other, more mature proof-assistants

[Arthur Adjedj]

Adam Topaz said:

Or there should at least be an option for "safe" implemented_by that takes a proof that the terms are equal (even if the proof is a sorry), and to only allow native_decide to evaluate using safe implementations.

How would that work when the "implementation function" is unsafe, but the "interface" one is safe ?

[Adam Topaz]

I don't know, it was just an idle thought :)

[Adam Topaz]

Maybe for unsafe implementations, the proof would be forced to be a sorry.

[Kyle Miller]

native_decide is basically "take the Lean #eval being correct as an axiom". You can see if you have a theorem that (transitively) depends on it:

theorem baz : False := by
  have : 1 = 0 := by
    show bar = foo
    native_decide
  simp at this

#print axioms baz
-- 'baz' depends on axioms: [propext, Lean.ofReduceBool]

[Kyle Miller]

In that sense it's perfectly safe, since you should only really trust a theorem if it doesn't have Lean.ofReduceBool as an axiom.

[Adam Topaz]

Okay, I feel better now :)

[Adam Topaz]

But for the average user who wouldn't be bothered using #print axioms baz, maybe there should be some warning (that can be turned off with an option)?

[Arthur Adjedj]

Kyle Miller said:

In that sense it's perfectly safe, since you should only really trust a theorem if it doesn't have Lean.ofReduceBool as an axiom.

Isn't the main goal of these axioms to be used to make proofs faster ? If so, what is the meaning behind having these in the first place if you shouldn't trust them ?

[Kyle Miller]

@Adam Topaz Should this have a warning too then?

axiom explosion {p : Prop} : p

example : False := explosion

The docstring for native_decide says you should be careful and mentions #print axioms.

Though maybe it'd be useful having an option that disallows adding new axioms or using native_decide. I'm thinking for Mathlib and for student homework submissions.

[Adam Topaz]

yeah, teaching is exactly what I had in mind.

[Adam Topaz]

I think it's common to check for extraneous axiom commands in homework submissions. But I wouldn't think to check for uses of built-in tactics.

[Kyle Miller]

@Arthur Adjedj I think there are different levels of trust you can have in a result. I trust that the Lean kernel with no additional axioms except for Classical.choice is extremely likely to be correct. If you use native_decide, then it's on you to verify that every implemented_by is correct and that the compiler and interpreter are producing the correct result. If you show me a Lean proof without native_decide, I'll believe it if Lean accepts it. If you show me a Lean proof with native_decide, I'll have to trust you that you've done all this additional work and haven't made a mistake.

I think native_decide could be useful, and it's no worse of a situation than writing programs to calculate things to support proofs in traditional math papers.

[Mario Carneiro]

I'm surprised that no one mentioned that unsafe inductive literally does what the OP requests and turns off the positivity checker:

unsafe inductive Foo : Type where
  | mk : (Foo → False) → Foo

[Henrik Böving]

Arthur Adjedj said:

Is there any set_option that lets one turn off the positivity checker for inductive types ? I know that non-strictly-positive inductives are allowed with unsafe, but I'm wondering if Lean 4 has an option to allow you to bypass this restriction outside of unsafe.

this sounded like they already knew and do specifically not want it?

[Mario Carneiro]

@Adam Topaz said:

Or there should at least be an option for "safe" implemented_by that takes a proof that the terms are equal (even if the proof is a sorry), and to only allow native_decide to evaluate using safe implementations.

This exists, it's called @[csimp]

[Mario Carneiro]

Kyle Miller said:

In that sense it's perfectly safe, since you should only really trust a theorem if it doesn't have Lean.ofReduceBool as an axiom.

I think this is a bit too strong, Lean.ofReduceBool is also not supposed to be inconsistent. The thing is, if you are using ofReduceBool then every occurrence of implemented_by or extern should be read as axiom and you should audit it for correctness

[Mario Carneiro]

If you want a safe version for unsafe inductive, then you need a design that gets that, because obviously you can't just take the unsafe off. Currently the way lean handles proving that inductives don't introduce inconsistency is the positivity checker; if you want to make an inductive which fails the positivity checker then you have to prove it is sound somehow. How do you intend to do that?

[Mario Carneiro]

One common way this is done in mathlib is to define your type as a regular def, and then prove the constructor and recursor as theorems. You can't prove the computation rule, though, and it is almost never the case that it happens to work out to a definitional equality

[Arthur Adjedj]

Hi Mario, I'm aware of all that, what I'm saying is that the positivity checker doesn't cover all "sound" inductive definitions (and I don't expect it to !), and that as such, it would be nice to be able, for people that are confident enough in their inductive definitions and who knows what they're doing, to be able to locally disable it for some inductive types. Both Coq and Agda (with Attribute bypass_check(guard= yes) and {-# NO_POSITIVITY_CHECK #-}) respectively) have such features, and it would be desirable to have that in Lean too in my opinion.

[Mario Carneiro]

you can axiomatize the inductive you want

[Mario Carneiro]

TBH I don't think it's a good idea to just have it as an option like in Coq + Agda, unless it comes with some really scary warning to never use it in production

[Arthur Adjedj]

I'd gladly take alarming warnings over losing nice reduction rules

[Mario Carneiro]

that's a theory extension

[Arthur Adjedj]

In what sense ?

[Mario Carneiro]

right now it's fine for unsafe inductive to do whatever it wants since it doesn't touch the kernel or the theory, but if you want this in a safe inductive then you have to modify the theory to accomodate it

[Mario Carneiro]

the only thing you can justify here without a theory change is something you could already do today: an axiomatization, or a def + theorems, and just make an elab which unfolds to that stuff

[Mario Carneiro]

again, you need to specify what you want the actual syntax of the feature to be. If it is just an option to turn off positivity checking without unsafe, that is unsound, so what is preventing things from going off the rails?

[Mario Carneiro]

axiom does not let you add kernel defeq rules

[Arthur Adjedj]

Mario Carneiro said:

again, you need to specify what you want the actual syntax of the feature to be. If it is just an option to turn off positivity checking without unsafe, that is unsound, so what is preventing things from going off the rails?

Nothing would prevent it, except from the trust in the user, in the same way that axioms are dependent on the trust in the user to not axiomatise something unsound.

[Mario Carneiro]

what would you give the kernel?

[Mario Carneiro]

the kernel refuses to supply you with an inductive unless you follow the rules

[Arthur Adjedj]

The declared inductive, as well as a tag to not check positivity

[Mario Carneiro]

so what about external kernels? they don't have such a flag

[Arthur Adjedj]

Is the kernel not called whatsoever on unsafe things currently ? I would have thought that the kernel simply turned off some features when checking unsafe things, not that only the elaborator checked them

[Mario Carneiro]

the lean kernel might get called on unsafe things, but IIRC they are not in the export

[Mario Carneiro]

double checked, yes the kernel has an unsafe mode and is used unconditionally

[Arthur Adjedj]

Mario Carneiro said:

so what about external kernels? they don't have such a flag

I understand that this might not be a trivial feature, but I am just surprised at how conservative lean is with regards to these things, compared to Coq and Agda which allows many different, possibly unsafe shenanigans, to be manually turned on if an experienced user so wished to use them. An example of this is how Coq UniMath uses type-in-type in its library to have propositional resizing.

[Mario Carneiro]

A lot of it is pushback on that whole ethos, where soundness is a far future goal (or worse, a non-goal) rather than something written up in a paper that you can point to whenever anyone asks

[Mario Carneiro]

it's an interactive theorem prover for cripes sakes, soundness is the value proposition

[Mario Carneiro]

I have still yet to see a proof of soundness of the complete coq kernel (or at least, a subset sufficient for the coq standard library), and agda is not even trying

[Arthur Adjedj]

Mario Carneiro said:

I have still yet to see a proof of soundness of the complete coq kernel (or at least, a subset sufficient for the coq standard library), and agda is not even trying

Coq has MetaCoq, in which it proves its own soundness, and the Calculus of (Co)Inductive constructions has many different models nowadays to prove its theoretical soundness. As for Agda, it's unsound in many ways, and doesn't hide from it much

[Arthur Adjedj]

To add to this, MetaCoq provides a verified "safe-checker", and although it is much slower than the real type-checking, I'm pretty sure it does type-check on the entire stdlib.

[Arthur Adjedj]

If anything, I think "default" Coq is more trusted than Lean is by its users

[Mario Carneiro]

no, CIC means whatever you want it to mean in those papers, every single one finds some way to be less than the whole

[Kevin Buzzard]

As a mathematician I am instinctively very suspicious of a prover which can prove false. Programs crashing is not a big deal in CS, but proving false is deadly.

[Mario Carneiro]

metacoq is the furthest along I have seen, but it's still assuming a nontrivial axiom about normalization (of course it has to assume some axiom since it is a proof in coq, but it should be something comparable to a large cardinal axiom)

[Arthur Adjedj]

MetaCoq does assume strong normalization, yes. As a side-note, some people are currently working on extending some logical relations formalisations to prove SN on a theory ever so closer to CIC, but it's only in its beginning.

[Mario Carneiro]

and also, is it actually usable to check the standard library / other plain coq developments? Too often people just cover the "theoretically interesting" bits and miss out on the part where 1 % N overflows when N = 2^32

[Mario Carneiro]

or, implementation bugs aside, stuff like modules, coinductive types, or other "fringe" features which are actually used in practice

[Mario Carneiro]

you can easily play a linguistic game where you say "I've proved Coq" when you mean "I've proved MLTT + inductive types" and people hear "I've proved modules + nested mutual co-inductive inductive types"

[Mario Carneiro]

this situation is especially bad for PCUIC because it is always changing (well, "always" is relative, but it has changed quite a bit across the various versions of Coq)

[Arthur Adjedj]

MetaCoq has support for CoInductive/CoFix, and I remember meeting an intern that was formalizing Coq modules in MetaCoq, it might have already been merged since then, but even if not, modules aren't present at the kernel level, they only help in avoiding code duplication when writing Coq.

[Arthur Adjedj]

Mario Carneiro said:

this situation is especially bad for PCUIC because it is always changing (well, always is relative, but it has changed quite a bit across the various versions of Coq)

Always expanding might be the right word here.

[Mario Carneiro]

do you know whether you can plug the "safe checker" in to the coq frontend and run real stuff on it?

[Arthur Adjedj]

The two last "fundamental" issues that differentiate between the "real" CIC behind Coq's implementation and PCUIC, as far as I know, are the guard condition, which isn't the exact same between the two because Coq tries many heuristics to accept more things, and eta-conversion.

[Arthur Adjedj]

Mario Carneiro said:

do you know whether you can plug the "safe checker" in to the coq frontend and run real stuff on it?

You can, as far as I know, though i've never tested myself. There's a MetaCoq SafeCheck <term> command available (if you've imported the safe-checker that is, of course)

[Mario Carneiro]

I mean without modifying the coq code, just point at a library

[Mario Carneiro]

I want to know that every dependency of this term is SafeChecked

[Arthur Adjedj]

Not that I know of, I can ask around on the coq zulip

[Mario Carneiro]

do you know whether metacoq supports a "semantic" model rather than one based on normalization?

[Mario Carneiro]

that would make it a lot easier to justify stuff like different reduction rules or eta conversion

[Arthur Adjedj]

Mario Carneiro said:

do you know whether metacoq supports a "semantic" model rather than one based on normalization?

What do you mean by "semantic" here ?

[Mario Carneiro]

types are sets, elements are elements, equality is equality, defeq is also equality

[Mario Carneiro]

do the terms have a denotational semantics

[Arthur Adjedj]

I do not know, I'm not that knowledgeable when it comes to MetaCoq, but I would believe not.

[Mario Carneiro]

In lean this is a major deciding criterion for the theory, if it doesn't have a natural model then it's not ok (hence all kinds of anti-classical things are excluded)

[Arthur Adjedj]

Well, yes, Lean is classical by all means and aims to be. There's nothing stopping Coq, which (appart from Coinductives) doesn't have any theoretical features Lean doesn't have, to also have a model in ZFC+ inaccessible cardinals.

[Mario Carneiro]

To add to what @Kevin Buzzard said, I think mathematicians want more than simple consistency from their axiom systems, they really want a sensible semantic interpretation of the theory, otherwise how can you say you have proved e.g. brouwer's fixed point theorem and not some bastardized version of it?

[Arthur Adjedj]

I mean, do you believe that Brouwer's fixed point proof in lean translates exactly to the usual ZFC one when embedding the proof though Lean's model ?

[Mario Carneiro]

the proof, maybe not, but the statement yes

[Mario Carneiro]

the lean real numbers embed to exactly the ZFC real numbers (up to isomorphism), and topological spaces, spheres, etc likewise

[Arthur Adjedj]

I can understand why mathematicians like that idea then, it certainly is a desirable property

[Arthur Adjedj]

But again, nothing stops Coq from being given the same exact interpretation as Lean's

[Mario Carneiro]

that would be great if someone could prove it :)

[Arthur Adjedj]

I find it funny to hear coming from the other isle, where Coq "type-theorists" usually doubt Lean's soundness (though mostly in regards to its implementation, not its theory)

[Mario Carneiro]

I think there are reasonable reasons to doubt Lean's implementation correctness, having mostly to do with the fact that it is younger and has a much smaller team behind it

[Henrik Böving]

They do? The only thing I hear from Coq people is that they don't like the fact that Lean does not always have subject reduction but that is not soundness.

[Mario Carneiro]

still, we can at least say that there are no known soundness bugs (which hopefully all major ITPs should also be able to claim)

[Henrik Böving]

Mario Carneiro said:

still, we can at least say that there are no known soundness bugs (which hopefully all major ITPs should also be able to claim)

*that we didn't fix^^

[Arthur Adjedj]

(all except Agda)

[Mario Carneiro]

(and Mizar)