Subtype.prop as a simp lemma

Stream: mathlib4

[Wrenna Robson]

Why do we not have Subtype.prop as a simp lemma? Does it add major performance issues? It seems like a thing that would be useful but maybe that is naive.

[Kenny Lau]

Probably because it's impossible to apply

[Kenny Lau]

you can't infer the correct term of the subtype

[Wrenna Robson]

Right. It's just that if I already have an x : Subtype p in my context, I would quite like simp to know that p ↑x so it can apply lemmas with that as a hypothesis.

[Kenny Lau]

huh i tried to make an example to show this but it works in my example!

structure Is37 : Type where
  val : Nat
  eq : val = 37

instance : Coe Is37 Nat where
  coe := Is37.val

@[simp] theorem Is37.coe_eq_37 (n : Is37) : (n : Nat) = 37 := n.eq

theorem foo (n : Is37) : (n : Nat) = 37 := by simp only [Is37.coe_eq_37]

[Wrenna Robson]

Hmm. What about {x : Subtype (¬ p ·)} - does it know that \not p ↑x?

[Yaël Dillies]

Subtype.prop unfortunately has a metavariable as head symbol, so it would have terrible performance most likely

[Wrenna Robson]

And I assume there's no way of fixing/avoiding that really?

[Wrenna Robson]

Broadly I am finding that the following very stupid lemmas might have a use.

variable {β : Sort*} {p : β → Prop} [DecidablePred p]

@[simp]
theorem dite_of_subtype {x : Subtype p} {t : p x → α} {e : ¬p x → α} :
  (if h : p x then t h else e h) = t x.prop := dif_pos x.2

@[simp]
theorem dite_of_subtype_not {x : Subtype (¬ p ·)} {t : p x → α} {e : ¬ p x → α} :
  (if h : p x then t h else e h) = e x.2 := dif_neg x.2

[Wrenna Robson]

Which feels real stupid. But simp kinda can't deal with that normally.

[Kenny Lau]

@Wrenna Robson but the lemmas you now proposed here are different from the general subtype prop lemma you asked in the beginning

[Wrenna Robson]

No, absolutely, but I was wondering if I was missing something and there was a simpler lemma that would be better.

[Aaron Liu]

It seems to work?

import Mathlib.Data.Subtype

example : type_of% @Subtype.prop := by
  simp

[Wrenna Robson]

Hmm!

[Edward van de Meent]

that's different though, if you check simp? you'll see why

[Edward van de Meent]

in particular, the current issue is having simp work after intros in your example

[Wrenna Robson]

In what sense?

[Edward van de Meent]

in the sense that the above simp acts on \all x:{a// p a}, foo x rather than on foo x with x : {a//p a}

[Wrenna Robson]

My dite_of_subtype?

[Wrenna Robson]

It does seem to work for me after intros.

[Edward van de Meent]

i think Aaron meant that the example works with current mathlib, and i wanted to point out that that's only before intros and when the subtype value is a variable. i wasn't commenting on your dite_of_subtype

[Wrenna Robson]

aha, thanks