## Stream: Beginner Questions

### Topic: divide

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

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

#### 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}"
``````

#### Mathias Fleury (Apr 27 2021 at 04:30):

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

Last updated: Aug 10 2022 at 20:22 UTC