Require Coq.Arith.Plus.
(** Dependent Inductive Types **)
(*******************************)

Section vectors.
  Variable T : Type.

  (* We can use dependent types to enrich types with their properties.
   * For example the type of 'lists with a given length'.
   * Traditionally, length-indexed lists are called 'vectors'.
   *)
  Inductive vector : nat -> Type :=
  | Vnil : vector 0
  | Vcons : forall {n}, T -> vector n -> vector (S n).

Print vector_ind.

  Arguments Vcons {_} _ _.
  Arguments Vnil.

  (** Let's define some more notation *)
  Local Notation "[|  |]" := Vnil.
  Local Notation "[|  x ; .. ; y  |]" := (@Vcons _ x (.. (@Vcons _ y Vnil) ..)).

  Section vector_examples.
    Variables a b c : T.

    Check [| |].
    Check [| a |].
    Check [| a ; b ; c |].
  End vector_examples.

  (* When we define dependent types inductively, we learn
   * information about the index (in this case the nat) when
   * we inspect the value.
   *
   * Coq's 'in'-clause allows us to express how the return
   * type depends on the indices
   *)

  Fixpoint append (l1 : list T) (l2 : list T) : list T.
  destruct l1.
  apply l2.
  apply cons. apply t. apply append. apply l1. apply l2.
  Defined.

  Require Import List.
  Theorem append_eq_app : append = @List.app T.
  reflexivity.
  Qed.

  (* 'in'-clause pattern matching *)
  Fixpoint vappend {n m : nat} (v1 : vector n) (v2 : vector m) {struct v1}
  : vector (n + m).
  refine
    match v1 in vector l' return vector (l' + m) with
    | Vnil => v2
    | Vcons x xs => Vcons x (vappend _ _ xs v2)
    end.
  Defined.
  
  Section test2.
    Variables a b c : T.
    Eval compute in vappend [| a ; b |] [| c |].
  End test2.

  (* Can you implement appending a single element to the vector? *)
  Fixpoint vsnoc {n : nat} (x : T) (v : vector n)
  : vector (S n) :=
    match v
          in vector l'
          return vector (S l')
    with
    | Vnil => [| x |]
    | Vcons  x' xs => Vcons x' (vsnoc x xs)
    end.

  Variables a b c : T.
  Eval compute in vsnoc c [| a ; b |].

  (* If we want to prove these two functions are related
   * in the obvious way, we run into a problem.
   *)
(*
  Theorem vappend_vsnoc : forall n x (v : vector n),
      vsnoc x v = vappend v [| x |].
*)











  (* The problem lies in the type of the theorem.
   * [vsnoc x v] has type [vector (S n)] while
   * [vappend v [| x |]] has type [vector (n + 1)].
   * While [S n = n + 1] is *provable* the two are
   * not definitionally equal.
   *
   * To state the above theorem, we need to use a
   * proof that [S n = n + 1] to 'cast'
   * [vappend v [| x |]] into the type [vector (S n)].
   * We can do this using dependent pattern matching
   * on equality types.
   *)
  Print eq.

  (* Dependent pattern matching on this type is quite
   * similar to dependent pattern matching on vectors.
   * Let's take a look by implementing [Vcast].
   *)
  Definition Vcast (n m : nat) (pf : n = m)
  : vector n -> vector m :=
    match pf with
    | eq_refl => fun x => x
    end.



  (* We can use dependent pattern matching on equality
   * proofs to state the associativity of [vappend].
   *)
  Theorem vappend_assoc
  : forall a b c (va : vector a) (vb : vector b) (vc : vector c),
      vappend (vappend va vb) vc
      = match Plus.plus_assoc a b c in @eq _ _ X return vector X with
        | eq_refl => vappend va (vappend vb vc)
        end.
  Proof.
    induction va.
    - simpl. admit.
    - simpl. intros. rewrite IHva.
      admit.
  Abort.




  (* Everything will work out if we have a transparent definition of
   * plus_assoc.
   *)
  Lemma plus_assoc_trans : forall n m p : nat, n + (m + p) = n + m + p.
  Proof.
    induction n.
    { reflexivity. }
    { simpl. intros.  f_equal. eapply IHn. }
  Defined.

  Theorem vappend_assoc
  : forall a b c (va : vector a) (vb : vector b) (vc : vector c),
      vappend (vappend va vb) vc
      = match plus_assoc_trans a b c in _ = X return vector X with
        | eq_refl => vappend va (vappend vb vc)
        end.
  Proof.
    induction va.
    - simpl. reflexivity.
    - simpl. intros. rewrite IHva.
      clear IHva.
      generalize dependent (plus_assoc_trans n b0 c0).
      destruct e. simpl. reflexivity.
  Qed.

Print vappend_assoc.

End vectors.