What is wrong here? The proof in the finally won't work with any proof method even though the equation was just proven?

```
have "of_int_mod_ring (to_int_mod_ring (-x)) = -x"
using of_int_mod_ring_to_int_mod_ring[of "-x"] by simp
also have "… = - of_int_mod_ring (to_int_mod_ring x)"
using of_int_mod_ring_to_int_mod_ring[of x] by simp
finally have "of_int_mod_ring (to_int_mod_ring (-x)) = - of_int_mod_ring (to_int_mod_ring x)"
. sorry
```

Proof state:

```
proof (prove)
using this:
of_int_mod_ring (to_int_mod_ring (- x)) = - of_int_mod_ring (to_int_mod_ring x)
goal (1 subgoal):
1. of_int_mod_ring (to_int_mod_ring (- x)) = - of_int_mod_ring (to_int_mod_ring x)
Failed to apply initial proof method:
using this:
of_int_mod_ring (to_int_mod_ring (- x)) = - of_int_mod_ring (to_int_mod_ring x)
goal (1 subgoal):
1. of_int_mod_ring (to_int_mod_ring (- x)) = - of_int_mod_ring (to_int_mod_ring x)
```

The x is always of type " 'a mod_ring".

This is a typing problem. In your first to statements the return type of `of_int_mod_ring`

is fixed to `'a mod_ring`

, as you compare it with `-x`

. In the third statement, nothing forces the return type of `of_int_mod_ring`

to be `'a mod_ring`

. If you add the type information explicitly the proof finishes. For example like this

```
finally have "of_int_mod_ring (to_int_mod_ring (-x)) = (- of_int_mod_ring (to_int_mod_ring x) :: 'a mod_ring)
```

Thanks!

Katharina Kreuzer has marked this topic as resolved.

Last updated: Dec 07 2023 at 20:16 UTC