Email Gateway (Mar 20 2025 at 12:02): Email Gateway (Mar 20 2025 at 12:02):From: Lawrence Paulson <lp15@cam.ac.uk>
Consider the following function definition:
lemma "quotient_of (rat_of_nat i) = (i, 1)"
Here i has type nat while the result type of quotient_of is int*int, so the right hand side needs the coercion int to be inserted. The lemma is seemingly equivalent to
lemma "quotient_of (rat_of_nat i) = (int i, 1)"
But in fact what Isabelle displays is
quotient_of (rat_of_nat i) = (case (i, 1) of (x, y) ⇒ (int x, y))
Unexpected, to say the least!
Larry
Email Gateway (Mar 20 2025 at 14:12):From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Hi Larry,
This is a recurrent question, and I recall that you and me already had some discussions about coercions in the past.
The guarantee of the coercion inference is two-fold
There is no guarantee where coercions will be inserted (and this behavior is not easily amended without compromising the prior completeness statement).
Thus you may or may not get the resulting well-typed term that you expect. (In your example, the two are equivalent, but in general they of course might even mean different things; coercion inference is purely syntactic.) The best way to avoid any surprises is still to write well-typed terms.
Dmitriy
On 20 Mar 2025, at 13.01, Lawrence Paulson <lp15@cam.ac.uk> wrote:
Consider the following function definition:
lemma "quotient_of (rat_of_nat i) = (i, 1)"
Here i has type nat while the result type of quotient_of is int*int, so the right hand side needs the coercion int to be inserted. The lemma is seemingly equivalent to
lemma "quotient_of (rat_of_nat i) = (int i, 1)"
But in fact what Isabelle displays is
quotient_of (rat_of_nat i) = (case (i, 1) of (x, y) ⇒ (int x, y))
Unexpected, to say the least!
Larry
Last updated: Apr 17 2025 at 20:22 UTC