relations with binders in calc

Stream: lean4

[Rob Lewis]

@Patrick Massot and I have been experimenting with some new notation and ran into some confusing behavior in calc. Here's a mathlib-free example:

def Set (α :  Type) := α → Prop

def Set.UniformlyLeOn (s : Set α) (f g : α → Nat) : Prop := ∃ C, ∀ x,  s x → (f x) ≤ C * (g x)

notation lhs:50 "≪["s", "x"]" rhs:50 => Set.UniformlyLeOn s (fun x => lhs) (fun x => rhs)

theorem f (s : Set Nat) : x ≪[s, x] x + x := by
calc
  x ≪[s, x] (x + x + x) := ⟨1, fun x hx => by simp [Set.UniformlyLeOn] ⟩
  _ ≪[s, x] (x + x) := sorry

The calc errors with

type mismatch
  ?m.2949
has type
  Nat → Nat : Type
but is expected to have type
  Nat : Type

It seems like calc annotates the underscore with type Nat -> Nat, which is the correct type for the LHS of the relation. But the underscore lives inside the binder for the relation's notation, so it really should be annotated Nat.

Any thoughts on how we could get this to work? (@Sebastian Ullrich ?)

[Eric Wieser]

Does the calc work if you replace the _ with (x + x + x)?

[Rob Lewis]

Here's a minor repair to the MWE (missed a few things in shrinking it):

def Set (α :  Type) := α → Prop

def Set.UniformlyLeOn (s : Set α) (f g : α → Nat) : Prop := ∃ C, ∀ x,  s x → (f x) ≤ C * (g x)

instance (α : Type) (s : Set α) :
  Trans (Set.UniformlyLeOn s) (Set.UniformlyLeOn s) (Set.UniformlyLeOn s) := sorry

notation lhs:50 "≪["s", "x"]" rhs:50 => Set.UniformlyLeOn s (fun x => lhs) (fun x => rhs)

theorem f (s : Set Nat) : x ≪[s, x] (x + x) := by
calc
  x ≪[s, x] x := ⟨1, fun x hx => by simp [Set.UniformlyLeOn] ⟩
  _ ≪[s, x] (x + x) := sorry

[Rob Lewis]

This does succeed if you replace the underscore with x (no longer x + x + x in the new MWE). But it also succeeds if you replace it with (_), since this disables the type annotation in calc.

[Eric Wieser]

Does this (_) trick work for the open issue about calc for morphisms?

[Rob Lewis]

You mean #6509? Seems like it does:

import Mathlib.Algebra.Module.Equiv

variable (R A B C D : Type _) [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D]
   [Module R A] [Module R B] [Module R C] [Module R D]

-- TODO: semilinearize
instance : Trans
  -- all but the last two arguments of `LinearEquiv`
  (@LinearEquiv R R _ _ (RingHom.id _) (RingHom.id _) _ _ A B _ _)
  (@LinearEquiv R R _ _ (RingHom.id _) (RingHom.id _) _ _ B C _ _)
  (@LinearEquiv R R _ _ (RingHom.id _) (RingHom.id _) _ _ A C _ _) where trans := LinearEquiv.trans

example (R A B C D : Type _) [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D]
   [Module R A] [Module R B] [Module R C] [Module R D] (f : A ≃ₗ[R] B) (g : B ≃ₗ[R] C) (h : C ≃ₗ[R] D) : A ≃ₗ[R] D := by
  calc
    A ≃ₗ[R] B := f
    (_) ≃ₗ[R] C := g
    (_) ≃ₗ[R] D := h

[Ruben Van de Velde]

What

[Rob Lewis]

Ruben Van de Velde said:

What

Calc only annotates a hole with an expected type if the hole is the very first thing it sees

[Ruben Van de Velde]

I thought that was just syntax, not a hole