content: ---
  layout: post
  title: Proof Reductions on Homomorphisms
  date: 2017-01-02
  comments: true
  external-url:
  author: Niki Vazou and Vikraman Choudhury
  published: true
  categories: reflection, abstract-refinements
  demo: Reductions.hs
  ---
  
  [Previously][refinement-reflection] we saw how Refinement Reflection
  can be used to specify and prove theorems about Haskell code.
  
  Today we will see how proof generation can be simplified by 
  proof reduction on homomorphic data types. 
  
  As an example, we define a user-defined `Peano` data type
  and prove that it enjoys various arithmetic properties 
  (like totality of comparison) by 
  
  1. creating a proof that an arithmetic property holds on Natural numbers, and then 
  2. reduce the proof from Natural numbers to Peano numbers. 
  This proof reduction is possible since Peano numbers are homomorphic to Natural numbers. 
  
  <!-- more -->
  
  <br>
  <br>
  <br>
  
  <div class="row-fluid">
    <div class="span12 pagination-centered">
    <img src="http://4.bp.blogspot.com/-oltF9WI2KhY/VBMwdj15IvI/AAAAAAAAAtg/V3-k6IylIZM/s1600/picasso_bull.jpg"
         alt="Picasso bull" width="400">
         <br>
         <br>
         <br>
    </div>
  </div>
  
  
  <div class="hidden">
  \begin{code}
  {-@ LIQUID "--higherorder"    @-}
  {-@ LIQUID "--totalhaskell"   @-}
  {-@ LIQUID "--exactdc"        @-}
  {-@ LIQUID "--diffcheck"      @-}
  {-@ LIQUID "--pruneunsorted"  @-}
  {-@ LIQUID "--eliminate=some" @-}
  
  module Reductions where
  
  import Language.Haskell.Liquid.ProofCombinators
  
  geqZero  :: Peano -> Proof 
  leqTotal :: Peano -> Peano -> Proof
  toNat    :: Peano -> Int
  
  geqZeroNat          :: Nat -> Proof 
  geqZeroByReduction  :: Peano -> Proof 
  leqTotalByReduction :: Peano -> Peano -> Proof 
  leqTotalNat         :: Nat -> Nat -> Proof
  
  \end{code}
  
  </div>
  
  Properties of Peano Numbers
  ----------------------------
  
  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 {prev :: Peano } @-}
  data Peano = Z | S { prev :: Peano } deriving (Eq)
  
  {-@ reflect 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 no Peano number is greater than zero (`Z`).
  
  \begin{code}
  {-@ geqZero :: n:Peano -> {leqPeano Z n} @-}
  geqZero n = leqPeano Z n *** QED 
  \end{code}
  
  The proof proceeds simply by invocation of the 
  first case of the `leqPeano` definition. 
  
  As another Peano property, we can use Refinement Reflection to 
  show 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}
  {-@ leqTotal :: n:Peano -> m:Peano 
               -> {(leqPeano n m) || (leqPeano m n)} 
               /  [toNat n + toNat m] @-}
  leqTotal Z m = leqPeano Z m *** QED
  leqTotal n Z = leqPeano Z n *** QED
  leqTotal (S n) (S m)
    =   (leqPeano (S n) (S m) || leqPeano (S m) (S n))
    ==. (leqPeano n m || leqPeano (S m) (S n)) 
        ? (leqTotal n m)
    ==. (leqPeano n m || leqPeano m n) 
        ? (leqTotal 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 Z     = 0
  toNat (S n) = 1 + toNat n
  \end{code}
  
  Note, that the type `Nat` is just a refinement on the Haskell's integers
  \begin{code}
  {-@ type Nat = { n:Int | 0 <= n } @-}
  type Nat     = Int
  \end{code}
  
  Following the totality proof, 
  one can prove further properties of Peano comparisons, 
  like reflexivity and transitivity.
  
  The above totality proof is verbose! 
  Moreover, it is very similar 
  to the classic totality on Natural numbers. 
  Since the SMT knowns that comparison of Nat is total, we can just reduce 
  Peano to Natural number totality!
  
  
  Reduction of Operators 
  -----------------------
  
  Since `toNat` is a homomorphism (i.e., a transformation) from `Peano` to `Nat`
  one can compare two Peano numbers via comparison of Natural numbers. 
  
  \begin{code}
  {-@ reflect leqPeanoNat @-}
  leqPeanoNat :: Peano -> Peano -> Bool 
  leqPeanoNat n m = toNat n `leqInt` toNat m  
  \end{code}
  
  where `leqInt` the Haskell comparison operator restricted to `Ints`.
  
  \begin{code}
  {-@ reflect leqInt @-}
  leqInt :: Int -> Int -> Bool 
  leqInt x y = x <= y
  \end{code}
  
  Note that `leqPeanoNat` is exactly equivalent to `leqPeano`. 
  For this blog post, we leave the equivalence proof as an exercise for the reader.
  
  
  Proof Reductions
  -----------------
  
  After reducing the Peano comparison operator to
  comparison on Natural numbers, we can reduce 
  proofs on Peano numbers to proofs on Natural numbers.
  The great benefit of this reduction is that proofs on Natural number
  are automated by the underlying SMT solver!
  
  For example, we prove that no Natural number is less than `0`
  by unfolding `leqInt` on `0` 
  and then let linear arithmetic decision procedure of the SMT complete the proof. 
  \begin{code}
  {-@ geqZeroNat :: n:Nat -> {leqInt 0 n} @-}
  geqZeroNat n = leqInt 0 n *** QED 
  \end{code}
  
  
  We then reduce the above property to the respective property on Peano numbers.
  \begin{code}
  {-@ geqZeroByReduction :: n:Peano -> {leqPeanoNat Z n} @-}
  geqZeroByReduction n 
    = leqPeanoNat Z n ==. True 
    ? reduction toNat geqZeroNat n 
    *** QED 
  \end{code}
  
  The reduction occurs via the function `reduction`.
  The function `reduction f thm n`, for each homomorphism `f :: a -> b`, 
  reduces a theorem `thm x` on `a`s to the respective theorems on `b` via 
  [Abstract Refinements][abstract-refinements].
  \begin{code}
  {-@ reduction :: forall<p :: a -> Proof -> Bool>. 
                   f:(b -> a) 
                -> (x:a -> Proof<p x>) 
                -> (y:b -> Proof<p (f y)>) @-}
  reduction :: (b -> a) -> (a -> Proof) -> (b -> Proof)
  reduction f thm y = thm (f y)              
  \end{code}
  
  Users with model theoretic background may observe that `reduction` 
  is actually encoding [Łoś–Tarski preservation theorem][preservation-theorem]!
  
  Similarly, `reduction2` reduces theorems with two `a` arguments
  to theorems with two `b` arguments via a homomorphism. 
  
  \begin{code}
  {-@ reduction2 :: forall<p :: a -> a -> Proof -> Bool >. 
                    f:(b -> a) 
                 -> (x1:a -> x2:a -> Proof<p x1 x2>) 
                 -> (y1:b -> y2:b-> Proof<p (f y1) (f y2)>) @-}
  reduction2 :: (b -> a) -> (a -> a -> Proof) -> (b -> b -> Proof)
  reduction2 f thm y1 y2  = thm (f y1) (f y2)
  \end{code}
  
  For example, the SMT-automated proof of totality on Natural numbers 
  \begin{code}
  {-@ leqTotalNat :: n:Nat -> m:Nat -> { leqInt n m || leqInt m n } @-}
  leqTotalNat n m = (leqInt n m || leqInt m n) *** QED 
  \end{code}
  
  can be easily reduced to totality on Peano numbers
  
  \begin{code}
  {-@ leqTotalByReduction :: n:Peano -> m:Peano
     -> { leqPeanoNat n m || leqPeanoNat m n } @-}
  leqTotalByReduction n m 
    = (leqPeanoNat n m || leqPeanoNat m n) ==. True 
    ? reduction2 toNat leqTotalNat n m  
    *** QED 
  \end{code}
  
  
  Conclusion
  -----------
  
  We presented an example of how the SMT-automated proofs on 
  Natural numbers can be reduced to the respective proofs on the 
  Peano numbers, because Peano are homomorphic to Natural numbers. 
  
  Proof reduction greatly simplifies proof composition
  as it allows for shorter and more elegant proofs 
  that take advantage of SMT-automated or other existing
  proofs on homomorphic data structures. 
  
  
  [refinement-reflection]: http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2016/09/18/refinement-reflection.lhs/
  [reduction-lib]: https://github.com/ucsd-progsys/liquidhaskell/tree/develop/include/Language/Haskell/Liquid/Reduction.hs
  [abstract-refinements]: http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/06/03/abstracting-over-refinements.lhs/
  [preservation-theorem]: https://en.wikipedia.org/wiki/%C5%81o%C5%9B%E2%80%93Tarski_preservation_theorem
  