The Coq mailing list

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

Thanks !
That's exactly what I needed.

Vincent

2011/4/18 Hugo Herbelin 
<Hugo.Herbelin AT inria.fr>:
> Hi Vincent,
>
> Since Acc is in Prop, its _rect elimination principle is non dependent
> by default. Here you need a dependent elimination principle. So you
> can first do
>
> Scheme Acc_rect_dep := Induction for Acc Sort Type.
>
> then use "induction ha using Acc_rect_dep".
>
> Hugo
>
> On Mon, Apr 18, 2011 at 02:41:10PM +0200, Vincent Siles wrote:
>> 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
>