Making a definition transparent to `grind`

Stream: lean4

[Théophile]

Hello,

In my usecase of grind, I need some predicate definitions to be transparent. What is the proper way to do this?

I tried to annotate these predicates as reducible, however this comes with the downside that we cannot ematch on this predicate anymore (see fg on the example below, there we cannot ematch on ∧).

Then I tried to add a grind pattern on the .eq_def theorem of my predicate, but this raises an error (see below). This feels like a bug to me, should I open an issue?

def f (n: Nat): Prop := sorry
def g (n: Nat): Prop := sorry

def fg (n: Nat) := f n ∧ g n

-- Error: Unknown constant `fg.eq_def`
grind_pattern fg.eq_def => fg n


-- workaround
def fg.grind_eq_def := fg.eq_def
grind_pattern fg.grind_eq_def => fg n

-- surprisingly, now this works??
grind_pattern fg.eq_def => fg n

[Marcus Rossel]

You can mark the definition itself with @[grind]:

def f (n: Nat): Prop := sorry
def g (n: Nat): Prop := sorry

@[grind]
def fg (n: Nat) := f n ∧ g n

example : fg 0 ↔ f 0 ∧ g 0 := by
  grind

[Marcus Rossel]

About the surprisingly, now this works??, there are some definitions in Lean which are only generated on first use. So fg.eq_def might be one of these, and is therefore only available after you used it in the fg.grind_eq_def.

[Robin Arnez]

That would be a bug though; in places like these identifiers should cause the necessary realizations to happen

[Théophile]

@Marcus Rossel ah indeed, I didn't think about that for some reason, thanks!

[Robin Arnez]

lean4#10426

[Théophile]

Thanks @Robin Arnez !!