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

subtyping problem



I am surprised by the proof obligations generated by the
following example where I define two predicates p and q with
  (q) <: (p)  ie. (q) is a subtype of (p)

Then I define the function f with an argument of type (q) which is
initialised by a lambda expression with an argument of type (p). 

The initialization should be correct if the type of the rhs value is
a subtype of the type of the lhs value. However, PVS requires the types
to be identical (f_TCC3). Why ? Furthermore the TCC (1) seems 
inverted : it requires (p) :< (q).
Thanks for any help

JP Bodeveix
University Paul Sabatier
118 route de Narbonne
31062 Toulouse - FRANCE

------------------------------------------------------------------------

subtype: THEORY
  BEGIN
  
  p: pred[nat] = (LAMBDA (x: nat): x > 0)
  
  q: pred[nat] = (LAMBDA (x: nat): x > 1)
  
  % Subtype TCC generated (line 8) for  x: (p)
f_TCC1: OBLIGATION (FORALL (x: (p)): q(x));
  
  % Subtype TCC generated (line 8) for  x - 1
f_TCC2: OBLIGATION (FORALL (x: (p)): x - 1 >= 0);
  
  % Domain mismatch subtype TCC generated (line 8) for  (LAMBDA (x:
(p)): x - 1)
f_TCC3: OBLIGATION (FORALL (x1: (p), y1: (q)): p(y1) AND q(x1));
  
  f: [(q) -> nat] = (LAMBDA (x: (p)): x - 1)
  
  END subtype