Combinator calculus proofs with Coq

combinator.v

(* definitions from section 7.3 of Coq Art *)

Section combinatory_logic.

Variables
  (CL : Set)
  (App : CL -> CL -> CL)
  (S : CL)
  (K : CL)
  (I : CL).

Hypotheses
  (S_rule :
   forall A B C : CL,
     App (App (App S A) B) C = App (App A C) (App B C))
  (K_rule :
   forall A B : CL,
     App (App K A) B = A).

Theorem I_eq_SKK : forall A : CL,
  App (App (App S K) K) A = A.
Proof.
 intros.
 rewrite S_rule.
 rewrite K_rule.
 reflexivity.
Qed.

Theorem I_eq_SKS : forall A : CL,
  App (App (App S K) S) A = A.
Proof.
  intros.
  rewrite S_rule.
  rewrite K_rule.
  reflexivity.
Qed.

Hypotheses
  (I_rule :
   forall A : CL,
     App I A = A).

Theorem SIIa_eq_aa : forall A : CL,
  App (App (App S I) I) A = (App A A).
Proof.
  intro A.
  rewrite S_rule.
  rewrite I_rule.
  reflexivity.
Qed.

Theorem reverses : forall A B : CL,
  App (App (App (App S (App K (App S I))) K) A) B = App B A.
Proof.
  intros A B.
  rewrite S_rule.
  rewrite K_rule.
  rewrite S_rule.
  rewrite K_rule.
  rewrite I_rule.
  reflexivity.
Qed.

End combinatory_logic.