# Recursion under binders

Using typeclasses, it is possible to recurse under binders. Here is an example of a tactic that recurses under binders to turn a proof of `A -> B -> C /\ D` into a proof of `A -> B -> C`:

```Class ret_and_left {T} (arg : T) {R} := make_recur_ret_and_left : R.
Ltac ret_and_left_helper f :=
let T := type of f in
lazymatch eval hnf in T with
| ?a /\ ?b => exact (proj1 f)
| ?T' -> _
=> exact (fun x' : T' => _ : ret_and_left (f x'))
end.
Hint Extern 0 (@ret_and_left _ ?f _) => ret_and_left_helper f : typeclass_instances.
Arguments ret_and_left / .
Goal forall A B : Prop, (A -> A -> A /\ B) -> True.
intros A B H.
pose (_ : ret_and_left H) as H'; simpl in H'.
(* fun x' x'0 : A => proj1 (H x' x'0) : A -> A -> A *)```

NB: In Coq >= 8.5, it will be possible to do this using tactics in terms rather than a separate typeclass for each tactic, and without having to `simpl` at the end:

```Ltac ret_and_left f :=
let tac := ret_and_left in
let T := type of f in
match eval hnf in T with
| ?a /\ ?b => exact (proj1 f)
| ?T' -> _ =>
let ret := constr:(fun x' : T' => let fx := f x' in
\$(tac fx)\$) in
let ret' := (eval cbv zeta in ret) in
exact ret'
end.
Goal forall A B : Prop, (A -> A -> A -> A /\ B) -> True.
intros A B H.
pose \$(ret_and_left H)\$.
(** [fun x' x'0 : A => proj1 (H x' x'0) : A -> A -> A] *)```

# Dependent case

`dcase` is a version of case that remembers the case you are in.

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

NB: This tactic has been integrated in Coq >= 8.1beta under the name `case_eq`

# Expand until

This tactic is useful when carefully unfolding definitions, for instance inductive ones. It also shows the use of tactic notation.

```Tactic Notation "expand" reference (t) "until" constr (s):=
let x:=fresh"x" in
(set (x:=s); unfold t; fold t;  unfold x).```

This has proved useful in a situation like `sorted (b :: a :: a0)` on which `unfold sorted; fold sorted` leads to:

```cmp b a = true /\
match a0 with
| nil => True
| a'' :: _ => cmp a a'' = true /\ sorted a0
end```

There's two levels expanded! Solution was "expand sorted until (a::a0)." (thanks roconnor)

# Clean duplicated hypothesis

This tactic removes redundant hypothesis from the context.

```Ltac exist_hyp t := match goal with
| H1:t |- _ => idtac
end.
Ltac clean_duplicated_hyps :=
repeat match goal with
| H:?X1 |- _ => clear H; exist_hyp X1
end.```

# Assert if necessary

This tactic assert a fact only if does not already exists in the context. This is intended to be used in more complex tactics.

```Ltac not_exist_hyp t := match goal with
| H1:t |- _ => fail 2
end || idtac.
Ltac assert_if_not_exist H :=
not_exist_hyp H;assert H.```

# RewriteAll

NB: A similar `rewrite_all` has been integrated in Coq >= 8.1beta (see file `theories/Init/Tactics.v`). Moreover, in the release following 8.1beta, the newly allowed syntax `rewrite ... in *` permits to define `rewrite_all` with a simple `repeat rewrite ... in *`.

Given an assumption `H : t1 = t2`, the tactic `rewrite_all H` replaces `t1` with `t2` both in goal and local context. We have to take care that `H` does not rewrite itself, for then we'd get `H : t2 = t2`, and a loop is entered.

```Ltac rewrite_in_cxt H :=
let T := type of H in
match T with
| ?t1 = ?t2 =>
repeat
(
generalize H; clear H;
match goal with
| id : context[t1] |- _ =>
intro H; rewrite H in id
end
)
end.
Ltac rewrite_all H :=
rewrite_in_cxt H; rewrite H.
Ltac replace_in_cxt t1 t2 :=
let H := fresh "H" in
(cut (t1 = t2); [ intro H; rewrite_in_cxt H; clear H | idtac ]).
Ltac replace_all t1 t2 :=
let H := fresh "H" in
(cut (t1 = t2); [ intro H; rewrite_all H; clear H | idtac ]).```

# RewriteAll, expert version

Given an assumption `H : t1 = t2`, the tactic `rewrite_all H` replaces `t1` with `t2` both in goal and local context. We have to take care that `H` does not rewrite itself, for then we'd get `H : t2 = t2`, and a loop is entered; this version generates a smarter proof term than the previous one.

```Ltac rewrite_all H :=
match type of H with
| ?t1 = ?t2 =>
let rec aux H :=
match goal with
| id : context [t1] |- _ =>
match type of id with
| t1 = t2 => fail 1
| _ => generalize id;clear id; try aux H; intro id
end
| _ => try rewrite H
end in
aux H
end.```

# Decide Equality

Coq's decide equality should be more accepting. It ought to behave more like the following.

```Ltac decideEquality :=
match goal with
| |- forall x y, {x = y}+{~x=y} => decide equality
| |- {?a=?b}+{~?a=?b} => decide equality a b
| |- {~?a=?b}+{?a=?b} => cut ({a=b}+{~a=b});[tauto | decide equality a b]
end.```
##### Clone this wiki locally
You can’t perform that action at this time.
Press h to open a hovercard with more details.