grewrite and reflexivity subgoals

Stream: mathlib4

[discuss9128]

Hi, I'm having trouble using grewrite with my custom relation.

grewrite supposedly doesn't close goals with rfl but I still get the error below.

Given that I have already declared an IsRefl instance, how do I get grewrite to find it automatically? In Rocq, rewrite will find Reflexivity instances automatically so I'm hoping for the equivalent of that.

import Mathlib.Tactic.GRewrite

inductive formula where
  | unit
  | conj (a b:formula)

def implies (p1 p2 : formula) : Prop := sorry

theorem implies_refl (x : formula) : implies x x := by
  sorry

instance : IsRefl _ implies where
  refl := implies_refl

@[gcongr]
theorem proper_implies a b (h1: implies a b) (h2: implies c d)
  (h3: implies b c) : implies a d
:= by
  sorry

example (a b c: formula) (h:implies b c): implies b a := by
  -- this does the rewrite i want, giving me implies c a

  -- apply proper_implies _ _ h
  -- apply implies_refl

  -- this doesn't, i get the error:
  -- Tactic `gcongr` failed: subgoal implies a a is not allowed by the provided pattern and is not closed by `rfl`
  grewrite [h]

[František Silváši 🦉]

@[refl]
theorem implies_refl (x : formula) : implies x x := by
  sorry

Should do it.

[František Silváši 🦉]

I don't think having an instance of IsRefl is tied to the tactic rfl. It's the attribute that registers statements for the rfl tactic.

[discuss9128]

Ah, thank you!