Zulip Chat Archive

Stream: general

Topic: choose


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 12 2019 at 19:13):

Is there any way to force this?

view this post on Zulip Patrick Massot (May 12 2019 at 19:25):

Oh, I was stupid

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 12 2019 at 20:08):

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

view this post on Zulip Johan Commelin (May 13 2019 at 05:04):

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

view this post on Zulip 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