The Coq mailing list

[Edsko de Vries <edskodevries AT gmail.com>]

Hi Chris,

To be able to write your function, you will need to posture that
equality on elements of your set V is decidable:

Parameter V_eq_dec : forall (v1 v2 : V), {v1 = v2} + {v1 <> v2}.

V_eq_dec is a function that, given two elements v1 and v2 of V, either
returns a proof that v1 is equal to v2 or returns a proof that v1 is
not equal to v2. You can use this function using a conditional
statement as follows if you don't care about the proofs:

Definition test (v1 v2 : V) : nat :=
  if V_eq_dec v1 v2 then 1 else 2.

Hope that helps,

Edsko

On Thu, Oct 28, 2010 at 12:45 AM, staecker 
<cstaecker AT fairfield.edu>
 wrote:
> 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
>