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

[PVS-Help] how to prove this lemma?



Hi,

Could anyone please show me how to prove the lemma "counterlemma" in the
attached theory "standard_environments"?

Thanks a lot.

Bin

===========================================================================
standard_environments [ domain: type+
                       ,registerRange: posnat ]
		: THEORY

  BEGIN

  % The number of registers in our model.
  registerNumber: type = {y:nat | y <= registerRange}

  % Suppose we have 2 counters
  counterRange: macro posnat = 1

  % The number of counters in our model.
  counterNumber: type = {y:nat | y <= counterRange}

  % Memory location and register are two datatypes in assembly language.
  % Also, in order to evaluate branch upward loops, we introduce
  % a datatype "counter". The datatype "term" consists of the three elements.
  term: DATATYPE
    BEGIN
      m(n:int): memory?
      r(n:registerNumber): register?
      counter(n:counterNumber): loopCounter?
    END term

  % Datatype "register" is injective. A widely used lemma in the proofs later.
  r_injective: sublemma
    FORALL (m,n:registerNumber): (r(m)=r(n)) = (m=n);

  % Datatype "memory" is injective.
  m_injective: sublemma
    FORALL (s,t:int): (m(s)=m(t)) = (s=t);

  % Counter and register are different types.
  counter_register: sublemma
    FORALL (n:counterNumber, m:registerNumber): counter(n) /= r(m);

  % The environment of the assembly language.
  env: TYPE = [ term -> domain]

  % Types: memory location, register, loop counter.
  memory: TYPE = (memory?);
  register: TYPE = (register?);
  loopCounter: TYPE = (loopCounter?);

  counterlemma: lemma
    FORALL (ctr:loopCounter): ctr=counter(0) or ctr=counter(1);

  END standard_environments


%% PVS Version 3.1
%% 6.2 [Linux (x86)] (Feb 14, 2003 18:46)
$$$PVSHOME/.pvs.lisp
(defun make-accessor-funtype (domain range deps)
  (if deps
      (let* ((tdom (typecheck* (copy domain) nil nil nil))
             (dtype (if (dep-binding? tdom)
                        tdom
                        (mk-dep-binding (make-new-variable 'd
                                          (list tdom range))
                                        tdom)))
             (dep-name (make-variable-expr dtype))
             (*bound-variables* (cons dtype *bound-variables*))
             (subst-range (substit range
                            (if (dep-binding? domain)
                                (pairlis
                                 (cons domain (mapcar #'declaration deps))
                                 (cons dtype
                                       (mapcar #'(lambda (dep)
                                                   (typecheck* (mk-application (id dep)
                                                                 dep-name)
                                                               (type dep) nil nil))
                                         deps)))
                                (pairlis
                                 (mapcar #'declaration deps)
                                 (mapcar #'(lambda (dep)
                                             (typecheck* (mk-application (id dep)
                                                           dep-name)
                                                         (type dep) nil nil))
                                   deps))))))
        (mk-funtype dtype subst-range))
      (mk-funtype domain range)))

(defmethod substit-binding (expr alist)
  (let* ((newtype (substit* (type expr) alist))
         (newdtype (if (tc-eq (print-type (type expr))
                              (declared-type expr))
                       (if (eq (print-type (type expr)) (print-type newtype))
                           (declared-type expr)
                           (print-type newtype))
                       (substit* (declared-type expr) alist))))
    (lcopy expr
      'type newtype
      'declared-type newdtype)))

(defmethod pp* ((ass assignment))
  (with-slots (arguments expression) ass
    (pprint-logical-block (nil nil)
      (pprint-indent :current 2)
      (if (and (typep ass 'uni-assignment)
               (simple-name? (caar arguments)))
          (pp* (caar arguments))
          (pp-arguments* arguments))
      (write-char #\space)
      (pprint-newline :fill)
      (write ":=")
      (write-char #\space)
      (pp* expression))))


$$$standard_environments.pvs
% Introduce a standard environment of assembly languages. "Term" consists of "memory 
% location", "register" and "counter". Data type "counter" is used to count the loops
% in branch upward structures. 
 
standard_environments [ domain: type+ 
                       ,registerRange: posnat ]
		: THEORY

  BEGIN

  % The number of registers in our model.
  registerNumber: type = {y:nat | y <= registerRange}
  
  % Suppose we have 2 counters
  counterRange: macro posnat = 1

  % The number of counters in our model. 
  counterNumber: type = {y:nat | y <= counterRange} 
 
  % Memory location and register are two datatypes in assembly language.
  % Also, in order to evaluate branch upward loops, we introduce 
  % a datatype "counter". The datatype "term" consists of the three elements. 
  term: DATATYPE
    BEGIN
      m(n:int): memory?
      r(n:registerNumber): register?
      counter(n:counterNumber): loopCounter?
    END term

  % Datatype "register" is injective. A widely used lemma in the proofs later.
  r_injective: sublemma
    FORALL (m,n:registerNumber): (r(m)=r(n)) = (m=n);

  % Datatype "memory" is injective. 
  m_injective: sublemma
    FORALL (s,t:int): (m(s)=m(t)) = (s=t);

  % Counter and register are different types.
  counter_register: sublemma
    FORALL (n:counterNumber, m:registerNumber): counter(n) /= r(m);

  % The environment of the assembly language.
  env: TYPE = [ term -> domain] 
  
  % Types: memory location, register, loop counter.
  memory: TYPE = (memory?);
  register: TYPE = (register?);
  loopCounter: TYPE = (loopCounter?); 

  counterlemma: lemma
    FORALL (ctr:loopCounter): ctr=counter(0) or ctr=counter(1); 

  END standard_environments

$$$standard_environments.prf
(standard_environments
 (term_r_eta_TCC1 0
  (term_r_eta_TCC1-1 nil 3284921102 3297206728
   ("" (skolem * "x")
    (("" (typepred "n(x)") (("" (assert) nil nil)) nil)) nil)
   proved
   ((n adt-accessor-decl "[d: term ->
   {x: int |
            IF memory?(d) THEN TRUE
            ELSE IF register?(d) THEN x >= 0 AND x <= registerRange
                 ELSE x >= 0 AND x <= 1
                 ENDIF
            ENDIF}]" standard_environments nil)
    (registerRange formal-const-decl "posnat" standard_environments
     nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (<= const-decl "bool" reals nil)
    (TRUE const-decl "bool" booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (>= const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (register? adt-recognizer-decl "[term -> boolean]"
     standard_environments nil)
    (memory? adt-recognizer-decl "[term -> boolean]"
     standard_environments nil)
    (term type-decl nil standard_environments nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (FALSE const-decl "bool" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   24 10 t shostak))
 (term_counter_eta_TCC1 0
  (term_counter_eta_TCC1-1 nil 3284921103 3297206728
   ("" (skolem * "x")
    (("" (typepred "n(x)") (("" (assert) nil nil)) nil)) nil)
   proved
   ((n adt-accessor-decl "[d: term ->
   {x: int |
            IF memory?(d) THEN TRUE
            ELSE IF register?(d) THEN x >= 0 AND x <= registerRange
                 ELSE x >= 0 AND x <= 1
                 ENDIF
            ENDIF}]" standard_environments nil)
    (registerRange formal-const-decl "posnat" standard_environments
     nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (<= const-decl "bool" reals nil)
    (TRUE const-decl "bool" booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (>= const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (register? adt-recognizer-decl "[term -> boolean]"
     standard_environments nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (loopCounter? adt-recognizer-decl "[term -> boolean]"
     standard_environments nil)
    (memory? adt-recognizer-decl "[term -> boolean]"
     standard_environments nil)
    (term type-decl nil standard_environments nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (FALSE const-decl "bool" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   14 20 t shostak))
 (r_injective 0
  (r_injective-1 nil 3284921102 3297206873
   ("" (skolem * ("m1" "n1"))
    (("" (iff)
      (("" (ground)
        (("" (case "n(r(n1))=n1 and n(r(m1))=m1")
          (("1" (flatten)
            (("1" (name "rn1" "r(n1)")
              (("1" (replace -1)
                (("1" (hide -1)
                  (("1" (name "rm1" "r(m1)")
                    (("1" (replace -1)
                      (("1" (hide -1) (("1" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide 2)
            (("2" (rewrite "term_n_r")
              (("2" (rewrite "term_n_r") nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   proved
   ((r adt-constructor-decl "[registerNumber -> (register?)]"
     standard_environments nil)
    (registerNumber type-eq-decl nil standard_environments nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (n adt-accessor-decl "[d: term ->
   {x: int |
            IF memory?(d) THEN TRUE
            ELSE IF register?(d) THEN x >= 0 AND x <= registerRange
                 ELSE x >= 0 AND x <= 1
                 ENDIF
            ENDIF}]" standard_environments nil)
    (registerRange formal-const-decl "posnat" standard_environments
     nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (<= const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
    (register? adt-recognizer-decl "[term -> boolean]"
     standard_environments nil)
    (TRUE const-decl "bool" booleans nil)
    (memory? adt-recognizer-decl "[term -> boolean]"
     standard_environments nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (term type-decl nil standard_environments nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number nonempty-type-decl nil numbers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (term_n_r formula-decl nil standard_environments nil))
   61573 2170 t nil))
 (m_injective 0
  (m_injective-1 nil 3284921102 nil
   ("" (skolem * ("s1" "t1"))
    (("" (iff)
      (("" (ground)
        (("" (case "n(m(t1))=t1 and n(m(s1))=s1")
          (("1" (flatten)
            (("1" (name "mt1" "m(t1)")
              (("1" (replace -1)
                (("1" (hide -1)
                  (("1" (name "ms1" "m(s1)")
                    (("1" (replace -1)
                      (("1" (hide -1) (("1" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide 2)
            (("2" (rewrite "term_n_m")
              (("2" (rewrite "term_n_m") nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   unfinished nil nil nil nil nil))
 (counter_register 0
  (counter_register-1 nil 3284921102 nil
   ("" (skolem!) (("" (grind) nil nil)) nil) unfinished nil nil nil nil
   nil))
 (counterlemma 0
  (counterlemma-1 nil 3297206732 3297207191
   ("" (skolem * "C")
    (("" (typepred "C")
      (("" (bddsimp) (("" (ground) (("" (postpone) nil nil)) nil))
        nil))
      nil))
    nil)
   unfinished nil 310521 2090 t shostak)))