isomorphism between binary and ternary cantor space

ternary.v

Require Import Wf_nat Lia.

Inductive three := a | b | c.

(* a => 0; b => 10; c => 11 *)

Fixpoint encode(f : nat -> three)(n : nat) : bool :=
  match f 0 with
  | a => match n with
         | 0 => false
         | S m => encode (fun x => f (S x)) m
         end
  | b => match n with
         | 0 => true
         | 1 => false
         | S (S m) => encode (fun x => f (S x)) m
         end
  | c => match n with
         | 0 => true
         | 1 => true
         | S (S m) => encode (fun x => f (S x)) m
         end
  end.

Fixpoint decode(g : nat -> bool)(n : nat) : three :=
  match g 0 with
  | false => match n with
             | 0 => a
             | S m => decode (fun x => g (S x)) m
             end
  | true => match g 1 with
            | false => match n with
                       | 0 => b
                       | S m => decode (fun x => g (S (S x))) m
                       end
            | true => match n with
                      | 0 => c
                      | S m => decode (fun x => g (S (S x))) m
                      end
            end
  end.

Lemma decode_encode : forall n f, decode (encode f) n = f n.
Proof.
  intro n.
  induction (lt_wf n) as [n _ IHn].
  intro.
  destruct n as [|[|m]].
  - simpl.
    destruct (f 0); reflexivity.
  - simpl.
    destruct (f 0),(f 1); reflexivity.
  - simpl.
    destruct (f 0),(f 1);
    (rewrite IHn; [reflexivity|lia]).
Qed.

Lemma encode_decode : forall n g, encode (decode g) n = g n.
Proof.
  intro n.
  induction (lt_wf n) as [n _ IHn].
  intro.
  destruct n as [|m].
  - simpl.
    destruct (g 0),(g 1); reflexivity.
  - simpl.
    destruct (g 0) eqn:G0; destruct (g 1) eqn:G1.
    + destruct m.
      * congruence.
      * rewrite IHn; [reflexivity|lia].
    + destruct m.
      * congruence.
      * rewrite IHn; [reflexivity|lia].
    + rewrite IHn; [reflexivity|lia].
    + rewrite IHn; [reflexivity|lia].
Qed.