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

   1 (*#* #stop file *)
   2
   3 Require Arith.
   4 Require base_tactics.
   5
   6 (* eq ***********************************************************************)
   7
   8 Hint eq : ltlc := Constructors eq.
   9
  10 Hint f1N : ltlc := Resolve (f_equal nat).
  11
  12 Hint f2NN : ltlc := Resolve (f_equal2 nat nat).
  13
  14 Hints Resolve sym_equal : ltlc.
  15
  16 Hints Resolve plus_sym plus_n_Sm plus_assoc_r simpl_plus_l : ltlc.
  17
  18 Hints Resolve minus_n_O : ltlc.
  19
  20 (* le ***********************************************************************)
  21
  22 Hint le : ltlc := Constructors le.
  23
  24 Hints Resolve le_O_n le_n_S le_S_n le_trans : ltlc.
  25
  26 Hints Resolve lt_le_S : ltlc.
  27
  28 Hints Resolve le_plus_plus le_plus_trans le_plus_l le_plus_r : ltlc.
  29
  30 (* lt ***********************************************************************)
  31
  32 Hints Resolve lt_trans : ltlc.
  33
  34 Hints Resolve lt_le_trans le_lt_n_Sm : ltlc.
  35
  36 Hints Resolve lt_reg_r lt_le_plus_plus le_lt_plus_plus : ltlc.
  37
  38 (* not **********************************************************************)
  39
  40 Hints Resolve sym_not_equal : ltlc.
  41
  42 (* missing in the standard library ******************************************)
  43
  44       Theorem simpl_plus_r: (n,m,p:?) (plus m n) = (plus p n) -> m = p.
  45       Intros.
  46       Apply (simpl_plus_l n).
  47       Rewrite plus_sym.
  48       Rewrite H; XAuto.
  49       Qed.
  50
  51       Theorem minus_plus_r: (m,n:?) (minus (plus m n) n) = m.
  52       Intros.
  53       Rewrite plus_sym.
  54       Apply minus_plus.
  55       Qed.
  56
  57       Theorem plus_permute_2_in_3: (x,y,z:?) (plus (plus x y) z) = (plus (plus x z) y).
  58       Intros.
  59       Rewrite plus_assoc_r.
  60       Rewrite (plus_sym y z).
  61       Rewrite <- plus_assoc_r; XAuto.
  62       Qed.
  63
  64       Theorem plus_permute_2_in_3_assoc: (n,h,k:?) (plus (plus n h) k) = (plus n (plus k h)).
  65       Intros.
  66       Rewrite plus_permute_2_in_3; Rewrite plus_assoc_l; XAuto.
  67       Qed.
  68
  69       Theorem plus_O: (x,y:?) (plus x y) = (0) -> x = (O) /\ y = (O).
  70       XElim x; [ XAuto | Intros; Inversion H0 ].
  71       Qed.
  72
  73       Theorem minus_Sx_SO: (x:?) (minus (S x) (1)) = x.
  74       Intros; Simpl; Rewrite <- minus_n_O; XAuto.
  75       Qed.
  76
  77       Theorem eq_nat_dec: (i,j:nat) ~i=j \/ i=j.
  78       XElim i; XElim j; Intros; XAuto.
  79       Elim (H n0); XAuto.
  80       Qed.
  81
  82       Theorem neq_eq_e: (i,j:nat; P:Prop) (~i=j -> P) -> (i=j -> P) -> P.
  83       Intros.
  84       Pose (eq_nat_dec i j).
  85       XElim o; XAuto.
  86       Qed.
  87
  88       Theorem le_false: (m,n:?; P:Prop) (le m n) -> (le (S n) m) -> P.
  89       XElim m.
  90 (* case 1 : m = 0 *)
  91       Intros; Inversion H0.
  92 (* case 2 : m > 0 *)
  93       XElim n0; Intros.
  94 (* case 2.1 : n = 0 *)
  95       Inversion H0.
  96 (* case 2.2 : n > 0 *)
  97       Simpl in H1.
  98       Apply (H n0); XAuto.
  99       Qed.
 100
 101       Theorem le_plus_minus_sym: (n,m:?) (le n m) -> m = (plus (minus m n) n).
 102       Intros.
 103       Rewrite plus_sym; Apply le_plus_minus; XAuto.
 104       Qed.
 105
 106       Theorem le_minus_minus: (x,y:?) (le x y) -> (z:?) (le y z) ->
 107                               (le (minus y x) (minus z x)).
 108       Intros.
 109       EApply simpl_le_plus_l.
 110       Rewrite le_plus_minus_r; [ Idtac | XAuto ].
 111       Rewrite le_plus_minus_r; XEAuto.
 112       Qed.
 113
 114       Theorem le_minus_plus: (z,x:?) (le z x) -> (y:?)
 115                              (minus (plus x y) z) = (plus (minus x z) y).
 116       XElim z.
 117 (* case 1 : z = 0 *)
 118       Intros x H; Inversion H; XAuto.
 119 (* case 2 : z > 0 *)
 120       Intros z; XElim x; Intros.
 121 (* case 2.1 : x = 0 *)
 122       Inversion H0.
 123 (* case 2.2 : x > 0 *)
 124       Simpl; XAuto.
 125       Qed.
 126
 127       Theorem le_minus: (x,z,y:?) (le (plus x y) z) -> (le x (minus z y)).
 128       Intros.
 129       Rewrite <- (minus_plus_r x y); XAuto.
 130       Apply le_minus_minus; XAuto.
 131       Qed.
 132
 133       Theorem le_trans_plus_r: (x,y,z:?) (le (plus x y) z) -> (le y z).
 134       Intros.
 135       EApply le_trans; [ EApply le_plus_r | Idtac ]; XEAuto.
 136       Qed.
 137
 138       Theorem le_gen_S: (m,x:?) (le (S m) x) ->
 139                         (EX n | x = (S n) & (le m n)).
 140       Intros; Inversion H; XEAuto.
 141       Qed.
 142
 143       Theorem lt_x_plus_x_Sy: (x,y:?) (lt x (plus x (S y))).
 144       Intros; Rewrite plus_sym; Simpl; XAuto.
 145       Qed.
 146
 147       Theorem simpl_lt_plus_r: (p,n,m:?) (lt (plus n p) (plus m p)) -> (lt n m).
 148       Intros.
 149       EApply simpl_lt_plus_l.
 150       Rewrite plus_sym in H; Rewrite (plus_sym m p) in H; Apply H.
 151       Qed.
 152
 153       Theorem minus_x_Sy: (x,y:?) (lt y x) ->
 154                           (minus x y) = (S (minus x (S y))).
 155       XElim x.
 156 (* case 1 : x = 0 *)
 157       Intros; Inversion H.
 158 (* case 2 : x > 0 *)
 159       XElim y; Intros; Simpl.
 160 (* case 2.1 : y = 0 *)
 161       Rewrite <- minus_n_O; XAuto.
 162 (* case 2.2 : y > 0 *)
 163       Cut (lt n0 n); XAuto.
 164       Qed.
 165
 166       Theorem lt_plus_minus: (x,y:?) (lt x y) ->
 167                              y = (S (plus x (minus y (S x)))).
 168       Intros.
 169       Apply (le_plus_minus (S x) y); XAuto.
 170       Qed.
 171
 172       Theorem lt_plus_minus_r: (x,y:?) (lt x y) ->
 173                                y = (S (plus (minus y (S x)) x)).
 174       Intros.
 175       Rewrite plus_sym; Apply lt_plus_minus; XAuto.
 176       Qed.
 177
 178       Theorem minus_x_SO: (x:?) (lt (0) x) -> x = (S (minus x (1))).
 179       Intros.
 180       Rewrite <- minus_x_Sy; [ Rewrite <- minus_n_O; XEAuto | XEAuto ].
 181       Qed.
 182
 183       Theorem lt_le_minus: (x,y:?) (lt x y) -> (le x (minus y (1))).
 184       Intros; Apply le_minus; Rewrite plus_sym; Simpl; XAuto.
 185       Qed.
 186
 187       Theorem lt_le_e: (n,d:?; P:Prop)
 188                        ((lt n d) -> P) -> ((le d n) -> P) -> P.
 189       Intros.
 190       Cut (le d n) \/ (lt n d); [ Intros H1; XElim H1; XAuto | Apply le_or_lt ].
 191       Qed.
 192
 193       Theorem lt_eq_e: (x,y:?; P:Prop) ((lt x y) -> P) ->
 194                        (x = y -> P) -> (le x y) -> P.
 195       Intros.
 196       LApply (le_lt_or_eq x y); [ Clear H1; Intros H1 | XAuto ].
 197       XElim H1; XAuto.
 198       Qed.
 199
 200       Theorem lt_eq_gt_e: (x,y:?; P:Prop) ((lt x y) -> P) ->
 201                           (x = y -> P) -> ((lt y x) -> P) -> P.
 202       Intros.
 203       Apply (lt_le_e x y); [ XAuto | Intros ].
 204       Apply (lt_eq_e y x); XAuto.
 205       Qed.
 206
 207       Theorem lt_gen_S': (x,n:?) (lt x (S n)) ->
 208                          x = (0) \/ (EX m | x = (S m) & (lt m n)).
 209       XElim x; XEAuto.
 210       Qed.
 211
 212 Hints Resolve le_lt_trans : ltlc.
 213
 214 Hints Resolve simpl_plus_r minus_plus_r minus_x_Sy
 215               plus_permute_2_in_3 plus_permute_2_in_3_assoc : ltlc.
 216
 217 Hints Resolve le_minus_minus le_minus_plus le_minus le_trans_plus_r : ltlc.
 218
 219 Hints Resolve lt_x_plus_x_Sy simpl_lt_plus_r lt_le_minus lt_plus_minus
 220               lt_plus_minus_r : ltlc.
 221
 222       Theorem lt_neq: (x,y:?) (lt x y) -> ~x=y.
 223       Unfold not; Intros; Rewrite H0 in H; Clear H0 x.
 224       LApply (lt_n_n y); XAuto.
 225       Qed.
 226
 227 Hints Resolve lt_neq : ltlc.
 228
 229       Theorem arith0: (h2,d2,n:?) (le (plus d2 h2) n) ->
 230                       (h1:?) (le (plus d2 h1) (minus (plus n h1) h2)).
 231       Intros.
 232       Rewrite <- (minus_plus h2 (plus d2 h1)).
 233       Apply le_minus_minus; [ XAuto | Idtac ].
 234       Rewrite plus_assoc_l; Rewrite (plus_sym h2 d2); XAuto.
 235       Qed.
 236
 237 Hints Resolve arith0 : ltlc.
 238
 239       Tactic Definition EqFalse :=
 240          Match Context With
 241             [ H: ~?1=?1 |- ? ] ->
 242                LApply H; [ Clear H; Intros H; Inversion H | XAuto ].
 243
 244       Tactic Definition PlusO :=
 245          Match Context With
 246             | [ H: (plus ?0 ?1) = (0) |- ? ] ->
 247                LApply (plus_O ?0 ?1); [ Clear H; Intros H | XAuto ];
 248                XElim H; Intros.
 249
 250       Tactic Definition SymEqual :=
 251          Match Context With
 252             | [ H: ?1 = ?2 |- ? ] ->
 253                Cut ?2 = ?1; [ Clear H; Intros H | Apply sym_equal; XAuto ].
 254
 255       Tactic Definition LeLtGen :=
 256          Match Context With
 257             | [ H: (le (S ?1) ?2) |- ? ] ->
 258                LApply (le_gen_S ?1 ?2); [ Clear H; Intros H | XAuto ];
 259                XElim H; Intros
 260             | [ H: (lt ?1 (S ?2)) |- ? ] ->
 261                LApply (lt_gen_S' ?1 ?2); [ Clear H; Intros H | XAuto ];
 262                XElim H; [ Intros | Intros H; XElim H; Intros ].