zibo yang (Apr 26 2021 at 16:08): 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}"
(untested but if you need the inverse, you know how to add it too)
Last updated: Apr 27 2024 at 01:05 UTC