# Re: [PVS-Help] Unit composition in PVS

```Hi Ben,

It does look like a bug - could you send me your PVS theory?

Thanks,
Sam

Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:

> Hi Sam,
>
> Got back to this after working on something else for a while, when I used the ‘C-u M-x show-expanded-sequent’ command, I got the following:
> ===================================
> length_plus_length_is_length :
>
> {-1}  length_pred((number_fields.+)(x, y))
>   |-------
> {1}   length_pred((number_fields.+)(x, y))
> ===================================
>
> As far as I can tell, {-1} should imply {1} fairly cleanly. Neither ‘(assert)’ nor even ‘(grind)’ resolve this, but possibly the output from ‘(grind)’ is useful:
> ===================================
> The following errors occurred within the strategy:
>
> Couldn't find a suitable quantified formula.
>
> No suitable (+ve FORALL/-ve EXISTS) quantified expression found.
>
> No change on: (grind)
> length_plus_length_is_length :
>
> [-1]  length_pred(x + y)
>   |-------
> [1]   length_pred(x + y)
> ===================================
>
> The proof (from show-proof) is simply:
>   ("" (skeep) (lemma "closed_plus" ("x" "x" "y" "y")) (postpone))
>
> Where the judgment being proven is:
>   length_plus_length_is_length:  JUDGEMENT +(x, y)   HAS_TYPE length
>
> And the axiom closed_plus is:
>   closed_plus:    AXIOM length_pred(x + y)
>
> And the definition for x, y is:
>   x, y: VAR length
>
> Best Regards,
> Ben Hocking
> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
>
>
>
>
> > On Apr 23, 2015, at 6:05 PM, Sam Owre <owre@xxxxxxxxxxx> wrote:
> >
> > Hi Ben,
> >
> > We tried to capture dimensions and units using the PVS type system, and
> > failed.  Since then we have started adding it to PVS, then worked on
> > adding it to Simulink, and wrote a paper laying out the theory:
> >
> > Automatic Dimensional Analysis of Cyber-Physical Systems,
> > by Sam Owre, Indranil Saha, and Natarajan Shankar,
> > in FM 2012: Formal Methods Lecture Notes in Computer Science pages 356-371.
> >
> > We will continue adding it to PVS when there is time available.
> >
> > As for your proof, you should try 'C-u M-x show-expanded-sequent'; this
> > often shows where mismatches occur.  My guess is you have two different
> > '+' operators.
> >
> > If you still have problems, please send your specs to me so I can debug
> > this.
> >
> > Thanks,
> > Sam
> >
> >
> > Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
> >
> >> For lengths, I’ve tried creating a “lengths” theory similar to the reals theory in the PVS
> >> prelude, but I’m stuck here:
> >> length_plus_length_is_length :
> >>
> >>  |-------
> >> {1}   FORALL (x, y): length_pred(x + y)
> >>
> >> Rule? (skeep)
> >> Skolemizing and keeping names of the universal formula in (+ -),
> >> this simplifies to:
> >> length_plus_length_is_length :
> >>
> >>  |-------
> >> {1}   length_pred(x + y)
> >>
> >> Rule? (lemma "lengths.closed_plus" ("x" "x" "y" "y"))
> >> Applying lengths.closed_plus where
> >>  x gets x,
> >>  y gets y,
> >> this simplifies to:
> >> length_plus_length_is_length :
> >>
> >> {-1}  length_pred(x + y)
> >>  |-------
> >> [1]   length_pred(x + y)
> >>
> >> Rule?
> >>
> >> I’ve tried “assert”, “smash”, “grind”, etc., but nothing seems to resolve this seemingly
> >> simple statement…
> >>
> >> (Note that length_pred is an undefined function that I’ve attempted to “define” via axioms,
> >> such as closed_plus, etc.)
> >>
> >> Best Regards,
> >> Ben Hocking
> >> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
> >>
> >>    On Apr 22, 2015, at 9:15 AM, Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
> >>
> >>    Alas, it appears that the simplicity comes with a price. I cannot figure out a way to
> >>    prevent meters and seconds from being added together, or more importantly of determining
> >>    whether a particular measurement is of time, length, or is unitless (as examples).
> >>
> >>    Best Regards,
> >>    Ben Hocking
> >>    ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
> >>
> >>        On Apr 22, 2015, at 8:01 AM, Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx>
> >>        wrote:
> >>
> >>        Viorel,
> >>
> >>        I really like the idea of using uninterpreted positive real constants. This is far
> >>        simpler than the approach I’ve been using.
> >>
> >>        Best Regards,
> >>        Ben Hocking
> >>        ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
> >>
> >>            On Apr 22, 2015, at 4:51 AM, Viorel Preoteasa <viorel.preoteasa@xxxxxxxx> wrote:
> >>
> >>            You can also do something like:
> >>
> >>              m: posreal
> >>              cm: posreal = m / 100
> >>              m_to_cm: lemma 2.5 * m = 250 * cm
> >>
> >>            Best regards,
> >>
> >>            Viorel Preoteasa
> >>
> >>            On 04/22/2015 01:16 AM, Ben Hocking wrote:
> >>
> >>                Is anyone familiar with work that has been done on unit composition in
> >>                formal specifications within PVS? E.g., verifying that when you multiply
> >>                meters by meters you get square meters?
> >>
> >>                I have some ideas on what I want to do (and have actually started down that
> >>                path), but I don’t want to reinvent the wheel if this has already been done.
> >>
> >>                Best Regards,
> >>                Ben Hocking
> >>                ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx
> >>

```