[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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
> 
>