Zulip Chat Archive

Stream: new members

Topic: Any tactics for evaluating a function fully?


view this post on Zulip Rui Liu (Dec 14 2020 at 23:52):

I have a boolean valued function f, and I want to prove goal f x during tactics mode, how do I evaluate f fully to its boolean value? Note that f might be complicated, so it would be good if it evaluates fast.

view this post on Zulip Yakov Pechersky (Dec 14 2020 at 23:59):

One possibility is

cases h : f x,
{ exact trivial },
{ --show contradiction here,
  sorry }

if I understood correctly

view this post on Zulip Floris van Doorn (Dec 15 2020 at 20:29):

It depends a bit on what you mean. Is x a term without variables? And your goal is ⊢ ↥(f x)? Then exact rfl should be able to compute f x down to either tt or ff and close the goal if it's tt.

view this post on Zulip Floris van Doorn (Dec 15 2020 at 20:29):

If x contains variables (or is a variable) dsimp [f] might help.

view this post on Zulip Rui Liu (Dec 15 2020 at 23:51):

Can I ask what do you mean by variable? Do you mean something defined by let or have? @Floris van Doorn

view this post on Zulip Floris van Doorn (Dec 16 2020 at 00:42):

I mean a local constant, which is a term in your context. So the x and y in the following goal:

x y : bool
 ...

view this post on Zulip Floris van Doorn (Dec 16 2020 at 00:43):

We can be more helpful if you post a small example of what you want. #mwe

view this post on Zulip Rui Liu (Dec 16 2020 at 01:20):

Yes @Floris van Doorn I understand that would be helpful, however I already got some code saved up, so it's a bit hard to distill the essential part of my question.

But if you don't mind downloading my code and play with it, I have attached it. I was trying to prove godel's incompleteness theorem (might be a bit too challenging for a lean beginner....). As part of the proof, I have defined functions to check proof for a formula, see q_proof_for. This function reduces to a boolean. However, I can't get it to reduce to a boolean in tactic mode, which is where I got stuck in the first sorry.

I have tried trivial, refl, and a bunch of simp/dsimp and I couldn't get it to work even when I know that I just need to trivially evaluate it to the boolean result....which is quite frustrating. Also note that this function might be complicated, so maybe better using #eval rather than #reduce to evaluate it?

main.lean

view this post on Zulip Floris van Doorn (Dec 16 2020 at 02:11):

Well, you cannot just evaluate it, since there is an unknown expression w', that depends on some variables

view this post on Zulip Floris van Doorn (Dec 16 2020 at 02:12):

(in the place of the first sorry)

view this post on Zulip Floris van Doorn (Dec 16 2020 at 02:12):

However, you can make progress by doing

dsimp [proof_for, proof, list.reverse_cons, proof_check],
simp,

The first line unfolds the mentioned definitions/let-expressions. The second line simplifies further, reducing some if ... then ... else ... expressions.

view this post on Zulip Floris van Doorn (Dec 16 2020 at 02:17):

However, I recommend that you write some equation lemmas for your definition. For example, I believe that proof axm (prf ++ [tl]) is equal to some other expression involving proof axm prf, which you can proof (it's not true by definition, since (prf ++ [tl]).reverse = tl :: prf.reverse is not true by definition, but it's close. Furthermore, after doing the above reductions, you need to prove simple lemmas like form_eql e e for all e.

view this post on Zulip Floris van Doorn (Dec 16 2020 at 02:18):

Oh wait, I see now that all your variables are specified...

view this post on Zulip Floris van Doorn (Dec 16 2020 at 02:19):

In this case you can do subst h, exact rfl. subst h eliminates the (only meaningful) variable y, and then exact rfl can evaluate the goal to tt.

view this post on Zulip Floris van Doorn (Dec 16 2020 at 02:24):

By the way, did you see Flypitch? In that project @Jesse Michael Han and I formalize the independence of the continuum hypothesis. We also do quite some first-order logic. It might not be directly related to your project (we don't give a decision procedure for proof checking), but it might give some ideas.

view this post on Zulip Rui Liu (Dec 16 2020 at 21:12):

@Floris van Doorn I have just tried replacing the first sorry with subst h, exact refl,. However, it doesn't seem to work and it's complaining at refl with some error message I don't understand.

view this post on Zulip Rui Liu (Dec 16 2020 at 21:22):

Thanks for linking the project! That definitely looks interesting, as I've always wanted to understand how forcing works (metamathematics feels like magic to me :) I got to know lean partly because every time I read about some interesting mathematics, I always feel "I kind of understand". But if I formalize it, then there's no way for me to not understand it. Computer will check the proof for me. It's useful for self study :)

view this post on Zulip Rui Liu (Dec 16 2020 at 21:55):

Just couldn't get it reduce to boolean!!!

view this post on Zulip Mario Carneiro (Dec 16 2020 at 21:56):

it's complaining at refl with some error message I don't understand.

Two suggestions: (1) read the message, all of it, carefully (2) post exact error messages here

view this post on Zulip Rui Liu (Dec 16 2020 at 22:08):

The error message says

invalid type ascription, term has type
   (a : ?m_1), ?m_2 a a
but is expected to have type
  (proof_for q_axm (let prf : list (form q) := [w'] in prf) (subst_fn w 0 xs))

view this post on Zulip Rob Lewis (Dec 16 2020 at 22:22):

Note that there's a difference between exact refl and exact rfl. The argument to the latter is implicit.

view this post on Zulip Rob Lewis (Dec 16 2020 at 22:23):

The tactic refl is approximately exact rfl.

view this post on Zulip Rui Liu (Dec 16 2020 at 22:31):

@Rob Lewis OMG you just saved me!

view this post on Zulip Rui Liu (Dec 16 2020 at 22:41):

Ok I see now, there's a refl that's a tactic name, somehow it doesn't work. However, refl is different from exact refl/rfl, in which refl/rfl is just normal objects, and we're using exact tactic. And it happens that rfl doesn't need you to specify argument. Now I understand why when I do exact refl it complains the type mismatch to me!

I was confused between refl and exact refl!

view this post on Zulip Rui Liu (Dec 16 2020 at 22:42):

Thank you so much! I may take days for me to figure this out on my own!

view this post on Zulip Floris van Doorn (Dec 16 2020 at 22:54):

Note: exact refl _ should also work, and is basically the same as exact rfl.

view this post on Zulip Floris van Doorn (Dec 16 2020 at 22:55):

In this case the tactic refl doesn't work, since that expect the goal to be of the form t = s (or using a relation other than =). Your goal is of the form ↥u, which is defined as t = bool.tt, but refl doesn't unfold that definition, so doesn't see that we're talking about an equality here.

view this post on Zulip Rui Liu (Dec 16 2020 at 23:39):

Do you know why when I replace the subst h to rw h, it again fails to work?

view this post on Zulip Mario Carneiro (Dec 16 2020 at 23:40):

those two are not interchangeable

view this post on Zulip Mario Carneiro (Dec 16 2020 at 23:41):

rw h tries to close the goal with refl, and subst h can replace some things that rw h can't (it gives a "motive is not type correct" error in these cases)


Last updated: May 12 2021 at 23:13 UTC