There are several types of numbers, and these can be arranged in two categories.
- The inductive types: nat, positive, Z, …
- the axiomatized types: R is the prominent one
The difference comes in how to compute with these numbers. If a type is inductive then we know how to describe simple rules of computation and force computations to reach simple forms, when these forms exist.
For instance, the Coq system knows that 3 and 1 + 1 + 1 compute to the same value.
In the case of the type R, the computation properties are only given as properties, and the inner layer of the Coq system does not have a clue that it should be using these computation properties. So, when it sees a number of the form 1 + 1 + 1 + 1, it does not know that it is one for which there could exist a simpler form.
Let’s compare two computations, one in Z and one in R.
First session:
Require Import ZArith. Open Scope Z_scope. Goal (10 + 5) * 10 + 2 = 152. Proof. compute.
At this point the goal is 152 = 152 the proof can obviously be finished for instance with the tactic easy.
Now let’s have another example with real numbers.
Require Import Reals. Open Scope R_scope. Goal (10 + 5) * 10 + 2 = 152. Proof. compute.
At this point, the goal becomes a huge formula that contains only the equality sign, additions, and multiplication. In a sense the formula is simpler because it uses only simple concepts, but in a sense it makes things more complex to the human eye. It feels like the natural rules of computation are not so natural after all.
From our mathematical knowledge, we know there are natural computation rules for real numbers, but simply these have not been given to the Coq system for use by the compute tactic. We need to use another tactic for this, it is called ring.
At the time of writing this post, it is necessary for Coq users to be aware of the difference between these two kinds of numbers.
