Local notation not recognised in 'intro' tactic

Stream: new members

[Yee-Jian Tan]

I defined a symbol for a locally postulated relation, but when I try to use it as the type in the intro tactic (for clarity/pedagogical purposes, I know it is possible to just omit the type of the introduced variable), it gives me an error saying that the type can only be sorry?

import Mathlib.Logic.Relation
-- BEGIN
section
variable (A : Type)
variable (R : A → A → Prop)
-- type \preceq for the symbol ≼
local infixl:50 " ≼ " => R

example (h1 : Irreflexive R) (h2 : Transitive R) :
    ∀ x y, x ≼ y → ¬ y ≼ x := by
  intro x y
  intro (h3 : x ≼ y)
  intro (h4 : y ≼ x)
  have h5 : x ≼ x := h2 h3 h4
  have h6 : ¬ x ≼ x := h1 x
  show False
  exact h6 h5

end
-- END

The error message is:

original tactic 'intro x y;
  intro (h3 : x ≼ y);
  intro (h4 : y ≼ x);
  have h5 : x ≼ x := h2 h3 h4' failed: Type mismatch: Hypothesis `h3` has type
  R x y
but is expected to have type
  sorry
due to the provided type annotation

This occurs for v4.23.0 onwards but not v4.22.0. Any solution?

[Kevin Buzzard]

The error message is Unknown constant R✝ , you are reporting a warning which is triggered by the error. The issue seems to be that ≼ is associated to a different R than the one you want when it's parsed.

[Kevin Buzzard]

Basically you're doing something a bit weird because variable doesn't mean what most people think it means. variable (R : A → A → Prop) does not mean "from now on we have something called R with that type", it means "do nothing, but whenever you see an R later on, insert (R : A → A → Prop) as an input somewhere before it". So " ≼ " is really a function of an input variable R, as opposed to one fixed thing with no input variables, and this is not most people's mental model of variables. For some reason I don't understand, Lean is now misguessing the input variable in this code.