File CoMoNum.Q

Require Import Arith Relations.

From CoMoNum Require Import Z.

Inductive quoteq : (Z × Z) → (Z × Z) → Prop :=
  | quoteq_1 : ∀ a b c d, a ×Z d =Z b ×Z c → quoteq (a,b) (c,d).

Infix "=Q" := quoteq (at level 80).

Theorem quoteq_reflexive : reflexive _ quoteq.
Proof.
  intros [x y];
  constructor;
  exact (mulZ_comm x y).
Qed.

Theorem quoteq_symmetric : symmetric _ quoteq.
Proof.
  intros x y H1;
  destruct H1 as [a b c d H2];
  constructor;
  eapply diffeq_transitive;
  [ exact (mulZ_comm c b)
  | apply diffeq_symmetric;
    eapply diffeq_transitive;
    [ exact (mulZ_comm d a)
    | exact H2
    ]
  ].
Qed.

Theorem quoteq_transitive : transitive _ quoteq.
Proof.
Admitted.

Corollary quoteq_equivalence : equivalence _ quoteq.
Proof.
  split.
  -
    exact quoteq_reflexive.
  -
    exact quoteq_transitive.
  -
    exact quoteq_symmetric.
Qed.

Definition Q : Set := Z × Z.

Theorem name_missing : ∀ a b k, quoteq (a,b) (a ×Z k,b ×Z k).
Proof.
Admitted.

Definition addQ (x y : Q) : Q :=
  let (a,b) := x in
  let (c,d) := y in
  (a ×Z d +Z c ×Z b,b ×Z d).

Infix "+Q" := addQ (at level 10).

Theorem addQ_comm : ∀ x y, x +Q y =Q y +Q x.
Proof.
Admitted.

Theorem addQ_assoc : ∀ x y z, x +Q (y +Q z) =Q (x +Q y) +Q z.
Proof.
Admitted.

Definition mulQ (x y : Q) : Q :=
  let (a,b) := x in
  let (c,d) := y in
  (a ×Z c, b ×Z d).

Infix "*Q" := mulQ (at level 9).

Theorem mulQ_comm : ∀ x y, x ×Q y =Q y ×Q x.
Proof.
  intros [a b] [c d];
  constructor.
Admitted.

Theorem mulQ_assoc : ∀ x y z, x ×Q (y ×Q z) =Q (x ×Q y) ×Q z.
Proof.
  intros [a b] [c d] [e f];
  constructor.
Admitted.

Theorem addQ_mulQ_distr : ∀ x y z, x ×Q (y +Q z) =Q x ×Q y +Q x ×Q z.
Proof.
  intros [a b] [c d] [e f];
  constructor.
Admitted.

Definition emb (x : Z) : Q := (x,Z.emb 1).

Theorem emb_add : ∀ x y, emb (x +Z y) =Q emb x +Q (emb y).
Proof.
Admitted.

Theorem emb_mul : ∀ x y, emb (x ×Z y) =Q (emb x) ×Q (emb y).
Proof.
Admitted.