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

   1 Require Arith.
   2 Require base_tactics.
   3 Require base_hints.
   4
   5 (*#* #stop file *)
   6
   7       Fixpoint blt [m,n: nat] : bool := Cases n m of
   8          | (0) m       => false
   9          | (S n) (0)   => true
  10          | (S n) (S m) => (blt m n)
  11       end.
  12
  13    Section blt_props. (******************************************************)
  14
  15       Theorem lt_blt: (x,y:?) (lt y x) -> (blt y x) = true.
  16       XElim x; [ Intros; Inversion H | XElim y; Simpl; XAuto ].
  17       Qed.
  18
  19       Theorem le_bge: (x,y:?) (le x y) -> (blt y x) = false.
  20       XElim x; [ XAuto | XElim y; Intros; [ Inversion H0 | Simpl; XAuto ] ].
  21       Qed.
  22
  23       Theorem blt_lt: (x,y:?) (blt y x) = true -> (lt y x).
  24       XElim x; [ Intros; Inversion H | XElim y; Simpl; XAuto ].
  25       Qed.
  26
  27       Theorem bge_le: (x,y:?) (blt y x) = false -> (le x y).
  28       XElim x; [ XAuto | XElim y; Intros; [ Inversion H0 | Simpl; XAuto ] ].
  29       Qed.
  30
  31    End blt_props.
  32
  33       Hints Resolve lt_blt le_bge : ltlc.