Re: [PVS-Help] Unrecognized equality

[Sam Owre <owre@xxxxxxxxxxx>]

The command pvs-set-proof-parens does this.

Sam

Jerome <jerome@xxxxxxxxxxxxxx> wrote:

> Is there a way to get PVS to explicitly parenthesize? I'm running into
> this issue again (in a separate proof) and it'd be nice to see what
> PVS is thinking rather than trying to infer it. Thanks.
> 
> jerome
> 
> On Wed, Jun 25, 2008 at 06:01:03PM -0400, Cesar Munoz wrote:
> >The reason you cannot replace -2 in 2 is that infix symbols are
> >associated to the left. Therefore, what you have in 2 (lhs) is actually:
> >
> >((s!1(e!1) o fold(s!1, U!1)) o (fold(t!1, U!1)) o t!1(e!1))
> >
> >which doesn't match -2 (rhs):
> >
> >(fold(s!1, U!1) o (fold(t!1, U!1)) o t!1(e!1)).
> >
> >Before the replacement you have to use the fact that "o" is associative,
> >and reorganize either -2 or 2.
> >
> >Cesar
> >
> >Jerome wrote:
> >> Here's another equality that should be straighforward, but PVS doesn't
> >> seem to understand:
> >> 
> >>   [-1]  t!1(e!1) o fold(t!1, U!1) = fold(t!1, U!1) o t!1(e!1)
> >>   [-2]  (fold(s!1, U!1) o fold(t!1, U!1)) o t!1(e!1) =
> >> 	  fold(s!1, U!1) o (fold(t!1, U!1) o t!1(e!1))
> >>   [-3]  fold(s!1, U!1) o fold(t!1, U!1) =
> >> 	 fold(LAMBDA (k: D): s!1(k) o t!1(k), U!1)
> >> 	  |-------
> >>   [1]   U!1(e!1)
> >>   {2}   s!1(e!1) o fold(s!1, U!1) o (fold(t!1, U!1) o t!1(e!1)) =
> >> 	 s!1(e!1) o t!1(e!1) o (fold(s!1, U!1) o fold(t!1, U!1))
> >> 
> >>   Rule? (replace -2 (2) :dir RL)
> >>   No change on: (REPLACE -2 (2) :DIR RL)
> >>   fold_distributive.2 :
> >> 
> >>   [-1]  t!1(e!1) o fold(t!1, U!1) = fold(t!1, U!1) o t!1(e!1)
> >>   [-2]  (fold(s!1, U!1) o fold(t!1, U!1)) o t!1(e!1) =
> >> 	  fold(s!1, U!1) o (fold(t!1, U!1) o t!1(e!1))
> >>   [-3]  fold(s!1, U!1) o fold(t!1, U!1) =
> >> 	  fold(LAMBDA (k: D): s!1(k) o t!1(k), U!1)
> >>     |-------
> >>   [1]   U!1(e!1)
> >>   {2}   s!1(e!1) o fold(s!1, U!1) o (fold(t!1, U!1) o t!1(e!1)) =
> >> 	  s!1(e!1) o t!1(e!1) o (fold(s!1, U!1) o fold(t!1, U!1))
> >> 
> >> What I want is for [2] to become:
> >> 
> >>   {2}   s!1(e!1) o (fold(s!1, U!1) o fold(t!1, U!1)) o t!1(e!1) =
> >>           s!1(e!1) o t!1(e!1) o (fold(s!1, U!1) o fold(t!1, U!1))
> >> 
> >> What could be going on? Unlike my last mysterious equality, doing a
> >> check of 'show-expanded-sequent' doesn't yield any red flags...
> >> 
> >> jerome
> >> 
> >> On Tue, Jun 24, 2008 at 03:25:55PM -0700, Jerome wrote:
> >>> Does anyone know why the following doesn't produce Q.E.D in PVS?
> >>>
> >>>  {-1}  strict_subset?(K!1, J!1) IMPLIES
> >>> 	  fold(s!1, J!1) = fold(s!1, K!1) o fold(s!1, difference(J!1, K!1))
> >>>  [-2]  strict_subset?(K!1, J!1)
> >>>    |-------
> >>>  [1]   fold(s!1, J!1) = fold(s!1, K!1) o fold(s!1, difference(J!1, K!1))
> >>>
> >>>  Rerunning step: (ASSERT)
> >>>  Simplifying, rewriting, and recording with decision procedures,
> >>>  this simplifies to:
> >>>  composable :
> >>>
> >>>  {-1}  fold(s!1, J!1) = fold(s!1, K!1) o fold(s!1, difference(J!1, K!1))
> >>>  [-2]  strict_subset?(K!1, J!1)
> >>>    |-------
> >>>  [1]   fold(s!1, J!1) = fold(s!1, K!1) o fold(s!1, difference(J!1, K!1))
> >>>
> >>> After I make ASSERT call I would think the proof was finished... am I
> >>> missing something? Thanks
> >>>
> >>> jerome
> >>>
> >> 
> >> 
> >
> >-- 
> >Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@xxxxxxxxxx
> >National Institute of Aerospace         mailto:Cesar.A.Munoz@xxxxxxxx
> >100 Exploration Way  Room 214       http://research.nianet.org/~munoz
> >Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988
> >GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6  1A18 6000 89F5 C114 E6C4
> >