The Coq mailing list

[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