(** Homework Assignment 1 Checker#<br>#
#<a href="http://www.cs.berkeley.edu/~adamc/itp/">#Interactive Computer Theorem
Proving#</a><br>#
CS294-9, Fall 2006#<br>#
UC Berkeley *)

(** Directions for using this file to check your solutions:
  - Have your solutions in a file named [Sol1.v].
  - Run [coqc Sol1] from the command line.
  - With the file you're reading now in the same directory, run [coqc Check1].
  - If you don't see any error messages, then you're done!
    (Actually, Coq will allow you to use the [Axiom] command and its synonyms to
    assert facts without justification, but just avoid using these and you can
    rely on this checker. [:-)])
  *)

Module Type HW1_SIG.
  Section propositional.
    Variables P Q R : Prop.

    Axiom truth : True.
    Axiom contradiction_P : False -> P.
    Axiom and_associates : (P /\ Q) /\ R -> P /\ (Q /\ R).
    Axiom cut_out_the_middle_man : P /\ Q /\ R -> P /\ R.
    Axiom make_up_your_mind : True \/ False.
    Axiom or_commutes : P \/ Q -> Q \/ P.
    Axiom or_associates : (P \/ Q) \/ R -> P \/ (Q \/ R).
    Axiom something_fishy : (P -> Q) -> P -> ~Q -> R.
    Axiom contrapositive : (P -> Q) -> ~Q -> ~P.
  End propositional.

  Axiom ofcourse :
    forall A : Set,
      A ->
      forall (f : A -> A) (P : A -> Prop),
	(forall x : A, P (f x)) -> exists y : A, P y.

  Section firstorder.
    Variable A : Set.
    Variable e : A.
    Variable f : A -> A.
    Variables P P' : A -> Prop.
    Variable Q : A -> A -> Prop.

    Axiom indeed : forall (A : Set) (e : A) (f : A -> A) (P : A -> Prop),
      (forall x : A, P x) -> P (f e).
    Axiom swap_quantifiers :
      (exists x : A, forall y : A, Q x y)
      -> (forall y : A, exists x : A, Q x y).
    Axiom nobody :
      (forall x : A, ~(P x))
      -> ~(exists x : A, P x).
    Axiom coalesce1 : (forall x : A, P x) /\ (forall x : A, P' x)
      -> (forall x : A, P x /\ P' x).
    Axiom coalesce2 : (forall x : A, P x /\ P' x)
      -> (forall x : A, P x) /\ (forall x : A, P' x).
    Axiom one_or_the_other :
      (forall x : A, P x -> P' e)
      -> ((forall y : A, P' y) \/ (exists z : A, P z))
      -> P' e.
    Axiom reverse_congruence : forall x : A, forall y : A,
      x = y -> f y = f x.
    Axiom small_world : (exists x : A, forall y : A, x = y)
      -> e = f e.
    Axiom nasty : forall x : A, forall y : A, forall z : A,
      f (f x) = x
      -> f z = f x
      -> f y = f z
      -> f (f (f (f (f x)))) = f y.
  End firstorder.
End HW1_SIG.

Require Sol1.

Module Sol1_Verified : HW1_SIG := Sol1.