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

[PVS-Help] Help proving that two array types are bijective



I have the following theory (motivation to be explained later*):
=====================
example: THEORY
BEGIN

int32 : TYPE = {i : int | -2^31 <= i AND i <=2^31-1}

Z4a: TYPE = {n: int32 | n >= 0 AND n <= 3}
Z4b: TYPE = below(4)
Z4_f(input: Z4a): Z4b = input
Z4_invf(input: Z4b): Z4a = input
IMPORTING function_inverse[Z4a, Z4b] AS inv_Z4
IMPORTING sets_aux@card_comp[Z4a, Z4b] AS card_Z4
SameZ4: LEMMA card_Z4.card_eq

SpeedA: TYPE = {n: int32 | n >= -100000 AND n <= 100000}
SpeedB: TYPE = {i: int | i >= -100000 AND i <= 100000}
Speed_f(input: SpeedA): SpeedB = input
Speed_invf(input: SpeedB): SpeedA = input
IMPORTING function_inverse[SpeedA, SpeedB] AS inv_speed
IMPORTING sets_aux@card_comp[SpeedA, SpeedB] AS card_speed
SameSpeed: LEMMA card_speed.card_eq

WSpeedsA: TYPE = ARRAY [Z4a -> SpeedA]
WSpeedsB: TYPE = ARRAY [Z4b -> SpeedB]
Wheel_Speeds_f(input: WSpeedsA): WSpeedsB =
  LAMBDA(wheel: Z4b): Speed_f(input(Z4_invf(wheel)))
Wheel_Speeds_invf(input: WSpeedsB): WSpeedsA =
  LAMBDA(wheel: Z4a): Speed_invf(input(Z4_f(wheel)))
IMPORTING function_inverse[WSpeedsA, WSpeedsB] AS inv_ws
IMPORTING sets_aux@card_comp[WSpeedsA, WSpeedsB] AS card_ws
SameWheelSpeeds: LEMMA card_ws.card_eq

END example
=====================
When I try to prove the theory, I get the following (note that I did provide necessary help to the prover for the TCCs):
=====================
 Proof summary for theory example
    Z4_f_TCC1.............................proved - complete   [shostak](0.03 s)
    Z4_invf_TCC1..........................proved - complete   [shostak](0.47 s)
    inv_Z4_TCC1...........................proved - complete   [shostak](0.59 s)
    SameZ4................................proved - complete   [shostak](0.75 s)
    Speed_invf_TCC1.......................proved - complete   [shostak](0.60 s)
    inv_speed_TCC1........................proved - complete   [shostak](0.61 s)
    SameSpeed.............................proved - complete   [shostak](0.74 s)
    SameWheelSpeeds.......................unfinished          [shostak](0.27 s)
    Theory totals: 8 formulas, 8 attempted, 7 succeeded (4.05 s)
=====================
I find that I a m unable to prove the lemma SameWheelSpeeds, i.e., that WSpeedsA and WSpeedB are bijective. I also find it interesting that no TCCs were generated for its conversion functions, unlike for the simpler Z4 and Speed types.
Where I'm stuck is with the following surjective/injective steps:
=====================
SameWheelSpeeds.1 :

[-1]  Wheel_Speeds_f(x1) = Wheel_Speeds_f(x2)
  |-------
[1]   (x1 = x2)
=====================
=====================
SameWheelSpeeds.2 :
  |-------
[1]   Wheel_Speeds_f(y) = y
=====================
I've also expanded Wheel_Speeds_f, and tried similar steps as to those that got me through SameZ4 and SameSpeed, but to no avail.

Any ideas?

*Motivation: This is an extract from a theory that an implementation of an example ABS system in SPARK Ada matches the original formal specification as given in PVS.

Ben Hocking
ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx