Library Coq.Init.Tactics
A tactic for proof by contradiction. With contradict H,
- H:~A |- B gives |- A
- H:~A |- ~B gives H: B |- A
- H: A |- B gives |- ~A
- H: A |- ~B gives H: B |- ~A
- H:False leads to a resolved subgoal.
Moreover, negations may be in unfolded forms,
and A or B may live in Type
Ltac contradict H :=
let save tac H :=
let x:=fresh
in intro x;
tac H;
rename x into H
in
let negpos H :=
case H;
clear H
in
let negneg H :=
save negpos H
in
let pospos H :=
let A :=
type of H in (
elimtype False;
revert H;
try fold (~A))
in
let posneg H :=
save pospos H
in
let neg H :=
match goal with
| |- (~_) =>
negneg H
| |- (
_->False) =>
negneg H
| |-
_ =>
negpos H
end in
let pos H :=
match goal with
| |- (~_) =>
posneg H
| |- (
_->False) =>
posneg H
| |-
_ =>
pospos H
end in
match type of H with
| (~_) =>
neg H
| (
_->False) =>
neg H
|
_ => (
elim H;
fail) ||
pos H
end.
Ltac swap H :=
idtac "swap is OBSOLETE: use contradict instead.";
intro;
apply H;
clear H.
Ltac absurd_hyp H :=
idtac "absurd_hyp is OBSOLETE: use contradict instead.";
let T :=
type of H in
absurd T.
Ltac false_hyp H G :=
let T :=
type of H in absurd T; [
apply G |
assumption ].
Ltac case_eq x :=
generalize (
refl_equal x);
pattern x at -1;
case x.
Tactic Notation "destruct_with_eqn"
constr(
x) :=
destruct x as []
_eqn.
Tactic Notation "destruct_with_eqn"
ident(
n) :=
try intros until n;
destruct n as []
_eqn.
Tactic Notation "destruct_with_eqn" ":"
ident(
H)
constr(
x) :=
destruct x as []
_eqn:H.
Tactic Notation "destruct_with_eqn" ":"
ident(
H)
ident(
n) :=
try intros until n;
destruct n as []
_eqn:H.
Tactic Notation "rewrite_all"
constr(
eq) :=
repeat rewrite eq in *.
Tactic Notation "rewrite_all" "<-"
constr(
eq) :=
repeat rewrite <-
eq in *.
Tactics for applying equivalences.
The following code provides tactics "apply -> t", "apply <- t",
"apply -> t in H" and "apply <- t in H". Here t is a term whose type
consists of nested dependent and nondependent products with an
equivalence A <-> B as the conclusion. The tactics with "->" in their
names apply A -> B while those with "<-" in the name apply B -> A.
Ltac find_equiv H :=
let T := type of H in
lazymatch T with
| ?A -> ?B =>
let H1 := fresh in
let H2 := fresh in
cut A;
[intro H1; pose proof (H H1) as H2; clear H H1;
rename H2 into H; find_equiv H |
clear H]
| forall x : ?t, _ =>
let a := fresh "a" with
H1 := fresh "H" in
evar (a : t); pose proof (H a) as H1; unfold a in H1;
clear a; clear H; rename H1 into H; find_equiv H
| ?A <-> ?B => idtac
| _ => fail "The given statement does not seem to end with an equivalence."
end.
Ltac bapply lemma todo :=
let H := fresh in
pose proof lemma as H;
find_equiv H; [todo H; clear H | .. ].
Tactic Notation "apply" "->" constr(lemma) :=
bapply lemma ltac:(fun H => destruct H as [H _]; apply H).
Tactic Notation "apply" "<-" constr(lemma) :=
bapply lemma ltac:(fun H => destruct H as [_ H]; apply H).
Tactic Notation "apply" "->" constr(lemma) "in" ident(J) :=
bapply lemma ltac:(fun H => destruct H as [H _]; apply H in J).
Tactic Notation "apply" "<-" constr(lemma) "in" ident(J) :=
bapply lemma ltac:(fun H => destruct H as [_ H]; apply H in J).
An experimental tactic simpler than auto that is useful for ending
proofs "in one step"
Ltac easy :=
let rec use_hyp H :=
match type of H with
| _ /\ _ => exact H || destruct_hyp H
| _ => try solve [inversion H]
end
with do_intro := let H := fresh in intro H; use_hyp H
with destruct_hyp H := case H; clear H; do_intro; do_intro in
let rec use_hyps :=
match goal with
| H : _ /\ _ |- _ => exact H || (destruct_hyp H; use_hyps)
| H : _ |- _ => solve [inversion H]
| _ => idtac
end in
let rec do_atom :=
solve [reflexivity | symmetry; trivial] ||
contradiction ||
(split; do_atom)
with do_ccl := trivial; repeat do_intro; do_atom in
(use_hyps; do_ccl) || fail "Cannot solve this goal".
Tactic Notation "now" tactic(t) := t; easy.
A tactic to document or check what is proved at some point of a script
Ltac now_show c := change c.
Clear an hypothesis and its dependencies
Tactic Notation "clear" "dependent" hyp(h) :=
let rec depclear h :=
clear h ||
match goal with
| H : context [ h ] |- _ => depclear H; depclear h
end ||
fail "hypothesis to clear is used in the conclusion (maybe indirectly)"
in depclear h.
Revert an hypothesis and its dependencies :
this is actually generalize dependent...
Tactic Notation "revert" "dependent" hyp(h) :=
generalize dependent h.