Zulip Chat Archive

Stream: new members

Topic: How can I get even to resolve to true


view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Nov 29 2020 at 17:50):

But don't we have decidable_pred even?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 29 2020 at 17:51):

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

view this post on Zulip Eric Wieser (Nov 29 2020 at 17:51):

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

view this post on Zulip Mario Carneiro (Nov 29 2020 at 17:51):

which should evaluate to tt

view this post on Zulip Eric Wieser (Nov 29 2020 at 17:52):

Where is to_bool?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 29 2020 at 17:53):

to_bool is in core

view this post on Zulip Mario Carneiro (Nov 29 2020 at 17:53):

src#decidable.to_bool

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Nov 29 2020 at 17:54):

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

view this post on Zulip Mario Carneiro (Nov 29 2020 at 17:55):

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

view this post on Zulip Mario Carneiro (Nov 29 2020 at 17:55):

it is used for some and none as well

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 29 2020 at 17:58):

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

view this post on Zulip Mario Carneiro (Nov 29 2020 at 17:58):

the real meat is src#nat.even.decidable_pred

view this post on Zulip Lars Ericson (Nov 29 2020 at 17:59):

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

view this post on Zulip Marc Huisinga (Nov 29 2020 at 18:01):

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

view this post on Zulip 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

view this post on Zulip Lars Ericson (Nov 29 2020 at 18:40):

@Mario Carneiro it's a possible application.

view this post on Zulip Mario Carneiro (Nov 29 2020 at 18:40):

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

view this post on Zulip Reid Barton (Nov 29 2020 at 18:41):

In any case, it's certainly not required

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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