convoy pattern and match involving inequality

Question

I have a problem implementing simple function and I am pretty sure the answer is a "convoy pattern" but I just could not figure out how to apply it in this particular case. Here is a full example:

Require Import Coq.Lists.List.

Definition index_map_spec (domain range: nat) :=
  forall n : nat, n < domain -> {v : nat | v < range}.

Lemma lt_pred_l {n m} (H: S n < m): n < m.
Proof. auto with arith. Defined.

Fixpoint natrange_f_spec
         (n:nat)
         {i o: nat}
         (nd: n<i)
         (f_spec: index_map_spec i o)
  : list nat
  :=
    match n return list nat with
    | 0 => nil
    | S n' => cons n' (natrange_f_spec n' (lt_pred_l nd) f_spec)
    end.

The error I am getting is:

The term "nd" has type "n < i" while it is expected to have type
 "S ?578 < ?579".

So basically I would like to match on 'n' in a way for (n=S p) it would rewrite (n

Answer 1

You just have to abstract over the nd proof on your match, changing its return type accordingly:

Require Import Coq.Lists.List.

Definition index_map_spec (domain range: nat) :=
  forall n : nat, n < domain -> {v : nat | v < range}.

Lemma lt_pred_l {n m} (H: S n < m): n < m.
Proof. auto with arith. Defined.

Fixpoint natrange_f_spec
         (n:nat)
         {i o: nat}
         (nd: n<i)
         (f_spec: index_map_spec i o)
  : list nat
  :=
    match n return n < i -> list nat with
    | 0 => fun _ => nil
    | S n' => fun nd => cons n' (natrange_f_spec n' (lt_pred_l nd) f_spec)
    end nd.