simp and subrel

Stream: mathlib4

[Violeta Hernández]

Writing Subrel r {x | p x} does not seem to interact well with simp.

import Mathlib.Order.RelIso.Set

/-- Avoid the `Set.setOf_true` simp suggestion. -/
def tt : Prop := True

/-- Example. -/
@[simps!]
def ex : (· < · : ℕ → ℕ → Prop) ↪r Subrel (· < ·) { _x : ℕ | tt } where
  toFun := fun a ↦ ⟨a, ⟨⟩⟩
  inj' _ _ h := Subtype.ext_iff.1 h
  map_rel_iff' := Iff.rfl

-- Found 1 error in 3 declarations (plus 4 automatically generated ones) in the current file with 15 linters

/- The `simpNF` linter reports:
SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.
see note [simp-normal form] for tips how to debug this.
https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form -/
#check ex_apply_coe /- Left-hand side simplifies from
  ↑(ex a)
to
  ↑(ex a)
using
  dsimp only [@Set.mem_setOf_eq, @Set.coe_setOf]
Try to change the left-hand side to the simplified term!
 -/
#lint

[Violeta Hernández]

Specifically, what seems to happen is that the type signature of the subrelation reads ↑{_x | tt} → ↑{_x | tt} → Prop, and simp wants this to be written as {_x // tt} → {_x // tt} → Prop instead

[Violeta Hernández]

This works perfectly:

import Mathlib.Order.RelIso.Set

/-- Avoid the `Set.setOf_true` simp suggestion. -/
def tt : Prop := True

/-- Subrelation. -/
def MySubrel {α : Type*} (r : α → α → Prop) (p : α → Prop) : { x // p x } → { x // p x } → Prop :=
  Subrel r (setOf p)

/-- Example. -/
@[simps!]
def ex : (· < · : ℕ → ℕ → Prop) ↪r MySubrel (· < ·) (fun _ : ℕ ↦ tt) where
  toFun := fun a ↦ ⟨a, ⟨⟩⟩
  inj' _ _ h := Subtype.ext_iff.1 h
  map_rel_iff' := Iff.rfl

-- Found 0 errors in 4 declarations (plus 4 automatically generated ones) in the current file with 15 linters
-- All linting checks passed!
#lint

[Violeta Hernández]

Would it make sense to change the type signature of Subrel to match? Or does that introduce other problems?

[Violeta Hernández]

...actually, that'd probably be a hell of a refactor

[Violeta Hernández]

Is there any simpler alternative to get this to work?

[Violeta Hernández]

In this example, specifying the types in RelEmbedding explicitly works

import Mathlib.Order.RelIso.Set

/-- Avoid the `Set.setOf_true` simp suggestion. -/
def tt : Prop := True

/-- Example. -/
@[simps!]
def ex : @RelEmbedding ℕ { _x : ℕ // tt} (· < ·) (Subrel (· < ·) _) where
  toFun := fun a ↦ ⟨a, ⟨⟩⟩
  inj' _ _ h := Subtype.ext_iff.1 h
  map_rel_iff' := Iff.rfl

-- Found 0 errors in 3 declarations (plus 4 automatically generated ones) in the current file with 15 linters
-- All linting checks passed!
#lint

[Eric Wieser]

(docs#Subrel)

[Daniel Weber]

Violeta Hernández said:

Would it make sense to change the type signature of Subrel to match? Or does that introduce other problems?

Violeta Hernández said:

...actually, that'd probably be a hell of a refactor

Subrel doesn't seem to be used in many places (https://github.com/search?q=repo%3Aleanprover-community%2Fmathlib4+Subrel&type=code&p=1), and most applications of it are with setOf, so I think it could make sense to change its type signature