# Zulip Chat Archive

## Stream: new members

### Topic: Any tactics for evaluating a function fully?

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

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

#### 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`

.

#### Floris van Doorn (Dec 15 2020 at 20:29):

If `x`

contains variables (or is a variable) `dsimp [f]`

might help.

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

#### 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
⊢ ...
```

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

#### 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?

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

#### Floris van Doorn (Dec 16 2020 at 02:12):

(in the place of the first `sorry`

)

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

#### 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`

.

#### Floris van Doorn (Dec 16 2020 at 02:18):

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

#### 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`

.

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

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

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

#### Rui Liu (Dec 16 2020 at 21:55):

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

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

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

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

#### Rob Lewis (Dec 16 2020 at 22:23):

The tactic `refl`

is approximately `exact rfl`

.

#### Rui Liu (Dec 16 2020 at 22:31):

@Rob Lewis OMG you just saved me!

#### 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`

!

#### 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!

#### Floris van Doorn (Dec 16 2020 at 22:54):

Note: `exact refl _`

should also work, and is basically the same as `exact rfl`

.

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

#### 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?

#### Mario Carneiro (Dec 16 2020 at 23:40):

those two are not interchangeable

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