# Basics of real numbers in mathcomp (Coq)

I'm trying to play around with the Mathematical Components library in Coq but am having trouble writing basic, concrete statements about real numbers. E.g., I'd like to define

Definition add_two_and_a_half (x : R) : R := x + (2 + 1/2).


and then prove

Lemma six_and_two_and_a_half_make_eight_and_a_half : add_two_and_a_half 6 = (8 + 1/2)%R.


This works fine if I use the Coq.Reals.Reals library, but once I introduce mathcomp the lemma no longer goes through. What are some ways I can make this work?

## 2 Answers

Assuming you have opened ring_scope, for instance with

Local Open Scope ring_scope.


you can use 2%:R to mean the constant 2 in a ring instead of nat (or use MathComp >= 1.15.0 where 2 should work).

• Ah, I had been trying to typecast with 2%R instead of 2%:R, this works. Thank you! Jul 14, 2022 at 16:00

This should work:

From mathcomp Require Import all_ssreflect all_algebra ssralg ssrint ssrnum.
From mathcomp.analysis Require Import reals.
From mathcomp.algebra_tactics Require Import ring.

Variable R: realType.

Definition add_two_and_a_half (x : R) : R := x + (2 + 1/2).

Lemma six_and_two_and_a_half_make_eight_and_a_half : add_two_and_a_half 6 = (8 + 1/2)%R.
Proof.
unfold add_two_and_a_half.
by ring.
Qed.

• Thanks! The definition of add_two_and_a_half still doesn't go through -- "The term "2" has type "nat" while it is expected to have type "GRing.Zmodule.sort ?V"." Jul 13, 2022 at 20:43
• Ah, perhaps you don't have a recent enough version of mathcomp & rest... Jul 14, 2022 at 8:07
• Could be! I just installed a couple weeks ago so I thought my version was newest... but perhaps not... Jul 14, 2022 at 15:59
• My mathcomp is 1.15.0, mathcomp-analysis 0.5.2 and mathcomp-algebra-tactics is 1.0.0. Jul 14, 2022 at 16:41
• Update: upgraded and this worked! Thank you! Jul 20, 2022 at 16:23