unhygienic by_cases

Stream: lean4

[Jon Eugster]

I would like to use by_cases in combination to tactic.hygienic false:

import Lean

set_option tactic.hygienic false

example : A ∨ ¬ A := by
  by_cases A
  · left
    exact h -- fails
  . right
    exact h -- fails

example (h : 1 < 5) : A ∨ ¬ A := by
  by_cases A
  · left
    exact h_1 -- fails
  . right
    exact h_1 -- fails

The tactic is implemented (now in core):

macro_rules
  | `(tactic| by_cases $e) => `(tactic| by_cases h : $e)

It seems to me that the right thing to use would be docs#Lean.Meta.mkFreshBinderNameForTactic but a macro rule is in MacroM, so I think it does not have access to CoreM. I don't have a perfect overview of all the monads, so is there an easy way to modify by_cases to respect the hygienic option?

[Mario Carneiro]

cc: @Sebastian Ullrich

[Sebastian Ullrich]

One (I) would think that set_option hygiene false should help here but it doesn't. In any case, it seems unfortunate that we have these two similar but unconnected options.

[Jon Eugster]

Sebastian Ullrich said:

One (I) would think that set_option hygiene false should help here but it doesn't. In any case, it seems unfortunate that we have these two similar but unconnected options.

Would it be reasonable to have by_casesto be an (tactic) elab instead of a macro? Like this:

import Init.ByCases
import Lean.Elab.Tactic.Basic
import Lean.Meta.Tactic.Intro

open Lean Meta Elab Tactic

syntax (name := by_cases') "by_cases' " (atomic(ident " : "))? term : tactic

@[tactic by_cases'] def evalByCases : Tactic := fun stx => withMainContext do
  let h ← mkFreshBinderNameForTactic <| (stx[1].getArgs.getD 0 (mkIdent `h) |>.getId)
  let h' : TSyntax `term := ⟨mkIdent h⟩
  let e : TSyntax `term := ⟨stx[2]⟩
  evalTactic (← `(tactic| open Classical in refine (dite $e (fun ($h' : $e) => ?pos) (fun ($h' : ¬ $e) => ?neg))))-- if $h' : $e then ?pos else ?neg))


-- Testing:
set_option tactic.hygienic false

example : A ∨ ¬ A := by
  by_cases' A
  · left
    exact h -- works
  . right
    exact h -- works

example (h : 1 < 5) : A ∨ ¬ A := by
  by_cases' A
  · left
    exact h_1 -- works
  . right
    exact h_1 -- works

(now I'm not particularly good at meta-coding, so the details feel a bit hacked, but conceptually...)

[Sebastian Ullrich]

Sure, that works, but we should still look into why hygiene doesn't

[Jon Eugster]

Sorry, I don't know anything about the hygiene option.

If I read the chapter "hygiene issues and how to solve them" in the meta-programming book and look at how there is just a hard-coded h in the by_cases-marco (source code), I'm not sure I understand how the two are related.

The former hygiene seems to talk about not accidentally using a wrong h when elaborating (like the example in the book with x=42 vs x=10, but that's not an issue here. The issue is only that the user-facing names are not as expected.

So according to the book, one should hard-code $(mkIdent `h) instead of just h but that would make the tactic always unhygienic (in the tactic.hygienic sense).

[Jon Eugster]

(Ah or maybe you're referring to the following quote from the docstring of the hygienic option:

Note that quotations/notations already defined are unaffected.

Let me try that!)

[Jon Eugster]

Indeed, adding set_option hygienic false in Init.ByCases before the syntax/macro definition does do what you expect it to do, i.e. h : A is now accessible after by_cases A

[Sebastian Ullrich]

Ah, I didn't even remember that. So hygiene is a compile-time option while tactic.hygienic is run-time...