The Coq mailing list

[t x <txrev319 AT gmail.com>]

Geoff: very nice, I'm starting to understand why "refine" is useful now.

Guillaume: thanks for the explanation of fix/abstract/Defined -- I ran into the exact same problem while playing with a modification of Geoff's example above, and "clear"-ing all the unnecessary hypotheses fixed it.

On Thu, Jun 27, 2013 at 11:03 AM, Geoff Reedy <geoff AT programmer-monk.net> wrote:

Another option besides those already mentioned is the refine tactic.
The refine tactic lets you specify a proof term with holes in it that
are then presented as goals. This lets you be sure that the definition
will have the correct computational effect while leaving the proof
portions to be found through interactive tactic application.

For your example I ended up with

Definition z_nth {A: Type}: forall (i: Z) (lst: list A) (H: 0 <= i < (Zlength lst)), A.
  refine (fix f (i: Z) (lst: list A) (H: 0 <= i < (Zlength lst)) : A :=
            match lst as x return (x = lst) -> A with
                | nil => (fun Heq => _)
                | x::xs => if Z_zerop i then (fun _ => x) else (fun Heq => f (Zpred i) xs _)
            end (eq_refl lst)).
  (* the nil case *)
  contradict H.
  rewrite <- Heq.
  rewrite Zlength_nil; omega.
  (* the cons case *)
  rewrite <- Heq in *.
  destruct H.
  split.
  apply Zlt_0_le_0_pred.
  omega.
  rewrite Zlength_cons in H0.
  apply Zsucc_lt_reg.
  rewrite <- Zsucc_pred.
  auto.
Defined.

Note the use of a dependent match to make sure that the relevant
hypotheses would be present in the context.

To see what I mean about getting the right computational effect,
consider

Definition z_nth_bad {A: Type}: forall (i: Z) (lst: list A) (H: 0 <= i < (Zlength lst)), A.
  intros.
  destruct lst.
  contradict H; rewrite Zlength_nil; omega.
  auto.
Defined.

which is well-typed, but doesn't do what you want. Instead it always
returns the first element of the list.