## Stream: new members

### Topic: How can I get even to resolve to true

#### Lars Ericson (Nov 29 2020 at 17:47):

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 (Nov 29 2020 at 17:49):

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 (Nov 29 2020 at 17:49):

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 (Nov 29 2020 at 17:50):

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

#### Eric Wieser (Nov 29 2020 at 17:50):

But don't we have decidable_pred even?

#### Mario Carneiro (Nov 29 2020 at 17:50):

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 (Nov 29 2020 at 17:51):

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

#### Eric Wieser (Nov 29 2020 at 17:51):

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

#### Mario Carneiro (Nov 29 2020 at 17:51):

which should evaluate to tt

#### Eric Wieser (Nov 29 2020 at 17:52):

Where is to_bool?

#### Mario Carneiro (Nov 29 2020 at 17:53):

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 (Nov 29 2020 at 17:53):

to_bool is in core

#### Mario Carneiro (Nov 29 2020 at 17:53):

src#decidable.to_bool

#### Eric Wieser (Nov 29 2020 at 17:54):

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 (Nov 29 2020 at 17:54):

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

#### Mario Carneiro (Nov 29 2020 at 17:55):

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

#### Mario Carneiro (Nov 29 2020 at 17:55):

it is used for some and none as well

#### Mario Carneiro (Nov 29 2020 at 17:56):

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

#### Lars Ericson (Nov 29 2020 at 17:56):

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 (Nov 29 2020 at 17:57):

with the resulting implementation being provably correct in some sense

eh, that's not on the agenda

#### Mario Carneiro (Nov 29 2020 at 17:57):

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 (Nov 29 2020 at 17:58):

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

#### Mario Carneiro (Nov 29 2020 at 17:58):

the real meat is src#nat.even.decidable_pred

#### Lars Ericson (Nov 29 2020 at 17:59):

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

#### Marc Huisinga (Nov 29 2020 at 18:01):

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

#### Mario Carneiro (Nov 29 2020 at 18:03):

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 (Nov 29 2020 at 18:40):

@Mario Carneiro it's a possible application.

#### Mario Carneiro (Nov 29 2020 at 18:40):

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

#### Reid Barton (Nov 29 2020 at 18:41):

In any case, it's certainly not required

#### Reid Barton (Nov 29 2020 at 18:42):

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

#### Lars Ericson (Nov 29 2020 at 18:46):

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 (Nov 29 2020 at 19:11):

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 (Nov 29 2020 at 19:11):

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 (Nov 29 2020 at 22:27):

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

Last updated: May 18 2021 at 16:25 UTC