• TacticExts

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)

> unfold sorted; fold sorted

   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 synax 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.