Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: if exists assumption else

Yury G. Kudryashov (Mar 20 2022 at 03:39):

What is the most readable way to have if (exists assumption of type t) then (code using t) else ..? Same question for if (lean can generate an instance of type t).

Simon Hudon (Mar 20 2022 at 05:12):

You can write this function

meta def has_asm (e : expr) : tactic bool :=
succeeds $ find_assumption e

and use it as:

do b <- has_asm t,
   if b then ...
   else ...

Simon Hudon (Mar 20 2022 at 05:12):

(I assume this is Lean 3)

Simon Hudon (Mar 20 2022 at 05:14):

We can write a similar function to find instances:

meta def has_instance (e : expr) : tactic bool :=
succeeds $ mk_instance e

Yury G. Kudryashov (Mar 20 2022 at 14:45):

So, I need to search for the assumption/instance twice (once for if and once in the then branch)?

Rob Lewis (Mar 20 2022 at 15:09):

You can do something like this:

(do e ← find_assumption t,
    something with e ) <|>
(something without e)

But note that in this case, something without e will run if something with e fails. If that's a possibility you need to be more careful with the logic.

Yury G. Kudryashov (Mar 20 2022 at 15:47):

We can have something like

meta def if_with {α β : Type*} (v : tactic α) (pos : α → tactic β) (neg : tactic β) :
  tactic β :=
do
  v' ← optional v,
  v'.elim neg pos

Yury G. Kudryashov (Mar 20 2022 at 15:48):

(probably, it works with some typeclass instead of just tactic)

Yury G. Kudryashov (Mar 20 2022 at 15:49):

Is it in the library under some name? If not, how should I call it?

Yury G. Kudryashov (Mar 20 2022 at 15:50):

#xy: in #12844 I want to add a branch for the case if there are assumptions [measurable_space α] [borel_space α].

Yury G. Kudryashov (Mar 20 2022 at 15:50):

(and the tactic should fail if there is a [measurable_space α] but no [borel_space α])

Yury G. Kudryashov (Mar 20 2022 at 15:57):

For now, I'm going to inline this function.

Yury G. Kudryashov (Mar 20 2022 at 16:25):

Done.

Mario Carneiro (Mar 20 2022 at 16:45):

The usual way I do something like that is o <- try_core tac, match o with ... or mcond (succeeds tac) ... ...

Yury G. Kudryashov (Mar 20 2022 at 17:05):

Is try_core the same as optional?

Eric Wieser (Mar 21 2022 at 13:58):

The question here amounts to asking for the lean translation of Python's:

try:
    t = get_assumption()
except:
    no_t()
else:
    with_t(t)

Right?

Yury G. Kudryashov (Mar 21 2022 at 15:25):

Yes. I use

meta def borel (t : parse texpr) : tactic unit :=
do
  α ← to_expr t,
  i' ← optional (to_expr ``(measurable_space %%α) >>= find_assumption),
  i'.elim _ _

Yury G. Kudryashov (Mar 21 2022 at 15:26):

in #12844

Eric Wieser (Jun 08 2022 at 11:52):

I found that you can spell this

some t ← try_core get_assumption | no_t,
with_t t

Last updated: Dec 20 2023 at 11:08 UTC