% Proof examples from Recitation 2 in Tutch

annotated proof example1 : (A => B => C) => (A => B) => A => C =
begin
  [ f : A => B => C;
    [ g : A => B;
      [ a : A;
        f a : B => C;
        g a : B;
        f a (g a) : C ];
      fn a => f a (g a) : A => C; ];
    fn g => fn a => f a (g a) : (A => B) => A => C ];
  fn f => fn g => fn a => f a (g a) : (A => B => C) => (A => B) => A => C;
end;

annotated proof example2 : (A => B => C) => (B => A => C) =
begin
  [ f : A => B => C;
    [ b : B;
      [ a : A;
        f a : B => C;
        f a b : C ];
      fn a => f a b : A => C ];
    fn b => fn a => f a b : B => A => C ];
  fn f => fn b => fn a => f a b : (A => B => C) => (B => A => C);
end;

annotated proof example3 : A & (B | C) => ((A & B) | (A & C)) =
begin
 [ x : A & (B | C);                                              % H1
   fst x : A;                                                    % C1: &E on H1
   snd x : B | C;                                                % C2: &E on H2
   [ b : B;                                                      % H2
     (fst x, b) : A & B;                                         % C3: &I on C1 and H2
     inl (fst x, b) : (A & B) | (A & C) ];                       % C4: |I1 on C3
   [ c : C;                                                      % H3
     (fst x, c) : A & C;                                         % C5: &I on C1 and H3
     inr (fst x, c) : (A & B) | (A & C) ];                       % C6: |I2 on C5
   case (snd x) of inl b => inl (fst x, b)
                 | inr c => inr (fst x, c)
                 end : ((A & B) | (A & C)) ];                    % C7: |E on C2 and H2..C4 and H3..C6
 fn x => case (snd x) of inl b => inl (fst x, b)
                       | inr c => inr (fst x, c)
                       end : A & (B | C) => ((A & B) | (A & C)); % C8: =>I on H1..C7
end;

annotated proof example4 : (T | T) => (T | T) => (T | T) =
begin
  [ a : T | T;                                                   % H1
    [ b : T | T;                                                 % H2
      [ x : T;                                                   % H3
        b : T | T ];                                             % C1: H2
      [ x : T;                                                   % H4
        () : T;                                                  % C2: TI
        inr () : T | T ];                                        % C3: |I2 on C2
      case a of inl x => b | inr x => inr () end : T | T ];      % C4: |E on H1, H3..C1, and H4..C3
    fn b => case a of inl x => b
                    | inr x => inr ()
                    end : (T | T) => (T | T) ];                  % C5: =>I on H2..C4
  fn a => fn b => case a of inl x => b
                          | inr x => inr ()
                          end : (T | T) => (T | T) => (T | T);   % C6: =>I on H1..C5
end;

annotated proof example5 : (T | T) => (T | T) => (T | T) =
begin
  [ a : T | T;                                                   % H1
    [ b : T | T;                                                 % H2
      [ x : T;                                                   % H3
        () : T;                                                  % C1: TI
        inl () : T | T ];                                        % C2: |I1 on C1
      [ x : T;                                                   % H4
        b : T | T ];                                             % C3: H2
      case a of inl x => inl () | inr x => b end : T | T ];      % C4: |E on H1, H3..C2, and H4..C3
    fn b => case a of inl x => inl ()
                    | inr x => b
                   end : (T | T) => (T | T) ];                   % C5: =>I on H2..C4
  fn a => fn b => case a of inl x => inl ()
                          | inr x => b
                          end : (T | T) => (T | T) => (T | T);   % C6: =>I on H1..C5
end;