The Coq mailing list

[Nuno Gaspar <(e29315a54f%hidden_head%e29315a54f)nmpgaspar(e29315a54f%hidden_at%e29315a54f)gmail.com(e29315a54f%hidden_end%e29315a54f)>]

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.