The Coq mailing list

[Agnishom Chattopadhyay <agnishom AT cmi.ac.in>]

Hi;

I have a record like this:

Record aggQueue : Type :=
    {
       ff : list B;
       ffA : list B;
       rr : list B;
       rrA : list B;
    }.

I want to define some kind of function on it, like this:

Fixpoint aggFlip (qq : aggQueue)  : aggQueue :=
    match (rr qq) with
    | [] => qq
    | (r :: rs) =>
      aggFlip {|
        ff := r :: (ff qq);
        ffA := (op r (aggff)) :: (ffA qq);
        rr := rs;
        rrA := tl (rrA qq)
      |}
    end.

When I try to define a function on a type expressed as a Record using a standard `Fixpoint` definition, Coq complains that the underlying data type is not recursive inductive.

One way to get around this problem seems to be to use the Function construct. However, when I do so, I cannot prove anything useful about the defined function because when I unfold it inside a proof it is terribly obscured by the surrounding proof terms.

Is there a way to do this cleanly?

--Agnishom