The Coq mailing list

["gallais @ ensl.org" <(e29315a54f%hidden_head%e29315a54f)guillaume.allais(e29315a54f%hidden_at%e29315a54f)ens-lyon.org(e29315a54f%hidden_end%e29315a54f)>]

Hi Nuno,

When you are dealing with an auxiliary function using an
accumulator, it's a safe bet to assume that you need two
theorems: a really general one which deals with a non
empty acc and its corollary which is the statement you
are looking for.

See in the attached file how [fact] is a trivial instance of
[more_general_fact].

Cheers,

--
guillaume


On 13 May 2012 22:06, Nuno Gaspar 
<(e29315a54f%hidden_head%e29315a54f)nmpgaspar(e29315a54f%hidden_at%e29315a54f)gmail.com(e29315a54f%hidden_end%e29315a54f)>
 wrote:
> Hello.
>
> Consider the following trivial definitions:
>
> Inductive X : Type := Const: nat -> X.
> Definition projX (x:X) : nat :=
>   match x with
>     | Const n => n
>   end.
>
>
> Function f (l:list X)  (id:nat) (acc:list X) {struct l} : option (X * list
> X) :=
>   match l with
>     | nil    => None
>     | c :: r => if beq_nat (projX c) id then Some ((c, r :: acc)) else f r
> id (c :: acc)
>   end.
>
> The above function simply looks for an element whose projection is equal to
> the given id. The problem arises due to the use of an accumulator - it will
> yield a weird induction hypothesis..
>
> For instance, in this following lemma
>
> Lemma fact:
>   forall l id X c r,
>   f l id X = Some (c,r) ->
>   X = nil ->    (*there's a reason for not directly including 'nil' in the
> function call above, but can be ignored for this question...*)
>   forall x, In x l <-> In x (c :: r).
> Proof.
>   intros.
>   functional induction f l id X0; inversion H; subst; clear H.
>   Case "branch true".
>     admit. (*trivially true*)
>   Case "branch false".
>     (*weird induction hyp*)
> Qed.
>
> The induction hypothesis generated for the branch with the recursive call is
> as follows:
>
> IHo : f r0 id (c0 :: nil) = Some (c, r) ->
>         c0 :: nil = nil ->
>         (In x r0 <-> In x (c :: r))
>
> This, of course, doesn't help much..
>
> The first thing that I taught was to define my own induction principle, but
> i'm wondering if I am missing a terribly easier approach to solve the above
> lemma (and many of the like..)?
>
> Or more generally, how do guys go about reasoning on functions with
> accumulators?
>
> Thank you!
>
> --
> Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600
> dollars last year.
> Marge: Bart! Don't make fun of grad students, they just made a terrible life
> choice.

Attachment: facts_with_accs.v
Description: Binary data