%%% 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 (!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.
%%%
%%%
%%%