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