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