Understanding the gcongr relation restriction

Stream: mathlib4

[Geoffrey Irving]

I'm trying to use gcongr to dispatch interval arithmetic lemmas. However, I don't seem to be able to define new gcongr lemmas in the way I expect:

import Mathlib.Data.Set.Pointwise.Basic

open Pointwise
open Set

variable {R A : Type}

/-- `A` approximates `R`, in that we can map `A → Set R` -/
class Approx (A : Type) (R : outParam Type) where
  approx : A → Set R

export Approx (approx)

/-- `x` represents `a` is `a ∈ approx x`.  This is an attempt to make `gcongr` work for us. -/
def reps [Approx A R] (a : A) (x : R) : Prop := x ∈ approx a

/-- `-A` is conservative -/
class ApproxNeg (A R : Type) [Neg R] [Neg A] [Approx A R] where
  approx_neg : ∀ x : A, -approx x ⊆ approx (-x)

export ApproxNeg (approx_neg)

-- Complains with
-- @[gcongr] attribute only applies to lemmas proving x₁ ~₁ x₁' → ... xₙ ~ₙ xₙ' → f x₁ ... xₙ ∼ f x₁' ... xₙ', got ∀
--  {R A : Type} [inst : InvolutiveNeg R] [inst_1 : Neg A] [inst_2 : Approx A R] [inst_3 : ApproxNeg A R] (a : A) {x : R},
--  reps a x → reps (-a) (-x)
@[gcongr] lemma reps_neg [InvolutiveNeg R] [Neg A] [Approx A R] [ApproxNeg A R]
    (a : A) {x : R} (ax : reps a x) : reps (-a) (-x) :=
  (approx_neg a) (neg_mem_neg.mpr ax)

Is reps not a valid relation, or am I doing something else wrong...

Ah, I see: the f has to be the same on both sides, which in particular means gcongr is restricted to relations between the same type?

[Yury G. Kudryashov]

@Heather Macbeth :up:

[Heather Macbeth]

Yep, that's right.

[Geoffrey Irving]

Sounds good, I can make my own related tactic if that’s the better way to go.

[Yaël Dillies]

This kind of looks like mono?

[Geoffrey Irving]

Ah, nice! I had forgotten about mono. That does work better, though I wasn't expecting to need the rfls at the end based on the documentation?

import Mathlib.Data.Set.Pointwise.Basic
import Mathlib.Tactic.Monotonicity.Basic
open Pointwise

variable {R A : Type} [Add R] [Add A]

/-- `A` approximates `R`, in that we can map `A → Set R` -/
class Approx (A : Type) (R : outParam Type) where
  approx : A → Set R

export Approx (approx)

@[mono] lemma subset_approx_add [Approx A R] {a b : Set R} (x y : A)
    (ax : a ⊆ approx x) (yb : b ⊆ approx y) : a + b ⊆ approx (x + y) :=
  sorry

/-- I hoped `mono` would do `rfl` for me -/
lemma approx_mono_test [Approx A R] (x y : A) : approx x + approx y ⊆ approx (x + y) := by
  mono; rfl; rfl

[Geoffrey Irving]

Ah, attribute [mono] subset_refl fixes it. Should subset_refl be registered as mono too?

[Yaël Dillies]

Probably! Not many people (no one?) use mono, especially since it was ported to Lean 4 relatively late, so you will find rough edges.

[Geoffrey Irving]

I'll send a PR.

[Heather Macbeth]

Note that in the mathlib4 implementation mono is just a bag of lemmas. So you can make it mimic continuity or whatever you want:

import Mathlib.Topology.Instances.Real

attribute [mono] Continuous.add Continuous.mul continuous_const

example {c : ℝ} {f : ℝ → ℝ} (hf : Continuous f) : Continuous (fun x ↦ 2 * f x + c) := by mono

[Heather Macbeth]

(not actually recommended ...)

[Geoffrey Irving]

Right, but I think subset_refl is a valid mono lemma, not a random lemma.

[Geoffrey Irving]

Hmm, actually, should mono just use all refl lemmas? subset_refl is already marked refl.

[Heather Macbeth]

It seems like this wouldn't have very good performance!

[Geoffrey Irving]

Is adding subset_refl specifically to mono correct to do here?

[Heather Macbeth]

I don't really have a mental model of what monotonicity means for a heterogeneous "relation."

[Heather Macbeth]

Oh, but you're asking about subset_refl which is homogeneous ... so yes, I think so.

[Heather Macbeth]

(by analogy with le_refl, which is marked as such)

[Geoffrey Irving]

In the cases I'm working with there are two types X, Y that are twinned, in that there are a bunch of f : X \to X with a corresponding f' : Y \to Y. E.g., both have arithmetic. This is why I sensibly want something like mono in a heterogenous case.

[Heather Macbeth]

You could try removing the logic in the gcongr tagging that enforces LHS/RHS of same type, and see if it still works ...

[Geoffrey Irving]

https://github.com/leanprover-community/mathlib4/pull/9547 does attribute [mono] subset_refl