Commit 8cf5a7ad authored by Hai Dang's avatar Hai Dang

add countability for Q, Qc, and Qp

parent ee6200b4
(* 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
Definition _Q2pair (p: Q): _ := (Qnum p, Qden p).
Definition _pair2Q (p: Z * positive) : Q :=
match p with
| (num,den) => Qmake num den
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
Global Instance Qc_countable : Countable Qc :=
injective_countable _Qc_to_Q (Some Q2Qc) _.
intros [p Can]. simpl. f_equal. apply Qc_is_canon.
simpl. rewrite Can. reflexivity.
Definition _Qc2Qp (p: Qc) : option Qp :=
match (decide (0 < p)%Qc) with
| left G0 => Some (mk_Qp p G0)
| _ => None
Global Instance Qp_countable : Countable Qp :=
injective_countable Qp_car (_Qc2Qp) _.
intros [p G0]. unfold _Qc2Qp. simpl.
destruct (decide (0 < p)%Qc); [|tauto].
f_equal. apply Qp_eq. auto.
......@@ -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.
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.
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment