Stream: Beginner Questions

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

view this post on Zulip 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".

view this post on Zulip 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_ringis 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)

view this post on Zulip Katharina Kreuzer (Sep 21 2021 at 08:56):

Thanks!

view this post on Zulip Notification Bot (Sep 21 2021 at 08:57):

Katharina Kreuzer has marked this topic as resolved.

Last updated: Apr 23 2024 at 20:15 UTC