%%% Author : Brigitte Pientka

%%%
%%% Definitions for plus and predecessor 
%%%

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

val pred : nat -> nat = fn x  => rec x
      of f(0) => 0
       | f(s(x')) => x'
    end;

%%%
%%% Reflexivity of =
%%%
proof reflEq : !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 term for reflexivity

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



%%%
%%% Transitivity
%%%
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;


proof verPred : !x:nat. ~(x = 0) => (s (pred x) = x) = 
begin
[ x: nat;                                 
      [ ~0 = 0;                               
        0 = 0;                                  % by =NI0
        F;                                      % by ImpE 2 3
        s (pred 0) = 0 ];                       % by FalseE 4
      ~0 = 0 => s (pred 0) = 0;                 % by ImpI 5
      [ x': nat, ~x' = 0 => s (pred x') = x';  
        [ ~s x' = 0;                          
          !z:nat. z = z;                        % by Lemma reflEq
         s x' : nat;                         
         s (pred (s x')) = s x' ];              % by ForallE 9 10
       ~s x' = 0 => s (pred (s x')) = s x' ];   % by ImpI 11
     ~x = 0 => s (pred x) = x ];                % by NatE 1 6 12
   !x:nat. ~x = 0 => s (pred x) = x;
end;


term vpred : !x:nat. ~(x = 0) => (s (pred x) = x) = 
fn x => rec x of 
  f 0 => (fn u => abort (u eq0))
| f (s x') => (fn u => (refl (s x')))
end;