%%% Assignment 6
%%% Out: Mon 29 Oct
%%% Due: Mon 5 Nov 
%%% Author : Brigitte Pientka
%
% This assignment is to be turned in on paper.
%
% 
% 1. Equality.
%
%  A type X is said to be infinite if 
%  there is an operation f : X -> X on it that is:
%
%  - injective, i.e. fx = fy implies x = y,
%
%  - not surjective, i.e. it's not the case that
%    for every y there is some x with y = fx.
%
%  Prove formally that the type of natural numbers is infinite.
%  Specifically, give natural deduction proofs of the following:
%
%  x : nat, y : nat |- sx = sy => x = y
%
%  x : nat |- ~(sx = 0)
%

Proving eqtest: !x:nat. !y:nat. (s x = s y => x = y) & ~s x = 0 ...
  1  [ x: nat;                                                         
  2    [ y: nat;                                                       
  3      [ s x = s y;                                                  
  4        x = y ];                                                    by =NEss 3
  5      s x = s y => x = y;                                           by ImpI 4
  6      [ s x = 0;                                                    
  7        F ];                                                        by =NEs0 6
  8      ~s x = 0;                                                     by ImpI 7
  9      (s x = s y => x = y) & ~s x = 0 ];                            by AndI 5 8
 10    !y:nat. (s x = s y => x = y) & ~s x = 0 ];                      by ForallI 9
 11  !x:nat. !y:nat. (s x = s y => x = y) & ~s x = 0                   by ForallI 10
QED

%
% 2. The predicate Even(n).
% 
%  Implement the predicate Even(n) on natural numbers
%  by giving formation, introduction, and elimination rules
%  following the pattern of m = n .
%

 Formation rules: 
 
  m prop 
 ----------- F
 even m prop
 
 Introduction rules :
 
                      even n true
 ------------Iev0    ------------------- Ievs
 even 0 true         even (s s n) true
 
 
 Elimination rules:
 
 even (s s n) true
 ------------------ Eevs
  even n  true
 
 
 even (s 0) true
 ---------------- Eev1
  C true
 

%  Prove, from your rules, that 4 is even, and that 3 is not.

 ----------- Iev0
  even 0 
------------------ Ievs      
 even (s s 0)
------------------ Ievs
 even (s s s s 0)



-------------------- u 
  even (s s s 0)
 ------------------- Eevs
  even (s 0)
 ------------------- Eev1
    false
-------------------- notI
 ~(even (s s s 0)) 

%
%
% 3. Induction.
%
%  Prove informally, by induction, that sn + sn is always greater than sn.
%
%  How much of your proof can be formalized in our current system?
%  Indicate which steps are justified by our rules, and which are not.
%

Induction on the structure of n

Case : n = 0 

          0  < (s 0)           by <I0
          0  < 0 + (s 0)       by def of +
       (s 0) < s (0 + (s 0))   by <Is
       (s 0) < (s 0) + (s 0)   by def of +  


Case : n = (s n')

  
      n' < s n'                 by lemma         
  (s n') < (s n') + (s n')      by IH
      n' < (s n') + (s n')      by transitivity
    s n' < s ((s n') + (s n'))  by <Is
   s n'  <  (s s n') + s n'     by def of +
  s n'   < s n' + (s s n')      by commutativity of +
 s s n') < s (s n' + (s s n'))  by <Is 
(s s n') < (s s n') + (s s n')  by def of +


To completely formalize this proof, we need the lemmas
n' < s n', commutativity of + and transitivity of <. 
All of them can be proven by induction.  

%
% 4. Quantifiers.
%
%  Give a natural deduction proof of the following proposition:
%
%  (?x:t. !y:t . A(x,y)) => (!y:t. ?x:t . A(x,y))
%
%  Do you think the converse of the above can be proved?
%  Justify your answer.
%
Proving : (?x:t. !y:t. A (x, y)) => !x:t. ?y:t. A (y, x) ...
  1  [ ?x:t. !y:t. A (x, y);                                           
  2    [ c: t, !y:t. A (c, y);                                         
  3      [ b: t;                                                       
  4        A (c, b);                                                   by ForallE 2 3
  5        ?y:t. A (y, b) ];                                           by ExistsI 2 4
  6      !x:t. ?y:t. A (y, x) ];                                       by ForallI 5
  7    !x:t. ?y:t. A (y, x) ];                                         by ExistsE 1 6
  8  (?x:t. !y:t. A (x, y)) => !x:t. ?y:t. A (y, x)                    by ImpI 7
QED

The converse is not provable, as there is no instantiation for x on the right or 
y on the left possible without violating the eigenvariablen condition.

%%%
%%%
%%%