playground/coq/cpdt/ilist.v

Inductive ilist {A:Type}: nat -> Type :=
| INil: ilist 0
| ICons: forall {n:nat},
    A -> ilist n -> ilist (S n).
Arguments ilist: clear implicits.

Inductive fin: nat -> Type :=
(* The [n] here is for the length of [ilist]
   And [ilist] length is always non-zero if there is anything to be indexed. *)
| First: forall {n:nat}, fin (S n)
| Next: forall {n:nat}, fin n -> fin (S n).

(* fin nat is like a bounded form of nat:

Eg:

[fin 3] is like {0, 1, 2} as in:
 - First 2
 - Next (First 1)
 - Next (Next (First 0))

Could think of the argument of [First] as the number of remaining elements in
the list
*)

Fail Fixpoint iget {A:Type} {n:nat}
  (ls:ilist A n): fin n -> A :=
  match ls with
  | INil => fun idx => _
  | ICons x xs => fun idx =>
      match idx with
      | First => x
      | Next idx' => iget xs idx'
      end
  end.

Fail Fixpoint iget {A:Type} {n:nat}
  (ls:ilist A n): fin n -> A :=
  match ls with
  | INil => fun idx =>
      match idx in fin n' return
        match n' with
        | O => A (* This can never happen because [fin 0] has no constructor *)
        | S _ => unit
        end with
      | First => tt
      | Next _ => tt
      end
  | ICons x ls' => fun idx =>
      match idx with
      | First => x
      | Next idx' => iget ls' idx'
      end
  end.

Fail Fixpoint iget {A:Type} {n:nat}
  (ls:ilist A n): fin n -> A :=
  match ls with
  | INil => fun idx =>
      match idx in fin n' return
        match n' with
        | O => A (* This can never happen because [fin 0] has no constructor *)
        | S _ => unit
        end with
      | First => tt
      | Next _ => tt
      end
  | ICons x ls' => fun idx =>
      match idx in fin n' return ilist (pred n') -> A with
      | First => fun _ => x
      | Next idx' => fun ls'' => iget ls'' idx'
      end
  end.

Fixpoint iget {A:Type} {n:nat}
  (ls:ilist A n): fin n -> A :=
  match ls with
  | INil => fun idx =>
      match idx in fin n' return
        match n' with
        | O => A (* This can never happen because [fin 0] has no constructor *)
        | S _ => unit
        end with
      | First => tt
      | Next _ => tt
      end
  | ICons x ls' => fun idx =>
      (match idx in fin n' return (fin (pred n') -> A) -> A with
      | First => fun _ => x
      | Next idx' => fun fin2A => fin2A idx'
      end) (iget ls')
  end.

Fixpoint imap {A B:Type} {n:nat}
  (f:A -> B) (ls:ilist A n): ilist B n :=
  match ls with
  | INil => INil
  | ICons x ls' => ICons (f x) (imap f ls')
  end.

Theorem get_imap_distr: forall (A B:Type) (n:nat)
  (idx: fin n) (ls: ilist A n) (f:A->B),
  iget (imap f ls) idx = f (iget ls idx).
Proof.
  intros.
  induction ls.
  - now simpl.
  - Require Import Coq.Program.Equality.
    dependent destruction idx.
    + now simpl.
    + simpl.
      apply IHls.
Qed.
(* Well... that was easier than what I expected..
   Dependent types do pay off, I guess.. *)

Require List.
Fixpoint listToIlist {A:Type} (l:list A): ilist A (List.length l) :=
  match l with
  | List.nil => INil
  | List.cons x xs => ICons x (listToIlist xs)
  end.

Fixpoint ilistToList {A:Type} {n:nat} (l:ilist A n): list A :=
  match l with
  | INil => nil
  | ICons x xs => List.cons x (ilistToList xs)
  end.

Module IListNotations.
  Declare Scope ilist_scope.
  Delimit Scope ilist_scope with ilist.

  Notation "[ ]" := INil : ilist_scope.
  Notation "[ x ]" := (ICons x INil) : ilist_scope.
  Notation "[ x ; .. ; y ]" := (ICons x .. (ICons y INil) ..) : ilist_scope.
End IListNotations.

Import IListNotations.
Open Scope ilist.

Check [].
(* [ ] : ilist ?A 0
where
?A : [ |- Type]
*)
Check [1].
(* [1] : ilist nat 1 *)
Check [1; 2].
(* [1; 2] : ilist nat 2 *)


Compute iget [1; 2] First.  (* Implicit arg of [First] is figured out by coq *)
(* = 1 : nat *)
Compute iget [1; 2] (Next First).
(* = 2 : nat *)
Fail Compute iget [1; 2] (Next (Next First)).


Compute listToIlist (cons 3 (cons 2 (cons 1 (cons 0 nil)))).
(* = [3; 2; 1; 0]
     : ilist nat (length (3 :: 2 :: 1 :: 0 :: nil))
 *)
Compute ilistToList (listToIlist (cons 3 (cons 2 (cons 1 (cons 0 nil))))).
(* = (3 :: 2 :: 1 :: 0 :: nil)%list
     : list nat
*)