Any tactics for evaluating a function fully?

Stream: new members

[Rui Liu]

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.

[Yakov Pechersky]

One possibility is

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

if I understood correctly

[Floris van Doorn]

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.

[Floris van Doorn]

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

[Rui Liu]

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

[Floris van Doorn]

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

x y : bool
⊢ ...

[Floris van Doorn]

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

[Rui Liu]

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

[Floris van Doorn]

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

[Floris van Doorn]

(in the place of the first sorry)

[Floris van Doorn]

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.

[Floris van Doorn]

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.

[Floris van Doorn]

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

[Floris van Doorn]

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.

[Floris van Doorn]

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.

[Rui Liu]

@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.

[Rui Liu]

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 :)

[Rui Liu]

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

[Mario Carneiro]

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

[Rui Liu]

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))

[Rob Lewis]

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

[Rob Lewis]

The tactic refl is approximately exact rfl.

[Rui Liu]

@Rob Lewis OMG you just saved me!

[Rui Liu]

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!

[Rui Liu]

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

[Floris van Doorn]

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

[Floris van Doorn]

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.

[Rui Liu]

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

[Mario Carneiro]

those two are not interchangeable

[Mario Carneiro]

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)