# Zulip Chat Archive

## Stream: general

### Topic: Boolean reflection

#### Andrej Bauer (Nov 17 2021 at 14:07):

I am trying to implement boolean reflection, but I am (again) failing to define the correct tactic. I show below three examples. The first two verify that boolean reflection works, but when I wrap it as a tactic, it stops working. Obviously, I am doing something wrong with tactics, but what?

```
import data.fintype.basic
import data.sym2
import data.set.finite
import tactic
open tactic
-- This works
example: ∀ i : fin 3, i = i := (to_bool_iff _).mp rfl
-- This works
example: ∀ i : fin 3, i = i := by exact ((to_bool_iff _).mp rfl)
-- We define a tactic that will do precisely the same as above
meta def tactic.interactive.bool_reflect : tactic unit :=
do { r ← i_to_expr_strict ``((to_bool_iff _).mp rfl),
exact r
}
-- And now this does not work
example: ∀ i : fin 3, i = i := by bool_reflect
```

#### Alex J. Best (Nov 17 2021 at 14:21):

```
import data.fintype.basic
import data.sym.sym2
import data.set.finite
import tactic
open tactic
-- This works
example: ∀ i : fin 3, i = i := (to_bool_iff _).mp rfl
-- This works
example: ∀ i : fin 3, i = i := by exact ((to_bool_iff _).mp rfl)
-- We define a tactic that will do precisely the same as above
meta def tactic.interactive.bool_reflect : tactic unit :=
do { r ← i_to_expr_strict ``((to_bool_iff _).mp rfl),
exact r
}
-- And now this does not work
example: ∀ i : fin 3, i = i := by bool_reflect
```

this version of the MWE works in the web editor (I guess a file moved in mathlib)

#### Andrej Bauer (Nov 17 2021 at 14:23):

You're saying that my non-example works for you?

#### Anne Baanen (Nov 17 2021 at 14:24):

Looks like the issue is that `i_to_expr_strict`

doesn't (can't) use the expected type to fill in the metavariables in the term.

#### Alex J. Best (Nov 17 2021 at 14:25):

no sorry, just saying that your MWE doesn't work with matlib master (it changes fast) and providing a version that does for anyone who wants to try it

#### Anne Baanen (Nov 17 2021 at 14:25):

Note that commenting out `exact r`

gives the same error.

#### Andrej Bauer (Nov 17 2021 at 14:26):

We can also explicitly stick in the goal, which still won't work:

```
-- We define a tactic that will do precisely the same as above
meta def tactic.interactive.bool_reflect : tactic unit :=
do { p ← get_goal,
r ← i_to_expr ``((to_bool_iff %%(p)).mp rfl),
exact r
}
-- And now this does not work
example: ∀ i : fin 3, i = i := by bool_reflect
```

#### Anne Baanen (Nov 17 2021 at 14:27):

But hinting the target type works:

```
-- We define a tactic that will do precisely the same as above
meta def tactic.interactive.bool_reflect : tactic unit :=
do { tgt ← target,
r ← i_to_expr_for_apply ``((to_bool_iff _).mp rfl : %%tgt),
exact r
}
```

#### Andrej Bauer (Nov 17 2021 at 14:27):

Commenting out `exact r`

does not work because the failure occurs alread at `i_to_expr`

.

#### Andrej Bauer (Nov 17 2021 at 14:28):

I confused `get_goal`

and `target`

!

#### Anne Baanen (Nov 17 2021 at 14:30):

See also the source code of src#tactic.interactive.exact where I got the `(_ : %%tgt)`

trick from.

#### Andrej Bauer (Nov 17 2021 at 14:31):

I knew about the trick, what really helped was to see that `target`

was the right thing (and I was using `get_goal`

). Thanks!

#### Anne Baanen (Nov 17 2021 at 14:32):

No problem!

#### Mario Carneiro (Nov 17 2021 at 16:48):

Also, I'm probably stating the obvious, but @Andrej Bauer I assume you know that we usually use `dec_trivial`

to do the equivalent of boolean reflection in lean:

```
import data.fintype.basic
example: ∀ i : fin 3, i = i := dec_trivial
```

#### Mario Carneiro (Nov 17 2021 at 16:50):

the implementation of `dec_trivial`

might be interesting to you because it's a notation (for `of_as_true (by trivial)`

), not a tactic

Last updated: Dec 20 2023 at 11:08 UTC