Batteries and LEM

Stream: batteries

[Mukesh Tiwari]

@Mario Carneiro Apologises for the orthogonal question but I am wondering how is it going to different from Mathlib? Is it going to be a self contained library that comes with Lean without excluded middle?

[Shreyas Srinivas]

Highly doubt that. Lean's core tactics liberally use LEM.

[Shreyas Srinivas]

And lean core has discouraged PRs which make tactic changes to cater to constructive logic.

[Shreyas Srinivas]

Batteries is still built on top of this core. This library is meant to be an extended version of the standard library, with useful programming utilities

[Mukesh Tiwari]

Shreyas Srinivas said:

Highly doubt that. Lean's core tactics liberally use LEM.

Interesting; I was not aware of this. Can you point me towards the theorem in Lean’s core library that uses LEM? I was under the impression that it’s just Mathlib.

[Mario Carneiro]

Core takes stuff from mathlib all the time

[Mario Carneiro]

I'm personally still committed to supporting constructive logic in lean but there's only so much I can do if upstream doesn't play ball

[Mukesh Tiwari]

One more thing: imagine I am formalising something in Lean but want to avoid the proofs and constructions that used LEM because in the end I want to compute. How can I keep track that I am not using LEM? (In Coq, it’s Print Assumptions so something similar to this Lean)

[Henrik Böving]

There is #print axioms. But you can still do computation with code that merely used LEM for a proof. It only gets difficult if you want to reduce proofs or run code that actually uses LEM as a decision procedure.

[Notification Bot]

9 messages were moved here from #batteries > Welcome New Batteries Maintainers! by Kyle Miller.

[Mukesh Tiwari]

Henrik Böving said:

There is #print axioms. But you can still do computation with code that merely used LEM for a proof. It only gets difficult if you want to reduce proofs or run code that actually uses LEM as a decision procedure.

Now I am slightly confused. Imagine I wrote a program in tactic mode and somewhere I sneaked LEM then you cannot turn it into a runtime code; can you?

[Kyle Miller]

in the end I want to compute

In Lean there are a couple notations of computing (reduction or #eval). It's possible to use LEM/choice and still get executable programs (via #eval or compilation), so long as it's not being used to make decisions when constructing concrete data. Definitions that can't be #eval'd need to be marked noncomputable, and if it's not noncomputable you can #eval it.

[Kyle Miller]

If you make a definition using tactics, and one of the tactics sneaks in choice, then that can make the definition fail to be computable in this #eval sense, and Lean would require you to mark the definition noncomputable.

[Mukesh Tiwari]

Kyle Miller said:

If you make a definition using tactics, and one of the tactics sneaks in choice, then that can make the definition fail to be computable in this #eval sense, and Lean would require you to mark the definition noncomputable.

Awesome; this is what I was looking for :) Now how to avoid those tactics? After each tactic, I should use print axiom or is there a better way than this?

[Kyle Miller]

Usually people don't use tactics to create definitions. Instead, they write the definition using "normal" functional programming, and embed tactic proofs where they are needed.

[Kyle Miller]

There's no problem for computability to have one of these embedded tactic proofs depend on choice/LEM, so #print axioms would be too conservative.

[Kyle Miller]

I don't mean to say that you definitely shouldn't use tactics to create definitions, but you can run into accidental noncomputability this way for example.

It's also easy to make non-reducing terms using tactics (if you use rw or simp for example), which can matter if you're trying to make reducible Decidable instances.

[Mukesh Tiwari]

Thanks @Kyle Miller ! Basically the idea is write the definition without tactics and then prove things using tactics, which possibly involve LEM.

[Mario Carneiro]

Actually LEM basically never blocks computation, because it is computationally irrelevant

[Kyle Miller]

By the way, it's definitely possible to make evaluatable functions using tactics. The tactic by_cases can introduce choice, but it doesn't always. For example, the following turns out to be fine:

def fact (n : Nat) : Nat := by
  by_cases n = 0
  exact 1
  exact n * fact (n - 1)

It's possible to use if directly to prevent choice from ever being possible:

def fact (n : Nat) : Nat := by
  refine if n = 0 then ?_ else ?_
  exact 1
  exact n * fact (n - 1)

Here's an example where by_cases introduces choice:

def allTrue (p : Nat → Bool) : Bool := by
  by_cases ∀ n, p n
  · exact true
  · exact false
/-
failed to compile definition, consider marking it as 'noncomputable' because it depends on
'Classical.propDecidable', and it does not have executable code
-/

Using refine if ... directly gives the immediate error:

def allTrue (p : Nat → Bool) : Bool := by
  refine if ∀ n, p n then ?_ else ?_
  /-
  failed to synthesize
    Decidable (∀ (n : Nat), p n = true)
  -/

[Mario Carneiro]

you need some of the stronger forms of LEM based on the axiom of choice to get something noncomputable in the generating-code sense

[Kyle Miller]

(I was using LEM as shorthand for "classical instances", but yes)

[Mukesh Tiwari]

And ‘by_cases’ lives in Lean core or some outside library? (I don’t see a way to encode allTrue in Coq ; I mean it is not possible constructively so Lean rejects it rightly so)

[Eric Wieser]

by_cases is part of core, but usually if you are building data you would use if h : P then _ else _ anyway

[Kyle Miller]

This isn't the cleanest example, but I think it is kind of neat, since it demonstrates that you can use choice to construct a definition that you can compute with. It's using the fact that every iteration of the loop makes H.choose - n smaller. I imagine it can be simplified. (And also, it doesn't need choice; mathlib has docs#Nat.find, which doesn't depend on any axioms.)

def find {p : ℕ → Bool} (H : ∃ n, p n) : ℕ :=
  go H 0 (by simp)
where
  go (H : ∃ n, p n) (n : ℕ) (H' : ∀ n' < n, ¬ p n') : ℕ :=
    if h : p n then
      n
    else
      go H (n + 1) <| by
        intro n' hn'
        obtain hn' | rfl := Nat.lt_or_eq_of_le (Nat.le_of_lt_succ hn')
        · exact H' n' hn'
        · exact h
  termination_by H.choose - n
  decreasing_by
    simp_wf
    have : n < H.choose := by
      by_contra hH
      simp at hH
      obtain hH | rfl := lt_or_eq_of_le hH
      · exact absurd H.choose_spec (H' _ hH)
      · exact absurd H.choose_spec h
    omega

[Mukesh Tiwari]

Yep; you may also want to have a look at Constructive Epsilon library (https://coq.inria.fr/doc/v8.20/stdlib/Coq.Logic.ConstructiveEpsilon.html). From programming perspective, all it is a linear search and it is bound to succeed because of H.

[François G. Dorais]

Kyle is on the right track. The most general case of this is Markov's Principle:

axiom MP (p : Nat → Bool) (h : ¬∀ n, p n = false) : {n : Nat // p n = true}

This axiom is not valid in intuitionistic constructive logic. This axiom basically says that classical logic is sound to prove termination of programs. The so-called Russian school of constructivism accepts MP as true, hence the name. Merely assuming LEM for Prop in Lean, allows one to prove MP as a theorem. Lean allows LEM arguments to be tucked into termination proofs without much fuss, so it is quite plausible that one could prove MP in Lean without any obvious red flags.

[Kim Morrison]

import Mathlib

def MP (p : Nat → Bool) (h : ¬∀ n, p n = false) : {n : Nat // p n = true} := by
  simp at h
  exact ⟨Nat.find h, Nat.find_spec h⟩

Am I missing something? :woman_shrugging:

[Yakov Pechersky]

I think what Francois is saying is that while that has constructed an expression that looks like a closed term, there are no guarantees that/when MP p will terminate for arbitrary p when actually executed

[Kim Morrison]

Sure it will. :-) That's what h says.

[François G. Dorais]

#print axioms MP

[François G. Dorais]

simp counts as a red flag.

[François G. Dorais]

Using Kyle's idea, I think it's perhaps possible to hide all the uses of LEM in the termination arguments.

[Kim Morrison]

I remain mystified by the idea that this is an interesting distinction. :-)

I don't really see how you would do it, in any case. WellFounded.fix can see the quantity you're saying is decreasing, and surely the choice has to happen then.

[François G. Dorais]

I'm not saying that Lean can prove MP without using any axioms! I'm saying that it can conceal them so that it looks like it's not using any axioms even after reasonable inspection. The following is a bit more concealed but the simp_all does raise my eyebrow.

import Mathlib

def MP (p : Nat → Bool) (h : ¬ ∀ n, p n = false) : {n : Nat // p n = true} :=
  go h 0
where
  go (h : ¬ ∀ n, p n = false) (n : Nat) :=
    match hn : p n with
    | true => ⟨n, hn⟩
    | false => go h (n+1)
termination_by Nat.find (p := (p ·)) (by simp_all) - n
decreasing_by sorry -- it's too late here to finish...

[François G. Dorais]

Ideally, the decreasing_by argument would be automatically generated and would hide the actual use of classical reasoning.

[Kim Morrison]

Surely #print axioms is the only meaningful sense of "reasonable inspection"?

[François G. Dorais]

Not really. Lean has a habit of using Classical.choice even when it's not needed, so #print axioms is not a reliable tool. In the case of MP, I know that no proof can get by with no axioms (or even just propext and Quot.sound). For a general theorem where I don't know that, the fact that #print axioms shows Classical.choice wouldn't tell me much and I would rely on old fashioned visual inspection.

[Kim Morrison]

I would say #print axioms is perfectly reliable, it's Lean you have a problem with. :-)

[François G. Dorais]

Well, I don't have a problem with Lean. But yes, anyone using Lean for constructive reasoning is misguided. This is to illustrate that the issues run really deep and "fixing" Lean for constructive reasoning is not possible in an add-on library.

[Mukesh Tiwari]

François G. Dorais said:

But yes, anyone using Lean for constructive reasoning is misguided. This is to illustrate that the issues run really deep and "fixing" Lean for constructive reasoning is not possible in an add-on library.

I am not a type theorist but I believe the underlying logic of Lean is CIC, same as Coq but with some caveats such as proof irrelevance. So I don’t understand why you need to fix Lean for constructive reasoning.

[Henrik Böving]

You don't need to fix Lean the type theory but lots of things that ordinary Lean users use for every day tasks make use of LEM/choice/etc. under the hood and you'd have to change that. It was determined in previous discussions that the Lean core developers don't want such a change.

[Ruben Van de Velde]

Or at least want to see some strong arguments to put in the work

[Mukesh Tiwari]

Henrik Böving said:

You don't need to fix Lean the type theory but lots of things that ordinary Lean users use for every day tasks make use of LEM/choice/etc. under the hood and you'd have to change that. It was determined in previous discussions that the Lean core developers don't want such a change.

This is fine but it is completely different from fixing Lean. I may choose not to use any of those libraries or just use the constructive ones. The only surprise to me is ‘by_cases’ living in core but I get the idea: write the computable part in functional programming style and do the proofs using tactics.

[Mukesh Tiwari]

Ruben Van de Velde said:

Or at least want to see some strong arguments to put in the work

There is already an excellent library Mathlib that provides reasoning support for mathematics, it would be nice to have one such constructive library for programming as well :)

[Ruben Van de Velde]

The practical problem is that "any of those libraries" includes the core library shipped with lean, including (AIUI) tactics like split and simp

[François G. Dorais]

Mukesh Tiwari said:

write the computable part in functional programming style and do the proofs using tactics.

It's a bit more complicated than that. Warning: I'm about to put my proof-theorist hat on and explain things in excessive detail!

There are several flavors of constructive reasoning. What you're proposing is often called recursive constructive reasoning (which follows Markov). Other flavors are intuitionistic constructive reasoning (which follows Brouwer) and Bishop's constructive reasoning (which is closest to CIC). The key difference between recursive constructive reasoning and the others is that it uses a classical meta-theory. This means that in recursive constructivism, Markov's principle from above is simply true because there is no logical distinction between ∃ n : Nat, p n and ¬ ∀ n : Nat, ¬ p n when p is a decidable predicate. In Bishop constructivism, hence in CIC, there is a distinction and Markov's principle is not a theorem, only Nat.find is.

The difference is subtle but it is consequential. In Bishop constructivism, a proof of ∃ n : Nat, p n must actually construct n, we can extract an actual algorithm from the proof. This is called proof mining. This means that when we prove that a definition is total in CIC, we can extract a run time bound from the proof.

This is not so in recursive constructivism. Proof mining doesn't work directly for classical logic. A classical proof of ∃ n : Nat, p n only gives a constructive proof of ¬ ∀ n : Nat, ¬ p n: if you search through Nat it's impossible you won't find an n such that p n. This is enough to convince me that n exists but it doesn't give much information at all about n. When you prove that a function is total this way, the only run time bound you get is the trivial bound: run it and see how long it takes.

Lean, with all its current bells and whistles, is perfectly sound for recursive constructive reasoning. Any function that is not marked noncomputable is total and the proof term given by Lean will convince any recursive constructivist. If #print axioms shows nothing for that proof term, then this is a plain CIC proof and you can mine a useful run time bound for the function. Otherwise, you can try to coax Lean into giving a better proof term but that's probably a lot of extra work and there is no guarantee you will succeed.

[Eric Wieser]

Yakov Pechersky said:

there are no guarantees that/when MP p will terminate for arbitrary p when actually executed

Is there a good resource somewhere about what it means to say "an algorithm only terminates if you assume LEM"?

[Eric Wieser]

"actually executed" also raises questions like the non-verified status of Lean's compiler and interpreter, or pragmatic limitations on runtime making eventual termination irrelevant.

[Eric Wieser]

Ruben Van de Velde said:

The practical problem is that "any of those libraries" includes the core library shipped with lean, including (AIUI) tactics like split and simp

Such a library could ship with elab "simp" => an_exact_copy_of_the_simp_code_without_choice

[Eric Wieser]

At once point there was discussion about Batteries doing this around lean4#2414, but it was deemed to cause too much fragmentation

[Eric Wieser]

(hey, that issue is now fixed!)

[Eric Wieser]

Ruben Van de Velde said:

The practical problem is that "any of those libraries" includes the core library shipped with lean, including (AIUI) tactics like split and simp

So actually I think this no longer holds

[Eric Wieser]

Ruben Van de Velde said:

The practical problem is that "any of those libraries" includes the core library shipped with lean, including (AIUI) tactics like split and simp

So actually I think this no longer holds

[Mario Carneiro]

the issue with split is fixed, but the issue with core's posture toward similar PRs is seemingly not, so I'm not sure whether I want to try looking again for eliminable uses of choice just to start another fight

[Mukesh Tiwari]

François G. Dorais said:

Otherwise, you can try to coax Lean into giving a better proof term but that's probably a lot of extra work and there is no guarantee you will succeed.

By this, you mean figuring out all the machinery and tactics that does not use classical stuff and then use them to write the proof?

Thanks for the elaborate answer. One of my colleagues Ulrich Berger at Swansea also has slightly different view on constructivism. His argument is to not use any classical stuff in a construction if we care about it and want to run on a computer, but happy to use LEM and all sort of classical stuff in proof if it is computationally irrelevant. And I should say I am not against it as long as I get the code that I care about :)

[François G. Dorais]

Yes, that's what I mean.

[François G. Dorais]

Eric Wieser said:

Is there a good resource somewhere about what it means to say "an algorithm only terminates if you assume LEM"?

There are several semantics for intuitionistic logic. The most accessible is probably Kripke Semantics.

The basic idea is that you have several "worlds" that are partially ordered by the "later" relation. Later worlds always have more knowledge: once you know something you can never forget it. Given this there is a standard way to interpret False, ∧, ∨, →, ∀, ∃, etc. This interpretation always satisfies intuitionistic logic but not always LEM.

For example, the Kripke interpretation of ∃ n : Nat, p n is: in the current world (and hence all future world) there exists a natural number n such that p n is true. The Kripke interpretation of ¬ ∀ n : Nat, ¬ p nis: in every future world there is a later world in which there exists a natural number n such that p n is true. These are clearly different: in the second case you don't necessarily have much information about n but in the first you definitely know what n is.

Using Kripke semantics, a statement "foo is true assuming LEM" means that in every Kripke model, if the model satisfies LEM then it also satisfies foo.

PS: The Kripke models for LEM are up to a specific notion of equivalence those with only one world. These one-world models are identical to the usual Tarski semantics for classical logic.

[Kyle Miller]

François G. Dorais said:

The difference is subtle but it is consequential. In Bishop constructivism, a proof of ∃ n : Nat, p n must actually construct n, we can extract an actual algorithm from the proof. This is called proof mining. This means that when we prove that a definition is total in CIC, we can extract a run time bound from the proof.

Something I've wondered is why worry too much about whether the proofs themselves have extractable data if instead, when you know you have a good algorithm, you can construct a term of {n : Nat // p n}? This is like how pure mathematicians operate (at least in my milieu of 3-manifold topology). Step 1: prove mere existence. Step 2: create an algorithm. Step 3: create an efficient algorithm.

François G. Dorais said:

Any function that is not marked noncomputable is total

Just for a point of information, noncomputable is independent of being total as far as Lean is concerned. Non-total functions are marked partial. Given the rest of the sentence maybe you mean that recursive constructivists need no noncomputable to be happy, but it's a bit ambiguous so I figured I'd mention it.

Eric Wieser said:

(hey, that issue is now fixed!)

Yes, core likes to see concrete applications. The lean4#4313 showed that tactics couldn't be used to construct some data, but lean4#2414 doesn't have a concrete application (or at least core doesn't see avoiding axioms in propositions to be an application). I'm not saying we should expect much progress in this direction, but something like Mario's example of def foo : Nat := by by_cases 2 + 2 = 4 <;> exact 1 in the issue discussion could be an issue on its own (something less artificial though; I think it's more likely to see split in definition automation, so that's now satisfied, and for those who care about creating definitions, there's always refine if h : 2 + 2 = 4 then ?_ else ?_ as an easy workaround).

[Eric Wieser]

I'm particularly pleased because I was sure precisely that circumstance would justify the non-classical split, but I wasn't able to work out the test case to demo it myself!

[François G. Dorais]

Kyle Miller said:

François G. Dorais said:

Any function that is not marked noncomputable is total

Just for a point of information, noncomputable is independent of being total as far as Lean is concerned. Non-total functions are marked partial. Given the rest of the sentence maybe you mean that recursive constructivists need no noncomputable to be happy, but it's a bit ambiguous so I figured I'd mention it.

Yes, thanks for clarifying! I did mean noncomputable though. What the kernel sees is what matters in this context: proofs are only relevant to the kernel, they're ignored by the compiler. As far as the kernel, partial functions are actually total, they're essentially constant functions with value default with a bit of extra sauce to prevent the kernel from using the specific value of default.

Not noncomputable is required to ensure that the function term doesn't use Classical.choice or other noncomputable axioms. Some constructivists, namely Bishop, may oppose Quot.sound and propext as well but that's another story.

[Kyle Miller]

I'm not sure I understand what you mean regarding noncomputable and partiality then.

Both noncomputable and partial/opaque declarations suffer the same problem from the perspective of the kernel — neither will fully reduce on all inputs, so you could say that these are both partial functions. However, even functions not marked with either can fail to reduce. So, if you're talking about reduction, it's not the case that no noncomputable means total in the reduction sense.

If we're talking about totality in the mathematical sense of whether the supplied equations for a declaration determine a total function, then noncomputable definitions are total, but partial functions are not. The implementation detail that partial functions are added to the environment as opaque declarations doesn't matter for this.

---

In early Lean, the noncomputability checker did try to determine whether a declaration would reduce for evaluation purposes, but my understanding is that this was abandoned because of how reduction can get stuck on Eq.rec. The solution was creating a separate compilation step where all computationally irrelevant material would be erased. (The reduction check was completely abandoned in Lean 4, and now the noncomputable checker is to try running the compiler.)

Nowadays we also have the simp (config := {ground := true}) evaluator. That evaluates terms and produces an equal (rather than defeq) term, with proof. I haven't had much experience with it to know what it can't do, but it should be at least as capable as reduction. There are probably still non-noncomputable definitions that are not total in this sense. There are also noncomputable definitions that are total in this sense, at least when allowing type parameters to be specialized to certain types. Think for example simp being able to replace an Inf term with Nat.find.

[François G. Dorais]

In the original post you were quoting, this was stated from the perspective of a recursive constructivist. That functions are computable (formerly known as recursive functions, hence the name "recursive constructivist") is essential to a recursive constructivist.

In CIC, all functions are total, so to say that something is total or not is basically meaningless: if you can define it then its total. The role of the kernel in Lean is to check that. To the kernel, axioms like Classical.choice are total and so is every opaque and partial definition. The kernel doesn't care at all about computability.

The compiler is the component of Lean that cares about computability. There is no reasonable code for Classical.choice so any term that involves that axiom is deemed noncomputable. The Lean compiler requires computable functions to rely on no axioms other than propext and Quot.sound (which have a computable interpretation that the compiler knows).

Lean combines both the kernel and the compiler. The codewords opaque and partial are just bridges that allow the two parts to work together where the kernel needs a total function but the compiler wants to run code with no termination proof.

The intersection, definitions that are not marked noncomputable is what a recursive constructivist cares about.

[François G. Dorais]

This slightly humorous table briefly summarizes many of the various sterotypical constructive stances out there that I can think of at the moment.

	Is it total?	Is it computable?
Lean Kernel	It better be!	I don't care
Lean Compiler	I don't care	It better be!
Lean Enthusiast	Obviously	That would be great!
Classical Mathematician	Yeah, why?	Maybe, why?
Recursive Constructivist	Is there a proof?	It better be!
Intuitionistic Constructivist	Here is a counterexample	What do you mean?
Bishop Constructivist	I have a proof!	Here's the code!
Computer Scientist	A proof would be great	What else is there?
Type Theorist	It better be!	In theory
Assembly Programmer	What?	What?

[Kyle Miller]

Ok, I see, I misunderstood your last message, thinking you were implying that noncomputable might still have anything to do with totality, sorry. You're saying "Every function is total, and if it is not noncomputable then it satisfies a recursive constructivist," which makes sense, but you would want to add "not partial" as well, right?

I would say that it's meaningful to ask whether a function declaration is total or not. This is something that the so-called "equation compiler" is responsible for. This is the component between the elaborator and the kernel that consumes the elaborated definition, which consists of some number of equations the function must satisfy, and tries to find a way construct a function term that implements the equations. If the equations determine only a partial function, then this process fails. The other compiler is independent of this, and it consumes the same elaborated definition. The partial modifier disables the equation compiler, and the noncomputable modifier disables the compiler. No matter what the details may be for how partial is represented in the kernel, wouldn't you agree that to satisfy a recursive constructivist you would want neither modifier on a definition?

I personally wouldn't try telling a recursive constructivist that the following is a total function :smile:

partial def allTrue (p : Nat → Bool) : Bool := Id.run do
  let mut i := 0
  while true do
    if p i then
      return true
  return false

The compiler is the component of Lean that cares about computability.

We do care sometimes about computability in other components. For example with the decide tactic we care about kernel reducibility of the Decidable instances. There's native_decide for this if you trust the compiler.

[François G. Dorais]

Agreed. I'm assuming the recursive constructivist is given the same input as the kernel, which excludes the code for the compiler in the case of partial functions.

I think the base issue is: what is trusted? The Lean kernel is implicitly trusted by any user. It would be great to have a trusted Lean compiler but that's not the case right now. Lean programmers are, of course, never to be trusted :-)

For a partial function, the kernel assumes that it is total as an unspecified "axiom". When a programmer writes partial def foo ... the promise to the kernel is that foo's code will always return on any valid input, thereby fulfilling the kernel's assumption. This is not exactly true since panic!, for example, is regularly used in Lean code, but panic! is intended as a bug signal not as an expected outcome. So, a "moral" Lean programmer fully intends to meet that kernel promise and the Lean language is designed to encourage this kind of "moral behavior".

[François G. Dorais]

This discussion is diverging into philosophy. This is not the right place for that but I am happy to keep discussing this topic elsewhere.

Just to be clear: I know a lot about constructivism but I am not a constructivist. I have always been a classical mathematician and moonlighting computer scientist. My goal here was to explain the constructive point of view and its legitimacy, but I am in no way supporting nor defending any kind of militant constructivism. I really hate fights and I will jump out never looking back as soon as I see one forming.

[Kyle Miller]

The thread I've been tugging on here is that noncomputable is not a kernel notion — it's for the definitions just before they're equation compiled and passed to the kernel, so it makes sense talking about functions at that level, and at that level functions can still be partial. There's no existing mechanism for saying that a kernel declaration would be noncomputable or not, and this is a reason why we've been talking past each other somewhat, since I've been working with my understanding of noncomputable-as-it-is.

I think this bit of precision is important. It's possible to write a not-noncomputable function that's partial, yet it's something a constructivist would never accept based on the type alone. The trick here is that it's easy to write a non-total definition that is a "computable" witness for the type.

instance (p : Prop) : Nonempty (Decidable p) := ⟨Classical.dec p⟩

partial def f (p : Prop) : Decidable p := f p

The kernel sees that the opaque definition for f is something involving Classical.choice, but this is not prevented by the lack of noncomputable.

I think my point here is that it doesn't matter that the kernel sees f as being total. What I get from this is that we need to accept not every function is total for the purpose of satisfying recursive constructivists.

[François G. Dorais]

I agree with everything you wrote. Our perspectives are a bit different but we don't really disagree as far as I can tell.

I see a partial def to mean: this is a total function, I promise! You see the actual definition as being somehow important. I don't think it is because, from my perspective, the kernel's response is: Okay, I trust you. But I won't make any assumptions about what the function returns. I will make sure that if the return value has the right type then everything else will check out.

[François G. Dorais]

To home in on our perceived disagreement: the key is where I wrote "I trust you" above. I classify the issue you point out as a trust issue but you don't see it like that. I like your perspective but I have to remove my proof-theorist hat to appreciate it.

[Kyle Miller]

François G. Dorais said:

Lean, with all its current bells and whistles, is perfectly sound for recursive constructive reasoning. Any function that is not marked noncomputable is total and the proof term given by Lean will convince any recursive constructivist.

I've just been trying to make sense of this quote given what you're saying. If we have a function marked partial and not marked noncomputable, will a recursive constructivist be happy with your informal claim that "this is a total function, I promise!"? (Is this what you had in mind when you wrote this earlier?)

I'll grant you that if there were a version of Lean where kernel definitions could be noncomputable, and where this noncomputability check sees through opaque definitions, and where the compiler can successfully compile the output of the equation compiler, then sure, why not, it's all implementable, and the noncomputable marker would be enough. But I hope you understand that I feel like this is a lot to assume without comment!

[Kyle Miller]

I do understand how opaque definitions work in the kernel, and the theoretical relationship between the original definition and the opaque definition. I have no problem with the idea that the definition is dropped once it reaches the kernel or the concept that in the type theory every function is total.

[François G. Dorais]

What the kernel verifies is that this is a valid oracle computation where the opaque and partial functions are considered as oracles. So if you substitute any suitable computable function for the oracles, the compiler will know what to do and result will be a computable function.

[François G. Dorais]

Substituting the computable function is what the compiler and programmer are responsible for. Axioms are different and the compiler/programmer are not expected nor allowed to substitute for them. They remain noncomputable.

[François G. Dorais]

Interestingly, there are oracle programs P[*] where P[f] is total computable whenever the oracle f is total computable but it is not true that P[f] is total whenever f is total. What the Lean kernel checks is the latter. In other words, there can be a real benefit to substituting partial defs with total ones when possible.

[François G. Dorais]

Kyle Miller said:

The kernel sees that the opaque definition for f is something involving Classical.choice, but this is not prevented by the lack of noncomputable.

Once again, you've blown my mind! This basically makes noncomputable meaningless!

partial def choice (α) [Nonempty α] : α := choice α

axiom F : Nat → Nat -- or any `noncomputable` function

instance (x : Nat) : Nonempty { y // y = F x} := ⟨⟨F x, rfl⟩⟩

def f (x : Nat) : Nat := choice { y // y = F x} |>.1

theorem f_eq_F : f = F := funext fun x => choice {y // y = F x} |>.2

This would be fixed if partial required Inhabited instead of Nonempty like in the old days...

When did that change? I remember there was a discussion about that long long ago but I didn't think people were seriously considering this.

[François G. Dorais]

I must have skipped a beat or two...

[Mario Carneiro]

(I agree it's surprising.) It's not meaningless, it differentiates between functions that have no implementation and functions that do have an implementation. Lean could auto-implement all noncomputable functions with looping behavior, but that would be undesirable since it would cause accidental use of them to cause busy looping instead of a useful error message.

[François G. Dorais]

I guess we really do need something like a total keyword. Otherwise it's questionable why we do termination proofs at all.

[Mario Carneiro]

the termination proofs are for the kernel

[Mario Carneiro]

because partial definitions don't satisfy their specification

[François G. Dorais]

Yes, but that puts a lot of pressure on trusting users. We at least need a convenient way to list the partial defs we're trusting in a def (excluding the termination proof).

[Mario Carneiro]

what do you mean by trusting?

[Mario Carneiro]

You can certainly have a #print opaques command, I think I wrote one a while back

[François G. Dorais]

In the sense above. I want my defs to be total computable functions.

[Mario Carneiro]

you gave very many definitions of what that means

[Mario Carneiro]

Most likely the answer will be either that it involves banning some axiom or lean feature being used in the closure of a given statement, in which case it is easy to implement a check for it as in #print axioms, or it's more complicated than that and it's not possible in lean without rewriting the kernel or elaborator

[François G. Dorais]

True, I did! It's funny to think that a def with a termination proof is actually not total.

[François G. Dorais]

Do you mind if I add #print opaques to Batteries?

[François G. Dorais]

(Unless you want to do it yourself, of course!)

[Mario Carneiro]

there is also a @[terminating] attribute later in the same thread, although I'm not sure how to approach the @[terminates] attribute from a library maintenance perspective

[Mario Carneiro]

feel free to PR it

[François G. Dorais]

batteries#966