How could I fix this line spacing?

The line spacing is huge now for no reason, how do I change it back? :/
not that anyone reads this anyway..

Just a fun Show instance for functions

import Data.List
import Data.Maybe
import Control.Monad
import Control.Arrow

(*) `on` f = \x y -> f x * f y

class Inhabitants a where inhabitants :: [a]
instance Inhabitants () where inhabitants = [()]
instance Inhabitants Bool where inhabitants = [True,False]
instance (Inhabitants x, Inhabitants y) => Inhabitants (x,y) where inhabitants = liftM2 (,) inhabitants inhabitants
instance Inhabitants x => Inhabitants (Maybe x) where inhabitants = Nothing : map Just inhabitants

instance (Inhabitants p, Show p, Show q) => Show (p -> q) where
  show f = "(fromJust . flip lookup " ++ show (map (id &&& f) inhabitants) ++ ")"


-- > not
-- (fromJust . flip lookup [(True,False),(False,True)])
-- > (fromJust . flip lookup [(True,False),(False,True)]) True
-- False
-- > \x -> Just Nothing
-- (fromJust . flip lookup [((),Just Nothing)])
-- > id
-- (fromJust . flip lookup [((),())])
-- > maybe not (&&)
-- (fromJust . flip lookup [(Nothing,(fromJust . flip lookup [(True,False),(False,True)])),(Just True,(fromJust . flip lookup [(True,True),(False,False)])),(Just False,(fromJust . flip lookup [(True,False),(False,False)]))])

Pure Type Systems type checker in Prolog

They ( http://people.cs.uu.nl/andres/LambdaPi/index.html http://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html ) said it was easy but actually it's very hard, of course these posts are very helpful though. My other reference is the book Lectures on the Curry-Howard Isomorphism (Studies in Logic and Foundations of Mathematics - Vol 149).

Assuming this doesn't have any bugs, does it..?

:- op(1200, xfx, :=).
:- op(150, xfx, ⊢).
:- op(140, xfx, :).
:- op(100, yfx, $).


sort(★).
sort(▢).

axiom(★,▢).

rule(★,★,★). % λ→
rule(★,▢,▢). % λP
rule(▢,★,★). % λ2
rule(▢,▢,▢). % λω


unfold(Term, TermU) :- unfold([],Term,TermU).
unfold(_, Sort, Sort) :- sort(Sort).
unfold(Γ, Ident, Value) :- member(Ident, Γ) -> Ident = Value ; ( Ident := ValueD ), unfold(ValueD, Value).
unfold(Γ, λ(Var:Type,Body), λ(Var:TypeU,BodyU)) :- unfold(Γ, Type, TypeU), unfold([Var|Γ], Body, BodyU).
unfold(Γ, π(Var:Type,Body), π(Var:TypeU,BodyU)) :- unfold(Γ, Type, TypeU), unfold([Var|Γ], Body, BodyU).
unfold(Γ, U $ V, P $ Q) :- unfold(Γ, U, P), unfold(Γ, V, Q).

alpha(X,Y) :- alpha([],X,Y).
alpha(_,Id,Id) :- !.
alpha(Γ,Var1,Var2) :- member(Var1=Var2,Γ).
alpha(Γ,λ(Var1:Type1,Body1), λ(Var2:Type2,Body2)) :- alpha(Γ,Type1,Type2), alpha([Var1=Var2|Γ],Body1,Body2).
alpha(Γ,π(Var1:Type1,Body1), π(Var2:Type2,Body2)) :- alpha(Γ,Type1,Type2), alpha([Var1=Var2|Γ],Body1,Body2).
alpha(Γ,U $ V,P $ Q) :- alpha(Γ,U,P), alpha(Γ,V,Q).

subst(X->Y,X,Y) :- !.
subst(_->_,Var,Var) :- atomic(Var).
subst(X->Y,λ(X:Type1,Body),λ(X:Type2,Body)) :- !, subst(X->Y,Type1,Type2).
subst(X->Y,λ(Z:Type1,Body1),λ(Z:Type2,Body2)) :- subst(X->Y,Type1,Type2), subst(X->Y,Body1,Body2).
subst(X->Y,π(X:Type1,Body),π(X:Type2,Body)) :- !, subst(X->Y,Type1,Type2).
subst(X->Y,π(Z:Type1,Body1),π(Z:Type2,Body2)) :- subst(X->Y,Type1,Type2), subst(X->Y,Body1,Body2).
subst(X->Y,U $ V,P $ Q) :- subst(X->Y,U,P), subst(X->Y,V,Q).

eval(λ(U:_,B) $ V, BetaVal) :- !, subst(U->V,B,Beta), eval(Beta,BetaVal).
eval(X $ Y, XY) :- !, eval(X,Xv), eval(Xv $ Y,XY).
eval(Value, Value).


type(Term, Type) :- unfold(Term,TermU), [] ⊢ TermU : Type.
hasType(Term, Type) :- type(Term, Type1), unfold(Type,TypeU), eval(TypeU, Type2), alpha(Type1,Type2).

_ ⊢ S1 : S2 :- axiom(S1,S2).
Γ ⊢ I : T :- once(member(I:T, Γ)).
Γ ⊢ λ(A:T,B) : π(A:Tv,C) :- Γ ⊢ T : S1, sort(S1), eval(T,Tv), [A:Tv|Γ] ⊢ B : C. %%, /* sanity checks: */ Γ ⊢ π(A:Tv,C) : S2, sort(S2).
Γ ⊢ π(A:T,B) : S :- Γ ⊢ T : S1, [A:T|Γ] ⊢ B : S2, rule(S1,S2,S).
Γ ⊢ P $ Q : T :- Γ ⊢ P : π(X:U,B), Γ ⊢ Q : V, alpha(U,V), eval(λ(X:U,B) $ Q,T).



id := λ(t:★, λ(x:t, x)).
idTy := π(x:★, π(e:x, x)).

const := λ(s:★, λ(t:★, λ(u:s, λ(v:t, u)))).
constTy := π(u:★, π(v:★, π(g0:u, π(g1:v, u)))).

%%bool := π(a:★, a -> a -> a).
bool := π(a:★, π(g1:a, π(g2:a, a))).
true := λ(a:★, λ(x:a, λ(y:a, x))).
false := λ(a:★, λ(x:a, λ(y:a, y))).

%%nat := π(u:★, u -> (u -> u) -> u).
nat := π(u:★, π(g1:u, π(g2:π(g3:u, u), u))).
zero := λ(a:★, λ(x:a, λ(f:π(g:a, a), x))).
%%succ := λ(n:nat, λ(a:★, λ(x:a, λ(f:(a -> a), f $ (n $ a $ x $ f))))).
succ := λ(n:nat, λ(a:★, λ(x:a, λ(f:π(g:a, a), f $ (n $ a $ x $ f))))).

add := λ(m:nat, λ(n:nat, m $ nat $ n $ succ)).

eq := λ(a:★, λ(x:a, λ(y:a,
       λ(p:π(x:a, ★), π(g:p$x, p$y))))).

%%eq(a:★, x:a, y:a) := λ(p:π(x:a, ★), π(g:p$x, p$y)).

Proving RLE encoding and decoding in Coq

Require Import List.
Require Import ListPlus.

Set Implicit Arguments.

Notation "y <- x" := (x -> y) (at level 94, left associativity, only parsing).

Definition compose A B C (f : C <- B) (g : B <- A) := fun x => f (g x).
Infix "∘" := compose (at level 30, right associativity).

(*
 * rle = map (length &&& head) ∘ group
 * unrle = concat ∘ map (uncurry replicate)
 *
 * is it always true that (unrle ∘ rle) x = x?
 *
 * notice:
 *  rle = f ∘ f'
 *  unrle = g' ∘ g
 *
 *)

Theorem sandwich : forall I M O
  (f : O <- M) (f' : M <- I)
  (g : O -> M) (g' : M -> I),
  (forall x, (f  ∘ g ) x = x) ->
  (forall x, (f' ∘ g') x = x) ->
  (forall x, (f ∘ f' ∘ g' ∘ g) x = x).
Proof.
  unfold compose; intros.
  rewrite (H0 (g x)).
  apply H.
Qed.

(*
 * so all that must be proved now is
 *    forall x, (concat ∘ group) x = x
 * /\ forall x, (map (uncurry replicate) ∘ map (length &&& head))
 *
 *)

Theorem map_fuse : forall A B C (f : C <- B) (g : B <- A),
  forall x, (map f ∘ map g) x = map (f ∘ g) x.
Proof.
  induction x.
  reflexivity.
  simpl; rewrite <- IHx.
  reflexivity.
Qed.

(*
 * Now we have "only" to prove
 *    forall x, (concat ∘ group) x = x
 * /\ forall x, (uncurry replicate ∘ (length &&& head)) x = x
 *
 * This is actually impossible though,
 * (uncurry replicate ∘ (length &&& head)) "foo" = "fff"
 *
 * The reason rle works is because group segments the list
 * into *homogenous* chunks, if we knew the input to (length && head)
 * was a homogenous list then it would be correct and provable.
 * It needs access to this precondition though
 *
 *)

Theorem sandwich' : forall I M O
  (P : M -> Prop)
  (f : O <- M) (f' : M <- I)
  (g : O -> M) (g' : M -> I),
  (forall x, (f  ∘ g ) x = x) ->
  (forall x, P x -> (f' ∘ g') x = x) ->
  (forall x, P (g x)) ->
  (forall x, (f ∘ f' ∘ g' ∘ g) x = x).
Proof.
  unfold compose; intros.
  rewrite (H0 (g x)).
  apply H.
  apply H1.
Qed.

Inductive Homogenous A : listP A -> Prop :=
| HEnd : forall u, Homogenous (nilP u)
| HOne : forall u, Homogenous (u:~:nilP u)
| HAdd : forall u us, Homogenous (u:~:us) -> Homogenous (u:~:u:~:us).
Hint Constructors Homogenous.

Inductive All X (P : X -> Prop) : list X -> Prop :=
| AllNil : All P nil
| AllCons : forall x xs, P x -> All P xs -> All P (x::xs).
Hint Constructors All.

Section RLE.
  
  Variable A : Type.
  Variable eq_dec : forall x y : A, { x = y } + { x <> y }.
  
  Definition head_consP X (e : X) (l : list (listP X)) :=
    match l with
      | nil => nil
      | x::xs => (e:~:x)::xs
    end.

  Fixpoint group (l : list A) : list (listP A) :=
    match l with
      | nil => nil
      | x::xs =>
        match xs with
          | nil => nilP x::nil
          | y::ys =>
            match eq_dec x y with
              | left equal => head_consP x (group xs)
              | right not_equal => nilP x::group xs
            end
        end
    end.
  Fixpoint concat (l : list (listP A)) : list A :=
    match l with
      | nil => nil
      | x::xs => appP' x (concat xs)
    end.
  
  Definition crush (l : listP A) : (nat * A) := (lengthP l, headP l).
  Definition expand (t : nat * A) : listP A := let (n,e) := t in replicateP n e.
  
  Definition rle := map crush ∘ group.
  Definition unrle := concat ∘ map expand.
  
  Functional Scheme group_ind := Induction for group Sort Prop.
  Lemma concat_group_inv : forall x, (concat ∘ group) x = x.
    unfold compose.
    intro x; functional induction (group x).
    
    reflexivity.
    
    reflexivity.
    
    Lemma cat_cons : forall u v vs, concat (head_consP u (v::vs)) = u :: concat (v::vs).
      destruct vs; reflexivity.
    Qed.
    
    destruct (group (y :: _x)).
    inversion IHl.
    rewrite cat_cons.
    rewrite IHl.
    reflexivity.
    
    simpl in *.
    rewrite IHl.
    reflexivity.
  Qed.
  
  Lemma expand_crush_inv : forall x, Homogenous x -> (expand ∘ crush) x = x.
    unfold compose.
    induction x.
    reflexivity.
    intro; inversion H.
    rewrite <- H2 in IHx.
    reflexivity.
    simpl in *.
    rewrite <- H2 in *.
    rewrite <- IHx.
    reflexivity.
    assumption.
  Qed.
  
  (*
   * some notes I had to write to crack this lemma,
   *
   * group [] = []
   * group [x] = [[x]]
   * group (x:y:ys) = if x == y then headCons x (group (y:ys))
   *                           else [x] : group (y:ys)
   *   where headCons x (y:ys) = (x:y):ys
   *
   * Theorem: forall xs, All Homogenous (group xs)
   * 
   * group [] ~ trivial
   * group [x] ~ trivial
   * group (x:y:ys) = [x] : group (y:ys)
   *            homo   ^          ^ homo by induction
   * 
   * group (x:x:ys) = headCons x (group (x:xs))
   * 
   * (group (x:xs)) = ((x:p):q)
   *          homogenous ^  ^ all homogenous by induction
   *
   * group (x:x:ys) = headCons x ((x:p):q)
   *                = ((x:x:p):q)
   *            homo cons ^
   *)
  
  Lemma group_homo : forall x, All (@Homogenous A) (group x).
    induction x.
    simpl; auto.
    destruct x.
    simpl; auto.
    
    simpl.
    destruct (eq_dec a a0).
    
    rewrite <- e in *.
    
    Lemma paper_plane : forall xs x,
      exists p, exists q,
        group (x::xs) = ((x:~:p)::q) \/ group (x::xs) = ((nilP x)::q).
      induction xs.
      simpl.
      intro x; exists (nilP x); exists nil; auto.
      intro x.
      simpl.
      destruct (eq_dec x a).
      rewrite <- e in *; clear e a.
      
      destruct (IHxs x).
      destruct H.
      destruct H.
      simpl in H.
      rewrite H.
      simpl.
      exists (x :~: x0).
      exists x1.
      left; reflexivity.
      simpl in H.
      rewrite H.
      simpl.
      exists (nilP x).
      exists x1.
      left; reflexivity.
      
      destruct (IHxs a).
      destruct H.
      destruct H.
      simpl in H.
      destruct xs.
      exists (nilP a).
      exists (nilP a :: nil).
      right; reflexivity.
      rewrite H.
      exists (nilP a).
      exists ((a :~: x0) :: x1).
      right; reflexivity.
      simpl in H.
      rewrite H.
      exists (nilP a).
      exists (nilP a :: x1).
      right; reflexivity.
    Qed.
    
    pose (paper_plane x a).
    inversion e0.
    inversion H.
    inversion H0.
    
    rewrite H1 in IHx.
    simpl in H1.
    rewrite H1.
    simpl.
    apply AllCons.
    apply HAdd.
    inversion IHx; auto.
    inversion IHx; auto.
    
    rewrite H1 in IHx.
    simpl in H1.
    rewrite H1.
    simpl.
    apply AllCons.
    apply HOne.
    inversion IHx.
    assumption.
    
    apply AllCons.
    auto.
    apply IHx.
  Qed.
  
  Theorem rle_inv : forall x, unrle (rle x) = x.
    intro; unfold unrle, rle.
    apply sandwich' with (P := All (@Homogenous A)).
    
    exact concat_group_inv.
    
    clear x; intros; rewrite map_fuse; induction x.
    reflexivity.
    simpl.
    inversion H.
    rewrite (IHx H3).
    rewrite (expand_crush_inv H2).
    reflexivity.
  
    exact group_homo.
  Qed.
    
End RLE.

Require Import Arith.

Eval compute in (rle eq_nat_dec (1::2::3::3::3::5::5::5::1::1::1::6::6::6::6::6::nil)).
(*
 *   = (0, 1) :: (0, 2) :: (2, 3) :: (2, 5) :: (2, 1) :: (4, 6) :: nil
 *   : list (nat * nat)
 *)

Eval compute in (unrle (rle eq_nat_dec (1::2::3::3::3::5::5::5::1::1::1::6::6::6::6::6::nil))).
(*   = 1::2::3::3 ::3 ::5 ::5 ::5::1::1::1::6::6::6::6::6::nil
 *   : list nat
 *)

Correctness of an Expression Compiler in Coq

This is based on Correctness Of A Compiler For Arithmetic Expressions and A type-correct, stack-safe, provably correct expression compiler in Epigram

Require Import List.

Fixpoint Tuple (types : list Set) : Type :=
  match types with
    | nil => unit
    | t::ts => (t * Tuple ts)%type
  end.

Inductive Exp : Set -> Type :=
| Num : nat -> Exp nat
| Boo : bool -> Exp bool
| Sum : Exp nat -> Exp nat -> Exp nat
| Eql : Exp nat -> Exp nat -> Exp bool
| Iff : forall (a : Set), Exp bool -> Exp a -> Exp a -> Exp a.

Fixpoint nat_eq_bool (x y : nat) {struct x} : bool :=
  match x, y with
    | O, O => true
    | S x', S y' => nat_eq_bool x' y'
    | _,_ => false
  end.

Fixpoint eval (a : Set) (e : Exp a) : a :=
  match e in Exp t return t with
    | Num n => n
    | Boo b => b
    | Sum p q => eval _ p + eval _ q
    | Eql x y => nat_eq_bool (eval _ x) (eval _ y)
    | Iff _ b t e => if eval _ b then eval _ t else eval _ e
  end.

(* example *)
Eval compute in
  (eval _
    (Iff _ (Eql (Num 7) (Sum (Num 4) (Num 3)))
      (Sum (Num 5) (Num 8))
      (Num 0))).

Notation "x --> y" := (x,y) (at level 120, right associativity).

Inductive INST : list Set * list Set -> Type :=
| PUSHN : forall s, nat -> INST (s --> nat::s)
| PUSHB : forall s, bool -> INST (s --> bool::s)
| SUM : forall s, INST (nat::nat::s --> nat::s)
| EQL : forall s, INST (nat::nat::s --> bool::s)
| COND : forall s, forall a, INST (bool::a::a::s --> a::s).

Inductive stack : list Set -> Type :=
| snil : stack nil
| scons : forall p q, INST (p --> q) -> stack p -> stack q.

Fixpoint compile
  (a : Set) (e : Exp a)
  (tail : list Set) (rest : stack tail)
  { struct e } : stack (a::tail) :=
  match e in Exp a return stack (a::tail) with
    | Num n =>
      scons _ _ (PUSHN _ n) rest
    | Boo b =>
      scons _ _ (PUSHB _ b) rest
    | Sum u v =>
      scons _ _ (SUM _)
      (compile _ u _
        (compile _ v _ rest))
    | Eql x y =>
      scons _ _ (EQL _)
      (compile _ x _
        (compile _ y _ rest))
    | Iff a b t e =>
      scons _ _ (COND _ _)
      (compile _ b _
        (compile _ t _
          (compile _ e _ rest)))
  end.

Definition evinst :
  forall p q,
    forall (i : INST (p --> q)),
      Tuple p -> Tuple q :=
      fun p q i =>
        match i in INST pq return Tuple (fst pq) -> Tuple (snd pq) with
          | PUSHN _ n => fun s =>
            (n, s)
          | PUSHB _ b => fun s =>
            (b, s)
          | SUM _ => fun s =>
            match s with
              | (u, (v, s)) => (u + v, s)
            end
          | EQL _ => fun s =>
            match s with
              | (x, (y, s)) => (nat_eq_bool x y, s)
            end
          | COND _ _ => fun s =>
            match s with
              | (b, (t, (e, s))) =>
                (if b then t else e, s)
            end
        end.

Fixpoint evstack typs (program : stack typs)
  { struct program } : Tuple typs :=
  match program in stack typs return Tuple typs with
    | snil => tt
    | scons t ts i is => evinst _ _ i (evstack _ is)
  end.

Eval compute in
  (evstack _ (compile _
    (Iff _ (Eql (Num 7) (Sum (Num 4) (Num 3)))
      (Sum (Num 5) (Num 8))
      (Num 0)) nil snil)).

Lemma eval_correct :
  forall a (e : Exp a),
    forall typs (program_tail : stack typs),
      (eval a e, (evstack typs program_tail))
      =
      evstack (a::typs) (compile a e typs program_tail).
Proof.
  induction e.
  
  reflexivity.
  
  reflexivity.
  
  intros.
  unfold compile; fold compile; simpl.
  rewrite <- IHe1.
  rewrite <- IHe2.
  reflexivity.
  
  intros.
  unfold compile; fold compile; simpl.
  rewrite <- IHe1.
  rewrite <- IHe2.
  reflexivity.
  
  intros.
  unfold compile; fold compile; simpl.
  rewrite <- IHe1.
  rewrite <- IHe2.
  rewrite <- IHe3.
  reflexivity.
Qed.

A Haskell Puzzle

chunk n list = case list of { [] -> [] ; (y:ys) -> ch' ys (n-1) (y:) } where
 ch' [] _ k = k [] : []
 ch' (y:ys) 0 k = k [] : ch' ys (n-1) (y:)
 ch' (y:ys) (c+1) k = ch' ys c (k . (y:))

Easy Examples of Pattern Matching in Coq

(*
 * A couple of difficulties in Coq or dependently typed programming
 * are having to write impossible cases in pattern matches and
 * getting at the new information provided by a pattern match.
 *)

(* I'll use vectors (lists which have their length as part of the
 * type) to explain this since they are very simple objects
 *)

Inductive Vec (A : Set) : nat -> Set :=
| VNil : Vec A 0
| VCons : forall n, A -> Vec A n -> Vec A (S n).

(* It's pretty easy to define a total function taking the head
 * of any vector using tactics:
 *
Definition head (A : Set)(n : nat) :
  Vec A (S n) -> A.
intros.
inversion H.
exact H1.
Defined.
 * but actually this results in something terrifying:
Print head.

head = 
fun (A : Set) (n : nat) (H : Vec A (S n)) =>
let H0 :=
  match H in (Vec _ n0) return (n0 = S n -> A) with
  | VNil =>
      fun H0 : 0 = S n =>
      let H1 :=
        eq_ind 0 (fun e : nat => match e with
                                 | 0 => True
                                 | S _ => False
                                 end) I (S n) H0 in
      False_rec A H1
  | VCons n0 H0 H1 =>
      fun H2 : S n0 = S n =>
      let H3 :=
        let H3 :=
          f_equal (fun e : nat => match e with
                                  | 0 => n0
                                  | S n1 => n1
                                  end) H2 in
        eq_rect n (fun n1 : nat => A -> Vec A n1 -> A)
          (fun (H4 : A) (_ : Vec A n) => H4) n0 (sym_eq H3) in
      H3 H0 H1
  end in
H0 (refl_equal (S n))
     : forall (A : Set) (n : nat), Vec A (S n) -> A
 *
 * It would be much shorter to simple define it by pattern matching
 * but there is a problem,
 *)

(*
Definition head (A : Set)(n : nat) :
  Vec A (S n) -> A :=
  fun v =>
    match v with
      | VCons n a _ => a
    end.
 *
 * it seems ok but what we know (that a vector of length one or more
 * cannot ever be VNil) hasn't been made clear to Coq:
 *
   Error: Non exhaustive pattern-matching:
          no clause found for pattern VNil
 *)

(* To define head by pattern matching we must cover all cases
 * but there is certainly not object of type A to return given
 * a VNil object of type Vec A (S _), of course this is absurd.
 * So I'll use the solution given here:
 * http://pauillac.inria.fr/pipermail/coq-club/2008/003508.html
 *)

Definition head (A : Set)(n : nat) :
  Vec A (S n) -> A :=
  fun v =>
    match v in Vec _ m return
      match m with
        | 0 => True
        | _ => A
      end
      with
      | VNil => I
      | VCons n a _ => a
    end.

(* This is perfect, the trick is very clever!
 * the key is that [match m with | 0 => True | _ => A end] is
 * convertable to A since m = (S n).
 * then VNil is given a trivial case which must be of type True
 * (chosen arbitrarily) and VCons gives the actual definition
 * we wished for.
 *)

(* this is a big hassle, let's avoid going through it again .. *)
Definition tail (A : Set)(n : nat) :
  Vec A (S n) -> Vec A n.
intros; inversion H; trivial.
Defined.

(*
Theorem worm (A : Set)(n : nat) :
  forall (v : Vec A (S n)),
    v = VCons _ _ (head _ _ v) (tail _ _ v).
Proof.
  intros.
  inversion v.
*)
(*
  A : Set
  n : nat
  v : Vec A (S n)
  n0 : nat
  H0 : A
  H1 : Vec A n
  H : n0 = n
  ============================
   v = VCons A n (head A n v) (tail A n v)
*)

(* so now I tried to prove a theorem relating these functions,
 * but of course hit a brick wall, there's just not enough information
 * relating the terms to prove it
 *)

(* before (when defining head), we met trouble due to not giving a
 * total coverage of the type, (that is we ignored Vec A 0) so a
 * possible lemma to consider would be an identity on all Vectors
 * which takes VNil to VNil and VCons _ _ to VCons (head v) (tail v)
 * Actually I had some trouble even writing this, so I let Coq do it
 * for me
 *)

(*
Definition Vid (A : Set)(n : nat) :
  Vec A n -> Vec A n.
destruct n.
tauto.
intro v.
exact (VCons _ _ (head _ _ v) (tail _ _ v)).
Qed.
Print Vid.
 *
 Vid = 
 fun (A : Set) (n : nat) =>
 match n as n0 return (Vec A n0 -> Vec A n0) with
 | 0 => fun H : Vec A 0 => H
 | S n0 => fun v : Vec A (S n0) => VCons A n0 (head A n0 v) (tail A n0 v)
 end
      : forall (A : Set) (n : nat), Vec A n -> Vec A n
 * but actually I'd like to have the proof term here in a simpler
 * form if possible, so I rewrote it in the way it way synthesized:
 *)

Definition Vid (A : Set)(n : nat) :
  Vec A n -> Vec A n :=
  match n return Vec A n -> Vec A n with
    | 0 => fun v => v
    | S m => fun v => VCons _ _ (head _ _ v) (tail _ _ v)
  end.

Lemma Vid_is_id (A : Set)(n : nat) :
  forall v : Vec A n,
    v = Vid _ _ v.
Proof.
  destruct v; reflexivity.
Qed.

Theorem worm (A : Set)(n : nat) :
  forall (v : Vec A (S n)),
    v = VCons _ _ (head _ _ v) (tail _ _ v).
Proof.
  intros; apply Vid_is_id with (v := v).
Qed.

(* What next? *)