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