Problems with coercion and function subsets

Stream: general

[Tomas Skrivan]

Let's define a set of all constant functions

def is_constant (f : ℕ→ℕ) : Prop := ∀ n m, f n = f m

def const_fun := { f : ℕ → ℕ // is_constant f}

I want to work with f : const_fun as with a function, thus I define coercion to fun

@[reducible, inline] instance const_fun.has_coe_to_fun : has_coe_to_fun const_fun := has_coe_to_fun.mk _ subtype.val

Just a simple lemma testing that the coercion works

lemma lemma1 (f : const_fun) (n : ℕ) : f n = f.val n :=
begin
  simp,
end

Now, here is the bizarre thing, if you import import data.set then the proof by simp does not work anymore.

In the proof, simp changes goal from ⇑f n = f.val n to ⇑f n = ↑f n. What is going on here?

[Bryan Gin-ge Chen]

You can add set_option trace.simplify.rewrite true before your code to see what simp is doing in each case.

[Bryan Gin-ge Chen]

In this case, without the import, simp is using eq_self_iff_true, and with the import simp uses subtype.val_eq_coe.

[Bryan Gin-ge Chen]

You could write simp only [eq_self_iff_true] to get the proof to work with the import.

[Tomas Skrivan]

I'm too lazy to write simp only [eq_self_iff_true], I just want simp to work as expected.

The solution I have found is to do:

@[reducible, inline] def get_coe {α : Sort*} {p : α → Prop} (x : subtype p) : α := ↑x
@[reducible, inline] instance const_fun.has_coe_to_fun : has_coe_to_fun const_fun := has_coe_to_fun.mk _ get_coe

For some reason I have to define the auxiliary function get_coe, because simply writing

@[reducible, inline] instance const_fun.has_coe_to_fun : has_coe_to_fun const_fun := has_coe_to_fun.mk (λ _, ℕ→ℕ) (λ f, ↑f)

I get an error

error: failed to synthesize type class instance for
f : const_fun
⊢ has_lift_t const_fun (ℕ → ℕ)

[Reid Barton]

This is all rather unidiomatic

[Reid Barton]

You can prove lemma1 by refl, and I wouldn't recommend putting @[reducible, inline] on everything (I don't even know what @[inline] does). If you want simp to do specific things, then add simp lemmas.

[Tomas Skrivan]

The main problem is when I state some lemma, like ⇑f (⇑f n) = ⇑f 0 and then I'm proving another lemma by using simp. I can end up with a goal F ↑f (⇑f n) = F ⇑f 0 for some F : ℕ → ℕ . Now I'm in a trouble, if ⇑f and ↑f are not equal by definition then rewrite tactic has problem using my original lemma ⇑f (⇑f n) = ⇑f 0.

[Johan Commelin]

It looks to me like they are defeq, they are just not syneq.

[Floris van Doorn]

mathlib has a simp lemma that subtype.val is reduced to the coercion. That's why you get the ↑f. Add your own simp lemma stating that ↑f reduces to ⇑f, and you should be good. (You might have to state the lemma explicitly with docs#coe_subtype)