Library Coq.Numbers.Rational.SpecViaQ.QSig
Interface of a rich structure about rational numbers.
Specifications are written via translation to Q.
Module Type QType.
Parameter t : Type.
Parameter to_Q : t -> Q.
Notation "[ x ]" := (to_Q x).
Definition eq x y := [x] == [y].
Parameter of_Q : Q -> t.
Parameter spec_of_Q: forall x, to_Q (of_Q x) == x.
Parameter zero : t.
Parameter one : t.
Parameter minus_one : t.
Parameter spec_0: [zero] == 0.
Parameter spec_1: [one] == 1.
Parameter spec_m1: [minus_one] == -(1).
Parameter compare : t -> t -> comparison.
Parameter spec_compare : forall x y, compare x y = ([x] ?= [y]).
Definition lt n m := compare n m = Lt.
Definition le n m := compare n m <> Gt.
Definition min n m := match compare n m with Gt => m | _ => n end.
Definition max n m := match compare n m with Lt => m | _ => n end.
Parameter eq_bool : t -> t -> bool.
Parameter spec_eq_bool : forall x y,
if eq_bool x y then [x]==[y] else ~([x]==[y]).
Parameter red : t -> t.
Parameter spec_red : forall x, [red x] == [x].
Parameter strong_spec_red : forall x, [red x] = Qred [x].
Parameter add : t -> t -> t.
Parameter spec_add: forall x y, [add x y] == [x] + [y].
Parameter sub : t -> t -> t.
Parameter spec_sub: forall x y, [sub x y] == [x] - [y].
Parameter opp : t -> t.
Parameter spec_opp: forall x, [opp x] == - [x].
Parameter mul : t -> t -> t.
Parameter spec_mul: forall x y, [mul x y] == [x] * [y].
Parameter square : t -> t.
Parameter spec_square: forall x, [square x] == [x] ^ 2.
Parameter inv : t -> t.
Parameter spec_inv : forall x, [inv x] == / [x].
Parameter div : t -> t -> t.
Parameter spec_div: forall x y, [div x y] == [x] / [y].
Parameter power : t -> Z -> t.
Parameter spec_power: forall x z, [power x z] == [x] ^ z.
End QType.
NB: several of the above functions come with ..._norm variants
that expect reduced arguments and return reduced results.
TODO : also speak of specifications via Qcanon ...