The Coq mailing list

[Vincent Siles <vincent.siles AT ens-lyon.org>]

Hi everyone,
I have defined a function by induction on an accessibility proof:

Definition build_list : forall (l: list A),
  Acc R l -> P l -> list A.
intros l h; induction h.
<rest of the code>
Defined.

(P is just some precondition about l)

Now I would like to prove things about build_list.
I managed to do it *while* defining the list with:

Definition build_list2 : forall (l: list A),
  Acc R l -> P l ->  { k : list A |  Q l k }.


But I would like to do it in two times, with something like
Lemma bl_Q : forall (l:list A) (ha: Acc R l) (hp: P l), Q l
(build_list l ha hp).

With this approach, if I try an "intros l ha; induction ha", I got an error:
 with Coq:
"Error: Abstracting over the term "l" leads to a term
  "fun l : list A =>
 forall hp : P l, Q l (build_list_fun_acc ha hp)" which is ill-typed."

 with Ssr:
"Error: ha is used in conclusion"


Anyone knows a way to do such a separation between code & proofs ?


Regards,
Vincent