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

PVS Bug 461


Synopsis:        GRIND inconsistency + nontermination
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Tue May  2 11:00:01 2000
Originator:      Myla Archer
Organization:    itd.nrl.navy.mil
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
      I have found a case where the termination of GRIND depends on the types
  of the elements of a tuple.  In addition, I have found a case when whether
  GRIND needs to be supplemented by APPLY-EXTENSIONALITY depends on the types
  of the elements of a tuple.
  
      Both of these cases involve only simple reasoning about the relationships
  between a tuple and its projections -- that is, they are independent of the
  actual element types in the tuples.
  
      Various versions of these cases can be found in the appended dump.
  
             -- Myla
  
  ****************************************************************************
  %Patch files loaded: patch2 version 1.2.2.36
  %                    patch2-test version NRL Patches of 1999-09-08
  
  $$$PVSHOME/.pvs.lisp
  (defun new-formula-nums (goal par-goal &optional (pos 1) (neg -1))
    (when goal
      (let ((pos-s-forms (pos-s-forms goal))
  	  (parent-pos-s-forms (pos-s-forms par-goal))
  	  (neg-s-forms (neg-s-forms goal))
  	  (parent-neg-s-forms (neg-s-forms par-goal)))
        (nconc (new-neg-formula-nums neg-s-forms parent-neg-s-forms neg)
               (new-pos-formula-nums pos-s-forms parent-pos-s-forms pos)))))
  
  $$$tuple_props.pvs
  tuple_props	: THEORY
  
    BEGIN
  
        T: TYPE+;
  
        Pair_1: TYPE = [T,T];
  
        Pair_2: TYPE = [integer,integer];
   
        Triple_1: TYPE = [T,T,T];
  
        Triple_2: TYPE = [integer, integer, integer];
  
        Triple_3: TYPE = [boolean, boolean, boolean];
  
     %grind does not prove this one; it does not terminate.
     lemma_1: LEMMA ( FORALL (p: Pair_1):
        p = (PROJ_2(p), PROJ_1(p)) => PROJ_1(p) = PROJ_2(p) );
  
     %grind does not prove this one; it does not terminate.
     lemma_1A: LEMMA ( FORALL (p: [Triple_2,Triple_2]):
        p = (PROJ_2(p), PROJ_1(p)) => PROJ_1(p) = PROJ_2(p) );
  
     %grind proves this one.
     lemma_2: LEMMA ( FORALL (p: Pair_2):
        p = (PROJ_2(p), PROJ_1(p)) => PROJ_1(p) = PROJ_2(p) );
  
     %grind at least terminates, but then one must use (apply-extensionality 2)
 .
     lemma_3: LEMMA ( FORALL (p: Pair_1):
        not(PROJ_1(p) = PROJ_2(p)) => (PROJ_1(p), PROJ_2(p)) = p );
  
     %grind proves this one.
     lemma_4: LEMMA ( FORALL (p: Pair_2):
        not(PROJ_1(p) = PROJ_2(p)) => (PROJ_1(p), PROJ_2(p)) = p );
  
     %grind at least terminates, but then one must use (apply-extensionality 3)
 .
     lemma_5: LEMMA ( FORALL (t: Triple_1):
        not(PROJ_1(t) = PROJ_2(t) or PROJ_1(t) = PROJ_3(t))
           => (PROJ_1(t), PROJ_2(t), PROJ_3(t)) = t );
  
     %grind proves this one.
     lemma_6: LEMMA ( FORALL (t: Triple_2):
        not(PROJ_1(t) = PROJ_2(t) or PROJ_1(t) = PROJ_3(t))
           => (PROJ_1(t), PROJ_2(t), PROJ_3(t)) = t );
  
     %grind proves this one.
     lemma_7: LEMMA ( FORALL (t: Triple_3):
        not(PROJ_1(t) = PROJ_2(t) or PROJ_1(t) = PROJ_3(t))
           => (PROJ_1(t), PROJ_2(t), PROJ_3(t)) = t );
  
     %grind at least terminates, but then one must use (apply-extensionality 3)
 .
     lemma_8: LEMMA ( FORALL (t: [Triple_3,Triple_3,Triple_3]):
        not(PROJ_1(t) = PROJ_2(t) or PROJ_1(t) = PROJ_3(t))
           => (PROJ_1(t), PROJ_2(t), PROJ_3(t)) = t );
  
    END tuple_props
  
  $$$tuple_props.prf
  (|tuple_props|
   (|T_nonempty| 0
    (|T_nonempty-1| NIL 3159291779 NIL NIL NIL NIL NIL NIL NIL NIL))
   (|lemma_1| 0
    (|lemma_1-1| NIL 3159291779 3159291922
     ("" (SKOLEM!)
      (("" (FLATTEN)
        (("" (CASE "p!1 = (PROJ_1(p!1), PROJ_2(p!1))")
          (("1" (ASSERT) NIL NIL) ("2" (APPLY-EXTENSIONALITY) NIL NIL))
          NIL))
        NIL))
      NIL)
     UNCHECKED
     ((T NONEMPTY-TYPE-DECL NIL |tuple_props| NIL)
      (|Pair_1| TYPE-EQ-DECL NIL |tuple_props| NIL)
      (|boolean| NONEMPTY-TYPE-DECL NIL |booleans| NIL)
      (= CONST-DECL "[T, T -> boolean]" |equalities| NIL))
     65893 170 T NIL))
   (|lemma_1A| 0
    (|lemma_1A-1| NIL 3159295341 3159295437
     ("" (SKOLEM!)
      (("" (FLATTEN)
        (("" (CASE "p!1 = (PROJ_1(p!1), PROJ_2(p!1))")
          (("1" (ASSERT) NIL NIL) ("2" (APPLY-EXTENSIONALITY) NIL NIL))
          NIL))
        NIL))
      NIL)
     PROVED
     ((|number| NONEMPTY-TYPE-DECL NIL |numbers| NIL)
      (|boolean| NONEMPTY-TYPE-DECL NIL |booleans| NIL)
      (|real_pred| CONST-DECL "[number -> boolean]" |reals| NIL)
      (|rational_pred| CONST-DECL
       "[{x: number | real_pred(x)} -> boolean]" |rationals| NIL)
      (|rational| NONEMPTY-TYPE-FROM-DECL NIL |rationals| NIL)
      (|integer_pred| CONST-DECL
       "[{x: {x: number | real_pred(x)} | rational_pred(x)} -> boolean]"
       |integers| NIL)
      (|integer| NONEMPTY-TYPE-FROM-DECL NIL |integers| NIL)
      (|Triple_2| TYPE-EQ-DECL NIL |tuple_props| NIL)
      (= CONST-DECL "[T, T -> boolean]" |equalities| NIL))
     70792 26720 T NIL))
   (|lemma_2| 0
    (|lemma_2-1| NIL 3159291779 3159291827 ("" (GRIND) NIL NIL) UNCHECKED
     NIL 2587 120 T NIL))
   (|lemma_3| 0
    (|lemma_3-1| NIL 3159292133 3159292230
     ("" (GRIND) (("" (APPLY-EXTENSIONALITY 2) NIL NIL)) NIL) UNCHECKED
     ((|Pair_1| TYPE-EQ-DECL NIL |tuple_props| NIL)
      (T NONEMPTY-TYPE-DECL NIL |tuple_props| NIL))
     25161 250 T NIL))
   (|lemma_4| 0
    (|lemma_4-1| NIL 3159292199 3159292239 ("" (GRIND) NIL NIL) UNCHECKED
     NIL 5680 40 T NIL))
   (|lemma_5| 0
    (|lemma_5-1| NIL 3159293179 3159294530
     ("" (GRIND) (("" (APPLY-EXTENSIONALITY 3) NIL NIL)) NIL) UNCHECKED
     ((|Triple_1| TYPE-EQ-DECL NIL |tuple_props| NIL)
      (T NONEMPTY-TYPE-DECL NIL |tuple_props| NIL))
     12632 210 T NIL))
   (|lemma_6| 0
    (|lemma_6-1| NIL 3159293179 3159294510 ("" (GRIND) NIL NIL) UNCHECKED
     NIL 2455 40 T NIL))
   (|lemma_7| 0
    (|lemma_7-1| NIL 3159293179 3159294494 ("" (GRIND) NIL NIL) UNCHECKED
     NIL 1843 70 T NIL))
   (|lemma_8| 0
    (|lemma_8-1| NIL 3159295117 3159295174
     ("" (GRIND) (("" (APPLY-EXTENSIONALITY 3) NIL NIL)) NIL) UNCHECKED
     ((|boolean| NONEMPTY-TYPE-DECL NIL |booleans| NIL)
      (|Triple_3| TYPE-EQ-DECL NIL |tuple_props| NIL))
     50092 220 T NIL)))

How-To-Repeat: 

Fix: 

 [davesc]
 Fixed in 2.3.1 

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