A countable sum of non-empty finite sets is countable

countable_sig_fin.v

Require Import Lia.
Require Import Wf_nat.

Section Fin.

Fixpoint Fin n : Type :=
  match n with
  | 0 => Empty_set
  | S m => unit + Fin m
  end.

Fixpoint Fin_to_nat{n} : Fin n -> nat :=
  match n with
  | 0 => fun e =>
    match e with
    end
  | S m => fun i =>
    match i with
    | inl _ => 0
    | inr j => S (Fin_to_nat j)
    end
  end.

Lemma Fin_to_nat_bound : forall n (i : Fin n),
  Fin_to_nat i < n.
Proof.
  induction n; intros.
  - destruct i.
  - destruct i as [[]|j].
    + simpl; lia.
    + simpl.
      pose (IHn j).
      lia.
Qed.

Fixpoint nat_to_Fin{n} : forall i, i < n -> Fin n :=
  match n with
  | 0 => fun i pf =>
    match PeanoNat.Nat.nlt_0_r _ pf with
    end
  | S _ => fun i =>
    match i with
    | 0 => fun _ => inl tt
    | S j => fun pf => inr (nat_to_Fin j (Lt.lt_S_n _ _ pf))
    end
  end.

Lemma Fin_to_nat_to_Fin : forall n i (pf : i < n),
  Fin_to_nat (nat_to_Fin i pf) = i.
Proof.
  induction n; intros.
  - lia.
  - simpl.
    destruct i.
    + reflexivity.
    + rewrite IHn.
      reflexivity.
Qed.

Lemma nat_to_Fin_to_nat : forall n (i : Fin n)(pf : Fin_to_nat i < n),
  nat_to_Fin (Fin_to_nat i) pf = i.
Proof.
  induction n; intros.
  - destruct i.
  - simpl.
    destruct i as [[]|j].
    + reflexivity.
    + rewrite IHn.
      reflexivity.
Qed.

Lemma Fin_to_nat_unique : forall n (i j : Fin n),
  Fin_to_nat i = Fin_to_nat j -> i = j.
Proof.
  induction n.
  - intros [].
  - intros [[]|i'] [[]|j'] H.
    + reflexivity.
    + discriminate.
    + discriminate.
    + inversion H.
      rewrite (IHn _ _ H1).
      reflexivity.
Qed.

End Fin.

(* sum_{i < n} f i *)
Fixpoint sum_func(f : nat -> nat)(n : nat) : nat :=
  match n with
  | 0 => 0
  | S m => sum_func f m + f m
  end.

Lemma sum_func_comp_S : forall f n,
  sum_func f (S n) = f 0 + sum_func (fun x : nat => f (S x)) n.
Proof.
  intros.
  induction n.
  - simpl; lia.
  - simpl.
    rewrite PeanoNat.Nat.add_assoc.
    rewrite <- IHn.
    reflexivity.
Qed.

Lemma sum_func_unique : forall q r q' r' f,
  sum_func f q + r = sum_func f q' + r' -> r < f q -> r' < f q' ->
  q = q'.
Proof.
  induction q; intros.
  - destruct q'.
    + reflexivity.
    + rewrite sum_func_comp_S in H.
      simpl in H.
      lia.
  - destruct q'.
    + rewrite sum_func_comp_S in H.
      simpl in H.
      lia.
    + repeat rewrite sum_func_comp_S in H.
      Search _ (?x + _ = ?x + _ -> _ = _).
      repeat rewrite <- PeanoNat.Nat.add_assoc in H.
      pose (Plus.plus_reg_l _ _ _ H).
      rewrite (IHq _ _ _ (fun x => f (S x)) e H0 H1).
      reflexivity.
Qed.

Definition sum_func_div : forall n f, (forall x, f x > 0) ->
   { p : nat * nat &
       sum_func f (fst p) + (snd p) = n
    /\ (snd p) < f (fst p) }.
Proof.
  intro n.
  induction (lt_wf n) as [n _ IHn].
  intros f f_pos.
  destruct (Compare_dec.le_lt_dec (f 0) n).
  - pose (f_pos 0).
    assert (n - f 0 < n) by lia.
    destruct (IHn _ H (fun x => f (S x))) as [[q r] [IHsum IHr]].
    + intro; apply f_pos.
    + exists (S q, r).
      split.
      * simpl fst.
        rewrite sum_func_comp_S.
        simpl in *.
        lia.
      * exact IHr.
  - exists (0, n).
    simpl; split; auto.
Defined.

Section Isomorphism.

Variable f : nat -> nat.

Hypothesis f_pos : forall x, f x > 0.

Definition nat_to_sig : nat -> { i : nat & Fin (f i) } :=
  fun n =>
    let '(existT _ p pf) := sum_func_div n f f_pos in
      existT _ (fst p) (nat_to_Fin _ (proj2 pf)).

Definition sig_to_nat : { i : nat & Fin (f i) } -> nat :=
  fun s =>
    sum_func f (projT1 s) + Fin_to_nat (projT2 s).

Lemma sig_to_nat_to_sig : forall n, sig_to_nat (nat_to_sig n) = n.
Proof.
  intro n.
  unfold nat_to_sig.
  destruct (sum_func_div n f f_pos) as [[q r] [pf1 pf2]].
  unfold sig_to_nat.
  simpl in *.
  rewrite Fin_to_nat_to_Fin.
  exact pf1.
Qed.

Lemma nat_to_sig_to_nat : forall s, nat_to_sig (sig_to_nat s) = s.
Proof.
  intro s.
  destruct s.
  unfold sig_to_nat.
  simpl.
  unfold nat_to_sig.
  destruct (sum_func_div _ f f_pos) as [[q r] [pf1 pf2]].
  simpl in *.
  pose (sum_func_unique q r _ _ f pf1 pf2 (Fin_to_nat_bound _ _)).
  destruct e.
  f_equal.
  assert (r = Fin_to_nat f0) by lia.
  apply Fin_to_nat_unique.
  rewrite Fin_to_nat_to_Fin.
  exact H.
Qed.

End Isomorphism.