A certified encoding of lists of natural numbers into natural numbers

nat list encoding.v

Set Implicit Arguments.
Require Import Omega.

(* equivalence of types along with elementary facts *)

Definition equiv(X Y : Type) := {f : X -> Y & {g : Y -> X & (forall x, g (f x) = x) /\
  (forall y, f (g y) = y)}}.

Lemma equiv_trans(X Y Z : Type) : equiv X Y -> equiv Y Z -> equiv X Z.
Proof.
  intros [f [g [Hgf Hfg]]] [h [i [Hih Hhi]]].
  exists (fun x => h (f x)).
  exists (fun z => g (i z)).
  split; congruence.
Defined.

Lemma equiv_sym(X Y : Type) : equiv X Y -> equiv Y X.
Proof.
  firstorder.
Defined.

Lemma prod_r_cong : forall X Y Z, equiv Y Z -> equiv (X * Y) (X * Z).
Proof.
  intros X Y Z [f [g [Hgf Hfg]]].
  exists (fun p => (fst p, f (snd p))).
  exists (fun p => (fst p, g (snd p))).
  split; intro x; destruct x; simpl; congruence.
Defined.

Lemma sum_r_cong : forall X Y Z, equiv Y Z -> equiv (X + Y) (X + Z).
Proof.
  intros X Y Z [f [g [Hgf Hfg]]].
  exists (fun s => match s with
                   |inl x => inl x
                   |inr y => inr (f y)
                   end).
  exists (fun s => match s with
                   |inl x => inl x
                   |inr z => inr (g z)
                   end).
  split; intros [x | w]; congruence.
Defined.

(* vectors *)

Fixpoint vec(X : Type)(n : nat) : Type :=
  match n with
  |0   => unit
  |S m => prod X (vec X m)
  end.

Fixpoint list_sig(X : Type)(xs : list X) : {n : nat & vec X n} :=
  match xs as xs return {n : nat & vec X n} with
  |nil       => existT _ 0 tt
  |cons x ys => match list_sig ys with
                |existT _ n v => existT _ (S n) (x,v)
                end
  end.

Fixpoint sig_list_aux(X : Type)(n : nat) : vec X n -> list X :=
  match n as n return vec X n -> list X with
  |0   => fun _ => nil
  |S m => fun v => cons (fst v) (sig_list_aux X m (snd v))
  end.

Definition sig_list(X : Type)(p : {n : nat & vec X n}) : list X :=
  sig_list_aux X (projT1 p) (projT2 p).

Lemma equiv_sig_list : forall (X : Type), equiv (list X) {n : nat & vec X n}.
Proof.
  intro X.
  exists (fun xs => list_sig xs).
  exists (fun p  => sig_list X p).
  unfold sig_list.
  split.
  induction x.
  reflexivity.
  simpl.
  destruct (list_sig x) eqn:G.
  simpl.
  simpl in IHx.
  congruence.
  intros [n v].
  induction n.
  destruct v.
  reflexivity.
  simpl.
  simpl in IHn.
  rewrite IHn.
  destruct v; reflexivity.
Defined.

Lemma sig_iso : forall (X Y : Type)(F : X -> Type),
  (forall x, equiv (F x) Y) -> equiv {x : X & F x} (X * Y).
Proof.
  intros.
  exists (fun p => (projT1 p, projT1 (X0 (projT1 p)) (projT2 p))).
  exists (fun p => existT F (fst p) (projT1 (projT2 (X0 (fst p))) (snd p))).
  split; intro.
  destruct x as [x Fx].
  simpl.
  destruct (X0 x) as [f [g [Hgf Hfg]]].
  simpl.
  rewrite Hgf.
  reflexivity.
  simpl.
  destruct (X0 (fst y)) as [f [g [Hgf Hfg]]].
  simpl.
  rewrite Hfg.
  destruct y; reflexivity.
Defined.

(* cantor pairing stuff *)

Definition next_pair(p : nat * nat) : nat * nat :=
  match p with
  |(x,0)   => (0,S x)
  |(x,S y) => (S x,y)
  end.

Fixpoint iter(X : Type)(f : X -> X)(n : nat)(x0 : X) : X :=
  match n with
  |0   => x0
  |S m => f (iter f m x0)
  end.

Lemma iter_sum : forall (X : Type)(f : X -> X)(n m : nat)(x0 : X),
  iter f (n + m) x0 = iter f n (iter f m x0).
  intros.
  induction n.
  auto.
  simpl.
  rewrite IHn; auto.
Qed.

Definition to_pair : nat -> nat * nat :=
  fun n => iter next_pair n (0,0).

Fixpoint triangle(n : nat) : nat :=
  match n with
  |0   => 0
  |S m => n + (triangle m)
  end.

Definition from_pair(p : nat * nat) : nat :=
  let (x,y) := p in (triangle (x+y) + x).

Lemma next_pair_lemma : forall x y, y <= x -> iter next_pair y (0,x) = (y,x - y).
Proof.
  intro x; induction y; intro.
  inversion H; reflexivity.
  simpl.
  assert (y <= x).
  omega.
  rewrite (IHy H0).
  simpl.
  destruct (x - y) eqn:G.
  omega.
  destruct x.
  omega.
  simpl.
  assert (S x - y = S (x - y)).
  omega.
  rewrite H1 in G.
  inversion G.
  reflexivity.
Qed.

Lemma pair_num : forall x, to_pair (from_pair (0,x)) = (0,x).
Proof.
  unfold from_pair.
  simpl.
  intro x.
  rewrite <- plus_n_O.
  induction x.
  reflexivity.
  assert (triangle (S x) = (S x) + triangle x).
  reflexivity.
  rewrite H.
  unfold to_pair.
  rewrite iter_sum.
  unfold to_pair in IHx.
  rewrite IHx.
  simpl.
  assert (iter next_pair x (0,x) = (x,0)).
  assert (x <= x).
  omega.
  pose (next_pair_lemma H0).
  rewrite e.
  assert (x - x = 0).
  omega.
  rewrite H1; reflexivity.
  rewrite H0.
  reflexivity.
Qed.

Lemma tp_fp_correct : forall p, to_pair (from_pair p) = p.
Proof.
  unfold to_pair, from_pair.
  destruct p.
  rewrite plus_comm.
  rewrite iter_sum.
  pose (pair_num (n + n0)).
  unfold to_pair, from_pair in e.
  simpl in e.
  rewrite <- plus_n_O in e.
  rewrite e.
  assert (n <= n + n0).
  omega.
  pose (next_pair_lemma H).
  rewrite e0.
  assert (n + n0 - n = n0).
  omega.
  congruence.
Qed.

Lemma fp_tp_correct : forall n, from_pair (to_pair n) = n.
Proof.
  unfold from_pair, to_pair.
  induction n.
  reflexivity.
  simpl.
  destruct (iter next_pair n (0,0)) eqn:G.
  simpl.
  destruct n1.
  simpl.
  rewrite <- plus_n_O.
  rewrite <- plus_n_O in IHn.
  omega.
  simpl.
  simpl in IHn.
  rewrite <- plus_n_Sm in IHn.
  simpl in IHn.
  omega.
Qed.

Lemma cantor_pair : equiv nat (nat * nat).
Proof.
  exists to_pair.
  exists from_pair.
  split.
  exact fp_tp_correct.
  exact tp_fp_correct.
Defined.

Lemma nat_plus_1 : equiv nat (unit + nat).
Proof.
  exists (fun n => match n with
                   |0   => inl tt
                   |S m => inr m
                   end).
  exists (fun s => match s with
                   |inl _ => 0
                   |inr m => S m
                   end).
  split; intro.
  destruct x; reflexivity.
  destruct y as [[]|n]; reflexivity.
Defined.

Lemma vec_Sn_nat : forall n, equiv nat (vec nat (S n)).
Proof.
  induction n.
  exists (fun x => (x,tt)).
  exists (fun v => fst v).
  split; intro.
  reflexivity.
  destruct y.
  destruct v.
  reflexivity.
  apply (@equiv_trans _ (nat * nat) _).
  exact cantor_pair.
  apply prod_r_cong.
  exact IHn.
Defined.

Lemma sig_change : equiv {n : nat & vec nat n} (unit + {n : nat & vec nat (S n)}).
Proof.
  exists (fun p => match p with
                   |existT _ 0 _     => inl tt
                   |existT _ (S m) v => inr (existT (fun n => vec nat (S n)) m v)
                   end).
  exists (fun s => match s with
                   |inl _ => existT _ 0 tt
                   |inr p => match p with
                             |existT _ n v => existT (fun n => vec nat n) (S n) v
                             end
                   end).
  split.
  destruct x.
  destruct x.
  destruct v.
  reflexivity.
  reflexivity.
  destruct y.
  destruct u; reflexivity.
  destruct s.
  reflexivity.
Defined.

Lemma equiv_nat_listnat : equiv nat (list nat).
Proof.
  apply (@equiv_trans _ (unit + nat) _).
  exact nat_plus_1.
  apply (@equiv_trans _ (unit + {n : nat & vec nat (S n)}) _).
  apply sum_r_cong.
  apply (@equiv_trans _ (nat * nat) _).
  exact cantor_pair.
  apply equiv_sym.
  apply sig_iso.
  intro; apply equiv_sym.
  apply vec_Sn_nat.
  apply (@equiv_trans _ {n : nat & vec nat n} _).
  apply equiv_sym.
  exact sig_change.
  apply equiv_sym.
  apply equiv_sig_list.
Defined.

Definition toList : nat -> list nat
 := projT1 equiv_nat_listnat.

Definition fromList : list nat -> nat
 := projT1 (projT2 equiv_nat_listnat).

Lemma toList_fromList : forall xs, toList (fromList xs) = xs.
Proof.
  unfold toList, fromList.
  destruct (equiv_nat_listnat) as [f [g [Hgf Hfg]]].
  exact Hfg.
Qed.

Lemma fromList_toList : forall x, fromList (toList x) = x.
Proof.
  unfold toList, fromList.
  destruct (equiv_nat_listnat) as [f [g [Hgf Hfg]]].
  exact Hgf.
Qed.