helm/coq-contribs/LAMBDA-TYPES/base_tactics.v

   1 (*#* #stop file *)
   2
   3       Tactic Definition XAuto := Auto with ltlc.
   4
   5       Tactic Definition XEAuto := EAuto with ltlc.
   6
   7       Tactic Definition XDEAuto d := EAuto d with ltlc.
   8
   9       Tactic Definition XElimUsing e v :=
  10          Try Intros until v; Elim v using e; Try Clear v.
  11
  12       Tactic Definition XElim v := Try Intros until v; Elim v; Try Clear v.
  13
  14       Tactic Definition XCase v := Try Intros until v; Case v; Try Clear v.
  15
  16       Tactic Definition XReplaceIn Z0 y1 y2 :=
  17          Cut y1=y2; [ Intros Z; Rewrite Z in Z0; Clear Z | XAuto ].
  18
  19       Theorem insert_eq: (S:Set; x:S; P:S->Prop; G:Prop)
  20                          ((y:S) (P y) -> y = x -> G) -> (P x) -> G.
  21       EAuto. Qed.
  22
  23       Tactic Definition InsertEq H y :=
  24          Pattern 1 y in H; Match Context With [ _: (?1 y) |- ? ] ->
  25          Apply insert_eq with x:=y P:=?1;
  26          [ Clear H; Intros until 1 | Pattern y; Apply H ].
  27
  28       Theorem unintro : (A:Set; a:A; P:A->Prop) ((x:A) (P x)) -> (P a).
  29       Auto.
  30       Qed.
  31
  32       Tactic Definition UnIntro Last H :=
  33          Move H after Last;
  34          Match Context With [ y: ?1 |- ?2 ] ->
  35             Apply (unintro ?1 y); Clear y.
  36
  37       Tactic Definition NonLinear :=
  38          Match Context With
  39             [ H: ?1 |- ? ] -> Cut ?1; [ Intros | XAuto ].
  40
  41       Tactic Definition XRewrite x :=
  42          Match Context With
  43             | [ H0: x = ? |- ? ] -> Try Rewrite H0
  44             | [ H0: ? = x |- ? ] -> Try Rewrite <- H0
  45             | _                  -> Idtac.