# Re: Questions on conversion/coercion.

```
a of type aset

is not the same as

a of type bset

they are different entities, of different types.

Here's something that will do what you want.  (grind) proves the
theorem.

comp  % [ parameters ]
: THEORY

BEGIN

% ASSUMING
% assuming declarations
% ENDASSUMING

bset : TYPE = {a, b, c, d, e, f}

aset_set : setof [bset] = {x : bset | x = a or x = b or x = c}

aset : TYPE = (aset_set)

t : THEOREM FORALL (e1:aset): EXISTS (e2:bset): e1 = e2

END comp

>
> Hi.
>
> I have a question about conversion/coercion.
>
> 1.
> I specified two enumerated types. Every member of A type
> is the member of B type. And I want to verify every member
> of A is the member of B (theorem t). But I cannot do it.
> Because the  set A type and the set B type is different.
> How can I prove it?
>
> comp : THEORY
> BEGIN
>   aset : TYPE = {a, b}
>   bset : TYPE = {a, b, c, d, e, f}
>
>   t : THEOREM FORALL (e1:aset): EXISTS (e2:bset): e1 = e2
> END comp
>

> 2.
> I tried to define and use a conversion funtion. It is
> incorrect. What is the false? How can I modify it?
> I know that conv function is incorrect (skipping g),
> but I cannot find theorem t is incorrect.

Theorem t is fine, if conv typechecks correctly.  But you'll notice
that there's a TCC that gets generated for the definition of conv.
You need to show that g is in the domain of conv.  It's not, so the
proof of the TCC fails.  If you look at the proof status screen,
you'll find that the proof status of theorem t is incomplete (or
something like that) that's because the TCC for conv is false, and t
can't be known to be true until conv is typechecked.

If you changed your definition of conv to

conv(aele:aset): bset =
cases aele OF
a : a:bset,
b : b:bset,
g : c:bset
endcases

you'll be fine.

> comp1 : THEORY
> BEGIN
>   aset : TYPE = {a, b, g}
>   bset : TYPE = {a, b, c, d, e, f}
>
>   conv(aele:aset): bset =
>     cases aele OF
>       a : a:bset,
>       b : b:bset
>     endcases
>
>   t : THEOREM FORALL(e1:aset):EXISTS (e2:bset): conv(e1) = e2
> END comp1
>
> --
> Kim, Tae-ho
> thkim@salmosa.kaist.ac.kr
> http://salmosa.kaist.ac.kr/~thkim
>
>

```