(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* 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. (* Transforming a negative goal [ H:~A |- ~B ] into a positive one [ B |- A ]*) 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 := idtac "absurd_hyp is OBSOLETE: use contradict instead."; 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 := let T := type of H in absurd T; [ apply G | assumption ]. (* A case with no loss of information. *) Ltac case_eq x := generalize (refl_equal x); pattern x at -1; case x. (* Rewriting in all hypothesis several times everywhere *) 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. *) (* The idea of the tactics is to first provide a term in the context whose type is the implication (in one of the directions), and then apply it. The first idea is to produce a statement "forall ..., A -> B" (call this type T) and then do "assert (H : T)" for a fresh H. Thus, T can be proved from the original equivalence and then used to perform the application. However, currently in Ltac it is difficult to produce such T from the original formula. Therefore, we first pose the original equivalence as H. If the type of H is a dependent product, we create an existential variable and apply H to this variable. If the type of H has the form C -> D, then we do a cut on C. Once we eliminate all products, we split (i.e., destruct) the conjunction into two parts and apply the relevant one. *) 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.