Coq Real numbers -lexing and parsing 3.14

Question

With Reals library imported

Require Import Reals.

How can I define constants such as 3.14 or 10.1 and use them for function definition or computation ?

Answer 1

You can define your constants like so:

Definition a := 10 + /10.
Definition b := 3 + 14/100.

Note, however, that the standard library defines reals axiomatically. You can find the main definitions here. Observe that the definitions are given as Parameters, which is a synonym for Axiom. For instance, R0 and R1 stand for the real numbers 0 and 1, Rplus and Rmult represent addition and multiplication, but those definitions are not inductive datatypes and functions as they lack definitions. To be able to deal with reals we need axioms, governing the interactions between them (given here).

You can think of the real numbers in the standard library as ASTs, made with nodes marked R0, R1, Rplus, and so on. And you are given some rules (axioms) which specify the (only) transformations you can perform on those ASTs.

Let's see how Coq represents real numbers:

Require Import Coq.Reals.Reals.
Local Open Scope R_scope.
Unset Printing Notations.
Check 5+/2  (* 5½ *).

(*
Rplus (Rplus R1
             (Rmult (Rplus R1 R1)
                    (Rplus R1 R1)))
      (Rinv (Rplus R1 R1)).
i.e. (1 + (1 + 1) * (1 + 1)) + (1 + 1)⁻¹ 
*)

Among the consequences of this axiomatic approach there is the fact that the following goal cannot be proved by reflexivity anymore (as it could be done for nats in an analogous situation):

Set Printing Notations.
Goal a = 9 + 1 + /10.
  Fail reflexivity.

This fails because the ASTs (terms) on the both sides of the equality are different and Coq doesn't convert them to some canonical values to compare them at the end. This time we need to show that the two ASTs are mutually convertible.

  enough (9 + 1 = 10).
  - now rewrite H.

Now we need to prove 9 + 1 = 10:

  - rewrite Rplus_comm, <-Rplus_assoc.
    rewrite <-(Rmult_1_r 2) at 1.
    rewrite <-Rmult_plus_distr_l.
    reflexivity.

Fortunately for us there is a tactic, which can do this tedious job for us:

    Restart.
    unfold a; field.
Qed.

The standard library approach is not the only one possible, however. This answer by @gallais can help you with exploring your other options.