Require Export Classical. 

(* Try to nuke goals that are easily seen to be provable. *)
Ltac close :=
  match goal with 
    H:False |- _ => elim H
  | H:?x <> ?x |- _ => elim H; reflexivity
  | H:?P, H1:~?P |- _ => elim H1; exact H

  (* repeated in gclose below *)
  | H:?P |- ?P => exact H
  | |- True => exact I
  | |- ?x = ?x => reflexivity
  | _ => idtac
  end.

(* like close, but only tries things where the goal formula matters. *)
Ltac gclose := 
  match goal with 
    H:?P |- ?P => exact H
  | |- True => exact I
  | |- ?x = ?x => reflexivity
  | _ => idtac
  end.

(* /\ *)

Ltac Ua H n1 n2 := elim H; intro n1; intro n2; close.
Ltac ua H := 
 let n1 := fresh in
 let n2 := fresh in
 (Ua H n1 n2).
Ltac ca H := 
 let n1 := fresh in
 let n2 := fresh in
 (Ua H n1 n2; clear H; rename n2 into H).
Ltac ca2 H n1 := 
 let n2 := fresh in
 (Ua H n1 n2; clear H; rename n2 into H).
Ltac pa := split; gclose.

(* \/ *)

Ltac Uo H n := elim H; intro n; close.
Ltac uo H := let n := fresh in Uo H n.
Ltac co H := 
  let n := fresh in
  (Uo H n; clear H; rename n into H).
Ltac po1 := left; gclose.
Ltac po2 := right; gclose.

(* -> *)

Ltac Ui0 H1 H2 n := 
  let x := type of (H1 H2) in
  (assert (n:x); [ exact (H1 H2) | idtac]).
Ltac Ui1 H1 H2 n := 
  let x := type of (H1 _ H2) in
  (assert (n:x); [ exact (H1 _ H2) | idtac]).
Ltac Ui2 H1 H2 n := 
  let x := type of (H1 _ _ H2) in
  (assert (n:x); [ exact (H1 _ _ H2) | idtac]).
Ltac Ui3 H1 H2 n := 
  let x := type of (H1 _ _ _ H2) in
  (assert (n:x); [ exact (H1 _ _ _ H2) | idtac]).
Ltac Ui4 H1 H2 n := 
  let x := type of (H1 _ _ _ _ H2) in
  (assert (n:x); [ exact (H1 _ _ _ _ H2) | idtac]).
Ltac Ui5 H1 H2 n := 
  let x := type of (H1 _ _ _ _ _ H2) in
  (assert (n:x); [ exact (H1 _ _ _ _ _ H2) | idtac]).
Ltac Ui6 H1 H2 n := 
  let x := type of (H1 _ _ _ _ _ _ H2) in
  (assert (n:x); [ exact (H1 _ _ _ _ _ _ H2) | idtac]).
Ltac Ui7 H1 H2 n := 
  let x := type of (H1 _ _ _ _ _ _ _ H2) in
  (assert (n:x); [ exact (H1 _ _ _ _ _ _ _ H2) | idtac]).
Ltac Ui H1 H2 n :=
 (Ui0 H1 H2 n || 
  Ui1 H1 H2 n || 
  Ui2 H1 H2 n || 
  Ui3 H1 H2 n || 
  Ui4 H1 H2 n || 
  Ui5 H1 H2 n || 
  Ui6 H1 H2 n || 
  Ui7 H1 H2 n); close.
Ltac ui H1 H2 := 
  let n := fresh in 
  (Ui H1 H2 n).
Ltac ci H1 H2 := 
  let n := fresh in 
  (Ui H1 H2 n; clear H2; rename n into H2).
Ltac pi := intro; close.

(* <-> *)

Ltac UI0a H1 H2 n := 
  let t := constr:((proj1 H1) H2) in
  let x := type of t in
  (assert (n:x); [ exact t | idtac ]).
Ltac UI0b H1 H2 n := 
  let t := constr:((proj2 H1) H2) in
  let x := type of t in
  (assert (n:x); [ exact t | idtac ]).
Ltac UI0 H1 H2 n := UI0a H1 H2 n || UI0b H1 H2 n.

Ltac UI1a H1 H2 n := 
  let t := constr:(proj1 (H1 _) H2) in
  let x := type of t in
  (assert (n:x); [ exact t | idtac ]).
Ltac UI1b H1 H2 n := 
  let t := constr:(proj2 (H1 _) H2) in
  let x := type of t in
  (assert (n:x); [ exact t | idtac ]).
Ltac UI1 H1 H2 n := UI1a H1 H2 n || UI1b H1 H2 n.

Ltac UI2a H1 H2 n := 
  let t := constr:(proj1 (H1 _ _) H2) in
  let x := type of t in
  (assert (n:x); [ exact t | idtac ]).
Ltac UI2b H1 H2 n := 
  let t := constr:(proj2 (H1 _ _) H2) in
  let x := type of t in
  (assert (n:x); [ exact t | idtac ]).
Ltac UI2 H1 H2 n := UI2a H1 H2 n || UI2b H1 H2 n.

Ltac UI3a H1 H2 n := 
  let t := constr:(proj1 (H1 _ _ _) H2) in
  let x := type of t in
  (assert (n:x); [ exact t | idtac ]).
Ltac UI3b H1 H2 n := 
  let t := constr:(proj2 (H1 _ _ _) H2) in
  let x := type of t in
  (assert (n:x); [ exact t | idtac ]).
Ltac UI3 H1 H2 n := UI3a H1 H2 n || UI3b H1 H2 n.
  
Ltac UI4a H1 H2 n := 
  let t := constr:(proj1 (H1 _ _ _ _) H2) in
  let x := type of t in
  (assert (n:x); [ exact t | idtac ]).
Ltac UI4b H1 H2 n := 
  let t := constr:(proj2 (H1 _ _ _ _) H2) in
  let x := type of t in
  (assert (n:x); [ exact t | idtac ]).
Ltac UI4 H1 H2 n := UI4a H1 H2 n || UI4b H1 H2 n.
  
Ltac UI5a H1 H2 n := 
  let t := constr:(proj1 (H1 _ _ _ _ _) H2) in
  let x := type of t in
  (assert (n:x); [ exact t | idtac ]).
Ltac UI5b H1 H2 n := 
  let t := constr:(proj2 (H1 _ _ _ _ _) H2) in
  let x := type of t in
  (assert (n:x); [ exact t | idtac ]).
Ltac UI5 H1 H2 n := UI5a H1 H2 n || UI5b H1 H2 n.
  
Ltac UI H1 H2 n := 
   (UI0 H1 H2 n
 || UI1 H1 H2 n
 || UI2 H1 H2 n
 || UI3 H1 H2 n
 || UI4 H1 H2 n
 || UI5 H1 H2 n); close.

Ltac uI H1 H2 := let n := fresh in UI H1 H2 n.
Ltac cI H1 H2 := let n := fresh in (UI H1 H2 n; clear H2; rename n into H2).
Ltac pI := pa; pi; close.

Ltac applyI0 H := apply (proj1 H) || apply (proj2 H).
Ltac applyI1 H := apply (fun x => proj1 (H x))
               || apply (fun x => proj2 (H x)).
Ltac applyI2 H := apply (fun x y => proj1 (H x y)) 
               || apply (fun x y => proj2 (H x y)). 
Ltac applyI3 H := apply (fun x y z => proj1 (H x y z)) 
               || apply (fun x y z => proj2 (H x y z)). 
Ltac applyI4 H := apply (fun w x y z => proj1 (H w x y z)) 
               || apply (fun w x y z => proj2 (H w x y z)). 
Ltac applyI5 H := apply (fun v w x y z => proj1 (H v w x y z)) 
               || apply (fun v w x y z => proj2 (H v w x y z)). 
Ltac applyI H := (applyI0 H 
               || applyI1 H
               || applyI2 H
               || applyI3 H
               || applyI4 H 
               || applyI5 H); close .

(* ~ *)

Ltac Un H1 H2 n := Ui H1 H2 n.
Ltac un H1 H2 := ui H1 H2.
Ltac cn H1 H2 := ci H1 H2.
Ltac pn := intro; gclose.

Ltac Contra n := apply NNPP; intro n; close.
Ltac contra := apply NNPP; intro; close.

(* False *)

Ltac uf H := elim H.

(* forall *)

Ltac UA H t n := 
  let x := type of (H t) in
  (assert (n:x); [ exact (H t) | close ]).
Ltac uA H t := let n := fresh in UA H t n.
Ltac cA H t := 
  let n := fresh in
  (UA H t n; clear H; rename n into H).
Ltac pA := intro; gclose.
Ltac pAs :=
  match goal with 
    |- ?p -> ?q => gclose
    | _ => (pA; pAs) || idtac
  end.

(* exists *)

Ltac UE H n1 n2 := elim H; intro n1; intro n2; close.
Ltac uE H := 
  let n1 := fresh "x" in 
  let n2 := fresh in 
  (UE H n1 n2).
Ltac cE H := 
  let n1 := fresh "x" in 
  let n2 := fresh in 
  (UE H n1 n2; clear H; rename n2 into H).
Ltac pE t := exists t; gclose. 

(* other *)

Ltac immediate := assumption.

Ltac Import n H :=
   let x := type of H in 
   (assert (n:x); [ exact H | idtac ]).

Ltac import H := 
   let n := fresh in
     Import n H.

(* case split *)
Ltac cs F :=
   let n := fresh in 
   (assert (n:F \/ ~F); [ apply classic | co n; close]).

Lemma not_forall : forall (t : Set) (phi : t -> Prop),
                   ~ (forall x:t, phi x) <-> exists x : t, ~ (phi x).
pAs.
pI.
contra.
assert (forall x:t, phi x).
pA.
contra.
assert (exists x:t, ~ phi x).
pE x; immediate.
ci H0 H2.
ci H H1.
pn.
cE H.
cA H0 x.
Qed.

Lemma demorgan1 : forall P Q : Prop, ~ (~ P \/ ~ Q) <-> P /\ Q.
pAs.
pI.
pa.
contra.
assert (~P \/ ~Q).
po1.
un H H1.
contra.
assert (~P \/ ~Q).
po2.
un H H1.
pn.
ua H.
uo H0.
Qed.

Lemma not_and : forall P Q : Prop, ~ (P /\ Q) <-> ~ P \/ ~Q.
pAs; pI.
contra.
cI demorgan1 H0.
pn.
ua H0.
uo H.
Qed.

Lemma not_imp : forall p q : Prop, ~ (p -> q) <-> p /\ ~q.
pAs.
pI.
contra.
cI not_and H0.
co H0.
assert (p -> q).
pi.
un H H1.
assert (p -> q).
pi.
contra.
cn H H1.
pn.
ca H.
un H0 H1.
Qed.

Lemma not_or : forall p q : Prop, ~ (p \/ q) <-> ~ p /\ ~ q.
pAs; pI.
contra.
cI not_and H0.
co H0.
assert (p \/ q).
po1.
contra.
cn H H1.
assert (p \/ q).
po2.
contra.
cn H H1; immediate.
ca H.
pn.
co H1.
Qed.

Lemma not_exists : forall (t : Set) (phi : t -> Prop), ~ (ex phi) <-> 
                              forall x:t, ~phi x.
pAs; pI.
pA.
pn.
assert (ex phi).
pE x.
cn H H1.
pn.
cE H0.
cA H x.
Qed.

Ltac bd H :=
  let f := type of H in
  let n := fresh in 
  let n1 := fresh in 
   match f with
   ?p \/ ?q => co H; bd H
  | ?p /\ ?q => 
     let n := fresh in 
     (ca2 H n; bd H; bd n)
  | ex ?phi => cE H; bd H
  |  ~ (?P -> ?Q) => 
         assert (n:P /\ ~Q); [ uI not_imp H; immediate 
                                     | clear H; Ua n H n1; clear n; bd H; bd n1]
  | ~ (ex ?P) => 
         assert(n:forall x, ~ P x); [ uI (not_exists _ P) H; immediate 
                                              | clear H; rename n into H; simpl in H]

  | ~ (?P /\ ?Q) =>
         assert (n:~P \/ ~Q); [uI not_and H; immediate
                                      | clear H; rename n into H; co n; bd n]
  | ~ (?P \/ ?Q) =>
         assert (n:~P /\ ~Q); [uI not_or H; immediate
                                      | clear H; Ua n H n1; clear n; bd H; bd n1]

  | ~ ~ ?P => ci NNPP H; bd H
  | True => clear H
  | ~ False => clear H
  | _ => close
  end.


Ltac change_with e :=
  let n := fresh in
  (assert (n:e); [ simpl; reflexivity | rewrite n; clear n]).

Ltac change_with_h e H :=
   let n := fresh in
   (assert (n:e); [ simpl; reflexivity | rewrite n in H; clear n]).

Ltac caseEq x := generalize (refl_equal x); pattern x at -1; case x.

(************************************************************)
(* begin substtac                                           *)
(*                                                          *)
(* substtac tries to eliminate all equations that can be    *)
(* eliminated by using the standard Coq tactic "subst".     *)
(* The strategy is first to mark all equations using a      *)
(* an identity function called mark, and then to call       *)
(* subst on each marked equation, removing the marks as we  *)
(* go.                                                      *)
(*                                                          *)
(************************************************************)

Definition marked(P:Prop) : Prop := P.

Ltac mark H :=
  let t := type of H in
  let n:= fresh in
    (assert (n:marked t); [exact H | clear H; rename n into H]).

Ltac unmark H := unfold marked in H.

Ltac unmark_all := unfold marked in *|-.

Ltac mark_equalities :=
  match goal with
  H : ?t1 = ?t2 |- _ => mark H; mark_equalities
| _ => idtac
end.

Ltac substtac_ :=
   match goal with
     H : marked (?t1 = ?t2) |- _ =>
       unfold marked in H; try (subst t1 || subst t2); substtac_
   | _ => idtac
   end.

Ltac substtac := mark_equalities; substtac_; close.

(************************************************************)
(* end substtac                                             *)
(************************************************************)

Ltac inv H := inversion H; substtac.
Ltac inv_clear H := inversion H; substtac; clear H.

Ltac clear_all :=
  match goal with
    H: ?P |- _ => clear H; clear_all
  | _ => idtac
  end.

Ltac singe a := caseEq a; intros; substtac.