FinMatrix.CoqExt.QExt

Require Export PositiveExt ZExt.
Require Export QArith Qround.
Require Export Hierarchy ElementType.
Open Scope Q.

Mathematical Structure

well-defined

Hint Resolve
Qplus_comp Qopp_comp Qminus_comp Qmult_comp Qinv_comp Qdiv_comp
: wd.

Decidable

#[export] Instance Qeq_Dec : Dec Qeq.
Proof. constructor. intros. apply Qeq_dec. Defined.

#[export] Instance Q_eq_Dec : Dec (@eq Q).
Proof.
  constructor. intros. destruct a as [p1 q1], b as [p2 q2].
  destruct (Aeqdec p1 p2), (Aeqdec q1 q2); subst; auto.
  all: right; intro; inversion H; easy.
Defined.

#[export] Instance Q_le_Dec : Dec Qle.
Proof.
  constructor. intros. destruct (Qlt_le_dec b a); auto.
  right. intro. apply Qle_not_lt in H. easy.
Defined.

#[export] Instance Q_lt_Dec : Dec Qlt.
Proof.
  constructor. intros. destruct (Qlt_le_dec a b); auto.
  right. intro. apply Qle_not_lt in q. easy.
Defined.

Instances for ElementType

Module ElementTypeQ <: ElementType.
  Definition A : Type := Q.
  Definition Azero : A := 0.
  Hint Unfold A Azero : A.

  Lemma AeqDec : Dec (@eq A).
  Proof. apply Q_eq_Dec. Defined.
End ElementTypeQ.

Convertion between Q and other types

Z to Q

Definition Z2Q (z : Z) : Q := inject_Z z.

nat to Q

Definition nat2Q (n : nat) : Q := Z2Q (Z.of_nat n).

Q to Z

Definition Q2Z_ceiling (q : Q) : Z := Qceiling q.
Definition Q2Z_floor (q : Q) : Z := Qfloor q.

Properties for Qeqb and Qeq

This axiom just for convenient printing and parsing, LIMITED USE IT.

For example, 32 and 64 is equivalent, but they are not the same. We mainly use this axiom to ensure 32 = 64, but not to say 3=6 and 2=4.

Be careful for use of any axiom!!

Definition Qeqb := Qeq_bool.

Infix "==" := Qeq : Q_scope.
Infix "=?" := Qeqb : Q_scope.

Reflection of (==) and (=?)

Lemma Qeqb_true_iff_equiv : forall x y, x =? y = true <-> x == y.
Proof.
  apply Qeq_bool_iff.
Qed.

Lemma Qeqb_false_iff_equiv : forall x y, x =? y = false <-> ~ x == y.
Proof.
  intros; split; intros.
  - intro. apply Qeqb_true_iff_equiv in H0. rewrite H in H0. easy.
  - destruct (Qeqb x y) eqn:E1; auto. apply Qeqb_true_iff_equiv in E1. easy.
Qed.

(==) is equivalence relation

Lemma Qeq_equiv : equivalence _ Qeq.
Proof.
split;intro;intros;try easy. rewrite H;try easy.
Qed.

Others

This is needed by field_theory (EQ version, original is equiv version)

sqrt of Q

A very rough algorithm for square root of rational number

Definition Qsqrt (q : Q) := Qmake (Z.sqrt (Qnum q)) (Pos.sqrt (Qden q)).