## Stream: general

### Topic: by_cases

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


#### Jeremy Avigad (Jul 28 2020 at 15:49):

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

#### 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.

#### 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.

#### 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...

#### Rob Lewis (Jul 28 2020 at 16:01):

This is a big danger of the vm_override attribute.

#### 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?

#### 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?

#### 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.

#### Simon Hudon (Jul 28 2020 at 16:06):

Yes it can work with non-meta stuff

#### 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.

#### Gabriel Ebner (Jul 28 2020 at 16:16):

lean#417

Last updated: May 12 2021 at 05:19 UTC