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

   1 (*#* #stop file *)
   2
   3 Require Arith.
   4
   5       Tactic Definition Arith0 x :=
   6          Replace (S x) with (plus (1) x); XAuto.
   7
   8       Tactic Definition Arith1 x :=
   9          Replace x with (plus x (0)); [XAuto | Auto with arith].
  10
  11       Tactic Definition Arith1In H x :=
  12          XReplaceIn H x '(plus x (0)).
  13
  14       Tactic Definition Arith2 x :=
  15          Replace x with (plus (0) x); XAuto.
  16
  17       Tactic Definition Arith3 x :=
  18          Replace (S x) with (S (plus (0) x)); XAuto.
  19
  20       Tactic Definition Arith3In H x :=
  21          XReplaceIn H '(S x) '(S (plus (0) x)).
  22
  23       Tactic Definition Arith4 x y :=
  24          Replace (S (plus x y)) with (plus (S x) y); XAuto.
  25
  26       Tactic Definition Arith4In H x y :=
  27          XReplaceIn H '(S (plus x y)) '(plus (S x) y).
  28
  29       Tactic Definition Arith4c x y :=
  30          Arith4 x y; Rewrite plus_sym.
  31
  32       Tactic Definition Arith5 x y :=
  33          Replace (S (plus x y)) with (plus x (S y)); Auto with arith.
  34
  35       Tactic Definition Arith5In H x y :=
  36          XReplaceIn H '(S (plus x y)) '(plus x (S y)); Auto with arith.
  37
  38       Tactic Definition Arith5' x y :=
  39          Replace (plus x (S y)) with (S (plus x y)); Auto with arith.
  40
  41       Tactic Definition Arith5'In H x y :=
  42          XReplaceIn H '(plus x (S y)) '(S (plus x y)); Auto with arith.
  43
  44       Tactic Definition Arith5'c x y :=
  45          Arith5' x y; Rewrite plus_sym.
  46
  47       Tactic Definition Arith6In H x y :=
  48          XReplaceIn H '(plus x (S y)) '(plus (1) (plus x y));
  49          [ Idtac | Simpl; Auto with arith ].
  50
  51       Tactic Definition Arith7 x :=
  52          Replace (S x) with (plus x (1));
  53          [ Idtac | Rewrite plus_sym; Auto with arith ].
  54
  55       Tactic Definition Arith7In H x :=
  56          XReplaceIn H '(S x) '(plus x (1)) ;
  57          [ Idtac | Rewrite plus_sym; Auto with arith ].
  58
  59       Tactic Definition Arith7' x :=
  60          Replace (plus x (1)) with (S x);
  61          [ Idtac | Rewrite plus_sym; Auto with arith ].
  62
  63       Tactic Definition Arith8 x y :=
  64          Replace x with (plus y (minus x y));
  65          [ Idtac | Auto with arith ].
  66
  67       Tactic Definition Arith8' x y :=
  68          Replace (plus y (minus x y)) with x;
  69          [ Idtac | Auto with arith ].
  70
  71       Tactic Definition Arith9'In H x :=
  72          XReplaceIn H '(S (plus x (0))) '(S x).
  73
  74       Tactic Definition Arith10 x :=
  75          Replace x with (minus (S x) (1));
  76          [ Idtac | Simpl; Rewrite <- minus_n_O; Auto with arith ].