## Stream: Beginner Questions

### Topic: ✔ using "term t" prove "term t" not working

#### Katharina Kreuzer (Sep 21 2021 at 08:23):

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".

#### Simon Roßkopf (Sep 21 2021 at 08:51):

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!

#### Notification Bot (Sep 21 2021 at 08:57):

Katharina Kreuzer has marked this topic as resolved.

Last updated: Dec 07 2023 at 20:16 UTC