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