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

```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
>>

```