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

Re: [PVS-Help] How to avoid/discharge an Existence TCC for my subtype



Hi Mark,

One simple "solution" is to state MyConstant /= SecondConstant as an axiom
and then use the axiom to prove the TCC1:
test : THEORY
BEGIN
  q: TYPE+
  r: TYPE+ FROM q
  MyConstant, SecondConstant : r
  MyAxiom : AXIOM
    MyConstant /= SecondConstant
  s: TYPE+ = { ra: r | ra /= MyConstant }
  firstrs : s
END test

Obviously, using axioms is not a very good idea in general. An alternative
solution may be to declare the types and the constants as parameters of
the theory and to state MyConstant /= SecondConstant as an assumption in
the assuming clause:

test2[q:TYPE+,r:TYPE+ from q, MyConstant,SecondConstant:r] : THEORY
BEGIN
  ASSUMING
    MyAssumption : ASSUMPTION
      MyConstant /= SecondConstant
  ENDASSUMING

  s: TYPE+ = { ra: r | ra /= MyConstant }

  firstrs : s

END test2

In either case, you may introduce inconsitencies. Therefore, it is a good
idea to provide a model of your theory. If you use axioms, you can provide
a model by using theory interpretations:

itest : THEORY
BEGIN
  IMPORTING test {{ q := int,
                    r_pred := LAMBDA(ra:int) : ra >= 0,
                    MyConstant := 0,
                    SecondConstant := 1 }}

END itest

If you use assumptions, you could define a theory that instantiate the
types and constants with concrete elements:

itest2 : THEORY
BEGIN
  IMPORTING test2[int,nat,0,1]
END itest2

Hope that this helps,
Cesar


Mark Brown said:
> Hello,
>
> I am having trouble discharging or avoiding this existence TCC:
>
> % Existence TCC generated (at line 199, column 2) for firstrs: s
>   % unfinished
> Firstrs_TCC1: OBLIGATION EXISTS (x: s): TRUE;
>
> The TCC is generated when I declare my first constant of type s:
>
> [199]  firstrs: s
>
> I have declared s to be a subtype of a subtype as follows:
>
> q: TYPE+
> r: TYPE+ FROM q
> MyConstant, SecondConstant: r
> s: TYPE = { ra: r | ra /= MyConstant }
>
> Alternatively, I get a slightly different Existence TCC that I don't
> know how to discharge if I declare s as a "TYPE+" as in:
>
> s: TYPE+ = { ra: r | ra /= MyConstant }
>
> Either way, I'd like to create the TYPE s which contains everything in
> TYPE r, except for one member.  Thanks in advance,
>
> Mark


-- 
Cesar A. Munoz H., Senior Staff Scientist
National Institute of Aerospace
100 Exploration Way
Hampton, VA 23666, USA
Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988