content: ---
  layout: post
  title: Isomorphisms for Proof Reductions
  date: 2016-12-25
  comments: true
  external-url:
  author: Vikraman Choudhury and Niki Vazou
  published: true
  categories: reflection 
  demo: Iso.hs
  ---
  
  [Previously][refinement-reflection] we saw how Refinement Reflection
  can be used to write and prove **in Haskell** theorems **about Haskell**
  functions and have such proofs machine checked by Liquid Haskell.
  
  As a limitation, Liquid Haskell offers no proof generation techniques: 
  The user needs to manually provide all the proofs. 
  
  Today we will see how proof generation can be simplified by data type isomorphisms. 
  
  As an example, a user defined `Peano` data type enjoyes all the 
  arithmetic properties of natural numbers since `Peano` and natural numbers 
  are provably **isomorphic**. 
  
  <!-- more -->
  
  <br>
  <br>
  <br>
  
  <div class="row-fluid">
    <div class="span12 pagination-centered">
    <img src="http://www.aaronartprints.org/images/Paintings/4597.jpg"
         alt="Recursion" width="300">
         <br>
         <br>
         <br>
         Recursive Paper and Pencil Proofs.
         "Drawing Hands" by Escher.
         <br>
         <br>
         <br>
    </div>
  </div>
  
  
  <div class="hidden">
  \begin{code}
  {-@ LIQUID "--higherorder" @-}
  {-@ LIQUID "--totalhaskell" @-}
  {-@ LIQUID "--exactdc" @-}
  {-@ LIQUID "--diffcheck" @-}
  {-@ LIQUID "--eliminate=some" @-}
  
  module Iso where
  
  import Language.Haskell.Liquid.ProofCombinators
  \end{code}
  
  </div>
  
  First, we define `Peano` numbers as a data type 
  and the function `leqPeano` that compares two peano numbers.
  
  
  \begin{code}
  {-@ data Peano [toNat] = Z | S Peano @-}
  data Peano = Z | S Peano deriving (Eq)
  
  {-@ axiomatize leqPeano @-}
  leqPeano :: Peano -> Peano -> Bool
  leqPeano Z _         = True
  leqPeano _ Z         = False
  leqPeano (S n) (S m) = leqPeano n m
  \end{code}
  
  We can use Refinement Reflection to provide an 
  explicit proof that comparison on peano numbers is *total*, 
  that is, for every two numbers `n` and `m` 
  either `leqPeano n m` or `leqPeano m n` always holds. 
  
  \begin{code}
  {-@ leqNTotal :: n:Peano -> m:Peano 
                -> {(leqPeano n m) || (leqPeano m n)} 
                / [toNat n + toNat m] @-}
  leqNTotal :: Peano -> Peano -> Proof
  leqNTotal Z m = leqPeano Z m *** QED
  leqNTotal n Z = leqPeano Z n *** QED
  leqNTotal (S n) (S m)
    =   (leqPeano (S n) (S m) || leqPeano (S m) (S n))
    ==. (leqPeano n m || leqPeano (S m) (S n)) 
        ? (leqNTotal n m)
    ==. (leqPeano n m || leqPeano m n) 
        ? (leqNTotal m n)
    *** QED
  \end{code}
  
  The proof proceeds by induction on the sum of `n` and `m`. 
  Liquid Haskell captures this generalized induction by 
  ensuring that the value `toNat n + toNat m` is decreasing
  where `toNat` maps Peano to Natural numbers. 
  
  \begin{code}
  {-@ measure toNat @-}
  {-@ toNat :: Peano -> Nat @-}
  toNat :: Peano -> Int
  toNat Z = 0
  toNat (S n) = 1 + toNat n
  \end{code}
  
  Note, that the type `Nat` is just a refinement for the Haskell's integers
  \begin{spec}
  type Nat = {v:Int | 0 <= v}
  \end{spec}
  
  
  First, we'll express verified typeclasses using Haskell records, but with LiquidHaskell refinements to express laws. As
  an example, let's define `VerifiedOrd`, which is the same as the `Ord` typeclass, but with total order laws added.
  
  \begin{code}
  {-@ data VerifiedOrd a = VerifiedOrd {
        leq     :: a -> a -> Bool
      , refl    :: x:a -> { leq x x }
      , antisym :: x:a -> y:a -> { leq x y && leq y x ==> x == y }
      , trans   :: x:a -> y:a -> z:a -> { leq x y && leq y z ==> leq x z }
      , total   :: x:a -> y:a -> { leq x y || leq y x }
      }
  @-}
  data VerifiedOrd a = VerifiedOrd {
      leq     :: a -> a -> Bool
    , refl    :: a -> Proof
    , antisym :: a -> a -> Proof
    , trans   :: a -> a -> a -> Proof
    , total   :: a -> a -> Proof
  }
  \end{code}
  
  The `leq` function represents the `<=` operator in `Ord`, and `refl`, `antisym`, `trans`, `total`, express the
  reflexivity, antisymmetry, transitivity and totality properties respectively, that a total order requires. Notice how
  the refinements express the laws, and the actual code is simply a function that returns `Proof` or `()`.
  
  Now, let's see how to define some simple verified instances. We need to instantiate `leq` for our type, "reflect" it
  into the logic, and prove all the required properties. For primitive types like `Int` or `Double`, it's "trivial"
  because we trust the SMT solver which already knows about integers.
  
  \begin{code}
  {-@ axiomatize leqInt @-}
  leqInt :: Int -> Int -> Bool
  leqInt x y = x <= y
  
  {-@ leqIntRefl :: x:Int -> { leqInt x x } @-}
  leqIntRefl :: Int -> Proof
  leqIntRefl x = leqInt x x ==. x <= x *** QED
  
  {-@ leqIntAntisym :: x:Int -> y:Int -> { leqInt x y && leqInt y x ==> x == y } @-}
  leqIntAntisym :: Int -> Int -> Proof
  leqIntAntisym x y = (leqInt x y && leqInt y x) ==. (x <= y && y <= x) ==. x == y *** QED
  
  {-@ leqIntTrans :: x:Int -> y:Int -> z:Int -> { leqInt x y && leqInt y z ==> leqInt x z } @-}
  leqIntTrans :: Int -> Int -> Int -> Proof
  leqIntTrans x y z = (leqInt x y && leqInt y z) ==. (x <= y && y <= z) ==. x <= z ==. leqInt x z *** QED
  
  {-@ leqIntTotal :: x:Int -> y:Int -> { leqInt x y || leqInt y x } @-}
  leqIntTotal :: Int -> Int -> Proof
  leqIntTotal x y = (leqInt x y || leqInt y x) ==. (x <= y || y <= x) *** QED
  
  vordInt :: VerifiedOrd Int
  vordInt = VerifiedOrd leqInt leqIntRefl leqIntAntisym leqIntTrans leqIntTotal
  \end{code}
  
  How about a complex datatype? Let's consider an inductive datatype, the peano natural numbers. Not surprisingly, the
  proofs follow by induction. For conciseness, we only show totality and elide the rest.
  
  Writing down proofs for more complex datatypes is tedious, it requires case analysis for each constructor and using the
  induction hypothesis. However, we can decompose Haskell datatypes into sums and products, and we can build up compound
  proofs using isomorphisms! To that end, we design some machinery to express isomorphisms, and prove that laws are
  preserved under isomorphic images.
  
  \begin{code}
  {-@ data Iso a b = Iso {
        to   :: a -> b
      , from :: b -> a
      , tof  :: y:b -> { to (from y) == y }
      , fot  :: x:a -> { from (to x) == x }
      }
  @-}
  data Iso a b = Iso {
      to   :: a -> b
    , from :: b -> a
    , tof  :: b -> Proof
    , fot  :: a -> Proof
  }
  \end{code}
  
  An isomorphism between types `a` and `b` is a pair of functions `to :: a -> b` and `from :: b -> a` that are mutually
  inverse to each other. We now claim that total order laws are preserved under `Iso`; this amounts to building up a
  `VerifiedOrd b`, given a `VerifiedOrd a` and an `Iso a b`.
  
  \begin{code}
  {-@ axiomatize leqFrom @-}
  leqFrom :: (a -> a -> Bool)
          -> (b -> a)
          -> (b -> b -> Bool)
  leqFrom leqa from x y = leqa (from x) (from y)
  
  {-@ leqFromRefl :: leqa:(a -> a -> Bool) -> leqaRefl:(x:a -> { leqa x x })
                  -> from:(b -> a)
                  -> x:b -> { leqFrom leqa from x x }
  @-}
  leqFromRefl :: (a -> a -> Bool) -> (a -> Proof)
              -> (b -> a)
              -> b -> Proof
  leqFromRefl leqa leqaRefl from x =
        leqFrom leqa from x x
    ==. leqa (from x) (from x)
    ==. True ? leqaRefl (from x)
    *** QED
  
  {-@ leqFromAntisym :: leqa:(a -> a -> Bool)
                     -> leqaAntisym:(x:a -> y:a -> { leqa x y && leqa y x ==> x == y })
                     -> to:(a -> b) -> from:(b -> a) -> tof:(y:b -> { to (from y) == y })
                     -> x:b -> y:b -> { leqFrom leqa from x y && leqFrom leqa from y x ==> x == y }
  @-}
  leqFromAntisym :: (Eq a, Eq b)
                 => (a -> a -> Bool) -> (a -> a -> Proof)
                 -> (a -> b) -> (b -> a) -> (b -> Proof)
                 -> b -> b -> Proof
  leqFromAntisym leqa leqaAntisym to from tof x y
    =   (leqFrom leqa from x y && leqFrom leqa from y x)
    ==. (leqa (from x) (from y) && leqa (from y) (from x))
    ==. from x == from y ? leqaAntisym (from x) (from y)
    ==. to (from x) == to (from y)
    ==. x == to (from y) ? tof x
    ==. x == y           ? tof y
    *** QED
  
  {-@ leqFromTrans :: leqa:(a -> a -> Bool)
                   -> leqaTrans:(x:a -> y:a -> z:a -> { (leqa x y) && (leqa y z) ==> (leqa x z) })
                   -> from:(b -> a)
                   -> x:b -> y:b -> z:b
                   -> { leqFrom leqa from x y && leqFrom leqa from y z ==> leqFrom leqa from x z }
  @-}
  leqFromTrans :: (a -> a -> Bool) -> (a -> a -> a -> Proof)
               -> (b -> a)
               -> b -> b -> b -> Proof
  leqFromTrans leqa leqaTrans from x y z =
        (leqFrom leqa from x y && leqFrom leqa from y z)
    ==. (leqa (from x) (from y) && leqa (from y) (from z))
    ==. leqa (from x) (from z) ? leqaTrans (from x) (from y) (from z)
    ==. leqFrom leqa from x z
    *** QED
  
  {-@ leqFromTotal :: leqa:(a -> a -> Bool) -> leqaTotal:(x:a -> y:a -> { (leqa x y) || (leqa y x) })
                   -> from:(b -> a) -> x:b -> y:b -> { leqFrom leqa from x y || leqFrom leqa from y x }
  @-}
  leqFromTotal :: (a -> a -> Bool) -> (a -> a -> Proof)
               -> (b -> a) -> b -> b -> Proof
  leqFromTotal leqa leqaTotal from x y =
        (leqFrom leqa from x y || leqFrom leqa from y x)
    ==. (leqa (from x) (from y) || leqa (from y) (from x))
    ==. True ? leqaTotal (from x) (from y)
    ==. leqFrom leqa from y x
    *** QED
  
  vordIso :: (Eq a, Eq b) => Iso a b -> VerifiedOrd a -> VerifiedOrd b
  vordIso (Iso to from tof fot) (VerifiedOrd leqa leqaRefl leqaAntisym leqaTrans leqaTotal) =
    VerifiedOrd
      (leqFrom leqa from)
      (leqFromRefl leqa leqaRefl from)
      (leqFromAntisym leqa leqaAntisym to from tof)
      (leqFromTrans leqa leqaTrans from)
      (leqFromTotal leqa leqaTotal from)
  \end{code}
  
  We can now write a `VerifiedOrd` for `Peano` by mapping it onto `type Nat = { n:Int | 0 <= n }`, which is easier to
  prove properties about because it's just an integer!
  
  \begin{code}
  {-@ type Nat = { n:Int | 0 <= n } @-}
  type Nat = Int
  
  {-@ axiomatize fromNat @-}
  {-@ fromNat :: Nat -> Peano @-}
  fromNat :: Nat -> Peano
  fromNat n
    | n == 0 = Z
    | otherwise = S (fromNat (n - 1))
  
  {-@ toFrom :: x:Nat -> { toNat (fromNat x) == x } @-}
  toFrom :: Nat -> Proof
  toFrom n
    | n == 0 = toNat (fromNat 0) ==. toNat Z ==. 0 *** QED
    | n > 0 = toNat (fromNat n)
          ==. toNat (S (fromNat (n - 1)))
          ==. 1 + toNat (fromNat (n - 1))
          ==. 1 + (n - 1) ? toFrom (n - 1)
          ==. n
          *** QED
  
  {-@ fromTo :: x:Peano -> { fromNat (toNat x) == x } @-}
  fromTo :: Peano -> Proof
  fromTo Z = fromNat (toNat Z) ==. fromNat 0 ==. Z *** QED
  fromTo (S n) = fromNat (toNat (S n))
             ==. fromNat (1 + toNat n)
             ==. S (fromNat ((1 + toNat n) - 1))
             ==. S (fromNat (toNat n))
             ==. S n ? fromTo n
             *** QED
  
  {-@ isoNatPeano :: Iso Nat Peano @-}
  isoNatPeano :: Iso Nat Peano
  isoNatPeano = Iso fromNat toNat fromTo toFrom
  
  vordNat :: VerifiedOrd Nat
  vordNat = VerifiedOrd leqInt leqIntRefl leqIntAntisym leqIntTrans leqIntTotal
  
  vordPeano :: VerifiedOrd Peano
  vordPeano = vordIso isoNatPeano vordNat
  \end{code}
  
  Similarly, we can break down compound datatypes into sums and products, just like what happens in `GHC.Generics`, and
  use the isomorphism to write down `VerifiedOrd` instances. We do however need to provide instances of `VerifiedOrd` for
  sums and products.
  
  \begin{code}
  vordProd :: VerifiedOrd a -> VerifiedOrd b -> VerifiedOrd (a, b)
  vordSum :: VerifiedOrd a -> VerifiedOrd b -> VerifiedOrd (Either a b)
  \end{code}
  
  \begin{comment}
  \begin{code}
  vordSum = undefined
  vordProd = undefined
  \end{code}
  \end{comment}
  
  Our [library](https://github.com/iu-parfunc/verified-instances) explores this idea to build some verified typeclasses,
  such as `VerifiedOrd` and `VerifiedMonoid`. We also provide combinators to build verified instances by using
  isomorphisms. Also, using a [reflection hack](https://www.schoolofhaskell.com/user/thoughtpolice/using-reflection), we
  can reify these "verified" terms to typeclass dictionaries at runtime, to call legacy functions which require `Ord`
  constraints and so on.
  