Changing instance priority

Stream: mathlib4

[Moritz Doll]

Hi, I am trying to do https://github.com/leanprover-community/mathlib4/issues/306 but I haven't found anything on how to change instance priority. I expect it to be somewhere in this file https://leanprover-community.github.io/mathlib4_docs//////Lean/Meta/Instances.html but there is nothing.

[Gabriel Ebner]

I think the Lean 4 version should just expand to open Classical (a tactic!).

[Moritz Doll]

I first tried

macro_rules
| `(tactic| classical_foo) => `(tactic| open Classical)

but that complained that open expects in, i.e., open Classical in .., so I thought that using open is no good

[Moritz Doll]

and

macro_rules
| `(tactic| classical_foo) => `(tactic| open Classical in {})

does obviously nothing

[Moritz Doll]

I don't even get it to work if I cheat with the syntax:

import Mathlib.Tactic.Basic
import Mathlib.Data.List.Basic

syntax "classical_foo " tactic : tactic

macro_rules
| `(tactic| classical_foo $a:tactic) => `(tactic| open Classical in { $a:tactic })

example : (by classical_foo (exact decide (0 = 1)) : Bool) = decide (0 = 1) := rfl

this runs into the error unknown namespace 'Classical._@.test.Classical._hyg.193'.

[Moritz Doll]

I guess that the problem is that the macro leaks the namespace, which is forbidden

[Mario Carneiro]

one hack to make open Classical work would be to make the syntax "classical" tacticSeq : tactic

[Mario Carneiro]

You can use set_option hygienic false in in the declaration of the macro so that the word Classicalis not marked up with hygiene info

[Moritz Doll]

thanks, I will try that

[Moritz Doll]

(after I am finished spamming the mathlib PR queue :big_smile: )

[Moritz Doll]

Thanks Mario, that got me almost to where I want to end up with, but the syntax is still not quite how it should be. If there is a way to get the tacticSeq of all following tactics I would be happy, but I could not find anything of that kind.

set_option hygiene false in
macro "classical_blubb " seq:tacticSeq : tactic => `(tactic| open Classical in { ($seq) })

example : (by classical_blubb { exact decide (0 = 1) } : Bool) = decide (0 = 1) := rfl

but the example by Gabriel was

example : (by classical_blubb; exact decide (0 = 1) : Bool) = decide (0 = 1) := rfl

[Moritz Doll]

I am sorry for bothering everyone with these stupidly simple questions, but I have a really hard time finding things in Lean4/mathlib4.

[Mario Carneiro]

Here you should be able to write

example : (by classical_blubb exact decide (0 = 1) : Bool) = decide (0 = 1) := rfl

[Mario Carneiro]

it won't work if you put a semicolon after it