5
$\begingroup$

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?

$\endgroup$

2 Answers 2

3
$\begingroup$

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).

$\endgroup$
1
  • $\begingroup$ Ah, I had been trying to typecast with 2%R instead of 2%:R, this works. Thank you! $\endgroup$
    – BallBoy
    Jul 14 at 16:00
3
$\begingroup$

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.
$\endgroup$
5
  • $\begingroup$ 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"." $\endgroup$
    – BallBoy
    Jul 13 at 20:43
  • $\begingroup$ Ah, perhaps you don't have a recent enough version of mathcomp & rest... $\endgroup$ Jul 14 at 8:07
  • $\begingroup$ Could be! I just installed a couple weeks ago so I thought my version was newest... but perhaps not... $\endgroup$
    – BallBoy
    Jul 14 at 15:59
  • $\begingroup$ My mathcomp is 1.15.0, mathcomp-analysis 0.5.2 and mathcomp-algebra-tactics is 1.0.0. $\endgroup$ Jul 14 at 16:41
  • $\begingroup$ Update: upgraded and this worked! Thank you! $\endgroup$
    – BallBoy
    Jul 20 at 16:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.