I am examining the following theory in Isabelle2020 /jEdit:
theory Sqrt
imports Complex_Main "HOL-Computational_Algebra.Primes"
begin
theorem
assumes "prime (p::nat)"
shows "sqrt p ∉ ℚ"
proof
from ‹prime p› have p: "1 < p" by (simp add: prime_nat_iff)
assume "sqrt p ∈ ℚ"
then obtain m n :: nat where
n: "n ≠ 0" and sqrt_rat: "¦sqrt p¦ = m / n"
and "coprime m n" by (rule Rats_abs_nat_div_natE)
[we omit the remainder of the proof]
The Output pane shows proof state:
have (⋀m n. n ≠ 0 ⟹ ¦sqrt (real p)¦ = real m / real n ⟹ coprime m n ⟹ ?thesis) ⟹ ?thesis
proof (state)
this:
n ≠ 0
¦sqrt (real p)¦ = real m / real n
coprime m n
goal (1 subgoal):
1. sqrt (real p) ∈ ℚ ⟹ False
My question is: Are those appearances of "real" a type coercion? I have read Chapter 8 discussing types in the so-called tutorial that accompanies the Isabelle distribution (title A Proof Assistant for Higher-Order Logic). I read Florian Haftman's document title Isabelle/HOL type-class hierarchy (also part of the Isabelle distribution). The rule used in the theory statements above, Rats_abs_nat_div_natE, is a lemma in the Real.thy theory.
I chased down the reference in that theory file and looked at §8.4.5 in A Proof
Assistant for Higher-Order Logic where I found that The natural
number type nat is a linearly ordered semiring, type int is an ordered ring,
and type real is an ordered field. Properties may not hold for a particular class, e.g., no abstract properties involving subtraction hold for type nat (since, of course, one might end up with a negative number, which would not be a natural number). Instead specific theorems are provided addressing subtraction on the type nat. More to the point, “all abstract properties involving division require a field." (A Proof Assistant for Higher-Order Logic.)
So, are we are seeing here a quotient type being used to lift a division of natural or integer types to the abstract real type in order to satisfy the field
requirement (see §11.9 The Isabelle/Isar Reference Manual)? The quotient type real is created from the equivalence relation definition realrel in the Real.thy file.
I was surprised to see real terms in a proof depending on primes, positive integers, and rational numbers and wanted to assure that I had at least gotten close to the explanation why this is occuring in the Isabelle proof.
The function sqrt is only defined over reals. Therefore, you need to convert its argument p from nat to real. There is a coercion that does that automatically for you; hence the real function you can.
After that, the only way to type m/n is real m / real n.
Generally, overloaded syntax is a problematic for proof assistants. For example, 2/3 on paper can be the rational number Fract 2 3 in Isabelle, the real number 2/3, or the inverse of 3 in a F_5 multiplied by two, or something else.
In Isabelle this is solved by (to a certain extend) avoiding overloading and using different notations.