An α → Prop classically equivalent to a computable α → Bool

Stream: new members

[LB]

I'm trying to get rid of Classical in one of my projects in Lean. Not that I have any particular objection against Classical, mind you (I use it recklessly in some of my projects), it's just that this particular project is about concrete manipulation of strings, and Classical in that context just seems, well, strange.

Let's say I have a binary relation R on strings, R : String → String → Prop, or R : String → String → Bool if you prefer. I assume it's computable, by doing a [cR : (a b) → Decidable R a b] in all the theorems I prove. I also assume (via other typeclasses) that R satisfies certain properties. All those properties are computable, assuming that R is computable/decidable. Actually they can all be reduced to inductive properties (only) using ite's and no fancy termination_by 's.

I then build some (R dependent) binary operator, still using only ite's, then I proceed to develop a small theory based on the associativity of this operator. That theory, as it's actually written in Lean, needs em (R a b), and only em (R a b) (an only to do case analysis on the ite's I started with), in addition to some dependency to propext (which I certainly won't try to remove).

Now let's say that I define two particular instances of R, R1 and R2, for both of which I'm able to prove the required properties and apply the theory, except that:

• R1 is computable, which means that all the development (checking the required properties, apply the theory) goes smoothly without using Classical at all
• R2 "isn't" (but you will soon see why I put quotes around "isn't") ; hence for this particular case I'm forced to assume Decidable (R2 a b), essentially to force Lean to accept my constructive definitions by ite's and my proofs by em's.

And ........ after a (rather large) bit of work using the theory I built, I end up proving that R1 = R2.

This proves (Classically) that R2 is computable, and meta-justifies the Decidable (R2 a b) I started with.

When I think of that, I realize that this is not the first time I'm faced with such a strange construct. It reminded me of nonstandard analysis, in which any "standard" ZF statement, when proved using nonstandard axioms, is still a valid statement in ZF.

Robinson proves this using models, but Nelson doesn't, if I remember correctly: he does this by reasoning directly on the statements. Maybe his reasoning can be formalized in Lean, and maybe not using Classical? I don't really know (I don't think so, I think he uses Zorn at some point to create a suitable ultrafilter). Anyway, that was just an analogy, irrelevant to my own problem.

All this prompts this question:

Is it possible to conclude (constructively) that R2 is computable?

Here is another way of saying this. Does there exist a theory, somewhere, that proves that any classical proof of the fact that R2 = R1 where R1 is (unconditionally) computable can be turned into a constructive proof of that same fact?

Of course, as the statement is correct, it would certainly be feasible to modify the proof to make it constructive. But in its current form, the proof uses heavily the associativity of the operator in multiple computations, each of one would be cumbersome to convert...

[Edward van de Meent]

concretely, would this be a correct summation?

opaque a:Type
opaque R1 : a → a → Prop


opaque R2 : a → a → Prop

instance instDecidableR1 : DecidableRel R1 := sorry

def foo [DecidableRel R2] : R1 = R2 := sorry

def instDecidableR2 : DecidableRel R2 := by
  sorry -- insert proof here


#print axioms instDecidableR2 -- no use of Choice here.

[LB]

Yes and no.

Yes, for summarizing the general context.

No, because my use case of Classical is specifically reduced to using em to do case analysis on ite's that are in the definitions.

I can't hope for the general result. I may hope for the restricted result.

[Edward van de Meent]

right... so rather than [Decidablerel R2], it'd be something like (h: ∀ p:Prop, p ∨ ¬ p)?

[LB]

No, it would be:

(h: ∀ a b: String, R2 a b ∨ ¬(R2 a b))

but even that can be restricted to a few very targeted applications.

Edit. I was not sure you can do ite's on a relation that just has em, and not the full Decidable property. I checked in VSCode: Lean doesn't accept the definition.

[Edward van de Meent]

right... i don't think there are tools for this... might i ask what precisely your use case is?

[LB]

Sure. I am in the process of formalizing a proof of results about look-and-say sequences.

[LB]

Having Classical in axioms wouldn't bother me at all. It's just that I was finding that particular stuff interesting...

[Edward van de Meent]

what specifically are the definitions of R1 and R2?

[LB]

def R1 (L M: List Nat) := L ≠ [] ∧ M ≠ [] ∧ ∀ (n: Fin 48), iterate ϕ n (L ++ M) = iterate ϕ n L ++ iterate ϕ n M

def R2 (L M: List Nat) := L ≠ [] ∧ M ≠ [] ∧ ∀ n, iterate ϕ n (L ++ M) = iterate ϕ n L ++ iterate ϕ n M

where ϕ is the look-and-say operator, and iterate is what you think it is

[Edward van de Meent]

i'm guessing the trouble is proving

(∀ (n: Fin 48), iterate ϕ n (L ++ M) = iterate ϕ n L ++ iterate ϕ n M) -> ∀ n, iterate ϕ n (L ++ M) = iterate ϕ n L ++ iterate ϕ n M

?

[LB]

No real bother once you have proved the main (Conway's) result.

I don't really need the result, it's just that when I finally put the draft on paper, I noticed the strange phenomenon I talked about in my OP. And thought that if there was a way to meta-reason about the proof, it would rid me of Classical magically...

48 is just what I had in mind (as I said, I'm not focused on that part), but I guess 25 would work as well (but probably not 24).

[Robert Maxton]

I'm pretty sure the answer to this is no in general, because Godel. The statement "R2 is computable" is a true statement in Lean's computable subset, but that doesn't necessarily mean that it can be proved true within Lean's computable subset. It might be, but there can't be a theorem that makes it true always, because Lean's computable subset is still stronger than Peano arithmetic.

[LB]

Not sure I follow you. "R2 is computable" isn't just any true statement in Lean's computable subset, it's a classically provable statement in Lean's computable subset.

When you use the word "true", you admit that it is equal to "R1 is computable" (whatever your reasons for that). By admitting it, you admit by the same process that it is computably true, as "R1 is computable" is computably true.

Could you please reformulate without using the word "true"?

[LB]

My analogy with nonstandard analysis wasn't just fortuitous. Nelson proves (using some ZFC as a meta-tool) that for any proof in IST of a standard statement, there is a proof in ZF.

[Giacomo Stevanato]

AFAIK there is a way for extracting constructive proofs from _some_ kind of classical proofs that use non-computable axioms like LEM. It basically boils down to proving your statement under a limited double-negation monad that would let you extract the result in the end. You can find an example of its use here (it's in Agda however). Unfortunately I don't remember the proper name of this technique.

[LB]

Yes!! That (the double negation) was exactly the direction I was thinking about! Thank you for this pointer, I'll follow your link with eagerness. Thanks!

[Luigi Massacci]

If I'm not mistaken, the stuff you should be googling is "realizability"

[LB]

@Luigi Massacci I gave it a look and what I saw is either too broad or too technical for me to find a hint about my specific problem. But yes, it seems to be the right direction. I'll try again later. Thank you!

[Robert Maxton]

LB said:

Not sure I follow you. "R2 is computable" isn't just any true statement in Lean's computable subset, it's a classically provable statement in Lean's computable subset.

When you use the word "true", you admit that it is equal to "R1 is computable" (whatever your reasons for that). By admitting it, you admit by the same process that it is computably true, as "R1 is computable" is computably true.

Could you please reformulate without using the word "true"?

Sure. The computable subset of Lean is a set of axioms, including several induction/type recognition axiom schema. open Classical (or using theorems or noncomputable) adds a number of additional axioms, including at least one stronger induction/recognition schema. "R2 = R1" is a statement that can be proved using the latter (stronger) axiom schema, but may be independent of the former. As a result, "R2 is computable" may not in fact be in Lean's computable subset at all.

To say something is computable is to say that there exists an algorithm for computing it. But a classical proof of that statement may not be constructive -- it may not actually provide the algorithm, in which case there is no general way of automatically converting that classical proof into a computable one. Alternatively, it might provide an algorithm with no computable proof of correctness; this case is essentially Godel's second theorem. Proving existence, exhibiting a concrete object, and recognizing a satisfactory object are all distinct problems.

[Daniel Weber]

Edward van de Meent said:

concretely, would this be a correct summation?

opaque a:Type
opaque R1 : a → a → Prop


opaque R2 : a → a → Prop

instance instDecidableR1 : DecidableRel R1 := sorry

def foo [DecidableRel R2] : R1 = R2 := sorry

def instDecidableR2 : DecidableRel R2 := by
  sorry -- insert proof here


#print axioms instDecidableR2 -- no use of Choice here.

Here's a specific example where it can't be done:

opaque a : Prop

#synth Decidable True

theorem foo [Decidable (a ∨ ¬ a)] : (a ∨ ¬ a) = True := by
  apply eq_true
  apply Decidable.of_not_not
  exact not_not_em a

#print axioms foo