diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown
--- a/CHANGELOG.markdown
+++ b/CHANGELOG.markdown
@@ -1,7 +1,13 @@
+1.0.0
+-----
+* use extended-reals package for representing endpoints
+* add (experimental) comparison operators that produce witnesses:
+  `(<??)`, `(<=??)`, `(==??)`, `(>=??)`, `(>??)`
+
 0.6.0
 -----
-* add hulls, intersections :: (Num r, Ord r) => [Interval r] -> Interval r
-* fix a bug of (<=?) operator
+* add `hulls, intersections :: (Num r, Ord r) => [Interval r] -> Interval r`
+* fix a bug of `(<=?)` operator
 
 0.5.0
 -----
@@ -9,4 +15,4 @@
 
 0.4.0
 -----
-* add simplestRationalWithin :: RealFrac r => Interval r -> Maybe Rational
+* add `simplestRationalWithin :: RealFrac r => Interval r -> Maybe Rational`
diff --git a/data-interval.cabal b/data-interval.cabal
--- a/data-interval.cabal
+++ b/data-interval.cabal
@@ -1,5 +1,5 @@
 Name:		data-interval
-Version:	0.6.0
+Version:	1.0.0
 License:	BSD3
 License-File:	COPYING
 Author:		Masahiro Sakai (masahiro.sakai@gmail.com)
@@ -26,7 +26,7 @@
 Library
   Hs-source-dirs: src
   Build-Depends:
-     base >=4 && <5, lattices >=1.2.1.1, deepseq, hashable >=1.1.2.5 && <1.3
+     base >=4 && <5, lattices >=1.2.1.1, deepseq, hashable >=1.1.2.5 && <1.3, extended-reals >=0.1 && <1.0
   Default-Language: Haskell2010
   Other-Extensions:
      ScopedTypeVariables
diff --git a/src/Data/Interval.hs b/src/Data/Interval.hs
--- a/src/Data/Interval.hs
+++ b/src/Data/Interval.hs
@@ -1,5 +1,5 @@
 {-# OPTIONS_GHC -Wall #-}
-{-# LANGUAGE ScopedTypeVariables, DeriveDataTypeable, DoAndIfThenElse #-}
+{-# LANGUAGE ScopedTypeVariables, DeriveDataTypeable #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Interval
@@ -25,7 +25,8 @@
   (
   -- * Interval type
     Interval
-  , EndPoint (..)
+  , Extended (..)
+  , EndPoint
 
   -- * Construction
   , interval
@@ -49,10 +50,13 @@
   , upperBound'
   , width
 
-  -- * Comparison
+  -- * Comparison operators
   , (<!), (<=!), (==!), (>=!), (>!)
   , (<?), (<=?), (==?), (>=?), (>?)
 
+  -- * Comparison operators that produce witnesses (experimental)
+  , (<??), (<=??), (==??), (>=??), (>??)
+
   -- * Combine
   , intersection
   , intersections
@@ -69,12 +73,12 @@
 import Control.Exception (assert)
 import Control.Monad hiding (join)
 import Data.Data
+import Data.ExtendedReal
 import Data.Hashable
 import Data.List hiding (null)
 import Data.Maybe
 import Data.Monoid
 import Data.Ratio
-import Data.Typeable
 import Prelude hiding (null)
 
 -- | Interval
@@ -388,6 +392,23 @@
     lb_a = lowerBound a
     ub_b = upperBound b
 
+-- | Does there exist an @x@ in @X@, @y@ in @Y@ such that @x '<' y@?
+(<??) :: (Real r, Fractional r) => Interval r -> Interval r -> Maybe (r,r)
+a <?? b = do
+  guard $ lowerBound a < upperBound b
+  let c = intersection a b
+  case pickup c of
+    Nothing -> do
+      x <- pickup a
+      y <- pickup b
+      return (x,y)
+    Just z -> do
+      let x:y:_ = take 2 $
+                    maybeToList (pickup (intersection a (NegInf <..< Finite z))) ++
+                    [z] ++
+                    maybeToList (pickup (intersection b (Finite z <..< PosInf)))
+      return (x,y)
+
 -- | Does there exist an @x@ in @X@, @y@ in @Y@ such that @x '<=' y@?
 (<=?) :: Real r => Interval r -> Interval r -> Bool
 a <=? b　=
@@ -403,10 +424,27 @@
     (lb_a, in1) = lowerBound' a
     (ub_b, in2) = upperBound' b
 
+-- | Does there exist an @x@ in @X@, @y@ in @Y@ such that @x '<=' y@?
+(<=??) :: (Real r, Fractional r) => Interval r -> Interval r -> Maybe (r,r)
+a <=?? b　= do
+  case pickup (intersection a b) of
+    Just x -> return (x,x)
+    Nothing -> do
+      guard $ upperBound a <= lowerBound b
+      x <- pickup a
+      y <- pickup b
+      return (x,y)
+
 -- | Does there exist an @x@ in @X@, @y@ in @Y@ such that @x '==' y@?
 (==?) :: Real r => Interval r -> Interval r -> Bool
 a ==? b = not $ null $ intersection a b
 
+-- | Does there exist an @x@ in @X@, @y@ in @Y@ such that @x '==' y@?
+(==??) :: (Real r, Fractional r) => Interval r -> Interval r -> Maybe (r,r)
+a ==?? b = do
+  x <- pickup (intersection a b)
+  return (x,x)
+
 -- | Does there exist an @x@ in @X@, @y@ in @Y@ such that @x '>=' y@?
 (>=?) :: Real r => Interval r -> Interval r -> Bool
 (>=?) = flip (<=?)
@@ -415,6 +453,14 @@
 (>?) :: Real r => Interval r -> Interval r -> Bool
 (>?) = flip (<?)
 
+-- | Does there exist an @x@ in @X@, @y@ in @Y@ such that @x '>=' y@?
+(>=??) :: (Real r, Fractional r) => Interval r -> Interval r -> Maybe (r,r)
+(>=??) = flip (<=??)
+
+-- | Does there exist an @x@ in @X@, @y@ in @Y@ such that @x '>' y@?
+(>??) :: (Real r, Fractional r) => Interval r -> Interval r -> Maybe (r,r)
+(>??) = flip (<??)
+
 appPrec, appPrec1 :: Int
 appPrec = 10
 appPrec1 = appPrec + 1
@@ -447,15 +493,15 @@
 
   abs x = ((x `intersection` nonneg) `hull` (negate x `intersection` nonneg))
     where
-      nonneg = Finite 0 <=..< PosInf
+      nonneg = 0 <=..< PosInf
 
   signum x = zero `hull` pos `hull` neg
     where
       zero = if member 0 x then singleton 0 else empty
-      pos = if null $ (Finite 0 <..< PosInf) `intersection` x
+      pos = if null $ (0 <..< PosInf) `intersection` x
             then empty
             else singleton 1
-      neg = if null $ (NegInf <..< Finite 0) `intersection` x
+      neg = if null $ (NegInf <..< 0) `intersection` x
             then empty
             else singleton (-1)
 
@@ -481,38 +527,7 @@
 cmpLB (x1,in1) (x2,in2) = compare x1 x2 `mappend` flip compare in1 in2
 
 -- | Endpoints of intervals
-data EndPoint r
-  = NegInf    -- ^ negative infinity (-∞)
-  | Finite !r -- ^ finite value
-  | PosInf    -- ^ positive infinity (+∞)
-  deriving (Ord, Eq, Show, Read, Typeable, Data)
-
-instance Bounded (EndPoint r) where
-  minBound = NegInf
-  maxBound = PosInf
-
-instance Functor EndPoint where
-  fmap _ NegInf = NegInf
-  fmap f (Finite x) = Finite (f x)
-  fmap _ PosInf = PosInf
-
-instance NFData r => NFData (EndPoint r) where
-  rnf (Finite x) = rnf x
-  rnf _ = ()
-
-instance Hashable r => Hashable (EndPoint r) where
-  hashWithSalt s NegInf     = s `hashWithSalt` (0::Int)
-  hashWithSalt s (Finite x) = s `hashWithSalt` (1::Int) `hashWithSalt` x
-  hashWithSalt s PosInf     = s `hashWithSalt` (2::Int)
-
-isFinite :: EndPoint r -> Bool
-isFinite (Finite _) = True
-isFinite _ = False
-
-negateEndPoint :: Num r => EndPoint r -> EndPoint r
-negateEndPoint NegInf = PosInf
-negateEndPoint PosInf = NegInf
-negateEndPoint (Finite x) = Finite (negate x)
+type EndPoint r = Extended r
 
 scaleInf' :: (Num r, Ord r) => r -> (EndPoint r, Bool) -> (EndPoint r, Bool)
 scaleInf' a (x1, in1) = (scaleEndPoint a x1, in1)
@@ -520,7 +535,7 @@
 scaleEndPoint :: (Num r, Ord r) => r -> EndPoint r -> EndPoint r
 scaleEndPoint a inf =
   case a `compare` 0 of
-    EQ -> Finite 0
+    EQ -> 0
     GT ->
       case inf of
         NegInf   -> NegInf
@@ -533,36 +548,14 @@
         PosInf   -> NegInf
 
 mulInf' :: (Num r, Ord r) => (EndPoint r, Bool) -> (EndPoint r, Bool) -> (EndPoint r, Bool)
-mulInf' (Finite 0, True) _ = (Finite 0, True)
-mulInf' _ (Finite 0, True) = (Finite 0, True)
-mulInf' (x1,in1) (x2,in2) = (mulEndPoint x1 x2, in1 && in2)
-
-mulEndPoint :: (Num r, Ord r) => EndPoint r -> EndPoint r -> EndPoint r
-mulEndPoint (Finite x1) (Finite x2) = Finite (x1 * x2)
-mulEndPoint inf (Finite x2) =
-  case compare x2 0 of
-    EQ -> Finite 0
-    GT -> inf
-    LT -> negateEndPoint inf
-mulEndPoint (Finite x1) inf =
-  case compare x1 0 of
-    EQ -> Finite 0
-    GT -> inf
-    LT -> negateEndPoint inf
-mulEndPoint PosInf PosInf = PosInf
-mulEndPoint PosInf NegInf = NegInf
-mulEndPoint NegInf PosInf = NegInf
-mulEndPoint NegInf NegInf = PosInf
+mulInf' (0, True) _ = (0, True)
+mulInf' _ (0, True) = (0, True)
+mulInf' (x1,in1) (x2,in2) = (x1*x2, in1 && in2)
 
 recipLB :: (Fractional r, Ord r) => (EndPoint r, Bool) -> (EndPoint r, Bool)
-recipLB (Finite 0, _) = (PosInf, False)
-recipLB (x1, in1) = (recipEndPoint x1, in1)
+recipLB (0, _) = (PosInf, False)
+recipLB (x1, in1) = (recip x1, in1)
 
 recipUB :: (Fractional r, Ord r) => (EndPoint r, Bool) -> (EndPoint r, Bool)
-recipUB (Finite 0, _) = (NegInf, False)
-recipUB (x1, in1) = (recipEndPoint x1, in1)
-
-recipEndPoint :: (Fractional r, Ord r) => EndPoint r -> EndPoint r
-recipEndPoint PosInf = Finite 0
-recipEndPoint NegInf = Finite 0
-recipEndPoint (Finite x) = Finite (1/x)
+recipUB (0, _) = (NegInf, False)
+recipUB (x1, in1) = (recip x1, in1)
diff --git a/test/TestInterval.hs b/test/TestInterval.hs
--- a/test/TestInterval.hs
+++ b/test/TestInterval.hs
@@ -10,7 +10,7 @@
 import Test.Framework.Providers.HUnit
 import Test.Framework.Providers.QuickCheck2
 
-import Data.Interval (Interval, EndPoint (..), (<=..<=), (<=..<), (<..<=), (<..<), (<!), (<=!), (==!), (>=!), (>!), (<?), (<=?), (==?), (>=?), (>?))
+import Data.Interval (Interval, Extended (..), (<=..<=), (<=..<), (<..<=), (<..<), (<!), (<=!), (==!), (>=!), (>!), (<?), (<=?), (==?), (>=?), (>?), (<??), (<=??), (==??), (>=??), (>??))
 import qualified Data.Interval as Interval
 
 {--------------------------------------------------------------------
@@ -210,13 +210,13 @@
   Interval.simplestRationalWithin Interval.empty @?= Nothing
 
 case_simplestRationalWithin_test1 =
-  Interval.simplestRationalWithin (Finite (-0.5 :: Rational) <=..<= Finite 0.5) @?= Just 0
+  Interval.simplestRationalWithin (Finite (-0.5 :: Rational) <=..<= 0.5) @?= Just 0
 
 case_simplestRationalWithin_test2 =
-  Interval.simplestRationalWithin (Finite (2 :: Rational) <..< Finite 3) @?= Just 2.5
+  Interval.simplestRationalWithin (Finite (2 :: Rational) <..< 3) @?= Just 2.5
 
 case_simplestRationalWithin_test2' =
-  Interval.simplestRationalWithin (Finite (-3 :: Rational) <..< Finite (-2)) @?= Just (-2.5)
+  Interval.simplestRationalWithin (Finite (-3 :: Rational) <..< (-2)) @?= Just (-2.5)
 
 case_simplestRationalWithin_test3 =
   Interval.simplestRationalWithin (Finite (1.4142135623730951 :: Rational) <..< Finite 1.7320508075688772) @?= Just 1.5
@@ -251,68 +251,68 @@
 case_lt_all_1 = (a <! b) @?= False
   where
     a, b :: Interval Rational
-    a = NegInf <..<= Finite 0
-    b = Finite 0 <=..< PosInf
+    a = NegInf <..<= 0
+    b = 0 <=..< PosInf
 
 case_lt_all_2 = (a <! b) @?= True
   where
     a, b :: Interval Rational
-    a = NegInf <..< Finite 0
-    b = Finite 0 <=..< PosInf
+    a = NegInf <..< 0
+    b = 0 <=..< PosInf
 
 case_lt_all_3 = (a <! b) @?= True
   where
     a, b :: Interval Rational
-    a = NegInf <..<= Finite 0
-    b = Finite 0 <..< PosInf
+    a = NegInf <..<= 0
+    b = 0 <..< PosInf
 
 case_lt_all_4 = (a <! b) @?= False
   where
     a, b :: Interval Rational
-    a = Finite 0 <=..< PosInf
-    b = Finite 1 <=..< PosInf
+    a = 0 <=..< PosInf
+    b = 1 <=..< PosInf
 
 case_lt_some_1 = (a <? b) @?= False
   where
     a, b :: Interval Rational
-    a = Finite 0 <=..< PosInf
-    b = NegInf <..<= Finite 0
+    a = 0 <=..< PosInf
+    b = NegInf <..<= 0
 
 case_lt_some_2 = (a <? b) @?= False
   where
     a, b :: Interval Rational
-    a = Finite 0 <..< PosInf
-    b = NegInf <..<= Finite 0
+    a = 0 <..< PosInf
+    b = NegInf <..<= 0
 
 case_lt_some_3 = (a <? b) @?= False
   where
     a, b :: Interval Rational
-    a = Finite 0 <=..< PosInf
-    b = NegInf <..< Finite 0
+    a = 0 <=..< PosInf
+    b = NegInf <..< 0
 
 case_lt_some_4 = (a <! b) @?= False
   where
     a, b :: Interval Rational
-    a = Finite 0 <=..< PosInf
-    b = Finite 1 <=..< PosInf
+    a = 0 <=..< PosInf
+    b = 1 <=..< PosInf
 
 case_le_some_1 = (a <=? b) @?= True
   where
     a, b :: Interval Rational
-    a = Finite 0 <=..< PosInf
-    b = NegInf <..<= Finite 0
+    a = 0 <=..< PosInf
+    b = NegInf <..<= 0
 
 case_le_some_2 = (a <=? b) @?= False
   where
     a, b :: Interval Rational
-    a = Finite 0 <..< PosInf
-    b = NegInf <..<= Finite 0
+    a = 0 <..< PosInf
+    b = NegInf <..<= 0
 
 case_le_some_3 = (a <=? b) @?= False
   where
     a, b :: Interval Rational
-    a = Finite 0 <=..< PosInf
-    b = NegInf <..< Finite 0
+    a = 0 <=..< PosInf
+    b = NegInf <..< 0
 
 prop_lt_all_not_refl =
   forAll intervals $ \a -> not (Interval.null a) ==> not (a <! a)
@@ -406,6 +406,51 @@
     not (Interval.null (Interval.intersection a b))
     ==> a ==? b
 
+prop_le_some_witness =
+  forAll intervals $ \a ->
+  forAll intervals $ \b ->
+    case a <=?? b of
+      Nothing ->
+        forAll arbitrary $ \(x,y) ->
+          not (Interval.member x a && Interval.member y b && x <= y)
+      Just (x,y) ->
+        Interval.member x a .&&. Interval.member y b .&&. x <= y
+
+prop_lt_some_witness =
+  forAll intervals $ \a ->
+  forAll intervals $ \b ->
+    case a <?? b of
+      Nothing ->
+        forAll arbitrary $ \(x,y) ->
+          not (Interval.member x a && Interval.member y b && x < y)
+      Just (x,y) ->
+        Interval.member x a .&&. Interval.member y b .&&. x < y
+
+prop_eq_some_witness =
+  forAll intervals $ \a ->
+  forAll intervals $ \b ->
+    case a ==?? b of
+      Nothing ->
+        forAll arbitrary $ \x ->
+          not (Interval.member x a && Interval.member x b)
+      Just (x,y) ->
+        Interval.member x a .&&. Interval.member y b .&&. x == y
+
+prop_le_some_witness_forget =
+  forAll intervals $ \a ->
+  forAll intervals $ \b ->
+    isJust (a <=?? b) == (a <=? b)
+
+prop_lt_some_witness_forget =
+  forAll intervals $ \a ->
+  forAll intervals $ \b ->
+    isJust (a <?? b) == (a <? b)
+
+prop_eq_some_witness_forget =
+  forAll intervals $ \a ->
+  forAll intervals $ \b ->
+    isJust (a ==?? b) == (a ==? b)
+
 {--------------------------------------------------------------------
   Num
 --------------------------------------------------------------------}
@@ -484,39 +529,45 @@
 
 case_mult_test1 = ival1 * ival2 @?= ival3
   where
-    ival1 = Finite 1 <=..<= Finite 2
-    ival2 = Finite 1 <=..<= Finite 2
-    ival3 = Finite 1 <=..<= Finite 4
+    ival1 :: Interval Rational
+    ival1 = 1 <=..<= 2
+    ival2 = 1 <=..<= 2
+    ival3 = 1 <=..<= 4
 
 case_mult_test2 = ival1 * ival2 @?= ival3
   where
-    ival1 = Finite 1 <=..<= Finite 2
-    ival2 = Finite 1 <..< Finite 2
-    ival3 = Finite 1 <..< Finite 4
+    ival1 :: Interval Rational
+    ival1 = 1 <=..<= 2
+    ival2 = 1 <..< 2
+    ival3 = 1 <..< 4
 
 case_mult_test3 = ival1 * ival2 @?= ival3
   where
-    ival1 = Finite 1 <..< Finite 2
-    ival2 = Finite 1 <..< Finite 2
-    ival3 = Finite 1 <..< Finite 4
+    ival1 :: Interval Rational
+    ival1 = 1 <..< 2
+    ival2 = 1 <..< 2
+    ival3 = 1 <..< 4
 
 case_mult_test4 = ival1 * ival2 @?= ival3
   where
-    ival1 = Finite 2 <..< PosInf
-    ival2 = Finite 3 <..< PosInf
-    ival3 = Finite 6 <..< PosInf
+    ival1 :: Interval Rational
+    ival1 = 2 <..< PosInf
+    ival2 = 3 <..< PosInf
+    ival3 = 6 <..< PosInf
 
 case_mult_test5 = ival1 * ival2 @?= ival3
   where
-    ival1 = NegInf <..< Finite (-3)
-    ival2 = NegInf <..< Finite (-2)
-    ival3 = Finite 6 <..< PosInf
+    ival1 :: Interval Rational
+    ival1 = NegInf <..< (-3)
+    ival2 = NegInf <..< (-2)
+    ival3 = 6 <..< PosInf
 
 case_mult_test6 = ival1 * ival2 @?= ival3
   where
-    ival1 = Finite 2 <..< PosInf
-    ival2 = NegInf <..< Finite (-2)
-    ival3 = NegInf <..< Finite (-4)
+    ival1 :: Interval Rational
+    ival1 = 2 <..< PosInf
+    ival2 = NegInf <..< (-2)
+    ival3 = NegInf <..< (-4)
 
 {--------------------------------------------------------------------
   Fractional
@@ -537,8 +588,8 @@
 case_recip_test1 = recip i1 @?= i2
   where
     i1, i2 :: Interval Rational
-    i1 = Finite 2 <=..< PosInf
-    i2 = Finite 0 <..<= Finite (1/2)
+    i1 = 2 <=..< PosInf
+    i2 = 0 <..<= (1/2)
 
 {--------------------------------------------------------------------
   Read
@@ -552,7 +603,7 @@
   Generators
 --------------------------------------------------------------------}
 
-instance Arbitrary r => Arbitrary (EndPoint r) where
+instance Arbitrary r => Arbitrary (Extended r) where
   arbitrary = 
     oneof
     [ return NegInf
@@ -567,16 +618,16 @@
   return $ Interval.interval lb ub
 
 pos :: Interval Rational
-pos = Finite 0 <..< PosInf
+pos = 0 <..< PosInf
 
 neg :: Interval Rational
-neg = NegInf <..< Finite 0
+neg = NegInf <..< 0
 
 nonpos :: Interval Rational
-nonpos = NegInf <..<= Finite 0
+nonpos = NegInf <..<= 0
 
 nonneg :: Interval Rational
-nonneg = Finite 0 <=..< PosInf
+nonneg = 0 <=..< PosInf
 
 ------------------------------------------------------------------------
 -- Test harness