Stream: Beginner Questions

Topic: divide


view this post on Zulip zibo yang (Apr 26 2021 at 16:08):

when I code like:

lemma delta2:"b^2 / a^2 = (b / a)^2"
proof-
  have "b*b / (a*a) = (b / a)*(b / a)"
    using
          Fields.field_class.times_divide_times_eq[of b a b a]
    by auto

why does it fail like:

Type unification failed: Variable 'b::{inverse,power} not of sort field

Failed to meet type constraint:

Term:  b :: 'b
Type:  ??'a

Coercion Inference:

Local coercion insertion on the operand failed:
Variable 'b::{inverse,power} not of sort field

Now trying to infer coercions globally.

Coercion inference failed:
sort mismatch

can someone explain the description here?

view this post on Zulip Mathias Fleury (Apr 27 2021 at 04:28):

Types have so-called sorts, which are extra-constraints over types. Isabelle computes the minimum required types and sorts to type a lemma.

Here the type'b has sorts inverse (this is required to have division) and power (because of the ^2). However you want to apply the theorem field_class.times_divide_times_eq that only works when 'b has also the sort field (i.e., when 'b is a field).

view this post on Zulip Mathias Fleury (Apr 27 2021 at 04:30):

The solution is to be more explicit about sorts:

lemma delta2:"b^2 / a^2 = ((b::'b :: {field,power}) / a)^2"

or

lemma delta2:"b^2 / a^2 = (b / a)^2" for b:: "'b :: {field,power}"

view this post on Zulip Mathias Fleury (Apr 27 2021 at 04:30):

(untested but if you need the inverse, you know how to add it too)


Last updated: Sep 25 2021 at 09:17 UTC