From 8cf5a7ad502182e5f2187c0b1a32161c781cec59 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Wed, 5 Jul 2017 15:33:41 +0200
Subject: [PATCH] add countability for Q, Qc, and Qp

---
 theories/countable.v | 45 +++++++++++++++++++++++++++++++++++++++++++-
 theories/decidable.v |  9 +++++++++
 2 files changed, 53 insertions(+), 1 deletion(-)

diff --git a/theories/countable.v b/theories/countable.v
index 47b93ece..a73ab5e7 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -1,6 +1,7 @@
 (* Copyright (c) 2012-2017, Coq-std++ developers. *)
 (* This file is distributed under the terms of the BSD license. *)
-From stdpp Require Export list.
+From Coq.QArith Require Import QArith_base Qcanon.
+From stdpp Require Export list numbers.
 Set Default Proof Using "Type".
 Local Open Scope positive.
 
@@ -268,3 +269,45 @@ Program Instance nat_countable : Countable nat :=
 Next Obligation.
   by intros x; lazy beta; rewrite decode_encode; csimpl; rewrite Nat2N.id.
 Qed.
+
+
+Definition _Q2pair (p: Q): _ := (Qnum p, Qden p).
+
+Definition _pair2Q (p: Z * positive) : Q :=
+  match p with
+  | (num,den) => Qmake num den
+  end.
+
+Instance Q_dec_eq : EqDecision Q :=
+  injective_dec_eq _Q2pair (Some ∘ _pair2Q) _.
+Proof. by destruct 0. Qed.
+
+Instance Q_countable : Countable Q :=
+  injective_countable _Q2pair (Some ∘ _pair2Q) _.
+Proof. by destruct 0. Qed.
+
+Definition _Qc_to_Q (p: Qc): _ :=
+  match p with
+  | Qcmake pb _ => pb
+  end.
+
+Global Instance Qc_countable : Countable Qc :=
+  injective_countable _Qc_to_Q (Some ∘ Q2Qc) _.
+Proof.
+  intros [p Can]. simpl. f_equal. apply Qc_is_canon.
+  simpl. rewrite Can. reflexivity.
+Qed.
+
+Definition _Qc2Qp (p: Qc) : option Qp :=
+  match (decide (0 < p)%Qc) with
+  | left G0 => Some (mk_Qp p G0)
+  | _ => None
+  end.
+
+Global Instance Qp_countable : Countable Qp :=
+  injective_countable Qp_car (_Qc2Qp) _.
+Proof.
+  intros [p G0]. unfold _Qc2Qp. simpl.
+  destruct (decide (0 < p)%Qc); [|tauto].
+  f_equal. apply Qp_eq. auto.
+Qed.
diff --git a/theories/decidable.v b/theories/decidable.v
index cb6213ad..1d2b54c3 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -200,3 +200,12 @@ Lemma not_and_l_alt {P Q : Prop} `{Decision P} : ¬(P ∧ Q) ↔ ¬P ∨ (¬Q 
 Proof. destruct (decide P); tauto. Qed.
 Lemma not_and_r_alt {P Q : Prop} `{Decision Q} : ¬(P ∧ Q) ↔ (¬P ∧ Q) ∨ ¬Q.
 Proof. destruct (decide Q); tauto. Qed.
+
+Lemma injective_dec_eq `{EqDecision A} {B : Type}
+  f (g : A -> option B) (Inj : ∀ x, g (f x) = Some x)
+  : EqDecision B.
+Proof.
+  intros x y. destruct (decide (f x = f y)) as [Eq%(f_equal g)|NEq].
+  - rewrite !Inj in Eq. inversion Eq. left; auto.
+  - right. intros Eq. apply NEq. rewrite Eq. auto.
+Qed.
-- 
GitLab