The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le 27/06/2013 06:54, t x a écrit :

>    I'd prefer to use functions with dependent types rather than
> returning an option A. However, I run into the problem where when I try
> to "unfold" my function to prove things about it, the unfolded function
> is very very ugly.
>
> Definition z_nth {A: Type}
>                 (i: Z)
>                 (lst: list A)
>                 (H: 0 <= i < (Z.of_nat (length lst))) : A.
> Proof.
>    generalize dependent i.
>    induction lst as [| x xs].
>    (* nil case *)
>      crush.
>    (* x :: xs *)
>      intros i H. simpl in *.
>      pose proof (Z_dec' 0 i) as H_i_0.
>      destruct H_i_0 as [ [H_i_gt_0| H_i_lt_0] | H_i_eq_0].
>    (* i > 0; inductive case *)
>      apply (IHxs (i-1)). split. crush. crush.
>      rewrite (Zpos_P_of_succ_nat (length xs)) in H1. crush.
>    (* i < 0; can't happen *)
>      crush.
>    (* i = 0; return front *)
>      exact x. Defined.

The point is that the unfolded function is "very very ugly" because your 
proof is. You cannot expect Coq to produce a lambda-term with three 
branches if your proof has four!

Below is a variant that has exactly the structure you wanted, though it 
is a bit more verbose because the "fun H : ugly_type =>" binders have to 
be present, obviously.

Definition z_nth {A: Type} : forall (i: Z) (lst: list A)
  (H: (0 <= i < Z.of_nat (length lst))%Z), A.
Proof.
fix 2.
intros i [|x xs] ; simpl ; intros H.
clear -H.
abstract omega.
case (Z_zerop i) ; intros H'.
exact x.
apply (z_nth (i - 1)%Z xs).
clear -H H'.
abstract (rewrite Zpos_P_of_succ_nat in H ; omega).
Defined.

The process of writing such functions is a bit convoluted, so you may 
first want to experiment with Program, as suggested by Daniel Schepler, 
as it offers a trade-off between ease-of-use and term ugliness.

Best regards,

Guillaume