pvs_hurry: THEORY


BEGIN


  % Challenge 1: Prove 2+2=4

  % Type a simple mathematical statement as a lemma and give it a name.

  name1: LEMMA 2+2=4

  % To prove the lemma above:
    %    1. Put your cursor anywhere on the lemma 
    %           (including name, the word lemma, and the statement)
    %    2. Type 'M-x pr' and hit enter.
    %    3. The proof window should open asking you to prove 2+2=4.
    %    4. Type '(assert)'. This should prove it, presenting you with 'Q.E.D.'
    %           (assert) is a applies decision logic that is built into PVS
    %           it can prove some simple things.


  % Challenge 2: Prove that for all real numbers x, x^2 >= 0

  squared_nonnegative: LEMMA FORALL (x:real): x^2 >= 0

  % (x:real) means a variable whose type is real. The colon ':'
  % is used after the name of a variable to specify its type.

  %    1. Type '(skeep)' to get ride of the FORALL. Now you just have
  %           a variable with the name x to work with.
  %    2. What does x^2 mean? Expand the '^' symbol by typing
  %           '(expand "^")' to find out.
  %    3. Now, what does expt(x,2) mean? Type '(expand "expt")' and
  %           hit enter three times to find out.
  %    4. Now you just have to prove x*x>=0. Prove this by typing
  %           '(assert)'. This command knows that x*x is nonnegative

  % Challenge 3: Prove that two aircraft do not hit.
  %   One aircraft is following the other in a straight line.
  %   The following aircraft is moving slower, so they can not hit.
  %   

  % Current Position of First Aircraft along the line:

  position1: VAR real

  % This means that so is a variable that has type 'real'

  % Position of Second Aircraft:

  position2: VAR real

  % Speeds of the two aircraft, which are positive real numbers:

  speed1,speed2: VAR posreal

  % A time t in the future:

  t: VAR posreal

  % The position of an aircraft at time t:

  position_at(position1,speed1,t): real =
    position1 + t*speed1

  % A predicate specifying whether they hit at some t:

  hit?(position1,speed1,position2,speed2): bool =
    EXISTS (t): position_at(position1,speed1,t) = 
    	   	position_at(position2,speed2,t)

  % Aircraft do not hit

  do_not_hit: LEMMA
    position1 < position2 % aircraft 1 is originally behind aircraft 2
    AND speed1 < speed2   % it is also moving slower
    IMPLIES
    NOT hit?(position1,speed1,position2,speed2)

  % The Proof Is:
  %   (skeep)
  %   (expand "hit?")
  %   (skeep -3)
  %   (expand "position_at")
  %   (mult-by -2 "t")
  %   (assert)


  % Challenge 4: Prove that x^2 < y^2 whenever x and 
  %                  y are positive and x < y.
  % Find the lemma in the prelude that proves this

  squared_increasing: LEMMA FORALL (x,y:posreal):
    x < y IMPLIES x^2 < y^2

  % Type 'M-x vpf' to view the prelude file
  % Find lemma 'both_sides_expt_pos_lt_aux'
  %   (skeep)
  %   (expand "^")
  %   (lemma "both_sides_expt_pos_lt_aux")
  %   (inst - "1" "x" "y")
  %   (assert)

  % MORAL OF THE STORY: DON'T REINVENT THE WHEEL


  % Question: What if you type something that doesn't make sense?

  % wrong_types: LEMMA FORALL (s:string,n:nat): s = n

  % Type 'M-x tc' to typecheck the whole file to see if all of the 
  % statements involving types are correct.

  % BE CAREFUL. There are some automatic conversions in PVS.
  % They can be turned off. The following lemma is type correct:

  type_correct_lem: LEMMA FORALL (b:bool,n:nat): b = n

  % This typechecks just fine, even though it is incorrect,
  % because the '=' is defined between reals and nats.
  % That is, it is possible for a real to equal a nat, but not a bool.

  % Subtyping is built-in in PVS. For instance, PVS knows that a nat is a real:

  nat_is_real: LEMMA FORALL (n:nat): EXISTS (x:real): n=x


  % Challenge 5: prove that the cardinality of the powerset of
  %  {0,1,...,10} is 2^11.

  % Use the libraries:

  IMPORTING sets_aux@power_sets

  set_below_11: finite_set[nat] = {n:nat | n < 11}

  card_below_11: LEMMA card(powerset(set_below_11)) = 2^11

  % The proof uses the command '(grind)', which applies (assert)
  % and a bunch of other stuff. It expands definitions, applies
  % rewriting, and uses (assert) to apply decision procedures.

  % The proof is:
  % (lemma "card_powerset[nat]")
  % (inst - "set_below_11")
  % (replace -1)
  % (hide -1)
  % (case "card(set_below_11) = 11")
  % (("1" (assert))
  %  ("2"
  %   (hide 2)
  %   (typepred "card(set_below_11)")
  %   (lemma "Card_bijection[nat]")
  %   (inst - "set_below_11" "11")
  %   (assert)
  %   (inst + "LAMBDA (i:{n:nat | n < 11}): i")
  %   (("1" (hide-all-but 1) (grind)) ("2" (hide-all-but 1) (grind)))))

  % Type 'M-x" prt to prove the whole theory.
  % Wait a minute!!! there is something unproved.
  % It is called a TCC (type check condition) related to the lemma
  % above. We used powerset of set_below_11, and powerset is only defined
  % for finite sets. Thus, it is asking us to prove that its argument, 
  % set_below_11, is finite.

  % To see all the TCCs generated, type 'M-x show-tccs' and hit enter.

  % Proof of the TCC is
  %   (expand "is_finite")
  %   (inst + "11" "LAMBDA (i:({n: nat | n < 11})): i")
  %   (grind)

  % MORAL OF THE STORY: DON'T REINVENT THE WHEEL


end pvs_hurry