Zulip Chat Archive

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: Aug 03 2023 at 10:10 UTC