The Coq mailing list

[staecker<cstaecker AT fairfield.edu>]

Hi all-
Sorry if this is an easy question. I hope there's an easy answer, but I can't
figure it out.

I have a datatype consisting of letters and letter-inverses taken from some
set, defined like: 

Variable V:Set.
Inductive Letter:Type :=
  | L : V -> Letter
  | Li : V -> Letter.

Now I want a function which adds a letter to the front of a list, but cancels
the letters if the newly added one is the inverse of the element on front. So:
Reduce_cons (L a) (Li b :: L c :: nil) = L a :: Li b :: L a :: nil,
and
Reduce_cons (L a) (Li a :: L c :: nil) = L c :: nil.

I'd originally written my function like this:
Definition Reduce_cons (l:Letter) (w:Word):Word :=
  match l with
    L c  => match w with
              Li c :: _ => tail w
            | _         => L c::w
            end
  | Li c => match w with
              L c :: _ => tail w
            | _        => Li c::w
            end
  end.

But I realized that the pattern matching is treating the inner c's as new
variables, so this doesn't work. (This would make Reduce_cons (L a) (Li b :: L
c :: nil) = L c :: nil, which I don't want.)

Any suggestions on defining this properly? I tried to do something with
if/else, but I get confused working with bools vs Props. I want to say
something like
Reduce_cons l w :=
match w with 
  nil => l :: nil
| b::bs => if (b = Linverse(l)) then bs else l::b::bs
(where Linverse exchanges L for Li)
But the above doesn't like the equal sign, wants a bool instead, and I don't
know how to make that work.

Thanks a lot-
chris