Nonconfluent simp for `↑{x | True}`

Stream: mathlib4

[Jovan Gerbscheid]

Although there is Set.coe_setOf {α : Type u} (p : α → Prop) : ↑{x | p x} = { x // p x }, the following fails:

example : ↑{x : α | True} = {x : α // True} := by
  /-
  unsolved goals

  α : Type u_1
  ⊢ ↑Set.univ = { x // True }
  -/
  simp

I ran into this when trying to show that Nat.card {x : Fin n // True} = n.

Should there be a simp lemma for rewriting { x // True } into ↑Set.univ?

[Kevin Buzzard]

This is equality of types so it makes me feel a bit queezy.

[Ruben Van de Velde]

Me too, though apparently this case is supported? It seems to be a simp confluence issue; simp [-Set.setOf_true] solves the original goal

[Jovan Gerbscheid]

Here's what I was looking at:

example : {s : Fin 19 → Fin 2 | ∀ n : Fin 19, 10 ≤ n.val → s n = 0}.ncard = 2 ^ 10 := by
    rw [← Set.Nat.card_coe_set_eq, Set.coe_setOf,
      Nat.card_congr <| @Equiv.subtypePiEquivPi (Fin 19) _ fun n i => 10 ≤ n.val → i = 0]
    rw [Nat.card_pi, Fin.prod_univ_add (a := 10) (b := 9)]
    simp
    rfl

This proof works, but it breaks down when replacing 2 by 200, because the rfl at the end can't expand that much.

And the only reason for working with types instead of sets was that there seems to be no equivalent to Equiv.subtypePiEquivPi that works with sets. Unfortunately I can't manage to rewrite back to the setOf representation, because I can't rewrite under a binder, and simp_rw [← Set.coe_setOf] gets stuck in a loop.

[Eric Wieser]

I would guess the answer is to add a Set version of Equiv.subtypePiEquivPi

[Jovan Gerbscheid]

Another point about Equiv.subtypePiEquivPi is that, similar to Classical.skolem, it contains a term that usually can't be figured out by unifiication, namely the p a (f a) in { f : (a : α) → β a // ∀ (a : α), p a (f a) }. Should the p be made an explicit parameter? (in Classical.skolem, it is not so bad because the lemma is the other way around, with the bad term on the rhs)

[Jovan Gerbscheid]

Or even better could there be some hint to the unification algorithm for how to deal with such unifications? The difficulty is that the term f a is not a single free variable, so it can't be abstracted as easily.

[Daniel Weber]

Kevin Buzzard said:

This is equality of types so it makes me feel a bit queezy.

As long as it stays defeq it's fine, I think

[Jovan Gerbscheid]

The way you would usually encounter {x // True} in simp is by running simp on {x // some complicated expression}. So simp would already do some non-defeq rewrites of this type. At that point the defeq rewrite into ↑Set.univ is not much to worry about.

[Daniel Weber]

Does simp do non-defeq rewrites in types?

[Jovan Gerbscheid]

Yes:

example : {x:Nat // n = n} = {x:Nat // True} := by
  simp

[Daniel Weber]

That's not a type here, it's only a term. For example:

example : Function.const {x:Nat // n = n} 1 ⟨1,rfl⟩ = Function.const {x:Nat // True} 1 ⟨1,.intro⟩ := by
  fail_if_success simp [-Function.const_apply]
  sorry

[Jovan Gerbscheid]

Wait, I thought a term x is a type if and only if x : Type _ holds.

[Daniel Weber]

It is a type, I meant "in contexts where it's a type of some other term"

[Jovan Gerbscheid]

But if I add this simp lemma, it does (defeq) simp the type:

import Mathlib

@[simp]
theorem subtype_true (α : Type) : {_x : α // True} = ↑(@Set.univ α) := rfl

example : Function.const {x:Nat // n = n} 1 ⟨1,rfl⟩ = Function.const {x:Nat // True} 1 ⟨1,.intro⟩ := by
  simp [-Function.const_apply]

[Daniel Weber]

(it's using Function.const_one since you imported Mathlib)

[Jovan Gerbscheid]

Oh oops, it doesn't

[Daniel Weber]

it does use it

import Mathlib

@[simp]
theorem subtype_true (α : Type) : {_x : α // True} = ↑(@Set.univ α) := rfl

example : Function.const {x:Nat // n = n} 1 ⟨1,rfl⟩ = Function.const {x:Nat // True} 1 ⟨1,.intro⟩ := by
  simp? [-Function.const_apply, -Function.const_one] says simp only [subtype_true]

[Daniel Weber]

in any case, that's my point - it only does dsimp on types, I think

[Jovan Gerbscheid]

Hmm, then would it make sense to tag this lemma as a non-dsimp lemma? And is that even possible?

[Daniel Weber]

I think that happens if the proof isn't literally rfl

[Jovan Gerbscheid]

Then should this lemma be added with the proof id rfl?

[Kyle Miller]

Daniel Weber said:

Does simp do non-defeq rewrites in types?

It's not about types vs terms, but which arguments are dependent on what. In Jovan's rewriting types in an equality example, there's no dependence in @Eq X a b for a and b, but X is depended upon. Types are commonly depended upon, but there are plenty of examples where terms are depended upon. In general, simp falls back to dsimp for arguments that are depended upon, with some exceptions (for example, if it's a proof or a Decidable instance that's the dependent, simp has a procedure to use the full simp procedure anyway).

[Kyle Miller]

For what it's worth, I've found simp lemmas that go between subtypes and coerced sets to cause issues. In the past, it made me think that they should not be simp lemmas at all, and they should be opt-in.

The alternative is to commit to choosing, for example, coerced sets to be the simp normal form for subtypes in general, and to never use subtypes directly.

[Jovan Gerbscheid]

Would there be any disadvantage to comitting to coerced set notation as the default, and banishing any occurrences of {x // _} from Mathlib?

[Kyle Miller]

Not sure. I floated this idea once awhile back, but I don't remember much agreement, and it seems like a lot of work. (Assuming no complications, I would think this would be a big improvement to normalize!)

[Jovan Gerbscheid]

The only thing that worried me a bit is that the definitional equality of the types doesn't hold in reducible transparency, but I don't think this is a problem.

[Jovan Gerbscheid]

I also noticed a discrepancy in the pretty printer: it shows {a | True}, but { a // True } has extra spaces