Library lib.Tactics

Various useful tactics

version 1.0

Ltac elimer e := try exact e; let H := fresh "H" in (generalize e; intro H).

Use a fact, whose type is a non-dependent product. This is modus ponens in forward chaining

use H e when the type of e is A1 -> A2 -> ... -> An -> B will introduce the subgoals Ai and on the last subgoal will add the hypothesis H : B
Ltac use H e :=
match type of e with
  | ?A -> ?B =>
    let H' := fresh "H'" in
    (assert (H' : A);
       [idtac (* we'll return the subgoal A *) | use H (e H'); try clear H' ])
 | ?B => assert (H : B);
          [exact e | idtac ]

Like use H H, (use a hypothesis and re-use its name)
Ltac usehyp H :=
 let H' := fresh "H'" in
 (use H' H; clear H; try rename H' into H).


This is like rewrite H in *
Ltac rewriteall H :=
     let n := fresh "val" in
     (match type of H with
        ?E1 = ?E2 =>
            set (n:= E1) in * ;
            clearbody n;
            subst n


  • version 1.0. First version.

This page has been generated by coqdoc