How can I get even to resolve to true

Stream: new members

[Lars Ericson]

The following expressions do not resolve down to true:

import data.nat.basic

#check even 2 -- results in "even 2 : Prop"
#reduce even 2 -- results in "∃ (k : ℕ), 2 = 2.mul k"
#eval even 2 -- results in "result type does not have an instance of type class 'has_repr', dumping internal representation, eval result #0"

What needs to be changed in the definition of even so that #eval will produce true? Or is there another # command which will produce true from even 2?

The definition of even is

def even (a : α) : Prop := ∃ k, a = 2*k

[Kevin Buzzard]

even 2 will not reduce to true because you need to input an idea, namely a value of k such that 2 = 2 * k (plus a proof that 2 = 2 * k for your choice of k).

[Mario Carneiro]

It is a proposition, it doesn't come with an algorithm to evaluate it on its own, and it is not definitionally equal to true

[Kevin Buzzard]

If we had algorithms which could figure out which propositions were true, we'd have something which contradicted Goedel's theorem.

[Eric Wieser]

But don't we have decidable_pred even?

[Mario Carneiro]

however, lean does have a mechanism for associating algorithms to propositions to decide them, and since you found this in mathlib I will wager it already exists

[Mario Carneiro]

to use it, try #eval to_bool (even 2)

[Eric Wieser]

docs#nat.even.decidable_pred (which I guess is found by docs#decidable.to_bool)

[Mario Carneiro]

which should evaluate to tt

[Eric Wieser]

Where is to_bool?

[Mario Carneiro]

a more common way to exploit this decidability algorithm is something like example : even 2 := dec_trivial, where we don't prove it is equal to true per se but rather that it is provable

[Mario Carneiro]

to_bool is in core

[Mario Carneiro]

src#decidable.to_bool

[Eric Wieser]

Looks like doc-gen can't find things exported from other namespaces - I assume decidable.to_bool is re-exported as to_bool somewhere?

[Mario Carneiro]

https://github.com/leanprover-community/lean/blob/ed6accfb611bbd28ef5b7e34361d2b58a366e2c9/library/init/logic.lean#L606

[Mario Carneiro]

export is used very rarely, but it's basically a permanent open for everybody

[Mario Carneiro]

it is used for some and none as well

[Mario Carneiro]

fun fact: every olean file starts with a list of every export that has been done by any upstream file

[Lars Ericson]

Thanks. I'm trying to get a sense of the bridge in Lean from theorem proving to "correct programming", that is, starting with a specification like

def even (a : α) : Prop := ∃ k, a = 2*k

and elaborating it into an algorithm. So the answer is to look at decidable.to_bool.

Since one of the goals of the Lean project is to program Lean in Lean, with the resulting implementation being provably correct in some sense, this transition from specification to algorithm has to happen when you have Lean in Lean.

[Mario Carneiro]

with the resulting implementation being provably correct in some sense

eh, that's not on the agenda

[Mario Carneiro]

I would be very happy if that were the case but I don't think lean 4 will make much of an attempt in this direction

[Mario Carneiro]

decidable.to_bool is a boring function, it won't tell you much

[Mario Carneiro]

the real meat is src#nat.even.decidable_pred

[Lars Ericson]

Thanks @Mario Carneiro I guess that was just a nice-to-have from @Sebastian Ullrich .

[Marc Huisinga]

@Lars Ericson where does that mention proving the correctness of lean 4?

[Mario Carneiro]

I will say that writing a verifier that can prove its own implementation correctness is the stated goal of the MM0 project, but it's not lean, that would be way too hard mode

[Lars Ericson]

@Mario Carneiro it's a possible application.

[Mario Carneiro]

yes it's possible, anything is possible, but it's not designed to be feasible

[Reid Barton]

In any case, it's certainly not required

[Reid Barton]

Lean lets you write both algorithms and specifications, and you can have either one without the other, or both together

[Lars Ericson]

Developing correct programs by correctly elaborating specifications is a goal. The link I gave to is to doing that is for Coq, but Lean is not too far from Coq. I guess you have to assume the correctness of the verifier, if it is not feasible to verify the verifier in other than an informal sense.

Certainly it is the case that decision procedures for many sublanguages of logic are intractable. That doesn't stop people from wanting to try. For example, Microsoft managers in funding Lean may have this objective in mind.

[Mario Carneiro]

I think you misunderstand. There is no theoretical difficulty, but both lean and coq are gigantic programs that have had years of effort put into them (without concern for verification). Verifying software is much harder than writing it, especially if it wasn't part of the plan originally. It's an engineering problem.

[Mario Carneiro]

Of course you can use lean and coq to verify other programs, particularly toy programs, without too much effort; in a sense that's what they are good at

[Lars Ericson]

Unverified Lean in Lean would still be nice. It's a good way to stress-test the whole language design. You'd have to bootstrap a little from a prior non-pure-Lean version but it should be doable. For example, Haskell is written in Haskell except for the runtime system: https://en.wikipedia.org/wiki/Glasgow_Haskell_Compiler#Architecture