Zulip Chat Archive

Stream: general

Topic: by_cases


view this post on Zulip Jeremy Avigad (Jul 28 2020 at 15:48):

Can someone tell me why the first example succeeds and the second one doesn't? As far as I can tell, by_cases gets the decidability instance by calling mk_instance.

import tactic
open tactic

variables {α : Type*} (x : α) (s : set α)

noncomputable example : decidable (x  s) :=
by { by_cases x  s; simp *; apply_instance }

noncomputable example : decidable (x  s) :=
by do
  e  target >>= mk_instance,
  -- "tactic.mk_instance failed to generate instance for decidable (x ∈ s)""
  exact e

view this post on Zulip Jeremy Avigad (Jul 28 2020 at 15:49):

(I am wondering how by_cases learned to use classical logic.)

view this post on Zulip Gabriel Ebner (Jul 28 2020 at 15:50):

We patched by_cases in #3354 (July 11). The changes have been merged into core Lean as of 3.18.0 today.

view this post on Zulip Gabriel Ebner (Jul 28 2020 at 15:51):

The reason to change the by_cases tactic was that it unfolded the proposition too much. The decidability assumption was just a pet peeve of mine.

view this post on Zulip Jeremy Avigad (Jul 28 2020 at 15:59):

I see. I am still using Lean 3.17.1 and clicking on by_cases takes me to the old definition. But now I see fix_by_cases.lean and the vm_override. Now it all makes sense. I was really confused...

view this post on Zulip Rob Lewis (Jul 28 2020 at 16:01):

This is a big danger of the vm_override attribute.

view this post on Zulip Gabriel Ebner (Jul 28 2020 at 16:03):

Luckily we only use it four times in mathlib+core. Should we make go-to definition go to the overriding definition?

view this post on Zulip Rob Lewis (Jul 28 2020 at 16:04):

Well, I guess that could be confusing for the same reason... vm_override can be used on non-meta decls, right?

view this post on Zulip Rob Lewis (Jul 28 2020 at 16:05):

Maybe vm_override could append a note to the doc string of the declaration being overridden? It wouldn't show up in source but at least it means the override isn't completely invisible.

view this post on Zulip Simon Hudon (Jul 28 2020 at 16:06):

Yes it can work with non-meta stuff

view this post on Zulip Simon Hudon (Jul 28 2020 at 16:09):

I don't think I had considered using vm_override like this before. I think it opens up a really nice style of interaction for debugging a tactic in the context of a specific proof.

view this post on Zulip Gabriel Ebner (Jul 28 2020 at 16:16):

lean#417


Last updated: May 12 2021 at 05:19 UTC