Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 636


Synopsis:        typecheck problem
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Wed Dec 12 03:25:00 2001
Originator:      Hendrik Tews
Organization:    tcs.inf.tu-dresden.de
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  
  --Tgb4DB7Bu2
  Content-Type: text/plain; charset=us-ascii
  Content-Description: message body text
  Content-Transfer-Encoding: 7bit
  
  Hi,
  
  the appended file typechecks in pvs 2.3 without the K_conversion
  (at least without reporting it). However typechecking in 2.4
  fails because some instanciation is not found. 
  
  Bye,
  
  Hendrik
  
  
  --Tgb4DB7Bu2
  Content-Type: text/plain
  Content-Disposition: inline;
  	filename="def.pvs"
  Content-Transfer-Encoding: 7bit
  
  Coproduct[X, Y : Type] : Datatype
  Begin
    in1(acc1 : X) : in1?
    in2(acc2 : Y) : in2?
  end Coproduct
  
  CoproductPair[X,Y,Z : Type] : Theory
  Begin
    Importing Coproduct[X,Y]
  
    f : Var [X -> Z]
    g : Var [Y -> Z]
  
    copair(f,g) : [Coproduct[X,Y] -> Z] =
      Lambda(xy : Coproduct[X,Y]) : Cases xy OF
  	in1(x) : f(x),
  	in2(y) : g(y)
      Endcases
  
  end CoproductPair
  
  Pi_12[ X, Y : Type] : Theory
  Begin
    pi_1( x : X, y : Y ) : X = x
    pi_2( x : X, y : Y ) : Y = y
  end Pi_12
  
  Product[A,B,C : Type] : Theory
  Begin
    IMPORTING Pi_12
  
    f : Var [C -> A]
    g : Var [C -> B]
  
    pair(f,g) : [C -> [A,B]] =
  	    lambda(c : C) : (f(c), g(c))
  
  end Product
  
  
  ProductFun[A,B,C,D : Type] : Theory
  Begin
    Importing Product
  
    f : Var [A -> C]
    g : Var [B -> D]
  
    times(f,g) : [[A,B] -> [C,D]] =
      pair(f o pi_1[A,B], g o pi_2[A,B])
  
  end ProductFun
  
  ExpCat1[A,B : Type] : Theory
  Begin
    eval(f : [A -> B], a : A) : B = f(a)
  end ExpCat1
  
  
  ExpCat2[A,B,C : Type] : Theory
  Begin
    Importing ProductFun, ExpCat1[A,B]
  
    abstr(g : [[C,A] -> B]) : [C -> [A -> B]] =
  	    lambda(c:C) : lambda(a:A) : g(c,a)
  
  end ExpCat2
  
  
  
  Exp[A,B,C,D : Type] : Theory
  Begin
    IMPORTING ExpCat2
  
    =>(g : [C -> A], f : [B -> D]) : [[A -> B] -> [C -> D]] =
      abstr(f o eval o times(id[[A->B]], g))
  
  End Exp
  
  Product3[A,B,C,D : Type] : Theory
  Begin
    f : Var [D -> A]
    g : Var [D -> B]
    h : Var [D -> C]
  
    pair3(f,g,h) : [D -> [A,B,C]] = 
  	  lambda(c : D) : (f(c), g(c), h(c))
  
  end Product3
  
  
  Product3Fun[A,B,C,D,E,F : Type] : Theory
  Begin
    Importing Product3
  
    f : Var [A -> D]
    g : Var [B -> E]
    h : Var [C -> F]
  
    times3(f,g,h) : [[A,B,C] -> [D,E,F]] = 
  	  let p1 = lambda(abc : [A,B,C]) : proj_1(abc),
  	      p2 = lambda(abc : [A,B,C]) : proj_2(abc),
  	      p3 = lambda(abc : [A,B,C]) : proj_3(abc)
  	  in pair3(f o p1, g o p2, h o p3)
  
  end Product3Fun
  
  J[Y,X : Type] : Theory
  Begin
    importing Exp
  
    JIface : Type = [nat, [nat -> X], [Y -> nat]]
  
  end J
  
  JMethods[X : Type] : Theory
  Begin
    IMPORTING J[X,X]
    
    jc : Var [X -> JIface[X,X]]
    val(jc)(x:X) : nat = Proj_1(jc(x))
    set_val(jc)(x:X,n:nat) : X = Proj_2(jc(x))(n)
    fun(jc)(x:X,y:X) : nat = Proj_3(jc(x))(y)
  
  end JMethods
  
  JFun[Y, X,V,U : Type] : Theory
  Begin
    IMPORTING J, Product3Fun
  
    f : Var [X -> U]
    g : Var [V -> Y]
  
    jf(g,f) : [JIface[Y,X] -> JIface[V,U]] =
  	  times3( id[nat], (id[nat] => f), (g => id[nat]))
  
  End JFun
  
  JSemantics[X : Type] : Theory
  Begin
    IMPORTING JMethods[X]
  
    jc : Var [X -> JIface[X,X]]
  
    fun_prop(jc)(x:X)(f : [nat,nat -> nat]) : bool = 
      Forall(y : X) :
  	 fun(jc)(x,y) = f(val(jc)(x), val(jc)(y)) AND
  	 (Forall(n : nat) : fun(jc)(set_val(jc)(x,n),y) = f(n, val(jc)(y)))
  
    JAssert?(jc) : PRED[X] = Lambda(x:X) :
      (Forall( n : nat) : val(jc)(set_val(jc)(x,n)) = n) AND
      (Forall( n1, n2 : nat, y : X) : 
  	  fun(jc)(set_val(jc)(set_val(jc)(x,n1), n2), y) = 
  		  fun(jc)(set_val(jc)(x, n2), y))        AND
      (Exists(f : [nat,nat -> nat]) : fun_prop(jc)(x)(f))
  	  
    JModel?(jc) : bool = Forall(x:X) : JAssert?(jc)(x)
  end JSemantics
  
  
  JTheory[X : Type] : Theory
  Begin
    IMPORTING JSemantics[X]
  
    c : Var (JModel?[X])
  
    get_fun(c)(x:X) : [nat,nat -> nat] = 
       choose(Lambda(f: [nat, nat -> nat]): fun_prop(c)(x)(f))
  
  end JTheory
  
  JMorph[X, Y : Type] : Theory
  Begin
    Importing JFun, JTheory
    
    f : Var [X -> Y]
    c : Var (JModel?[X])
    d : Var (JModel?[Y])
  
    J_morph?(c,d)(f) : bool = 
  	  (jf[X,X,X,Y](id[X],f) o c) = (jf[Y,Y,X,Y](f,id[Y]) o d o f)
  
    jmorph_char : Lemma J_morph?(c,d)(f) IFF Forall(x : X) : 
      (val(c)(x) = val(d)(f(x))) AND
      (Forall(n : nat) : f(set_val(c)(x,n)) = set_val(d)(f(x),n)) AND
      (Forall(y : X) : fun(c)(x, y) = fun(d)(f(x), f(y)))
  
  end JMorph
  
  JCoproduct[X,Y : Type] : Theory
  Begin
    IMPORTING JMorph, Coproduct
  
    c : Var (JModel?[X])
    d : Var (JModel?[Y])
  
    XpY : Type = Coproduct[X,Y]
  
    val(c,d) : [XpY -> nat] = Lambda( z : XpY ) : 
  	cases z of
  	  in1(x) : val(c)(x),
  	  in2(y) : val(d)(y)
  	endcases
  
    get_fun(c,d)(z : XpY) : [nat,nat -> nat] = 
  	cases z of
  	  in1(x) : get_fun(c)(x),
  	  in2(y) : get_fun(d)(y)
  	endcases
  
    cpd(c,d) : [XpY -> JIface[XpY,XpY]] = Lambda( z : XpY ) :
      cases z of 
  	in1(x) : ( val(c)(x), 
  		   Lambda(n : nat) : in1[X,Y](set_val(c)(x,n)), 
  		   Lambda(z1 : XpY) : fun(c)(x, set_val(c)(x, val(c,d)(z1)))),
  	in2(y) : ( val(d)(y), 
  		   Lambda(n : nat) : in2[X,Y](set_val(d)(y,n)), 
  		   Lambda(z1 : XpY) : fun(d)(y, set_val(d)(y, val(c,d)(z1))))
      endcases
  
  end JCoproduct
    
  
  JCoproductProp[X,Y,Z : Type] : Theory
  Begin
    IMPORTING JCoproduct, CoproductPair
  
    c : Var (JModel?[X])
    d : Var (JModel?[Y])
    e : Var (JModel?[Z])
  
    copair(c,d,e)(f : (J_morph?(c,e)), g : (J_morph?(d,e))) : [XpY[X,Y] -> Z] =
  
  	  copair(f,g)
  
    copair_unique : Lemma Forall(f : (J_morph?(c,e)), g : (J_morph?(d,e))) : 
  	Forall(h : (J_morph?(cpd(c,d), e))) : 
  	   h o in1 = f AND h o in2 = g IMPLIES
  		h = copair(c,d,e)(f,g)
  
  end JCoproductProp
  
  
  
  --Tgb4DB7Bu2--
  

How-To-Repeat: 

Fix: 
Modified instantiate-resolution to not require all actuals to be matched.
This is required because tc-match actually does a better job in 2.4, so
when the partially instantiated type is compared to the expected type, it
b provides fewer bindings.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools