On fractions

Every strictly positive rational number can be obtained in a unique manner by a succession of applications of functions N and D on the number 1, where N and D are defined by the following equations:

N(x) = 1 + x
D(x) =  1
       ------
           1
       1 + -
           x

We can associate any strictly positive rational number to an element of an inductive type with one constructor for one, and two other constructors representing the functions N and D.
Define this inductive type.

Build the function that takes an element of this type defined and returns the numerator and denominator of the corresponding reduced fraction.

Solution

This file

Note: this file solution contains also a proof that the fraction we compute is irreducible. We admit Bezout's equality. Notice that we use techniques described in the chapter devoted to inductive predicates

Going home

Pierre Castéran