Re: [PVS-Help] choose problem

[Holger Pfeifer <Holger.Pfeifer@xxxxxxxxxx>]

Dear Song,

[NB: the declarations you've included in your mail contain a few
mistakes; I've tried to mend these in the PVS theory attached to this
mail. The following is relative to that theory which might differ from
yours.]

> <<(env1:VarEnv,env2:VarEnv): bool= FORALL (x:Vars): env1(x)=env2(x)
>
> c(f,g): trans =
>   LAMBDA (s: Env): choose({y: VarEnv|y<<f(s) or y<<g(s)})
>
> how can I to proof the nonemptyness of {y: VarEnv|y<<f(s) or y<<g(s)}?

You need to find a "y" such that "y << f(s)" or "y << g(s)". Since
"<<" essentially denotes equality on environments, you can pick, e.g.,
"f(s)" for "y".

A step-by-step proof of the TCC would be

 (skosimp*)
 (expand "nonempty?")
 (expand "empty?")
 (expand "member")
 (inst -1 "f!1(s!1)")
 (flatten)
 (expand "<<")

a more automatic version would use (grind :if-match best).


>   |-------
> {1}   choose({y: VarEnv | y << f!1(Init_env) OR y << g!1(Init_env)}) =
>        choose({y: VarEnv | y << g!1(Init_env) OR y << f!1(Init_env)}
>
> then I do not know how to proof this issue

Since "OR" is commutative, the two sets are equal. To tell PVS that
you know this, use the command "case-replace". In a subsequent step
you need to show that the sets are indeed equal; you need the command
"apply-extensionality" to do this. A complete step-by-step proof is as
follows:

 (skosimp*)
 (expand "c")
 (case-replace
  "{y: Env | y << f!1(init_env) OR y << g!1(init_env)} = {y: Env | y <<
g!1(init_env) OR y << f!1(init_env)}")
 (apply-extensionality :hide? t)
 (iff)
 (ground)

Regards,

	- Holger

song : THEORY

BEGIN

  Vars  : TYPE
  Value : TYPE+  

  % Env   : TYPE = [Env->Value]  % mistake:  Env also occurs on right-hand side

  Env   : TYPE = [Vars -> Value]
  trans : TYPE = [Env  -> Env]

  f,g   : VAR trans


  % <<(env1:VarEnv,env2:VarEnv): bool =   % VarEnv not declared, should be Env?
  %  FORALL (x:Vars): env1(x)=env2(x)

  <<(env1:Env,env2:Env): bool = 
    FORALL (x:Vars): env1(x)=env2(x)


  c(f,g): trans = 
    LAMBDA (s: Env): choose({y: Env | y<<f(s) OR y<<g(s)})


  init_env : Env

% Existence TCC  for  init_env: Env
% init_env_TCC1: OBLIGATION EXISTS (x: Env): TRUE;
%
% Solution: type Value must be non-empty: Value : TYPE+

  L1 : LEMMA
    FORALL (f, g: trans):
         c(f, g)(init_env) = c(g, f)(init_env)

END song