Zulip Chat Archive

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?

Patrick Massot (May 12 2019 at 19:25):

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

Patrick Massot (May 12 2019 at 20:08):

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

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: Dec 20 2023 at 11:08 UTC