by_cases

Stream: general

[Jeremy Avigad]

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]

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

[Gabriel Ebner]

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

[Gabriel Ebner]

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]

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]

This is a big danger of the vm_override attribute.

[Gabriel Ebner]

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

[Rob Lewis]

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

[Rob Lewis]

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]

Yes it can work with non-meta stuff

[Simon Hudon]

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]

lean#417