There are several types of numbers, and these can be arranged in two categories.<\/p>\n
The difference comes in how to compute with these numbers. If a type is inductive<\/i> then we know how to describe simple rules of computation and force computations to reach simple forms, when these forms exist.
\nFor instance, the Coq system knows that 3<\/tt> and 1 + 1 + 1<\/tt> compute to the same value.<\/p>\n
In the case of the type R<\/tt>, the computation properties<\/i> 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<\/tt>, it does not know that it is one for which there could exist a simpler form.<\/p>\n
Let’s compare two computations, one in Z<\/tt> and one in R<\/tt>.<\/p>\n
First session:<\/p>\n
\r\nRequire Import ZArith.\r\n\r\nOpen Scope Z_scope.\r\n\r\nGoal (10 + 5) * 10 + 2 = 152.\r\nProof.\r\ncompute.\r\n<\/pre>\nAt this point the goal is 152 = 152 <\/tt> the proof can obviously be finished for instance with the tactic easy<\/tt>.<\/p>\n
Now let’s have another example with real numbers.<\/p>\n
\r\nRequire Import Reals.\r\n\r\nOpen Scope R_scope.\r\n\r\nGoal (10 + 5) * 10 + 2 = 152.\r\nProof.\r\ncompute.\r\n<\/pre>\nAt 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<\/i> rules of computation are not so natural after all.<\/p>\n
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<\/tt> tactic. We need to use another tactic for this, it is called ring<\/tt>.<\/p>\n
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.<\/p>\n","protected":false},"excerpt":{"rendered":"
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\u2026<\/p>\n