%%% Assignment 8 %%% Out: Mon 19 Nov %%% Due: Mon 26 Nov % % 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. % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % 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. % % proof sym : !x:nat.!y:nat. (x = y) => (y = x) ; % % Extra credit (10pt): Write and check the proof in Tutch! % % Then give a proof term and check the proof term with Tutch: % term sym : !x:nat.!y:nat. (x = y) => (y = x) ; % % % % 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); % % Give an equational specification of a corresponding proof term. % % % % 3. Successor and Addition. % % Prove formally the following proposition, in which x + y represents % the addition function plus x y, defined in lecture 13: % % % proof Sa : !x:nat.!y:nat. plus x (s y) = s (plus x y); % % Extra credit (10pt): Write and check the proof in Tutch! % % % % Now give a term for your proof and check the proof term with Tutch. % term Sa : !x:nat.!y:nat. (plus x (s y) = s (plus x y); % % % % 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); % % % Extra credit (10pt): Write and check the proof in Tutch! % % % Extra Credit (25 pts). % % Give an equational specification of a term for your proof of problem 4. % % %%%