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

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