## Stream: general

### Topic: choose

#### Patrick Massot (May 12 2019 at 12:07):

The choose tactic has the annoying habit of generating terms featuring ∃ h : P where P is a Prop. In my lectures I use a variant which blindly applies simp only [exists_prop] at *, because I don't know how to do that only to hypotheses that are created by choose. Does anyone know how to do that? Would a PR changing this behavior be welcome?

#### Rob Lewis (May 12 2019 at 15:03):

I'd be happy to see a PR changing this in choose, but I'm not sure I've ever looked at that tactic, and don't know how to do it off the top of my head.

#### Patrick Massot (May 12 2019 at 19:13):

My problem with choose is the parsing magic. One of the arguments of choose is (names : parse ident*) (where * is the usual notation for many). Sometimes Lean magically converts names to type list (option name) but sometimes not

#### Patrick Massot (May 12 2019 at 19:13):

Is there any way to force this?

Oh, I was stupid

#### Patrick Massot (May 12 2019 at 19:26):

It's optional that corresponds to option of course. many ident is secretely list name not list (option name)

#### Patrick Massot (May 12 2019 at 19:35):

So I get as a new interactive choose:

meta def tactic.interactive.choose' (first : parse ident) (names : parse ident*) (tgt : parse (tk "using" *> texpr)?) :
tactic unit := do
tgt ← match tgt with
| none := get_local this
| some e := i_to_expr_strict e
end,
choose tgt (first :: names),
interactive.simp none tt [simp_arg_type.expr (exists_prop)] [] (ns $some <$> names),
try (tactic.clear tgt)


I even manage to use (ns $some <$> names). I hope Simon will be proud

#### Johan Commelin (May 13 2019 at 05:04):

One thing I've been thinking is that maybe choose could become a classical rcases.

#### Johan Commelin (May 13 2019 at 05:05):

I also like that choose flips the syntax compared to rcases.

choose \<the, names, you, want\> using hyp
-- vs
rcases hyp with \<the, names, you, want\>
`

Last updated: May 14 2021 at 23:14 UTC