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.