http://gallica.bnf.fr/
*)
+(** @author The Coq Development Team *)
+
+
(* Un peu de calcul sur les rationnels...
Les opérations rendent des rationnels normalisés,
i.e. le numérateur et le dénominateur sont premiers entre eux.
*)
-type rational = {num:int;
- den:int}
-;;
+
+
+(** Type for coefficents *)
+type rational = {
+num:int; (** Numerator *)
+den:int; (** Denumerator *)
+};;
+
+(** Debug function.
+ @param x the rational to print*)
let print_rational x =
print_int x.num;
print_string "/";
let rec pgcd x y = if y = 0 then x else pgcd y (x mod y);;
-
+(** The constant 0*)
let r0 = {num=0;den=1};;
+(** The constant 1*)
let r1 = {num=1;den=1};;
let rnorm x = let x = (if x.den<0 then {num=(-x.num);den=(-x.den)} else x) in
else (let d=pgcd x.num x.den in
let d= (if d<0 then -d else d) in
{num=(x.num)/d;den=(x.den)/d});;
-
+
+(** Calculates the opposite of a rational.
+ @param x The rational
+ @return -x*)
let rop x = rnorm {num=(-x.num);den=x.den};;
+(** Sums two rationals.
+ @param x A rational
+ @param y Another rational
+ @return x+y*)
let rplus x y = rnorm {num=x.num*y.den + y.num*x.den;den=x.den*y.den};;
-
+(** Substracts two rationals.
+ @param x A rational
+ @param y Another rational
+ @return x-y*)
let rminus x y = rnorm {num=x.num*y.den - y.num*x.den;den=x.den*y.den};;
-
+(** Multiplyes two rationals.
+ @param x A rational
+ @param y Another rational
+ @return x*y*)
let rmult x y = rnorm {num=x.num*y.num;den=x.den*y.den};;
-
+(** Inverts arational.
+ @param x A rational
+ @return x{^ -1} *)
let rinv x = rnorm {num=x.den;den=x.num};;
-
+(** Divides two rationals.
+ @param x A rational
+ @param y Another rational
+ @return x/y*)
let rdiv x y = rnorm {num=x.num*y.den;den=x.den*y.num};;
let rinf x y = x.num*y.den < y.num*x.den;;
let rinfeq x y = x.num*y.den <= y.num*x.den;;
+
(* {coef;hist;strict}, où coef=[c1; ...; cn; d], représente l'inéquation
c1x1+...+cnxn < d si strict=true, <= sinon,
hist donnant les coefficients (positifs) d'une combinaison linéaire qui permet d'obtenir l'inéquation à partir de celles du départ.
!lie
;;
-(* donne [] si le système a des solutions,
+(* donne [] si le système a des find solutions,
sinon donne [c,s,lc]
où lc est la combinaison linéaire des inéquations de départ
qui donne 0 < c si s=true
ou 0 <= c sinon
cette inéquation étant absurde.
*)
+(** Tryes to find if the system admits solutions.
+ @param lie the list of inequations
+ @return a list that can be empty if the system has solutions. Otherwise it returns a
+ one elements list [\[(c,s,lc)\]]. {b c} is the rational that can be obtained solving the system,
+ {b s} is true if the inequation that proves that the system is absurd is of type [c < 0], false if
+ [c <= 0], {b lc} is a list of rational that represents the liear combination to obtain the
+ absurd inequation *)
let unsolvable lie =
let lr = deduce lie in
let res = ref [] in
deduce test2;;
unsolvable test2;;
-*)
\ No newline at end of file
+*)