request clarification on appearance of apparent real coercion in theory involving natural numbers in Isabelle theory

Question

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.

Mathias Fleury Mathias Fleury · Accepted Answer · 2021-01-22T06:24:17

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.

request clarification on appearance of apparent real coercion in theory involving natural numbers in Isabelle theory

1 Answers