summaryrefslogtreecommitdiff
path: root/theories/Init/Tactics.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /theories/Init/Tactics.v
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'theories/Init/Tactics.v')
-rw-r--r--theories/Init/Tactics.v85
1 files changed, 64 insertions, 21 deletions
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 48b4568d..3e860fd4 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -6,45 +6,52 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Tactics.v 13198 2010-06-25 22:36:20Z letouzey $ i*)
+(*i $Id$ i*)
Require Import Notations.
Require Import Logic.
+Require Import Specif.
(** * Useful tactics *)
-(** A tactic for proof by contradiction. With contradict H,
+(** Ex falso quodlibet : a tactic for proving False instead of the current goal.
+ This is just a nicer name for tactics such as [elimtype False]
+ and other [cut False]. *)
+
+Ltac exfalso := elimtype False.
+
+(** 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,
+ 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
+ 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))
+ let pospos H :=
+ let A := type of H in (exfalso; revert H; try fold (~A))
in
let posneg H := save pospos H
- in
- let neg H := match goal with
+ in
+ let neg H := match goal with
| |- (~_) => negneg H
| |- (_->False) => negneg H
| |- _ => negpos H
- end in
- let pos H := match goal with
+ end in
+ let pos H := match goal with
| |- (~_) => posneg H
| |- (_->False) => posneg H
| |- _ => pospos H
end in
- match type of H with
+ match type of H with
| (~_) => neg H
| (_->False) => neg H
| _ => (elim H;fail) || pos H
@@ -52,20 +59,20 @@ Ltac contradict H :=
(* Transforming a negative goal [ H:~A |- ~B ] into a positive one [ B |- A ]*)
-Ltac swap H :=
+Ltac swap H :=
idtac "swap is OBSOLETE: use contradict instead.";
intro; apply H; clear H.
(* To contradict an hypothesis without copying its type. *)
-Ltac absurd_hyp H :=
+Ltac absurd_hyp H :=
idtac "absurd_hyp is OBSOLETE: use contradict instead.";
- let T := type of H in
+ let T := type of H in
absurd T.
(* A useful complement to contradict. Here H:A while G allows to conclude ~A *)
-Ltac false_hyp H G :=
+Ltac false_hyp H G :=
let T := type of H in absurd T; [ apply G | assumption ].
(* A case with no loss of information. *)
@@ -76,13 +83,21 @@ 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) :=
+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) :=
+Tactic Notation "destruct_with_eqn" ":" ident(H) ident(n) :=
try intros until n; destruct n as []_eqn:H.
+(** Break every hypothesis of a certain type *)
+
+Ltac destruct_all t :=
+ match goal with
+ | x : t |- _ => destruct x; destruct_all t
+ | _ => idtac
+ end.
+
(* Rewriting in all hypothesis several times everywhere *)
Tactic Notation "rewrite_all" constr(eq) := repeat rewrite eq in *.
@@ -148,7 +163,7 @@ 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
@@ -167,14 +182,42 @@ Ltac easy :=
solve [reflexivity | symmetry; trivial] ||
contradiction ||
(split; do_atom)
- with do_ccl := trivial; repeat do_intro; do_atom in
+ with do_ccl := trivial with eq_true; 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.
+(** Support for rewriting decidability statements *)
+
+Set Implicit Arguments.
+
+Lemma decide_left : forall (C:Prop) (decide:{C}+{~C}),
+ C -> forall P:{C}+{~C}->Prop, (forall H:C, P (left _ H)) -> P decide.
+Proof.
+intros; destruct decide. apply H0. contradiction.
+Qed.
+
+Lemma decide_right : forall (C:Prop) (decide:{C}+{~C}),
+ ~C -> forall P:{C}+{~C}->Prop, (forall H:~C, P (right _ H)) -> P decide.
+Proof.
+intros; destruct decide. contradiction. apply H0.
+Qed.
+
+Tactic Notation "decide" constr(lemma) "with" constr(H) :=
+ let try_to_merge_hyps H :=
+ try (clear H; intro H) ||
+ (let H' := fresh H "bis" in intro H'; try clear H') ||
+ (let H' := fresh in intro H'; try clear H') in
+ match type of H with
+ | ~ ?C => apply (decide_right lemma H); try_to_merge_hyps H
+ | ?C -> False => apply (decide_right lemma H); try_to_merge_hyps H
+ | _ => apply (decide_left lemma H); try_to_merge_hyps H
+ end.
+
(** Clear an hypothesis and its dependencies *)
Tactic Notation "clear" "dependent" hyp(h) :=