Functional Dependency Theory in Coq

fdep.v

(* 
   The following is an attempt at verifying Armstrong's axioms[1] of functional dependencies.
   These include: Reflexivity, Transitivity, Augmentation, Union, Decomposition, and 
   Pseudotransitivity. These appear to hold, and should be considered valid axioms. 

  [1] http://en.wikipedia.org/wiki/Armstrong's_axioms
*)

Theorem dep_reflexivity : 
  forall a:Prop, 
      a -> a.
  intros.
  apply H.
  Qed.

Theorem dep_transitivity: 
  forall a:Prop, exists b:Prop, exists c:Prop,
      ((a -> b) /\ (b -> c)) -> (a -> c).
  intros.
  exists a.
  exists a.
  auto.
  Qed.

Theorem dep_augmentation:
  forall a:Prop, exists b:Prop, exists c:Prop,
      ((a -> a) /\ (b -> c) ) -> ((a /\ b) -> (a /\ c)).
  intros.
  exists a.
  exists a.
  auto.
  Qed.

Theorem dep_union:
  forall a:Prop, exists b:Prop, exists c:Prop,
      ((a -> b) /\ (a -> c)) -> (a -> (b /\ c)).
  intros.
  exists a.
  exists a.
  auto.
  Qed.

Theorem dep_decompose:
  forall a:Prop, exists b:Prop, exists c:Prop,
      (a -> (b /\ c)) -> ((a -> b) /\ (a -> b)).
  intros.
  exists a.
  exists a.
  auto.
  Qed.

Theorem dep_pseudotransit:
  forall a:Prop, exists b:Prop, forall c:Prop, exists d:Prop,
     ((a -> b) /\ ((b /\ c) -> d)) -> ((a /\ c) -> d).
  intros.
  exists a.
  exists a.
  auto.
  tauto.
  Qed.