Axiom skip : False.
Ltac skip := assert False; [ apply skip | contradiction ].
Ltac contradictions :=
assert False; [ try discriminate | contradiction ].
Ltac cuts H E :=
cut (E); [ intro H | idtac ].
Ltac inversions H :=
inversion H; subst.
Ltac poses H E :=
pose (H := E); clearbody H.
Ltac puts E :=
let H := fresh in poses H E.
Ltac asserts H E :=
assert (H : E).
Ltac sets X E :=
set (X := E) in *; clearbody X.
Ltac introz :=
intro; try introz.
Tactic Notation "folds" constr(H) :=
fold H in *.
Tactic Notation "folds" constr(H1) constr(H2) :=
folds H1; folds H2.
Tactic Notation "folds" constr(H1) constr(H2) constr(H3) :=
folds H1; folds H2; folds H3.
Tactic Notation "unfolds" reference(F1) :=
unfold F1 in *.
Tactic Notation "unfolds" reference(F1) reference(F2) :=
unfold F1 in *; unfold F2 in *.
Tactic Notation "unfolds" reference(F1) reference(F2) reference(F3) :=
unfold F1 in *; unfold F2 in *; unfold F3 in *.
Tactic Notation "unfold_hd" :=
match goal with
| |- ?P => unfold P
| |- ?P _ => unfold P
| |- ?P _ _ => unfold P
| |- ?P _ _ _ => unfold P
| |- ?P _ _ _ _ => unfold P
end.
Tactic Notation "simpls" :=
simpl in *.
Tactic Notation "simpls" reference(F1) :=
simpl F1 in *.
Tactic Notation "simpls" reference(F1) reference(F2) :=
simpl F1 in *; simpl F2 in *.
Tactic Notation "simpls" reference(F1) reference(F2) reference(F3) :=
simpl F1 in *; simpl F2 in *; simpl F3 in *.
Tactic Notation "unsimpl" constr(E) :=
let F := (eval simpl in E) in change F with E.
Tactic Notation "unsimpl" constr(E) "in" hyp(H) :=
let F := (eval simpl in E) in change F with E in H.
Tactic Notation "rewrites" constr(E) :=
repeat rewrite E.
Tactic Notation "rewrites" "<-" constr(E) :=
repeat rewrite <- E.
Tactic Notation "rewrites" constr(E) "in" ident(H) :=
repeat rewrite E in H.
Tactic Notation "rewrites" "<-" constr(E) "in" ident(H) :=
repeat rewrite <- E in H.
Tactic Notation "asserts_rew" constr(E) :=
let EQ := fresh in (assert (EQ : E);
[ idtac | rewrite EQ; clear EQ ]).
Tactic Notation "asserts_rew" "<-" constr(E) :=
let EQ := fresh in (assert (EQ : E);
[ idtac | rewrite <- EQ; clear EQ ]).
Tactic Notation "asserts_rew" constr(E) "in" hyp(H) :=
let EQ := fresh in (assert (EQ : E);
[ idtac | rewrite EQ in H; clear EQ ]).
Tactic Notation "asserts_rew" "<-" constr(E) "in" hyp(H) :=
let EQ := fresh in (assert (EQ : E);
[ idtac | rewrite <- EQ in H; clear EQ ]).
Tactic Notation "do_rew" constr(E) tactic(T) :=
rewrite E; T; try rewrite <- E.
Tactic Notation "do_rew" "<-" constr(E) tactic(T) :=
rewrite <- E; T; try rewrite E.
Tactic Notation "do_rew_2" constr(E) tactic(T) :=
do 2 rewrite E; T; try do 2 rewrite <- E.
Tactic Notation "do_rew_2" "<-" constr(E) tactic(T) :=
do 2 rewrite <- E; T; try do 2 rewrite E.
Tactic Notation "gen_eq" constr(c) "as" ident(x) ident(H) :=
set (x := c); assert (H : x = c) by reflexivity; clearbody x.
Tactic Notation "gen_eq" constr(c) "as" ident(x) :=
set (x := c) in *;
let H := fresh in (assert (H : x = c) by reflexivity; clearbody x; revert H).
Tactic Notation "gen" ident(X1) :=
generalize dependent X1.
Tactic Notation "gen" ident(X1) ident(X2) :=
gen X2; gen X1.
Tactic Notation "gen" ident(X1) ident(X2) ident(X3) :=
gen X3; gen X2; gen X1.
Tactic Notation "gen" ident(X1) ident(X2) ident(X3) ident(X4) :=
gen X4; gen X3; gen X2; gen X1.
Tactic Notation "gen" ident(X1) ident(X2) ident(X3) ident(X4) ident(X5) :=
gen X5; gen X4; gen X3; gen X2; gen X1.
Tactic Notation "split3" :=
split; [ idtac | split ].
Tactic Notation "split4" :=
split; [ idtac | split3 ].
Tactic Notation "splits" :=
repeat split.
Tactic Notation "esplit2" :=
esplit; esplit.
Tactic Notation "esplit3" :=
esplit; esplit; esplit.
Tactic Notation "esplit4" :=
esplit; esplit; esplit; esplit.
Tactic Notation "or_31" := left.
Tactic Notation "or_32" := right; left.
Tactic Notation "or_33" := right; right.
Tactic Notation "destructi" constr(T) :=
let rec doit H :=
match type of H with
| ?P -> ?Q => let A := fresh "A" in
(assert (A : P); [ idtac | doit (H A); clear A ])
| _ => first [destruct H | puts H]
end in doit T.
Tactic Notation "destructi" constr(T) "as" simple_intropattern(I) :=
let rec doit H :=
match type of H with
| ?P -> ?Q => let A := fresh "A" in
(assert (A : P); [ idtac | doit (H A); clear A ])
| _ => first [destruct H as I | poses I H]
end in doit T.
Ltac destructs H :=
let X := fresh in let Y := fresh in
first [ destruct H as [X Y]; destructs X; destructs Y | idtac ].
Tactic Notation "introv" :=
let rec go _ := match goal with
| |- ?P -> ?Q => idtac
| |- forall _, _ => intro; try go tt
end in first [ go tt | intro; go tt ].
Tactic Notation "introv" simple_intropattern(I) :=
introv; intros I.
Tactic Notation "introv" simple_intropattern(I1) ident(I2) :=
introv; intros I1 I2.
Tactic Notation "introv" simple_intropattern(I1) ident(I2) ident(I3) :=
introv; intros I1 I2 I3.
Tactic Notation "introv" simple_intropattern(I1) ident(I2) ident(I3) ident(I4) :=
introv; intros I1 I2 I3 I4.
Tactic Notation "introv" simple_intropattern(I1) ident(I2) ident(I3) ident(I4) ident(I5) :=
introv; intros I1 I2 I3 I4 I5.
Tactic Notation "exists" constr(T1) :=
exists T1.
Tactic Notation "exists" constr(T1) constr(T2) :=
exists T1; exists T2.
Tactic Notation "exists" constr(T1) constr(T2) constr(T3) :=
exists T1; exists T2; exists T3.
Tactic Notation "exists" constr(T1) constr(T2) constr(T3) constr(T4) :=
exists T1; exists T2; exists T3; exists T4.
Lemma modus_ponens : forall (P Q : Prop),
P -> (P -> Q) -> Q.
Proof. auto. Qed.
Implicit Arguments modus_ponens [P Q].
Tactic Notation "forward" constr(x) "as" simple_intropattern(H) :=
(refine (modus_ponens (x _ _ _ _ _ _ _ _ _) _); [ | | | | | | | | | intros H ])
|| (refine (modus_ponens (x _ _ _ _ _ _ _ _) _); [ | | | | | | | | intros H ])
|| (refine (modus_ponens (x _ _ _ _ _ _ _) _); [ | | | | | | | intros H ])
|| (refine (modus_ponens (x _ _ _ _ _ _) _); [ | | | | | | intros H ])
|| (refine (modus_ponens (x _ _ _ _ _) _); [ | | | | | intros H ])
|| (refine (modus_ponens (x _ _ _ _) _); [ | | | | intros H ])
|| (refine (modus_ponens (x _ _ _) _); [ | | | intros H ])
|| (refine (modus_ponens (x _ _) _); [ | | intros H ])
|| (refine (modus_ponens (x _) _); [ | intros H ])
|| (refine (modus_ponens (x _ _ _ _ _ _ _ _ _) _); [ | | | | | | | | intros H ])
|| (refine (modus_ponens (x _ _ _ _ _ _ _ _) _); [ | | | | | | | intros H ])
|| (refine (modus_ponens (x _ _ _ _ _ _ _) _); [ | | | | | | intros H ])
|| (refine (modus_ponens (x _ _ _ _ _ _) _); [ | | | | | intros H ])
|| (refine (modus_ponens (x _ _ _ _ _) _); [ | | | | intros H ])
|| (refine (modus_ponens (x _ _ _ _) _); [ | | | intros H ])
|| (refine (modus_ponens (x _ _ _) _); [ | | intros H ])
|| (refine (modus_ponens (x _ _) _); [ | intros H ])
|| (refine (modus_ponens (x _) _); [ intros H ]).
Tactic Notation "forward" constr(x) :=
refine (modus_ponens (x _ _ _ _ _ _ _ _ _ _) _)
|| refine (modus_ponens (x _ _ _ _ _ _ _ _ _) _)
|| refine (modus_ponens (x _ _ _ _ _ _ _ _) _)
|| refine (modus_ponens (x _ _ _ _ _ _ _) _)
|| refine (modus_ponens (x _ _ _ _ _ _) _)
|| refine (modus_ponens (x _ _ _ _ _) _)
|| refine (modus_ponens (x _ _ _ _) _)
|| refine (modus_ponens (x _ _ _) _)
|| refine (modus_ponens (x _ _) _)
|| refine (modus_ponens (x _) _).
Tactic Notation "auto" "*" :=
try solve [ auto | intuition eauto ].
Tactic Notation "auto" "*" int_or_var(n) :=
try solve [ auto | intuition (eauto n) ].
Tactic Notation "asserts" "*" ident(H) constr(E) :=
assert (H : E); [ auto* | idtac ].
Tactic Notation "apply" "*" constr(H) :=
first [ apply H | eapply H ]; auto*.
Tactic Notation "apply" "*" constr(H) :=
first [ apply H | eapply H ]; auto*.
Tactic Notation "contradictions" "*" :=
contradictions; auto*.
Tactic Notation "destruct" "*" constr(H) :=
destruct H; auto*.
Tactic Notation "destruct" "*" constr(H) "as" simple_intropattern(I) :=
destruct H as I; auto*.
Tactic Notation "f_equal" "*" :=
f_equal; auto*.
Tactic Notation "induction" "*" constr(H) :=
induction H; auto*.
Tactic Notation "inversion" "*" constr(H) :=
inversion H; auto*.
Tactic Notation "inversions" "*" constr(H) :=
inversions H; auto*.
Tactic Notation "rewrite" "*" constr(H) :=
rewrite H; auto*.
Tactic Notation "rewrite" "*" "<-" constr(H) :=
rewrite <- H; auto*.
Tactic Notation "do_rew" "*" constr(E) tactic(T) :=
(do_rew E T); auto*.
Tactic Notation "do_rew" "*" "<-" constr(E) tactic(T) :=
(do_rew <- E T); auto*.
Tactic Notation "do_rew_2" "*" constr(E) tactic(T) :=
(do_rew_2 E T); auto*.
Tactic Notation "do_rew_2" "*" "<-" constr(E) tactic(T) :=
(do_rew_2 <- E T); auto*.
Tactic Notation "simpl" "*" :=
simpl; auto*.
Tactic Notation "simpls" "*" :=
simpls; auto*.
Tactic Notation "unsimpl" "*" constr(E) :=
unsimpl E; auto*.
Tactic Notation "unsimpl" "*" constr(E) "in" hyp(H) :=
unsimpl E in H; auto*.
Tactic Notation "split" "*" :=
split; auto*.
Tactic Notation "split3" "*" :=
split3; auto*.
Tactic Notation "split4" "*" :=
split4; auto*.
Tactic Notation "splits" "*" :=
splits; auto*.
Tactic Notation "esplit2" "*" :=
esplit2; auto*.
Tactic Notation "esplit3" "*" :=
esplit3; auto*.
Tactic Notation "esplit4" "*" :=
esplit4; auto*.
Tactic Notation "right" "*" :=
right; auto*.
Tactic Notation "left" "*" :=
left; auto*.
Tactic Notation "or_31" "*" :=
or_31; auto*.
Tactic Notation "or_32" "*" :=
or_32; auto*.
Tactic Notation "or_33" "*" :=
or_33; auto*.
Tactic Notation "destructi" "*" constr(H) :=
destructi H; auto*.
Tactic Notation "subst" "*" :=
subst; auto*.
Tactic Notation "use" constr(expr) :=
puts expr; auto*.
Tactic Notation "use" constr(expr1) constr(expr2) :=
puts expr1; use expr2.
Tactic Notation "use" constr(expr1) constr(expr2) constr(expr3) :=
puts expr1; use expr2 expr3.
Tactic Notation "exists" "*" constr(T1) :=
exists T1; auto*.
Tactic Notation "exists" "*" constr(T1) constr(T2) :=
exists T1 T2; auto*.
Tactic Notation "exists" "*" constr(T1) constr(T2) constr(T3) :=
exists T1 T2 T3.
Tactic Notation "exists" "*" constr(T1) constr(T2) constr(T3) constr(T4) :=
exists T1 T2 T3 T4.
Tactic Notation "forward" "*" constr(x) "as" simple_intropattern(H) :=
forward x; auto*.
Tactic Notation "forward" "*" constr(x) :=
forward x; auto*.
Tactic Notation "rewrite" "~" constr(H) :=
rewrite H; auto.
Tactic Notation "rewrite" "~" "<-" constr(H) :=
rewrite <- H; auto.
Tactic Notation "apply" "~" constr(H) :=
first [ apply H | eapply H ]; auto.
Tactic Notation "destructi" "~" constr(H) :=
destructi H; auto.
Tactic Notation "destruct" "~" constr(H) :=
destruct H; auto.
Tactic Notation "destruct" "~" constr(H) "as" simple_intropattern(I) :=
destruct H as I; auto.
Tactic Notation "destructi" "~" constr(H) "as" simple_intropattern(I) :=
destructi H as I; auto.
Tactic Notation "split" "~" :=
split; auto.
Tactic Notation "split3" "~" :=
split3; auto.
Tactic Notation "split4" "~" :=
split4; auto.
Tactic Notation "splits" "~" :=
splits; auto.
Tactic Notation "forward" "~" constr(x) "as" simple_intropattern(H) :=
forward x as H; auto.
Tactic Notation "forward" "~" constr(x) :=
forward x; auto.
Notation "'proj31' P" := (proj1 P) (at level 69).
Notation "'proj32' P" := (proj1 (proj2 P)) (at level 69).
Notation "'proj33' P" := (proj2 (proj2 P)) (at level 69).
Notation "'proj41' P" := (proj1 P) (at level 69).
Notation "'proj42' P" := (proj1 (proj2 P)) (at level 69).
Notation "'proj43' P" := (proj1 (proj2 (proj2 P))) (at level 69).
Notation "'proj44' P" := (proj2 (proj2 (proj2 P))) (at level 69).