% Several Proofs in propositional logic

annotated proof andAss : (A & B) & C => A & (B & C) =
begin
[x: (A & B) & C;
 fst x : A & B;
  fst (fst x) : A;
  snd (fst x) : B;
  snd x : C;
  (snd (fst x), snd x) : B & C;
  (fst (fst x), (snd (fst x), snd x)) : A & (B & C) ];
fn x => (fst (fst x), (snd (fst x), snd x)) : (A & B) & C => A & (B & C)
end;


annotated proof dist2r : (A | B) & (A | C) => A | B&C =
begin
[ x : (A | B) & (A | C);
  fst x : A | B;
  [ y : A;
    inl y : A | B&C ];
  [ z : B;
    snd x : A | C;
    [ u : A;
      inl u : A | B&C ];
    [ v : C;
      (z, v) : B&C;
      inr (z, v) : A | B&C ];
    case (snd x) of inl u => inl u
                  | inr v => inr (z, v) end : A | B&C ];
  case (fst x) of 
      inl y => inl y 
    | inr z => case (snd x) of 
                   inl u => inl u
                 | inr v => inr (z, v) 
               end 
  end : A | B&C ];
fn x => 
  case (fst x) of 
      inl y => inl y 
    | inr z => case (snd x) of 
                   inl u => inl u
                 | inr v => inr (z, v) 
               end 
  end :(A | B) & (A | C) => A | B&C
end;

annotated proof K : A => B => A =
begin
[x : A;
 [y : B;
  x : A];
 fn y => x : B => A];
fn x => fn y => x : A => B => A;
end;


% "Implication definition" ~A|B => A=>B

annotated proof impDef : ~A|B => A=>B =
begin
[ x : ~A|B;
  [ y : A;
    [ u : ~A;
      u y: F;	                % by impE na a
      abort (u y) : B  ];	% by falseE
    [ v : B;
      v : B	];	% by b
   case x of inl u => abort (u y) 
           | inr v => v end : B ];		% by orE x
 fn y => 
    case x of inl u => abort (u y) 
            | inr v => v end :  A=>B ];	        % by impI
fn x => fn y => 
   case x of inl u => abort (u y) 
           | inr v => v end : ~A|B => A=>B	% by impI
end;

% Annotated Proof of the principle of the excluded middle
% ~~(A|~A)