This file is part of CoqEAL, the Coq Effective Algebra Library.
(c) Copyright INRIA and University of Gothenburg, see LICENSE
Add LoadPath "../
theory".
Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp.
Require Import path choice fintype tuple finset ssralg bigop ssrint ssrnum rat.
Require Import refinements pos hrel.
Non-normalized rational numbers refinest SSReflects rational numbers (rat)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Local Open Scope ring_scope.
Import GRing.Theory Num.Theory Refinements.Op AlgOp.
PART I: Defining datastructures and programming with them
Section Q.
Variable Z P :
Type.
Definition Q := (
Z *
P)%
type.
Section Q_ops.
Local Open Scope computable_scope.
Context `{
zero Z,
one Z,
add Z,
opp Z,
mul Z,
eq Z,
leq Z,
lt Z}.
Context `{
one P,
sub P,
add P,
mul P,
eq P,
leq P,
lt P}.
Context `{
cast_class P Z,
cast_class Z P}.
Context `{
spec_of Z int,
spec_of P pos}.
Global Instance zeroQ :
zero Q := (0, 1).
Global Instance oneQ :
one Q := (1, 1).
Global Instance addQ :
add Q :=
fun x y =>
(
x.1 *
cast y.2 +
y.1 *
cast x.2,
x.2 *
y.2).
Global Instance mulQ :
mul Q :=
fun x y => (
x.1 *
y.1,
x.2 *
y.2).
Global Instance oppQ :
opp Q :=
fun x => (-
x.1,
x.2).
Global Instance eqQ :
eq Q :=
fun x y => (
x.1 *
cast y.2 ==
y.1 *
cast x.2).
Global Instance leqQ :
leq Q :=
fun x y => (
x.1 *
cast y.2 <=
y.1 *
cast x.2).
Global Instance ltQ :
lt Q :=
fun x y => (
x.1 *
cast y.2 <
y.1 *
cast x.2).
Global Instance invQ :
inv Q :=
fun x =>
if (
x.1 == 0)%
C then 0
else if (0 <
x.1)
then (
cast x.2,
cast x.1)
else (- (
cast x.2),
cast (-
x.1)).
Global Instance subQ :
sub Q :=
fun x y => (
x + -
y).
Global Instance divQ :
div Q :=
fun x y => (
x *
y^-1).
Global Instance expQnat :
exp Q nat :=
fun x n =>
iter n (
mulQ x) 1.
Global Instance cast_ZQ :
cast_class Z Q :=
fun x => (
x, 1).
Global Instance cast_PQ :
cast_class P Q :=
fun x =>
cast (
cast x :
Z).
End Q_ops.
End Q.
PART II: Proving the properties of the previous objects
Section Qint.
Instance zero_int :
zero int := 0%
R.
Instance one_int :
one int := 1%
R.
Instance add_int :
add int := +%
R.
Instance opp_int :
opp int := -%
R.
Instance mul_int :
mul int := *%
R.
Instance eq_int :
eq int :=
eqtype.eq_op.
Instance leq_int :
leq int :=
Num.le.
Instance lt_int :
lt int :=
Num.lt.
Instance one_pos :
one pos :=
posS 0.
Instance add_pos :
add pos :=
fun m n =>
insubd (
posS 0) (
val m +
val n)%
N.
Instance sub_pos :
sub pos :=
fun m n =>
insubd (
posS 0) (
val m -
val n)%
N.
Instance mul_pos :
mul pos :=
fun m n =>
insubd (
posS 0) (
val m *
val n)%
N.
Instance leq_pos :
leq pos :=
fun m n => (
val m <=
val n)%
N.
Instance lt_pos :
lt pos :=
fun m n => (
val m <
val n)%
N.
Instance eq_pos :
eq pos :=
eqtype.eq_op.
Instance cast_pos_int :
cast_class pos int :=
pos_to_int.
Instance cast_int_pos :
cast_class int pos :=
int_to_pos.
Local Notation Qint := (
Q int pos).
Lemma absz_denq_gt0 r : (0 < `|
denq r|)%
N.
Proof.
by rewrite absz_gt0 denq_eq0. Qed.
Definition rat_to_Qint (
r :
rat) :
Qint := (
numq r,
pos_of (
absz_denq_gt0 r)).
Definition Qint_to_rat (
r :
Qint) :
rat := (
r.1%:
Q / (
val r.2)%:
Q).
Lemma Qrat_to_intK :
cancel rat_to_Qint Qint_to_rat.
Proof.
by move=> x; rewrite /Qint_to_rat /= absz_denq divq_num_den. Qed.
Definition Rrat :
rat ->
Q int pos ->
Prop :=
fun_hrel Qint_to_rat.
Lemma RratE (
x :
rat) (
a :
Qint) :
param Rrat x a ->
x =
a.1%:~
R / (
val a.2)%:~
R.
Proof.
by rewrite paramE => <-. Qed.
Instance Rrat_0 :
param Rrat 0 0%
C.
Proof.
by rewrite paramE. Qed.
Instance Rrat_1 :
param Rrat 1 1%
C.
Proof.
by rewrite paramE. Qed.
Instance Rrat_embed :
param (
Logic.eq ==>
Rrat)
intr cast.
Proof.
rewrite paramE => n _ <-.
by rewrite /Rrat /Qint_to_rat /fun_hrel /= mulr1.
Qed.
Definition pos_to_rat (
x :
pos) :
rat := (
val x)%:
R.
Instance Rrat_embed_pos :
param (
Logic.eq ==>
Rrat)
pos_to_rat cast.
Proof.
rewrite paramE => n _ <-.
rewrite /Rrat /Qint_to_rat /fun_hrel /pos_to_rat /= mulr1.
by rewrite /cast /cast_pos_int /pos_to_int natz.
Qed.
Instance Rrat_add :
param (
Rrat ==>
Rrat ==>
Rrat) +%
R +%
C.
Proof.
apply param_abstr2 => x [na [da da_gt0]] rx y [nb [db db_gt0]] ry.
rewrite paramE /Rrat /fun_hrel /Qint_to_rat /= /cast /cast_pos_int /=.
rewrite /pos_to_int /mul_op /mul_pos /mul_int /add_op /add_int /=.
rewrite val_insubd muln_gt0 da_gt0 db_gt0 /=.
rewrite [x]RratE [y]RratE /= addf_div ?intr_eq0 -?lt0n //.
by rewrite ?dom_Rrat ?(rmorphD, rmorphM) //= PoszM intrM !natz.
Qed.
Instance Rrat_opp :
param (
Rrat ==>
Rrat) -%
R -%
C.
Proof.
apply param_abstr => x a rx; rewrite paramE /Rrat /fun_hrel /Qint_to_rat /=.
by rewrite /opp_op /opp_int [x]RratE -mulNr rmorphN.
Qed.
Instance Rrat_mul :
param (
Rrat ==>
Rrat ==>
Rrat) *%
R *%
C.
Proof.
apply param_abstr2 => x [na [da da_gt0]] rx y [nb [db db_gt0]] ry.
rewrite paramE /Rrat /fun_hrel /Qint_to_rat /= /mul_op /mul_int /mul_pos /=.
rewrite val_insubd muln_gt0 da_gt0 db_gt0 /=.
rewrite [x]RratE [y]RratE mulrACA -invfM ?(rmorphD, rmorphM) /=.
by rewrite PoszM rmorphM /=.
Qed.
Instance Rrat_expnat :
param (
Rrat ==>
Logic.eq ==>
Rrat) (@
GRing.exp _)
exp_op.
Proof.
apply param_abstr2 => x a rx y n; rewrite !paramE => -> {y}.
by elim: n => //= n ihn; rewrite exprS [x * x ^+ n]RratE.
Qed.
Instance Rrat_inv :
param (
Rrat ==>
Rrat)
GRing.inv inv_op.
Proof.
apply param_abstr => x [na [da da_gt0]] /= rx.
rewrite paramE /Rrat /fun_hrel /Qint_to_rat /= /inv_op /invQ /=.
rewrite [x]RratE /= -[(_ == _)%C]/(_ == _) -[(_ < _)%C]/(_ < _) /cast.
rewrite /cast_pos_int /cast_int_pos /pos_to_int /int_to_pos /int_to_nat /=.
have [-> /=|na_neq0 /=] := altP (na =P 0).
by rewrite !mul0r ?invr0.
have [na_gt0|na_le0] /= := ltrP 0 na.
rewrite val_insubd absz_gt0 na_neq0 abszE ger0_norm ?ltrW //.
by rewrite invfM invrK natz mulrC.
rewrite val_insubd /= /opp_op /opp_int /=.
rewrite oppr_gt0 ltr_neqAle na_neq0 na_le0 /= absz_gt0 oppr_eq0 na_neq0.
rewrite abszN mulrNz mulNr -mulrN -invrN -rmorphN /=.
by rewrite lez0_abs // opprK invfM invrK mulrC natz.
Qed.
Instance Rrat_eq :
param (
Rrat ==>
Rrat ==>
Logic.eq)
eqtype.eq_op eq_op.
Proof.
apply param_abstr2 => x [na [da da_gt0]] rx y [nb [db db_gt0]] ry.
rewrite paramE /eq_op /eqQ /cast /cast_pos_int /pos_to_int /=; simpC.
rewrite [x]RratE [y]RratE /= divq_eq; last 2 first.
- by rewrite gtr_eqF // ltr0z.
- by rewrite gtr_eqF // ltr0z.
by rewrite -!rmorphM /= eqr_int !natz.
Qed.
Instance Rrat_leq :
param (
Rrat ==>
Rrat ==>
Logic.eq)
Num.le leq_op.
Proof.
apply param_abstr2 => x [na [da da_gt0]] rx y [nb [db db_gt0]] ry.
rewrite paramE /leq_op /leqQ /cast /cast_pos_int /pos_to_int /=; simpC.
rewrite [x]RratE [y]RratE /= !natz.
rewrite ler_pdivr_mulr ?ltr0z // mulrAC ler_pdivl_mulr ?ltr0z //.
by rewrite -!rmorphM /= ler_int.
Qed.
Instance Rrat_lt :
param (
Rrat ==>
Rrat ==>
Logic.eq)
Num.lt lt_op.
Proof.
apply param_abstr2 => x [na [da da_gt0]] rx y [nb [db db_gt0]] ry.
rewrite paramE /leq_op /leqQ /cast /cast_pos_int /pos_to_int /=; simpC.
rewrite [x]RratE [y]RratE /= !natz.
rewrite ltr_pdivr_mulr ?ltr0z // mulrAC ltr_pdivl_mulr ?ltr0z //.
by rewrite -!rmorphM /= ltr_int.
Qed.
PART III: We take advantage of parametricity to extend correctness of
operation on Q int to correctness of operations on Q Z, for any Z that
refines int
Section Qparametric.
Context (
Z P :
Type).
Context (
Rint :
int ->
Z ->
Prop) (
Rpos :
pos ->
P ->
Prop).
Local Notation Q := (
Q Z P).
Definition RratA :
rat ->
Q ->
Prop := (
Rrat \
o Rint *
Rpos)%
rel.
Context `{
zero Z,
one Z,
add Z,
opp Z,
sub Z,
mul Z,
eq Z,
leq Z,
lt Z}.
Context `{
one P,
sub P,
add P,
mul P,
eq P,
leq P,
lt P}.
Context `{
cast_class P Z,
cast_class Z P}.
Context `{
spec_of Z int,
spec_of P pos}.
Context `{!
param Rint 0%
R 0%
C, !
param Rint 1%
R 1%
C}.
Context `{!
param (
Rint ==>
Rint) -%
R -%
C}.
Context `{!
param (
Rint ==>
Rint ==>
Rint) +%
R +%
C}.
Context `{!
param (
Rint ==>
Rint ==>
Rint)
subr sub_op}.
Context `{!
param (
Rint ==>
Rint ==>
Rint) *%
R *%
C}.
Context `{!
param (
Rint ==>
Rint ==>
Logic.eq)
eqtype.eq_op eq_op}.
Context `{!
param (
Rint ==>
Rint ==>
Logic.eq)
Num.le leq_op}.
Context `{!
param (
Rint ==>
Rint ==>
Logic.eq)
Num.lt lt_op}.
Context `{!
param (
Rpos ==>
Rint)
cast cast}.
Context `{!
param (
Rint ==>
Rpos)
cast cast}.
Context `{!
param Rpos one_pos 1%
C}.
Context `{!
param (
Rpos ==>
Rpos ==>
Rpos)
add_pos +%
C}.
Context `{!
param (
Rpos ==>
Rpos ==>
Rpos)
mul_pos *%
C}.
Context `{!
param (
Rpos ==>
Rpos ==>
Logic.eq)
eqtype.eq_op eq_op}.
Context `{!
param (
Rpos ==>
Rpos ==>
Logic.eq)
leq_pos leq_op}.
Context `{!
param (
Rpos ==>
Rpos ==>
Logic.eq)
lt_pos lt_op}.
Global Instance RratA_zeroQ :
param RratA 0 0%
C.
Proof.
exact: param_trans. Qed.
Global Instance RratA_oneQ :
param RratA 1 1%
C.
Proof.
exact: param_trans. Qed.
Global Instance RratA_cast_ZQ :
param (
Rint ==>
RratA)
intr cast.
Proof.
exact: param_trans. Qed.
Global Instance RratA_cast_PQ :
param (
Rpos ==>
RratA)
pos_to_rat cast.
Proof.
exact: param_trans. Qed.
Global Instance RratA_addQ :
param (
RratA ==>
RratA ==>
RratA) +%
R +%
C.
Proof.
exact: param_trans. Qed.
Global Instance RratA_mulQ :
param (
RratA ==>
RratA ==>
RratA) *%
R *%
C.
Proof.
exact: param_trans. Qed.
Global Instance RratA_expQnat :
param (
RratA ==>
Logic.eq ==>
RratA) (@
GRing.exp _)
exp_op.
Proof.
exact: param_trans. Qed.
Global Instance RratA_oppQ :
param (
RratA ==>
RratA) -%
R -%
C.
Proof.
exact: param_trans. Qed.
Global Instance RratA_invQ :
param (
RratA ==>
RratA)
GRing.inv inv_op.
Proof.
exact: param_trans. Qed.
Global Instance RratA_subQ :
param (
RratA ==>
RratA ==>
RratA)
subr sub_op.
Proof.
by rewrite /AlgOp.subr /sub_op /subQ; apply: get_param. Qed.
Global Instance RratA_divq :
param (
RratA ==>
RratA ==>
RratA)
divr div_op.
Proof.
by rewrite /AlgOp.divr /div_op /divQ; apply: get_param. Qed.
Global Instance RratA_eqQ :
param (
RratA ==>
RratA ==>
Logic.eq)
eqtype.eq_op eq_op.
Proof.
eapply param_trans; tc.
by rewrite /eq_op /eqQ; tc.
Qed.
Global Instance RratA_leqQ :
param (
RratA ==>
RratA ==>
Logic.eq)
Num.le leq_op.
Proof.
eapply param_trans; tc.
by rewrite /leq_op /leqQ; tc.
Qed.
Global Instance RratA_ltQ :
param (
RratA ==>
RratA ==>
Logic.eq)
Num.lt lt_op.
Proof.
eapply param_trans; tc.
by rewrite /lt_op /ltQ; tc.
Qed.
End Qparametric.
End Qint.