The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Programs written like this with proof scripts seem hard to read and 
maintain.  Does anyone have any arguments for writing in this style 
instead of in the style I used in my solution?

Venanzio Capretta wrote:
> Here is a solution. I'm not sure it is better than yours: it just 
> hides the ugly parts (to do with inversions) into a couple of 
> auxiliary functions (definitions below):
>  bound_0_elim: forall A:Type, (Bounded 0) -> A
>  bounded_zero_succ: forall (n:nat)(i:Bounded (S n)),
>                     {j:Bounded n | i = Succ j} + {i=Zero n}.
>
> But at least you can define prefix in a shorter and more intuitive way:
>
> Definition prefix: forall (A:Set)(n:nat)(i:Bounded (S n)),
>  vector A n -> vector A (Bounded_to_nat i).
> induction 1.
> case (bounded_zero_succ 0 i).
>  intros [j Hij]; apply bound_0_elim with (1:=j).
>  intros Hi; rewrite Hi; exact (Vnil A).
> case (bounded_zero_succ (S n) i).
>  intros [j Hij]; rewrite Hij; simpl.
>  apply Vcons.
>  exact a.
>  exact (IHvector j).
>  intro Hi; rewrite Hi; exact (Vnil A).
> Defined.