%%% Assignment 8
%%% Out: Mon 19 Nov
%%% Due: Mon 26 Nov 
%%% Author: Brigitte Pientka
%
% This assignment is to be submitted electronically using Tutch.
% Comment out those parts of the problems that 
% cannot be checked by Tutch.
%
% Remember that if you give a proof or term in Tutch, you need to give all
% the definitions and lemmas explicitely. 
%
% Extra Credit problems are due 3rd Dec. 
%
%
% Remark :
% --------------------------
% We will write label all assumptions with u, u', v etc.
% and write u:A_1 .... |- A where the left hand side |- 
% represents all our assumptions 
%
% Abbreviation of proof terms for equality are eq0 eqS eqE0S eqES0 eqESS
% Abbreviations of actual equality rules are =NI0, =NIss, =NE0s, =NEs0, =NEss
%
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%
% 1. Symmetry of Equality.
%
%  For this problem, use the rules for equality given in lecture 16.
%
%  First, give a formal proof of symmetry:
%  Try to be precise. 
%
%
%{
Conjecture !x:nat.!y:nat. (x = y => y = x) 

Proof by induction on x 

Case : x = 0 
-----
  to show                      |- !y:nat. (0 = y => y = 0)            
  by forallI   y:nat           |-  0 = y => y = 0 
  by impI      y:nat u : 0 = y |- y = 0  
  
  Sub-case: y = 0 
  ---------
     to show    y:nat, u : 0 = 0 |- 0 = 0  
     by hypothesis u 

  Sub-Case: y = s y'
  --------
     to show    y:nat, u : 0 = s y' |- s y' = 0   
     by =NEs0

Step Case : x = s x' ; IH: !y:nat. x' = y => y = x' 
----------
  to show (IC) : !y:nat.   (s x') = y => y = (s x')
  by forallI      y:nat |- (s x') = y => y = (s x')
  by impI     y:nat, u: (s x') = y |- y = (s x')
  
  Sub-case : y = 0 
  -----------------
  to show     y:nat, u: (s x') = 0 |- 0 = (s x') 
  by =NEs0

  Sub-case : y = s y'
  ------------------
  to show     y:nat, u: (s x') = (s y') |- (s y') = (s x')
  by =NEss    y:nat, u: (s x') = (s y'), u': x' = y' 
                    |- (s y') = (s x')

  by IH we know  !y:nat. x' = y => y = x' ,
  by applying forallE to IH  and instantiating y with y' we get
              x' = y' => y' = x'   (**)

  by impE u' and (**) 
             y:nat, u: (s x') = (s y'), u': x' = y' 
                    |- y' = x'
  by =NIss   y:nat, u: (s x') = (s y'), u': x' = y' 
                    |- (s y') = (s x')

  which is what we needed to show.
        
qed.
}%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%
%% Formal Tutch proof
%% 
%% Note that Tutch does not know the difference between 
%% Case analysis and induction. It treats all case analysis 
%% as potential inductions. This means we are required 
%% to give the induction hypothesis, even if we don't 
%% need it. 
%% 
%% In the proof above, we do induction on x and a case
%% analysis on y. In the Tutch proof below, we will
%% give the corresponding IH not only for x = 0 
%% and x = s x', but also for the case distinctions on y
%%
%%
proof sym : !x:nat.!y:nat. (x = y => y = x) =
begin          					 
[x:nat;						%  1
 [y:nat;					%  2
  [0 =	0;					%  3 
   0 = 0];					%  4 by Hyp 3
   0 = 0 => 0 = 0;				%  5 by ImpI 4 : Base Case : x = 0 and y = 0 ; 
 [y':nat, 0 = y' => y' = 0;			%  6 Step Case : x = 0 and y = s y' ; 
  [0 = s y';					%  7 
   s y' = 0];					%  8 by =NE0s 7
   0 = s y' => s y' = 0];			%  9 by ImpI 8
   0 = y => y = 0];				% 10 by NatE 2 5 9
  !y:nat. 0 = y => y = 0;			% 11 by ForallI 10 : Base Case : x = 0
 [x':nat, !y:nat. x' = y => y = x';		% 12 Step Case : x = s x'; IH 
  [y:nat;					% 13 
   [s x' = 0;					% 14 
    0 = s x'];					% 15 by =NEs0 14
    s x' = 0 => 0 = s x';			% 16 by ImpI 15   Base Case x = s x' and y = 0
   [y':nat, s x' = y' => y' = s x';		% 17 Step Case x = s x' and y = s y' ;
    [s x' = s y';				% 18 
       x' = y';					% 19 by =NEss 18
  x' = y' => y' = x';				% 20 by ForallE 12 17
y' = x';					% 21 by ImpE 20 19
s y' = s x'];					% 22 by =NIs 21
s x' = s y' => s y' = s x'];			% 23 by ImpI 22
s x' = y => y = s x'];				% 24 by NatE 13 16 23
!y:nat. s x' = y => y = s x'];			% 25 by ForallI 24
!y:nat. x = y => y = x];			% 26 by NatE 1 11 25
!x:nat.!y:nat. x = y => y = x;			% 27 by ForallI 26
end;

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%  Then give a proof term and check the proof term with Tutch:
%

term sym : !x:nat.!y:nat. ((x = y) => (y = x)) = 
 fn x => rec x of 
   f 0 => (fn y => rec y of g 0 => (fn u => u)
                          | g (s y') => (fn u => (eqE0S u))
           end)
 | f (s x') => (fn y => rec y of 
                  g 0 => (fn u => (eqES0 u))
                | g (s y') => (fn u => (eqS ((f x' y') (eqESS u)))) end)
 end;

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%
% 2. Transitivity of x < y .
%
% Give an informal proof of the following,
% using the rules for x < y from lecture 16.
%
% !x:nat.!y:nat.!z:nat. (x < y) => (y < z) => (x < z);
%

%{
Proof by induction on x 

Case : x = 0 
------------
 to show !y:nat.!z:nat. (0 < y) => (y < z) => (0 < z);
 by forallI  y:nat |- !z:nat. (0 < y) => (y < z) => (0 < z);
 by forallI y:nat, z:nat |-  (0 < y) => (y < z) => (0 < z); 


  Sub-Case : y = 0 
  -----------------
   to show    y:nat, z:nat |- (0 < 0) => (0 < z) => (0 < z);
   by ImpI    y:nat, z:nat, u : 0 < 0 |- (0 < z) => (0 < z);
   by lessE0 using assumption u 

  Sub-Case : y = s y'  
  -------------------
   to show   y:nat, z:nat, y':nat 
                 |-  (0 < s y') => (s y' < z) => (0 < z);

   by ImpI   y:nat, z:nat, y':nat, u : (0 < s y') 
                 |- (s y' < z) => (0 < z);

   by ImpI   y:nat, z:nat, y':nat, u : (0 < s y'), v : (s y' < z) 
                 |-  (0 < z);
   
     Sub-sub-case : z = 0 
     ---------------------
       to show  y:nat, z:nat, u : (0 < s y'), v : (s y' < 0) 
                  |-  (0 < 0);
       by lessE0 assumption v 

     Sub-sub-case : z = s z' 
     ----------------------
       to show  y:nat, z:nat, z':nat, u : (0 < s y'), v : (s y' < s z') 
                  |-  (0 < s z');
       by less0


Case : x = s x'   ;  IH : !y:nat.!z:nat. (x' < y) => (y < z) => (x' < z);
----------------

 to show    x':nat |-  !y:nat.!z:nat. (s x' < y) => (y < z) => (s x' < z);
 by forallI x':nat, y:nat |- !z:nat. (s x' < y) => (y < z) => (s x' < z);
 by forallI x':nat, y:nat, z:nat |- (s x' < y) => (y < z) => (s x' < z);


  Sub-Case : y = 0 
  -----------------
    to show : x':nat, y:nat, z:nat |- (s x' < 0) => (0 < z) => (s x' < z);
    by ImpI : x':nat, y:nat, z:nat, u : (s x' < 0) |- (0 < z) => (s x' < z);
    by lessE0 using assumption u
 
  Sub-Case : y = s y'
  ------------------
    to show : x':nat, y:nat, z:nat, y':nat
                |- (s x' < s y') => (s y' < z) => (s x' < z);
    by ImpI : x':nat, y:nat, z:nat, y':nat, u : (s x' < s y')
  		|- (s y' < z) => (s x' < z);
    by ImpI : x':nat, y:nat, z:nat, y':nat, u : (s x' < s y'), v : (s y' < z)
  		|- (s x' < z);
   
 
     Sub-sub-case : z = 0 
     --------------------- 
       to show : x':nat, y:nat, z:nat, y':nat, u : (s x' < s y'), v : (s y' < 0)
  		|- (s x' < 0);

       by lessE0 by assumption v


     Sub-sub-case : z = s z' 
     ----------------------
       to show : x':nat, y:nat, z:nat, y':nat, z':nat,
                 u : (s x' < s y'), v : (s y' < s z')
  		   |- (s x' < s z');
       by lessEss : x':nat, y:nat, z:nat, y':nat, z':nat,
                    u : (s x' < s y'), v : (y' < z')
    		      |- (s x' < s z');

       by lessEss : x':nat, y:nat, z:nat, y':nat, z':nat,
                    u : (x' < y'), v : (y' < z')
    		      |- (s x' < s z');

       by IH (applying forallE to IH and instantiating y with y' and z with z')
                    x' < y' => y' < z' => x' < z'   (**)

       by ImpE using u : (x' < y') and (**) we know 
               
                    y' < z' => x' < z' (*)
        
       by ImpE using v : y' < z'  and (*) we know 

                    x' < z'

       by lessS   (s x' < s z') 

qed.

}%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% Give an equational specification of a corresponding proof term.
%
%{

trans    0      0      z    u	w = lessE0 u
trans    0   (s y')    0    u	w = lessE0 v
trans    0   (s y') (s z')  u	w = less0
trans (s x')    0      z    u	w = lessE0 u
trans (s x') (s y')    0    u	w = lessE0 v
trans (s x') (s y') (s z')  u	w = lessS (trans x' y' z' (lessES u) (lessES v))

}%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%
% 3. Successor and Addition.
%
% Prove formally the following proposition, in which x + y represents
% the addition function plus x y, defined in lecture 13:
% 

% Definition of plus 

val plus : nat -> nat -> nat
  = fn x => fn y => rec x of
        p 0 => y
      | p (s x') => s (p x')
    end;

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%{
 Lemma (from class) : !x:nat. x = x.
 
 Conjecture : !x:nat. !y:nat. plus x (s y) = s (plus x y) 

Proof by induction on x

Case : x = 0 
-------------

 to show    : !y:nat. plus 0 (s y) = s (plus 0 y) 
 by forallI    y:nat |- plus 0 (s y) = s (plus 0 y)  

 by unfolding the definition of plus  
               y:nat |- s y = s y

 by reflexivity lemma and instantiating the 
 lemma with s y for x


Case : x = s x'   IH : !y:nat. plus x' (s y) = s (plus x' y) 
----------------

 to show   :  x' : nat |- !y:nat. plus (s x') (s y) = s (plus (s x') y) 
 by forallI   x' : nat, y:nat 
                 |- plus (s x') (s y) = s (plus (s x') y) 

 by unfolding the definition of plus 
              x' : nat, y:nat 
                 |- s (plus x' (s y) = s (s (plus x' y)) 

 by IH and instantiating y with y we know 
        x' : nat, y:nat |- plus x' (s y) = s (plus x' y)
 
 by =NIss x' : nat, y:nat |-  s(plus x' (s y)) = s s (plus x' y)

 which is what we needed to show.

qed.
}%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%
%% Formal Tutch proof
%% 

proof refl : !x:nat. (x = x) =
begin
[x:nat;
 0 = 0;
 [x':nat, x' = x';
  s x' = s x';
  ];
 x = x];
!x:nat. (x = x);
end;


proof plusS : !x:nat. !y:nat. plus x (s y) = s (plus x y) = 
begin
!z:nat. z = z;
[ x: nat;
  [ y: nat;
    (s y) : nat;
     (s y) = (s y);                                 
    plus 0 (s y) = s (plus 0 y) ];                  

  !y:nat. plus 0 (s y) = s (plus 0 y);              

  [ x': nat, !y:nat. plus x' (s y) = s (plus x' y);
    [ y: nat;
      plus x' (s y) = s (plus x' y); 
      s (plus x' (s y)) = s (s (plus x' y));
      plus (s x') (s y) = s (plus (s x') y) ];      
   !y:nat. plus (s x') (s y) = s (plus (s x') y) ]; 

 !y:nat. plus x (s y) = s (plus x y) ];             

!x:nat. !y:nat. plus x (s y) = s (plus x y) 
end;



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%
% Now give a term for your proof and check the proof term with Tutch.
%
%

term refl : !x:nat. (x = x) =
  fn x => rec x of
      f 0 => eq0
    | f (s x') => eqS (f x')
  end; 


term plusS: !x:nat.!y:nat. plus x (s y) = s (plus x y) =
  fn x => rec x of
      f 0 => fn y => (refl (s y))
    | f (s x') => fn y => eqS (f x' y)
  end;


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% 
%
% 4. Commutativity of Addition.
%
% Using only what we have so far proved about addition and equality,
% together with any additional lemmas you require,
% give an informal proof of the following:
%
%  !x:nat.!y:nat. (plus x y) = (plus y x);
%  
%
%
%{
====================================

Lemma : Transitivity of equality 

====================================

!x:nat.!y:nat.!z:nat.(x=y & y=z => x=z)


The proof is similar to transitivity of <. 

Proof by induction on x

Case : x = 0
-------------
 to show   :  !y:nat.!z:nat.(0=y & y=z => 0=z)
 by forallI y:nat |- !z:nat.(0=y & y=z => 0=z)
 by forallI y:nat, z:nat |- (0=y & y=z => 0=z)
 by impI    y:nat, z:nat, u: 0=y & y=z |- 0=z
 by andE    y:nat, z:nat, u: 0=y & y=z, u1: 0=y |- 0=z
 by andE    y:nat, z:nat, u: 0=y & y=z, u1: 0=y, u2:y=z 
             |- 0=z

  Sub-Case : y = 0
  -----------------
  to show : y:nat, z:nat, u: 0=0 & 0=z, u1: 0=0, u2:0=z 
             |- 0=z

     Sub-Case : z = 0 
     ----------------
       to show : y:nat, z:nat, u: 0=0 & 0=0, u1: 0=0, u2:0=0
             |- 0=0

       by =NI0

     Sub-Case : z = s z'
     -------------------
       to show : y:nat, z:nat, z' : nat, u: 0=0 & 0= s z', 
                 u1: 0=0, u2:0 = s z'
                   |- 0 = s z'
       by =NE0s using assumption u2

  Sub-case : y = s y'
  --------------------
  to show  y:nat, z:nat, y':nat u: 0= s y' & s y' =z, 
           u1: 0 = s y', u2: s y' = z 
             |- 0 = z

  by =NE0s using assumption u1

Case : x = s x'   IH : !y:nat.!z:nat.(x' = y & y = z => x' = z)
----------------
  to show !y:nat.!z:nat.(s x' = y & y = z => s x' = z)
  by forallI y:nat |- !z:nat.(s x' = y & y = z => s x' = z)
  by forallI y:nat, z:nat |- (s x' = y & y = z => s x' = z)
  by impI    y:nat, z:nat, u: s x' = y & y = z |-  s x' = z
  by andE    y:nat, z:nat, u: s x' = y & y = z 
             u1 : s x' = y, u2: y = z 
                |-  s x' = z

  Sub-Case : y = 0 
  -----------------
     to show  y:nat, z:nat, u: s x' = 0 & 0 = z 
             u1 : s x' = 0, u2: 0 = z 
                |-  s x' = z
    by =NEs0 using assumption u1

  Sub-Case : y = s y'
  --------------------
     to show  y:nat, z:nat, y':nat, u: s x' = s y' & s y' = z 
             u1 : s x' = s y', u2: s y' = z 
                |-  s x' = z

     Sub-sub-case : z = 0 
     --------------------
        to show  y:nat, z:nat, y':nat, u: s x' = s y' & s y' = 0
                 u1 : s x' = s y', u2: s y' = 0 
                    |-  s x' = 0
        by =NEs0 using assumption u2

     Sub-sub-case : z = s z'
     --------------------
        to show  y:nat, z:nat, y':nat, z':nat, 
                 u: s x' = s y' & s y' = s z'
                 u1 : s x' = s y', u2: s y' = s z' 
                    |-  s x' = s z'
        by =NEss using assumption u1 we get the assumption
                 u1' : x' = y'
        by =NEss using assumption u2 we get the assumption
                 u2' : y' = z'
        by andI using u1' and u2' we know 
                 u': x' = y' & y' = z'
           
        by IH (instantiating y with y' and z with z')
          x' = y' & y' = z' => x' = z' (**)

        by ImpE using u' and (**) we know
           x' = z'

        by =NIss

           s x' = s z' 

        which is what we needed to prove.

qed.

====================================

Lemma plus0 : !y:nat. (y = (plus y 0));

====================================

Proof by induction on y


Case : y = 0 
-----------------
  to show : 0 = plus 0 0 
  by unfolding definition of plus 
              0 = 0 
  by reflexivity lemma

Case : y = s y'  IH : y' = (plus y' 0);
--------------------------------------------
  to show : s y' = plus (s y') 0
  by IH we know : y' = plus y' 0
  by =NIss       s y' = s (plus y' 0)
  by definition of plus this is equal to
            s y' = plus (s y') 0

qed.

====================================

Theorem : Commutativity of plus 

!x:nat.!y:nat. (plus x y) = (plus y x);

====================================

Proof by induction on x 

Case : x = 0 
------------

 to show   !y:nat.   (plus 0 y) = (plus y 0);
 by forallI y:nat |- (plus 0 y) = (plus y 0);

 by Lemma plus0 (instantiating y with y) we know 
            y:nat |- y = plus y 0 

 by defintion of plus this is equivalent to
             y:nat |- (plus 0 y) = (plus y 0);

Case : x = s x'  IH : !y:nat. (plus x' y) = (plus y x');
--------------------------------------------------------

 to show : !y:nat.   (plus (s x') y) = (plus y (s x'));
 by forallI y:nat |- (plus (s x') y) = (plus y (s x'));
 by def. of plus 
            y:nat |- s (plus x' y) = (plus y (s x'));
 by lemma plusS (instantiating x with y and y with x')
plus x (s y) = s (plus x y) = 

            y:nat |- (plus y (s x')) = s (plus y x')  

 by symmetry lemma(instantiating x with (plus y (s x'))
     and y with s (plus x' y))
  
 (plus y (s x')) = s (plus y x') => s (plus y x') = (plus y (s x'))   (*)

 by impE (**) and (*)
  
 s (plus y x') = (plus y (s x')) 

 by IH (instantiating y with y) 
  plus x' y = plus y x'
 by eqSS
  s (plus x' y) = s (plus y x');

 by andI   
  s (plus x' y) = s (plus y x') & s (plus y x') = (plus y (s x')) 

 by transitivity 
  s (plus x' y) = s (plus y x') & s (plus y x') = (plus y (s x')) 
      => s (plus x' y) = (plus y (s x')) 

 by ImpE 
    s (plus x' y) = (plus y (s x')) 
 
 which is what we needed to prove. 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%
% Give an equational specification of a term for your proof of problem 4.
%
% Symmetry : 

sym    0    0     u = u
sym    0   (s y') u = eqE0S u
sym (s x')    0   u = eqES0 u
sym (s x') (s y') u = eqS ((sym x' y') (eqESS u))


% transitivity : 
trans    0      0      0    u = eq0
trans    0      0   (s z')  u = eqE0S (snd u)
trans    0   (s y')    z    u = eqE0S (fst u)
trans (s x')    0   (s z')  u = eqES0 (fst u)
trans (s x') (s y')    0    u = eqES0 (snd u)
trans (s x') (s y')  (s z') u = 
     eqS (trans x' y' z' <eqESS (fst u) (eqESS (snd u))>)


Commutativity
--------------

com    0    y = (plus0 y)
com (s x')  y =  
trans (s (plus x' y))  (s (plus y x'))  (plus y (s x'))
   <(com x' y) , sym (plus y (s x')) (s (plus x' y)) (plusS y x')> 


Note that I use & in the specification of the transitivity lemma,
consequently, I use pairs in the proof term and in the equational 
specification for transitivity. 

In the notes you find the specification of the transitivity lemma,
in curried form using implications. The equational specification of transitivity  
from the notes reflects this and the function trans takes 5 arguments. 

Using the curried form of trans, the equational specification of commutativity 
turns into 

com    0    y = (plus0 y)
com (s x')  y =  
trans (s (plus x' y))  (s (plus y x'))  (plus y (s x'))
   (com x' y)  (sym (plus y (s x')) (s (plus x' y)) (plusS y x'))

}%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% I now give the proofs implemented in Tutch.
%
%
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% Transitivity of equality
%

proof trans : !x:nat.!y:nat.!z:nat.(x=y & y=z => x=z) =
begin
[x:nat;
 [y:nat;
  [z:nat;
   [0=0 & 0 = 0;
    0=0];
   0=0 & 0=0 =>0=0;
   [z':nat, 0=0 & 0=z' => 0=z';
    [0=0 & 0= s z';     
     0=s z'];
    0=0 & 0=s z'=> 0=s z'];
   0=0 & 0=z => 0=z];
  !z:nat.0=0 & 0=z => 0=z;                                   % BASE CASE : y = 0
			
 [y':nat, !z:nat.0 = y'& y'= z => 0 = z;                     % IH (x=0 and y = y')
  [z:nat;
    [0 = s y' & s y'=z;
     0 = s y';
     0=z];
   0=s y' & s y'=z=>0=z];                   
  !z:nat.0=s y' & s y'=z => 0=z];                            % Step case : y = s y' 
  !z:nat.0=y & y=z => 0=z];                                  % Induction on y
  !y:nat.!z:nat.0=y & y=z => 0=z;                            % Base Case : x = 0 

 [x':nat, !y:nat.!z:nat. (x' = y) & (y = z) => (x' = z);     % IH (x = x')
  [y:nat;
   [z:nat;
    [s x'=0 & 0 = z;
     s x'=0;
     s x'=z];
     s x'=0 & 0=z => s x'=z];

   !z:nat.s x'=0 & 0=z => s x'=z;                            % Case : x = s x' and y = 0 


   [y':nat, !z:nat. (s x' = y') & (y' = z) => (s x' = z );   % Case x = s x' and y = (s y') 
    [z:nat;
     [s x'=s y' & s y'=0;                                                 
      s y'=0;  
     s x'=0];
     s x'=s y' & s y'=0=>s x'=0;                             % sub-case : z = 0 

	
     [z':nat, s x'=s y' & s y'=z' => s x'=z';                % sub-case : z = s (z')
      y':nat;                                                % Instantiate IH y'/y, z'/z
      !z:nat. (x' = y') & (y' = z) => (x' = z);              % 
      z':nat;                                                %
      (x' = y') & (y' = z') => (x' = z');                    %

      [s x'=s y' & s y'=s z';
       s x'=s y'; 
         x' = y';
       s y' = s z';
         y' = z';
         x' = y' & y' = z';         
         x' = z';
       s x' = s z'];       
  s x'=s y' & s y'=s z'=>s x'=s z'];

        s x'=s y' & s y'=z => s x'=z];
 !z:nat.s x'=s y' & s y'=z=>s x'=z];

 !z:nat.s x'=y & y=z => s x'=z];
!y:nat.!z:nat.s x'=y & y=z => s x'=z];
!y:nat.!z:nat.x=y & y=z => x=z];
!x:nat.!y:nat.!z:nat.x=y & y=z => x=z;
end;


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% Lemma plus0
%

proof plus0 : !y:nat. (y = (plus y 0)) = 
begin
[y:nat;
 0:nat;
 0 = 0;
 0 = plus 0 0;
 [y':nat, y' = plus y' 0;
 s y' = s(plus y' 0);
 s y' = plus (s y') 0];
 y = (plus y 0)];
!y:nat. y = (plus y 0);
end;

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% Theorem: Commutativity of plus
%

proof com : !x:nat.!y:nat. ((plus x y) = (plus y x)) =
begin
[x:nat;
 [y:nat;
  !y:nat. (y = (plus y 0));
  y = (plus y 0);
  (plus 0 y) = (plus y 0)];                       
 !y:nat. ((plus 0 y) = (plus y 0));                % Base Case : x = 0 

  [x':nat, !y:nat. ((plus x' y) = (plus y x'));    % Step Case : x = s x'
   [y:nat;

    !u:nat. !v:nat. plus u (s v) = s (plus u v);   % by lemma plusS
    s x':nat;
    !v:nat. plus y (s v) = s (plus y v);
    plus y (s x') = s (plus y x');                 

    !u:nat. !v:nat. u = v => v = u;                % by lemma sym
    plus y (s x') : nat;                           
    !v:nat . (plus y (s x') = v) => (v = plus y (s x'));
    s (plus y x') : nat; 
    (plus y (s x')) = s (plus y x') => s (plus y x') = (plus y (s x'));

    s (plus y x') = (plus y (s x'));               % by applying lemma sym

    ((plus x' y) = (plus y x'));                   % by IH
    s(plus x' y) = s (plus y x');

    s(plus x' y) = s (plus y x') & (s (plus y x')) = plus y (s x');
  
    !u:nat.!v:nat.!w:nat.(u=v & v=w => u=w);        % by lemma trans
     s(plus x' y): nat; s (plus y x'):nat; plus y (s x'):nat;
    !v:nat.!w:nat.(s(plus x' y) =v & v=w => s(plus x' y)=w);
    !w:nat.(s(plus x' y) = s (plus y x') & s (plus y x') = w => s(plus x' y) = w);
    (s(plus x' y) = s (plus y x') & s (plus y  x') = plus y (s x')) 
        => s(plus x' y)= plus y (s x');
    
    s(plus x' y)= plus y (s x');                    % by applying lemma trans
   (plus (s x') y) = (plus y (s x'))];
  !y:nat. ((plus (s x') y) = (plus y (s x')))];
 !y:nat. ((plus x y) = (plus y x))];
!x:nat.!y:nat. ((plus x y) = (plus y x));
end;