Skip to content

Instantly share code, notes, and snippets.

@paldepind

paldepind/qp.v

Last active October 3, 2020 17:09
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save paldepind/d085ba6f7512fee655f7e65e174f8e33 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save paldepind/d085ba6f7512fee655f7e65e174f8e33 to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. paldepind revised this gist Oct 3, 2020. 1 changed file with 2 additions and 2 deletions.
    4 changes: 2 additions & 2 deletions qp.v
    View file
    Original file line number Diff line number Diff line change
    @@ -45,8 +45,8 @@ Proof. Admitted.
    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).
    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)).

  2. paldepind created this gist Oct 3, 2020.
    72 changes: 72 additions & 0 deletions qp.v
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,72 @@
    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.