## Stream: general

### Topic: Problems with coercion and function subsets

#### Tomas Skrivan (Oct 21 2020 at 23:54):

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 (Oct 21 2020 at 23:59):

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 (Oct 22 2020 at 00:00):

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 (Oct 22 2020 at 00:00):

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

#### Tomas Skrivan (Oct 22 2020 at 01:09):

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 (Oct 22 2020 at 01:12):

This is all rather unidiomatic

#### Reid Barton (Oct 22 2020 at 01:18):

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 (Oct 22 2020 at 01:23):

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 (Oct 22 2020 at 03:24):

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

#### Floris van Doorn (Oct 22 2020 at 21:28):

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)

Last updated: Aug 03 2023 at 10:10 UTC