# Zulip Chat Archive

## 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