% Several Proofs in propositional logic

proof andAss : (A & B) & C => A & (B & C) =
begin
[ (A & B) & C;
  A & B;
  A;
  B;
  C;
  B & C;
  A & (B & C) ];
(A & B) & C => A & (B & C)
end;

proof andComm : A & B => B & A =
begin
[ A & B;
  A;
  B;
  B & A ];
A & B => B & A  
end;

proof dist1l : A & (B | C) => A&B | A&C =
begin
[ A & (B | C);
  A;
  B | C;
  [ B;
    A&B; 
    A&B | A&C ];
  [ C;
    A&C;
    A&B | A&C ];
  A&B | A&C ];
A & (B | C) => A&B | A&C
end;

proof dist1r : A&B | A&C => A & (B | C) = 
begin
[ A&B | A&C;
  [ A & B;
    A ];
  [ A & C;
    A ];
  A; 
  [ A & B;
    B;
    B | C ];
  [ A & C;
    C;
    B | C ];
  B | C;
  A & (B | C) ];
A&B | A&C => A & (B | C)
end;


proof S : (A => B => C) => (A => B) => A => C =
begin
[ A => B => C;
  [ A => B;
    [ A;
      B;
      B => C;
      C ];
    A => C ];
  (A => B) => A => C];
(A => B => C) => (A => B) => A => C
end;

proof impDef : ~A|B => A=>B =
begin
[ ~A|B;
  [ A;
    [ ~A;
      F;	
      B	];	
    [ B;
      B	];	
    B ];	
  A=>B ];	
~A|B => A=>B	
end;


proof pem: ~~(B|~B) =
begin
[ ~(B|~B);
  [ B;
    B|~B;	
    F
  ];		
  ~B;		
  B|~B;		
  F
];		
~~(B|~B)	
end;



proof peirce : (~~A => A) => (~~B => B) => ((A => B) => A) => A =
begin
  [ (~~A => A);
    [ (~~B => B);
      [ ((A => B) => A);
        [ ~A;
          [ A;
            F;
            B ];
          A => B;
          A;
          F ];
        ~~A;
        A ];
      ((A => B) => A) => A ];
    (~~B => B) => ((A => B) => A) => A ];
(~~A => A) => (~~B => B) => ((A => B) => A) => A;
end;