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

PVS Bug 495


Synopsis:        Possible bug with PVS 2.3 patches
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Thu Nov  9 03:00:02 2000
Originator:      Paul Y Gloess
Organization:    labri.u-bordeaux.fr
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  This is a multi-part message in MIME format.
  --------------EC83624259F1C4A40A64AE81
  Content-Type: text/plain; charset=us-ascii
  Content-Transfer-Encoding: 7bit
  
  Dear PVS hackers:
  
  I found something strange with PVS datatype reasoning: this involves a
  datatype with subtypes, and the extensionality principle. I think it is
  a bug. A detailed bug report is provided with the attached dump.
  
  Best regards,
  
  --
  Paul Y Gloess
            LaBRI:   http://dept-info.labri.u-bordeaux.fr/~gloess
     E.N.S.E.R.B.:   http://www.enserb.fr/~gloess
  
  
  
  --------------EC83624259F1C4A40A64AE81
  Content-Type: text/plain; charset=us-ascii;
   name="bug.adt_subtype_accessors.7_november_2000.apply_extensionality.dump"
  Content-Transfer-Encoding: 7bit
  Content-Disposition: inline;
   filename="bug.adt_subtype_accessors.7_november_2000.apply_extensionality.dum
 p"
  
  %Patch files loaded: patch2 version 1.2.2.36
  
  $$$apply_extensionality.pvs
  %%%
  %%% Paul Y Gloess <Paul.Gloess@LaBRI.U-Bordeaux.Fr>
  %%%   http://dept-info.labri.u-bordeaux.fr/~gloess/
  %%%   http://www.enserb.fr/~gloess/
  %%%
  %%% Bug report, 7 november 2000, with PVS 2.3 (and above patches):
  %%%
  %%%   The abstract datatype "adt" (defined in the imported theory "adt")
  %%%    has a subtype "color" with two constructors named "green" and "red"
  %%%    which share the same "sh" component of type "shell".
  %%%   This results in two accessors
  %%%    bearing the same name:
  %%%      sh: [(green?) -> shell]
  %%%      sh: [(red?) -> shell]    .
  %%%   The proof of first lemma, "shell_csh_extensionality_failing_proof",
  %%%    does not get through, which seems related to the fact that PVS does
  %%%    not handle the "(green?)" and "(red?)" cases symmetrically: it looks
  %%%    like PVS does not know that (green?) and (red?) are disjoint types.
  %%%   The second (identical) lemma, "shell_csh_extensionality", displays a
  %%%    complete proof which is explicitely split into two cases:
  %%%    "(green?(c))" and "(red?(c))": the first case is proved using
  %%%    (APPLY-EXTENSIONALITY); this command does not get rid of the second
  %%%    case which requires explicit use of "adt_shell_eta[str]" axiom
  %%%    generated by "adt[str]" theory. Furthermore, it appears necessary
  %%%    to use type coercion for "sh" when instantiating "shell?_var" with
  %%%    "sh::[(red?) -> shell](c)". [Additional comments are provided with
  %%%    the proof itself].
  %%%   Remark: the same problem occurs whether old or new decision procedures
  %%%            are in effect.
  %%%
  apply_extensionality[str: TYPE]: THEORY
  
    BEGIN
  
      IMPORTING adt[str]
  
      csh(c: color): shell
        = CASES c OF
            green(s): s,
            red(s): s
          ENDCASES ;
  
      cs(c: color): str
        = s(csh(c)) ;
  
      shell_csh_extensionality_failing_proof: LEMMA
        (FORALL (c: color):
           shell(cs(c)) = csh(c)) ;
  
      shell_csh_extensionality: LEMMA
        (FORALL (c: color):
           shell(cs(c)) = csh(c)) ;
  
    END apply_extensionality
  
  $$$apply_extensionality.prf
  (|apply_extensionality| (|csh_TCC1| "" (CASES-TCC) NIL NIL)
   (|shell_csh_extensionality_failing_proof| (:NEW-GROUND? T) ""
    (SKOLEM * "c")
    (("" (EXPAND "cs")
      (("" (EXPAND "csh")
        (("" (LIFT-IF)
          (("" (APPLY-EXTENSIONALITY)
            (("" (APPLY-EXTENSIONALITY) (("" (POSTPONE) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|shell_csh_extensionality| (:NEW-GROUND? T) "" (SKOLEM * "c")
    (("" (TYPEPRED "c")
      (("" (EXPAND "cs")
        (("" (EXPAND "csh")
          (("" (SPLIT)
            (("1" (LIFT-IF) (("1" (APPLY-EXTENSIONALITY) NIL NIL)) NIL)
             ("2" (LIFT-IF)
              (("2"
                (COMMENT "Why is (apply-extensionality) not proving this
  exactly like in the previous case where green?(c)?")
                (("2" (LEMMA "adt_shell_eta[str]")
                  (("2" (INST * "sh::[(red?) -> shell](c)")
                    (("2"
                      (COMMENT "Why are these LAMBDAs generated?
  Why don't they disappear with (beta)?")
                      (("2" (GROUND) NIL
                        ";;;Why are these LAMBDAs generated?
  ;;;Why don't they disappear with (beta)?"))
                      NIL))
                    NIL))
                  ";;;Why is (apply-extensionality) not proving this
  ;;;exactly like in the previous case where green?(c)?"))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  
  
  $$$adt.pvs
  adt[ str: TYPE ]: THEORY
  
    BEGIN
  
      adt: DATATYPE
        WITH SUBTYPES shell, color
  
      BEGIN
  
        shell(s: str): shell?: shell
  
        green(sh: shell): green?: color
        red(sh: shell): red?: color
  
      END adt
  
    END adt
  
  --------------EC83624259F1C4A40A64AE81--

How-To-Repeat: 

Fix: 

 [davesc]
 apply-extensionality does the right thing in 2.3.1 

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