Positive fractions where 1 = 1/2 + 1/2 holds by reflexivity.

qp.v

From Coq Require Import QArith Qcanon.
From stdpp Require Export base decidable option numbers.

(* Strictly positive rationals *)

(* Positive fractions. *)
Record Qpos : Set := mk_Qpos {
  Qpos_num : positive;
  Qpos_den : positive
}.

(* Reduce a fraction. *)
Definition Qpos_red (q : Qpos) : Qpos :=
  let (q1,q2) := q in
  let (r1,r2) := snd (Z.ggcd (Zpos q1) (Zpos q2))
  in mk_Qpos (Z.to_pos r1) (Z.to_pos r2).

(* A strictly positive rational is a reduced positive fraction. *)
Record Qp : Set := MkQp { Qp_car : Qpos; Qp_canon : Qpos_red Qp_car = Qp_car }.

Delimit Scope Qp_scope with Qp.
Bind Scope Qp_scope with Qp.
Open Scope Qp.

Compute (1%Qc).
Compute (1/2 + 1/2)%Qc.

Notation "a # b" := (mk_Qpos a b) (at level 55, no associativity) : Qp_scope.

(* Operations for Qpos *)

Definition Qpos_plus (x y : Qpos) :=
  (Qpos_num x * Qpos_den y + Qpos_num y * Qpos_den x) # (Qpos_den x * Qpos_den y).

Definition Qpos_mult (x y : Qpos) := (Qpos_num x * Qpos_num y) # (Qpos_den x * Qpos_den y).

Definition Qpos_inv (x : Qpos) := Qpos_den x # Qpos_num x.

(* Results about Qpos_red. *)

Lemma Qpos_red_involutive : ∀ q : Qpos, Qpos_red (Qpos_red q) = Qpos_red q.
Proof. Admitted.

(* NOTE: [q] is reduced twice!! *)
Definition mk_Qp (q : Qpos) :=
  MkQp (Qpos_red (Qpos_red q)) (Qpos_red_involutive (Qpos_red q)).
(* Note that with this definition (similar to how Qc is defined in Qcanon would
  make the proof of `Qp_one_half_plus_hafl` below fail:
  MkQp (Qpos_red q) (Qpos_red_involutive q). *)

Definition Qp_plus (x y : Qp) := mk_Qp (Qpos_plus (Qp_car x) (Qp_car y)).

Definition Qp_mult (x y : Qp) := mk_Qp (Qpos_mult (Qp_car x) (Qp_car y)).

Definition Qp_inv (x : Qp) := mk_Qp (Qpos_inv (Qp_car x)).

Definition Qp_div (x y : Qp) := Qp_mult x (Qp_inv y).

Definition Qp_one : Qp := mk_Qp (1 # 1).

Infix "+" := Qp_plus : Qp_scope.
Infix "*" := Qp_mult : Qp_scope.
Infix "/" := Qp_div : Qp_scope.

Notation "1" := Qp_one : Qp_scope.
Notation "2" := (1 + 1)%Qp : Qp_scope.

Compute 1%Qp.
Compute ((1 / 2) + (1 / 2))%Qp.

Lemma Qp_one_half_plus_hafl : 1 = (1 / 2) + (1 / 2).
Proof. reflexivity. Qed.