Library Numbers.countable_sets

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Faissole, Martin, Mayero
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.


From Coq Require Import ZArith Lia Qreals Reals.

From Logic Require Import logic_compl.
From Numbers Require Import nat_compl.

Lemma Nat_div2_gt : a b, (2 × a + 1 < b)%nat (a < Nat.div2 b)%nat.
Proof.
intros a b H.
apply Nat.mul_lt_mono_pos_l with (p:=2%nat); try (constructor; easy).
destruct (Nat.even b) eqn:parity.
- apply Nat.even_spec in parity as [b' ->].
  rewrite Nat.div2_double; try easy.
  apply (Nat.lt_trans _ (2 × a + 1) _); try easy.
  now rewrite Nat.add_1_r; constructor.
- assert (odd_b : Nat.odd b = true) by now unfold Nat.odd; rewrite parity.
  apply Nat.odd_spec in odd_b as [b' ->].
  rewrite Nat.add_1_r, Nat.div2_succ_double.
  now rewrite (Nat.add_lt_mono_r _ _ 1).
Qed.

Section Z_countable.
Open Scope nat_scope.
Definition bij_ZN : Z nat :=
  fun zmatch Z_lt_le_dec z 0 with
    | right _ ⇒ (2 × Z.abs_nat z)
    | left _ ⇒ (2 × Z.abs_nat z - 1)
    end.

Definition bij_NZ : nat Z :=
  fun nmatch Nat.even n with
    | true ⇒ (Z.of_nat (Nat.div2 n))%Z
    | false ⇒ (- Z.of_nat (Nat.div2 (n + 1)))%Z
    end.

Lemma bij_NZN : z, bij_NZ (bij_ZN z) = z.
Proof.
intros z; unfold bij_ZN.
destruct (Z_lt_le_dec z 0) as [zlt0 | zge0].
-
  unfold bij_NZ.
  remember (Z.abs_nat z) as k eqn:def_k.
  destruct k as [|k']; try lia.
  replace (2 × (S k') - 1) with (2 × k' + 1) by lia.
  assert (Odd_2k'1 : Nat.Odd (2 × k' + 1)) by now k'.
  apply Nat.odd_spec in Odd_2k'1 as ->%negb_true_iff.
  replace (Nat.div2 (2 × k' + 1 + 1)) with (k' + 1); try lia.
  replace (2 × k' + 1 + 1) with (2 × (k' + 1)) by lia.
  now rewrite Nat.div2_double.
-
  unfold bij_NZ.
  assert (Even_2abs : Nat.Even (2 × Z.abs_nat z)) by now (Z.abs_nat z).
  apply Nat.even_spec in Even_2abs as →.
  rewrite Nat.div2_double; lia.
Qed.

Lemma bij_ZNZ : n, bij_ZN (bij_NZ n) = n.
Proof.
intros n; unfold bij_NZ, bij_ZN.
destruct (Nat.even n) eqn:parity.
- apply Nat.even_spec in parity as [k ->].
  rewrite Nat.div2_double.
  now destruct (Z_lt_le_dec (Z.of_nat k) 0) as [k_lt0 | k_geq0]; lia.
- assert (n_odd : Nat.odd n = true) by now unfold Nat.odd; rewrite parity.
  apply Nat.odd_spec in n_odd as [k ->].
  replace (2 × k + 1 + 1) with (2 × (k + 1)) by lia.
  rewrite Nat.div2_double.
  now destruct (Z_lt_le_dec (-Z.of_nat (k + 1)) 0) as [k_lt0 | k_geq0]; lia.
Qed.
End Z_countable.

Section N2_countable.
Open Scope nat_scope.

Fixpoint bij_NN2_aux (n p : nat) : nat × nat :=
  match p with
  | O(0, 0)
  | S p'match Nat.even n with
    | true
      let (u1, v1) := bij_NN2_aux (Nat.div2 n) p' in
      (S u1, v1)
    | false(0, Nat.div2 n)
    end
  end.

Lemma eq_couple {A B : Type} (a : A) (b : B) (z : A × B) :
  (a, b) = z (a = fst z) (b = snd z).
Proof.
  now intros <-.
Qed.

Lemma bij_NN2_aux_p :
   n p u v,
    (n 0)%nat (n p)%nat
    (u, v) = bij_NN2_aux n p
    (n = Nat.pow 2 u × (S (2 × v)))%nat.
Proof.
apply (nat_ind_strong (fun n
        (p u v:nat), (n 0)%nat (n p)%nat
         (u,v) = bij_NN2_aux n p
        (n = Nat.pow 2 u × (S (2×v)))%nat)).
intros n; case n; try lia.
clear n; intros n H p u v _ H2 H1.
case_eq p.
intros K; absurd (0 < p)%nat; auto with zarith.
intros p' Hp'; generalize H1.
rewrite Hp'; simpl.
destruct n as [| n']; try now intros [= → ->].
destruct (Nat.even n') eqn:parity.
- apply Nat.even_spec in parity as [k ->]; rewrite Nat.div2_double.
  destruct (bij_NN2_aux (S k) p') as [u' v1] eqn:E.
  intros [-> ->]%eq_couple; simpl.
  assert (Sk_ltSSk : (S k) < S (S (2 ×k))) by lia.
  replace (S (S (k + (k + 0)))) with (2 × (S k)) by lia.
  rewrite (H (S k) Sk_ltSSk p' u' v1); try easy; try lia.
- apply negb_true_iff in parity.
  replace (negb (Nat.even n')) with (Nat.odd n') by easy.
  apply Nat.odd_spec in parity as [k ->].
  rewrite Nat.add_1_r, Nat.div2_succ_double.
  now intros [-> ->]%eq_couple; simpl; lia.
Qed.

Lemma bij_NN2_aux_u :
   u v u' v',
    (2 ^ u × (S (2 × v)) = 2 ^ u' × (S (2 × v')))%nat
    (u,v) = (u',v').
Proof.
assert (Hu: u v u' v', (u < u')%nat
  (2 ^ u × (S (2×v)) = 2 ^ u' × (S (2×v')))%nat
  False). {
  intros u v u' v' H1 H2.
  apply (Nat.Even_Odd_False (2^(u'-u)*(S (2×v'))))%nat.
  - destruct (u' - u) eqn:u'u; try lia.
     (2^n × S (2 × v')).
    now rewrite Nat.mul_assoc, Nat.pow_succ_r'.
  - replace (2 ^ (u' - u) × S (2 × v'))%nat with (S (2×v)).
    now v; rewrite Nat.add_1_r.
    apply Nat.mul_cancel_l with (Nat.pow 2 u).
    apply Nat.pow_nonzero; auto with arith.
    rewrite H2, Nat.mul_assoc.
    rewrite <- Nat.pow_add_r.
    f_equal; f_equal.
    auto with zarith.
}

intros u v u' v' H.
case (Nat.le_gt_cases u u'); intros H1.
case (ifflr (Nat.lt_eq_cases _ _) H1); intros H2.
absurd (False); try easy.
apply (Hu u v u' v'); easy.
rewrite H2.
replace v with v'; try easy.
apply Nat.mul_cancel_l with 2%nat.
auto with arith.
assert (S (2 × v')%nat = S (2 × v)%nat); auto with zarith.
apply Nat.mul_cancel_l with (Nat.pow 2 u).
apply Nat.pow_nonzero; auto with arith.
rewrite H, H2; easy.
absurd (False); try easy.
apply (Hu u' v' u v); easy.
Qed.

Definition bij_NN2 : nat nat × nat := fun nbij_NN2_aux (S n) (S n).

Definition bij_N2N : nat × nat nat :=
  fun Nlet (x,y) := N in
    pred (Nat.pow 2 x × (S (2 × y)))%nat.

Lemma bij_NN2N : (N : nat × nat), bij_NN2 (bij_N2N N) = N.
Proof.
intros (n,m).
unfold bij_N2N; simpl.
unfold bij_NN2.
case_eq (bij_NN2_aux (S (Init.Nat.pred (2 ^ n × S (m + (m + 0)))))
    (S (Init.Nat.pred (2 ^ n × S (m + (m + 0))))) ).
intros u v H.
apply bij_NN2_aux_u.
rewrite <- bij_NN2_aux_p with (S (Init.Nat.pred (2 ^ n × S (m + (m + 0)))))
   (S (Init.Nat.pred (2 ^ n × S (m + (m + 0))))) u v; try easy.
rewrite Nat.succ_pred_pos; try easy.
apply Nat.mul_pos_pos; auto with zarith.
assert (Nat.pow 2 n 0)%nat; auto with zarith.
apply Nat.pow_nonzero; auto with zarith.
Qed.

Lemma bij_N2NN2 : n, bij_N2N (bij_NN2 n) = n.
Proof.
intros n.
unfold bij_NN2.
case_eq (bij_NN2_aux (S n) (S n)); intros u v H.
unfold bij_N2N.
rewrite <- (bij_NN2_aux_p (S n) (S n) u v); easy.
Qed.

End N2_countable.

Section Q_countable.

Definition bij_NQ : nat Q :=
  fun nlet (u, v) := bij_NN2 n in
    Qmake (bij_NZ u) (Pos.of_succ_nat v).

Definition bij_QN : Q nat :=
  fun qmatch q with | Qmake u v
      let w1 := bij_ZN u in
      let w2 := pred (Pos.to_nat v) in
      bij_N2N (w1, w2)
    end.

Lemma bij_NQN : q, bij_NQ (bij_QN q) = q.
Proof.
intros q; unfold bij_QN, bij_NQ.
destruct q as (u,v).
rewrite bij_NN2N.
rewrite bij_NZN.
f_equal.
rewrite <- (Pos2SuccNat.pred_id v) at 2.
generalize (Pos2Nat.is_pos v).
generalize (Pos.to_nat v); intros n.
case n; try easy.
clear n; intros n _; simpl.
rewrite Pos.pred_succ; easy.
Qed.

Lemma bij_QNQ : n, bij_QN (bij_NQ n) = n.
Proof.
intros n; unfold bij_QN, bij_NQ.
case_eq (bij_NN2 n); intros u v H.
rewrite bij_ZNZ.
rewrite SuccNat2Pos.pred_id.
rewrite <- H.
apply bij_N2NN2.
Qed.

End Q_countable.

Section XY_countable.

Context {X Y : Type}.

Variable bij_NX : nat X.
Variable bij_XN : X nat.
Variable bij_NY : nat Y.
Variable bij_YN : Y nat.

Hypothesis bij_NXN : x, bij_NX (bij_XN x) = x.
Hypothesis bij_XNX : n, bij_XN (bij_NX n) = n.
Hypothesis bij_NYN : y, bij_NY (bij_YN y) = y.
Hypothesis bij_YNY : n, bij_YN (bij_NY n) = n.

Definition bij_NXY : nat X × Y :=
  fun nlet (n1, n2) := bij_NN2 n in
    (bij_NX n1, bij_NY n2).

Definition bij_XYN : X × Y nat :=
  fun xymatch xy with | (x, y)
      let n1 := bij_XN x in
      let n2 := bij_YN y in
      bij_N2N (n1, n2)
    end.

Lemma bij_NXYN : xy, bij_NXY (bij_XYN xy) = xy.
Proof.
intros (x, y); unfold bij_XYN, bij_NXY.
now rewrite bij_NN2N, bij_NXN, bij_NYN.
Qed.

Lemma bij_XYNXY : n, bij_XYN (bij_NXY n) = n.
Proof.
intros n; unfold bij_XYN, bij_NXY.
case_eq (bij_NN2 n); intros n1 n2 Hn.
now rewrite bij_XNX, bij_YNY, <- Hn, bij_N2NN2.
Qed.

End XY_countable.

Section compounds.

Definition bij_NZ2 := bij_NXY bij_NZ bij_NZ.
Definition bij_Z2N := bij_XYN bij_ZN bij_ZN.

Lemma bij_NZ2N : zz, bij_NZ2 (bij_Z2N zz) = zz.
Proof.
apply bij_NXYN; apply bij_NZN.
Qed.

Lemma bij_Z2NZ2 : n, bij_Z2N (bij_NZ2 n) = n.
Proof.
apply bij_XYNXY; apply bij_ZNZ.
Qed.

Definition bij_NQ2 := bij_NXY bij_NQ bij_NQ.
Definition bij_Q2N := bij_XYN bij_QN bij_QN.

Lemma bij_NQ2N : qq, bij_NQ2 (bij_Q2N qq) = qq.
Proof.
apply bij_NXYN; apply bij_NQN.
Qed.

Lemma bij_Q2NQ2 : n, bij_Q2N (bij_NQ2 n) = n.
Proof.
apply bij_XYNXY; apply bij_QNQ.
Qed.

End compounds.