The Coq mailing list

[Vincent Laporte <vincent.laporte AT gmail.com>]

2013-06-27 18:03, Geoff Reedy:
> 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)).

Hi,

Notice that there is no need for the extra `eq_refl` after the match.
Indeed if the hypothesis `H: 0 ≤ i < Zlength lst` is not introduced too
early, it can enjoy a different type in the two branches of the match.

Require Import ZArith List Psatz.
Local Open Scope Z_scope.

Definition z_nth {A: Type}: forall (i: Z) (lst: list A), 0 <= i <
Zlength lst -> A.
  refine (fix f (i: Z) (lst: list A) : 0 <= i < Zlength lst -> A :=
            match lst as x return 0 <= i < Zlength x -> A with
            | nil => fun H => False_rect _ _
            | x::xs => fun H =>
                         match Z_zerop i with
                         | left _ => x
                         | right K => f (i - 1) xs _
                         end
            end).
Proof.
  change (Zlength nil) with 0 in H. clear -H. abstract intuition.
  clear -H K. abstract (rewrite Zlength_cons in H; lia).
Defined.

Happy τ day,
--
Vincent.