%=====================================================================
%
%              Exercise 4: The Advanced Aerospace Caucus
%
%   Senators:  Loquacius, Repetitius, Tedius, Verbosus
%   Projects:  Stealth blimp, Supersonic helicopter,
%              Solar-powered cargo plane, Flying submarine
%   Budgets:   $58 million, $72 million, $79 million, $86 million
%
%=====================================================================

caucus: THEORY

BEGIN

  SENATOR: TYPE = {Loq, Rep, Ted, Verb}
  PROJECT: TYPE = {Blimp, Copter, Plane, Sub}

  % The "Containing" declaration lets PVS know the set is nonempty.

  BUDGET:  TYPE = {i: int | i = 58 OR i = 72 OR i = 79 OR i = 86}
                  CONTAINING 58

  s,x,y,z: VAR SENATOR
  p,q:     VAR PROJECT
  b,c:     VAR BUDGET

  % The following are uninterpreted functions that relate senators, 
  % projects, and budgets.

  proj(s): PROJECT
  budget(s): BUDGET
  cost(p): BUDGET

  % The following lemmas provide the range type information for budget
  % and cost.  These are both proven using typepred.  

  budget_lem: LEMMA budget(s) = 58 OR budget(s) = 72 OR budget(s) = 79 OR budget(s) = 86

  cost_lem: LEMMA cost(p) = 58 OR cost(p) = 72 OR cost(p) = 79 OR cost(p) = 86


  % The following axioms ensure the functions are injective 
  % (one-to-one).

  proj_inj: AXIOM proj(s) = proj(x) => s = x

  budget_inj: AXIOM budget(s) = budget(x) => s = x

  cost_inj: AXIOM cost(p) = cost(q) => p = q 

  project_rule: AXIOM cost(p) = budget(s) IMPLIES proj(s) = p

% This rule expresses a type of "triangulation" constraint, namely, that
% if the cost of a project and a senator's budget match, the senator
% must be promoting that particular project.  This restriction could
% (and should, to be safe) be expressed as additional constraints on the
% proj, cost, and budget functions.  This would require a more elaborate
% setup than is warranted here.

% The three puzzle clues are formalized as axioms.  Again, a formulation
% without axioms would be preferred in practice.

  clue1: AXIOM budget(Loq) < budget(Ted) AND
               budget(Loq) = cost(Copter) + 7

  clue2: AXIOM cost(Sub) /= 58 AND cost(Sub) < cost(Blimp)

  clue3: AXIOM budget(Verb) = cost(Plane) + 14


%=======================  EXERCISES ==================================

%=====================================================================
% The solution to the puzzle is expressed by the following lemmas.
% Each can be proved using only the prover commands from the set
% {SPLIT, FLATTEN, LEMMA, ASSERT, INST, and TYPEPRED (and their variants)}.
% Multiple applications of ASSERT might be needed in some places.
%=====================================================================

  L1: LEMMA budget(Loq) = 79

      % Hint:  From Clue 1, we know that budget(Loq) is neither the
      %        min nor the max value, so 58 < budget(Loq) < 86.  Also,
      %        cost(Copter) can't be 58 because the next possible value 
      %        is 72.  Hence, the only remaining choice is 79.  You will 
      %        need to use use typepred to make explicit the range type of
      %        the functions.

  L2: LEMMA  cost(Copter) = 72

      % Hint:  Follows from Clue 1 and lemma L1.


  L3a: LEMMA  cost(Sub) = 79

      % Hint:  From Clue 2 it follows that
      %        58 < cost(Sub) < cost(Blimp) <= 86,
      %        narrowing cost(Sub) to two choices.  Lemma 2 gives 
      %        cost(Copter) = 72, so only one choice remains.
      %        You will need to use "cost_inj" and "cost_lem".

  L3b: LEMMA  cost(Blimp) = 86

      % Hint:  Clue 2 and lemma L3a give 79 = cost(Sub) < cost(Blimp),
      %        meaning 86 is the only possibility (after showing 
      %        the range by using "cost_lem").

  L3c: LEMMA  cost(Plane) = 58

      % Hint:  Lemmas L2, L3a, L3b give costs for Copter, Sub, Blimp.
      %        cost(Plane) must be the fourth alternative.  Again,
      %        you will need to make explicit the range of cost and the
      %        fact that it is injective.

  L4: LEMMA proj(Loq) = Sub

      % Hint:  Lemmas L1 and L3a give matching values for budget(Loq)
      %        and cost(Sub).  The project rule implies the Sub must be
      %        Loq's project.


  L5a: LEMMA budget(Verb) = 72

      % Hint:  Follows from Clue 3 and lemma L3c.

  L5b: LEMMA budget(Ted) = 86

      % Hint:  Follows from Clue 1 and lemma L1 (and the constraint
      %        on the budget function).

  L5c: LEMMA budget(Rep) = 58

      % Hint:  The budget for Rep is the only one remaining after
      %        considering those in lemmas L1, L5a, L5b.  "budget_lem"
      %        and "budget_inj" will be used.

  L6a: LEMMA proj(Rep) = Plane

      % Hint:  Using the project rule, this result follows from lemmas
      %        L3c and L5c.

  L6b: LEMMA proj(Ted) = Blimp

      % Hint:  Similar to L6a.

  L6c: LEMMA proj(Verb) = Copter

      % Hint:  Similar to L6a.

END caucus