%%% Assignment 3 %%% Out: Monday Sep 24 %%% Due: Monday Oct 1 %%% Author : Brigitte Pientka %%% annotate the proofs from Assignment 1: annotated proof a : (A & (B & C)) => (A & B) = begin [x : A & (B & C); fst x : A; snd x : B & C; fst (snd x) : B; (fst x, fst (snd x)) : A & B]; fn x => (fst x, fst (snd x)) : (A & (B & C)) => (A & B) end; annotated proof b : (A => B) => ((B => C) => (A => C)) = begin [x : A => B; [y : B => C; [z : A; x z : B; y (x z) : C]; fn z => y (x z) : A => C]; fn y => fn z => y (x z) : (B => C) => (A => C)]; fn x => fn y => fn z => y (x z) : (A => B) => ((B => C) => (A => C)) end; annotated proof c : ((A => B) & (A | C)) => (B | C) = begin [x : ((A => B) & (A | C)); % 1 Assumption fst x : A => B; % 2 AndE1 1 snd x : A | C; % 3 AndE2 2 [y : A; % 4 Assumption (OrE(1)) (fst x) y : B; % 5 ImpE 2,4 inl ((fst x) y) : B | C]; % 6 OrE(1) [y : C; % 7 Assumption (OrE(2)) inr y : B | C]; % 8 OrI2 case (snd x) of inl y => inl ((fst x) y) | inr y => inr y end : B | C]; % 9 OrE fn x => case (snd x) of inl y => inl ((fst x) y) | inr y => inr y end : ((A => B) & (A | C)) => (B | C); % 10 ImpI 1,9 end; annotated proof d : (A => ~ A) => (~ A) = begin [x : A => ~ A; % 1 Assumption [y : A; % 2 Assumption x y : ~ A; % 3 ImpE 2 x y y : F]; % 4 ImpE 2 fn y => x y y : ~ A; % 5 ImpI ]; fn x => fn y => (x y) y : (A => ~ A) => ~ A; % 6 ImpI end; annotated proof da : (A => (A => F)) => (A => F) = begin [x : (A => (A => F)); % 1 Assumption (from ImpI ) [y : A; % 2 Assumption (from ImpI on ~A) x y : A => F; % 3 ImpE 1, 2 (x y) y : F]; % 4 Imp fn y => (x y) y : A => F; ]; fn x => fn y => (x y) y : (A => (A => F)) => (A => F); end; annotated proof e : (~ A & ~ B) => ~ (A | B) = begin [x : ~ A & ~ B; fst x : ~ A; snd x : ~ B; [y : A | B; [z : A; (fst x) z : F]; [z : B; (snd x) z : F]; case y of inl z => (fst x) z | inr z => (snd x) z end : F]; fn y => case y of inl z => (fst x) z | inr z => (snd x) z end: ~ (A | B)]; fn x => fn y => case y of inl z => (fst x) z | inr z => (snd x) z end: (~ A & ~ B) => ~ (A | B); end; annotated proof f : A <=> A = begin [x : A; x : A]; fn x => x : A => A; (fn x => x, fn x => x) : A <=> A; end; annotated proof g1 : (A <=> T) => A = begin [x : A <=> T; snd x : T => A; () : T; (snd x) () : A]; fn x => (snd x) () : (A <=> T) => A; end; annotated proof g2: A => (A <=> T) = begin [x : A; [y : T; x : A]; fn y => x : T => A; [y : A; () : T]; fn y => () : A => T; (fn y => (), fn y => x) : A <=> T]; fn x => (fn y => (), fn y => x) : A => (A <=> T); end; annotated proof g : (A <=> T) <=> A = begin [x : A; [y : T; x : A]; fn y => x : T => A; [y : A; () : T]; fn y => () : A => T; (fn y => (), fn y => x) : A <=> T]; fn x => (fn y => (), fn y => x) : A => (A <=> T); [x : A <=> T; snd x : T => A; () : T; (snd x) () : A]; fn x => (snd x) () : (A <=> T) => A; (fn x => (snd x) (), fn x => (fn y => (), fn y => x)) : (A <=> T) <=> A; end; annotated proof h : ((A & B) => C) <=> (A => (B => C)) = begin [x : (A & B) => C; [y : A; [z : B; (y, z) : A & B; x (y, z) : C]; fn z => x (y, z) : B => C]; fn y => fn z => x (y, z) : A => (B => C)]; fn x => fn y => fn z => x (y, z) : ((A & B) => C) => (A => (B => C)); [x : A => (B => C); [y : A & B; fst y : A; snd y : B; x (fst y) : (B => C); x (fst y) (snd y) : C]; fn y => x (fst y) (snd y) : (A & B) => C]; fn x => fn y => x (fst y) (snd y) : (A => (B => C)) => ((A & B) => C); (fn x => fn y => fn z => x (y, z) , fn x => fn y => x (fst y) (snd y)) : ((A & B) => C) <=> (A => (B => C)); end;