Boolean reflection

Stream: general

[Andrej Bauer]

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]

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]

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

[Anne Baanen]

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]

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]

Note that commenting out exact r gives the same error.

[Andrej Bauer]

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]

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]

Commenting out exact r does not work because the failure occurs alread at i_to_expr.

[Andrej Bauer]

I confused get_goal and target!

[Anne Baanen]

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

[Andrej Bauer]

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]

No problem!

[Mario Carneiro]

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]

the implementation of dec_trivial might be interesting to you because it's a notation (for of_as_true (by trivial)), not a tactic