Zulip Chat Archive

Stream: mathlib4

Topic: Changing instance priority


Moritz Doll (Aug 06 2022 at 11:26):

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 (Aug 06 2022 at 11:40):

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

Moritz Doll (Aug 06 2022 at 11:44):

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 (Aug 06 2022 at 11:46):

and

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

does obviously nothing

Moritz Doll (Aug 06 2022 at 12:29):

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 (Aug 06 2022 at 12:32):

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

Mario Carneiro (Aug 06 2022 at 14:13):

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

Mario Carneiro (Aug 06 2022 at 14:15):

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 (Aug 06 2022 at 14:38):

thanks, I will try that

Moritz Doll (Aug 06 2022 at 14:48):

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

Moritz Doll (Aug 06 2022 at 22:59):

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 (Aug 06 2022 at 23:00):

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 (Aug 07 2022 at 02:27):

Here you should be able to write

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

Mario Carneiro (Aug 07 2022 at 02:28):

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


Last updated: Dec 20 2023 at 11:08 UTC