choose

Stream: general

[Patrick Massot]

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]

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]

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]

Is there any way to force this?

[Patrick Massot]

Oh, I was stupid

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

See https://github.com/leanprover-community/mathlib/pull/1014/files

[Johan Commelin]

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

[Johan Commelin]

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\>