the [grind] attribute cannot be applied at all

Stream: general

[Asei Inoue]

I found an example where the [grind] attribute cannot be applied at all, but I don’t understand why.
I’d like to know the reason.

variable {A B C : Type}

theorem comp_eq {f : A → B} {g : B → C} {h : A → C} (heq : g ∘ f = h) (a : A) : g (f a) = h a := calc
  _ = (g ∘ f) a := rfl
  _ = h a := by rw [heq]

-- For some reason, the `[grind]` attribute cannot be applied at all
/--
error: `@[grind] theorem comp_eq` failed to find patterns, consider using different options or the `grind_pattern` command
-/
#guard_msgs in
attribute [grind] comp_eq

/--
error: `@[grind =>] theorem comp_eq` failed to find patterns searching from left to right, consider using different options or the `grind_pattern` command
-/
#guard_msgs in
attribute [grind =>] comp_eq

/--
error: invalid pattern, (non-forbidden) application expected
  @#3 (@#4 #0)
-/
#guard_msgs in
attribute [grind =] comp_eq

[Floris van Doorn]

Did you try the grind_pattern command? See reference manual: https://lean-lang.org/doc/reference/latest//The--grind--tactic/E___matching/#The-Lean-Language-Reference--The--grind--tactic--E___matching

[Asei Inoue]

Did you try the grind_pattern command? See reference manual: https://lean-lang.org/doc/reference/latest//The--grind--tactic/E___matching/#The-Lean-Language-Reference--The--grind--tactic--E___matching

I don't know how to use grind_pattern...

[Jovan Gerbscheid]

I don't think this is a reasonable grind lemma. Do you want it to apply if g ∘ f = h is in the context? in that case there is no way to find a.

[Asei Inoue]

Originally, I was trying to golf the following proof using grind.
If there's a good way to do it, I'd love to know.

namespace Function

variable {A B : Type}

/-- Injectivity of a function -/
def Injective (f : A → B) : Prop :=
  ∀ (x y : A), f x = f y → x = y

/-- Surjectivity of a function -/
def Surjective (f : A → B) : Prop :=
  ∀ y : B, ∃ x : A, f x = y

variable {C : Type}
variable {f : B → C} {g : A → B}

/-- If the composition is surjective, then so is the outer function. -/
theorem surj_of_comp_surj (h : Surjective (f ∘ g)) : Surjective f := by
  dsimp [Surjective] at *
  -- Actually, this can be solved with `try?`
  intro c
  have ⟨a, ha⟩ := h c
  grind

/-- If the composition is injective, then the inner function is injective. -/
theorem inj_of_comp_inj (h : Injective (f ∘ g)) : Injective g := by
  dsimp [Injective] at *
  -- Actually, this can be solved with `try?`
  intro a₁ a₂ g_eq
  replace h := h a₁ a₂
  grind

/-- Monomorphism -/
def mono (f : A → B) : Prop :=
  ∀ C : Type, ∀ g₁ g₂ : C → A, f ∘ g₁ = f ∘ g₂ → g₁ = g₂

/-- An injective function is a monomorphism -/
theorem mono_of_inj {f : A → B} (h : Injective f) : mono f := by
  intro C g₁ g₂ g_eq
  dsimp [Injective] at h
  ext c
  fail_if_success grind -- **TODO** How can we prove this using `grind`?
  have eq : f (g₁ c) = f (g₂ c) := calc
    _ = (f ∘ g₁) c := rfl
    _ = (f ∘ g₂) c := by rw [g_eq]
    _ = f (g₂ c) := rfl
  replace h := h (g₁ c) (g₂ c) eq
  assumption

/-- A monomorphism is injective -/
theorem inj_of_mono {f : A → B} (h : mono f) : Injective f := by
  intro a₁ a₂ f_eq
  dsimp [mono] at h

  let C := Fin 2
  let g₁ : C → A := fun _ => a₁
  let g₂ : C → A := fun _ => a₂
  replace h := h C g₁ g₂

  fail_if_success grind -- **TODO** How can we prove this using `grind`?
  have : f ∘ g₁ = f ∘ g₂ := by grind
  replace h := h this

  have : a₁ = a₂ := calc
    _ = g₁ 0 := rfl
    _ = g₂ 0 := by rw [h]
    _ = a₂ := rfl
  assumption

/-- Epimorphism -/
def epi (f : A → B) := ∀ C : Type, ∀ g₁ g₂ : B → C, g₁ ∘ f = g₂ ∘ f → g₁ = g₂

/-- A surjective function is an epimorphism -/
theorem epi_of_surj {f : A → B} (h : Surjective f) : epi f := by
  intro C g₁ g₂ g_eq
  dsimp [Surjective] at h
  ext b
  obtain ⟨a, ha⟩ := h b
  rw [← ha]

  -- Why does `grind` not succeed here?
  fail_if_success grind

  have : g₁ (f a) = g₂ (f a) := calc
    _ = (g₁ ∘ f) a := rfl
    _ = (g₂ ∘ f) a := by rw [g_eq]
    _ = g₂ (f a) := rfl
  assumption

end Function

[Kim Morrison]

Change your definitions of mono and epi so they are about fully applied functions. grind will be happier.

[Asei Inoue]

@Kim Morrison

they are about fully applied functions

what is "fully applied functions"? How should I change the definitions?

[Patrick Massot]

If f has type α → β → γ then f a b is fully applied while f a is only partially applied.

[Asei Inoue]

:(

/-- モノ射 -/
def mono (f : A → B) : Prop :=
  ∀ C : Type, ∀ g₁ g₂ : C → A, f ∘ g₁ = f ∘ g₂ → g₁ = g₂

/- `@[grind] theorem Function.mono_grind` failed to find patterns, consider using different options or the `grind_pattern` command -/
@[grind]
theorem mono_grind (f : A → B) (h : mono f) {C : Type} {g₁ g₂ : C → A} (hcomp : ∀ c, (f ∘ g₁) c = (f ∘ g₂) c) :
  ∀ c, g₁ c = g₂ c := by
  intro c
  have eq : f ∘ g₁ = f ∘ g₂ := by grind
  have g_eq : g₁ = g₂ := h C g₁ g₂ eq
  grind

[Jovan Gerbscheid]

I think what @Kim Morrison means is to make epi and mono into a one field structure, or to use irreducible_def.

I was also wondering: in the grind manual, it says that grind has special support for the injectivity of inductive constructors. But as far as I could tell, grind does not support any other kinds of injectivity lemmas. Is that right?