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

[LET .. IN ..]



Dear pvs users,

I have got a problem with the LET statement of the pvs language. I work
on an embedding of a simple process algebra with value passing. To
express the substitution of an input variable by an output value, I
chooses to use the LET construction. Yet, I face a problem at the proof
level. Indeed, when I apply the 'skosimp' and 'lemma' rules, I am
surprised to note that the variable 'x' appearing in LET x=t IN is not
renamed with 'x!1'. Then, the substitution becomes impossible. I try
different ways to get round this lock, but my attempts do not suceed.
Have you got ideas to help me ?

Thanks in advance,
Gwen SalaŁn

% -------------------------
gloups : THEORY

BEGIN

N : TYPE+
M : TYPE+

B: TYPE

tau: M
I : [N, nat -> M]
O : [N, nat -> M]

conv : [M -> B] CONVERSION conv

nil : B
+, o, / : [B, B -> B]

n, m, n1, n2 : VAR N
F, G, H, I : VAR B
x, t : VAR nat

% ...

ax1 : AXIOM n1=n2 AND F = I(n1,x) o H AND G = O(n2,t) o I IMPLIES F/G =
I(n1,x) o (H/G) + O(n2,t) o (F/I) + tau o ((LET x=t IN H) / I)

% ...

th : THEOREM
  I(n,x) o O(m,x) o nil / O(n,2) o nil =
      I(n,x) o (O(n,2) o (O(m,x) o nil))
      + I(n,x) o (O(m,x) o (O(n,2) o nil))
      + O(n,2) o (I(n,x) o (O(m,x) o nil))
      + tau o O(m,2) o nil


END gloups

% --------------------------

Starting pvs-allegro5.0 -qq ...
Loading /usr/local/pvs/bin/ix86-redhat5/runtime/libacl503.so.
Mapping /usr/local/pvs/bin/ix86-redhat5/runtime/pvs-allegro5.dxl:
Setting up C heap, Setting up Lisp heap.
Allegro CL Professional Edition 5.0 [Linux/X86] (9/4/99 13:27)
Copyright (C) 1985-1998, Franz Inc., Berkeley, CA, USA.  All Rights
Reserved.
;; Optimization settings: safety 1, space 1, speed 3, debug 1.
;; For a complete description of all compiler switches given the
;; current optimization settings evaluate (EXPLAIN-COMPILER-SETTINGS).
USER(1):
USER(2):
th :

  |-------
{1}   FORALL (m, n: N, x: nat):
        conv(I(n, x)) o conv(O(m, x)) o nil / conv(O(n, 2)) o nil =
         conv(I(n, x)) o (conv(O(n, 2)) o (conv(O(m, x)) o nil)) +
          conv(I(n, x)) o (conv(O(m, x)) o (conv(O(n, 2)) o nil))
          + conv(O(n, 2)) o (conv(I(n, x)) o (conv(O(m, x)) o nil))
          + conv(tau) o conv(O(m, 2)) o nil

Rule? (skosimp)
Skolemizing and flattening,
this simplifies to:
th :

  |-------
{1}   conv(I(n!1, x!1)) o conv(O(m!1, x!1)) o nil / conv(O(n!1, 2)) o
nil =
       conv(I(n!1, x!1)) o (conv(O(n!1, 2)) o (conv(O(m!1, x!1)) o nil))
+
        conv(I(n!1, x!1)) o (conv(O(m!1, x!1)) o (conv(O(n!1, 2)) o
nil))
        + conv(O(n!1, 2)) o (conv(I(n!1, x!1)) o (conv(O(m!1, x!1)) o
nil))
        + conv(tau) o conv(O(m!1, 2)) o nil

Rule? (LEMMA "ax1"
     ("F" "conv(I(n!1, x!1)) o conv(O(m!1, x!1)) o nil" "G"
      "conv(O(n!1, 2)) o nil" "H" "conv(O(m!1, x!1)) o nil" "I" "nil"
      "n1" "n!1" "n2" "n!1" "t" "2" "x" "x!1"))

Applying ax1 where
  F gets conv(I(n!1, x!1)) o conv(O(m!1, x!1)) o nil,
  G gets conv(O(n!1, 2)) o nil,
  H gets conv(O(m!1, x!1)) o nil,
  I gets nil,
  n1 gets n!1,
  n2 gets n!1,
  t gets 2,
  x gets x!1,
this simplifies to:
th :

{-1}  n!1 = n!1 AND
       conv(I(n!1, x!1)) o conv(O(m!1, x!1)) o nil =
        conv(I(n!1, x!1)) o (conv(O(m!1, x!1)) o nil)
        AND conv(O(n!1, 2)) o nil = conv(O(n!1, 2)) o nil
       IMPLIES
       conv(I(n!1, x!1)) o conv(O(m!1, x!1)) o nil / conv(O(n!1, 2)) o
nil
        =
        conv(I(n!1, x!1)) o
         (conv(O(m!1, x!1)) o nil / conv(O(n!1, 2)) o nil)
         +
         conv(O(n!1, 2)) o
          (conv(I(n!1, x!1)) o conv(O(m!1, x!1)) o nil / nil)
         + conv(tau) o ((LET x = 2 IN conv(O(m!1, x!1)) o nil) / nil)
  |-------
[1]   conv(I(n!1, x!1)) o conv(O(m!1, x!1)) o nil / conv(O(n!1, 2)) o
nil =
       conv(I(n!1, x!1)) o (conv(O(n!1, 2)) o (conv(O(m!1, x!1)) o nil))
+
        conv(I(n!1, x!1)) o (conv(O(m!1, x!1)) o (conv(O(n!1, 2)) o
nil))
        + conv(O(n!1, 2)) o (conv(I(n!1, x!1)) o (conv(O(m!1, x!1)) o
nil))
        + conv(tau) o conv(O(m!1, 2)) o nil

Rule?