Just my personal opinion, but; on complicated cases of dependent pattern matching, i think it’s simpler to understand what’s going on with eliminators instead. Don’t get me wrong, i like “match” as a construct, but dependent matching mixes too much stuff, i feel. For example, an earlier reply was talking about how “Coq first substitutes the parameters of the inductive type of x into T”: using an eliminator makes it clear this isn’t some sort of specific mechanism to pattern matching, it’s just regular function application.
Take the " hd’ " function you posted, for instance. With an eliminator, its definition looks like :
Definition hd'_alt (n:nat) (ls : ilist (S n)) : A :=
@ilist_rec (fun n' _ => n' = S n -> A)
(fun eq => False_rect A (PeanoNat.Nat.neq_succ_0 n (eq_sym eq)))
(fun m h hs _ => (fun _ => h))
(S n) ls eq_refl.
At first glance, this is a mouthful no one would be advised to write, but: you can define it partially. For example, you can check that
Definition hd'_start (n:nat) :
((0 = S n) -> A) ->
(forall m (h:A) hs, ((m = S n) -> A) -> (S m = S n) -> A) ->
forall i, ilist i -> i = S n -> A
:= @ilist_rec (fun n' _ => n' = S n -> A).
…and from there it’s a matter of filling holes. Proof mode makes this task simpler, of course.