Preorder Reasoning Examples

Sublist.idr

module Sublist
import Syntax.PreorderReasoning

%default total

data Sublist : List a -> List a -> Type where
  Keep : Sublist xs ys -> Sublist (x::xs) (x::ys)
  Drop : Sublist xs ys -> Sublist xs (y::ys)
  Vacuous : Sublist [] ys

sublistRefl : Sublist xs xs
sublistRefl {xs=[]} = Vacuous
sublistRefl {xs=(x::xs)} = Keep sublistRefl

sublistTrans : {xs, ys, zs : List a} -> Sublist xs ys -> Sublist ys zs ->
               Sublist xs zs
sublistTrans (Keep xy) (Keep yz) = Keep (sublistTrans xy yz)
sublistTrans (Keep xy) (Drop yz) = Drop (sublistTrans (Keep xy) yz)
sublistTrans (Drop xy) (Keep yz) = Drop (sublistTrans xy yz)
sublistTrans (Drop xy) (Drop yz) = Drop (sublistTrans (Drop xy) yz)
sublistTrans Vacuous x1 = Vacuous

step : (zs : List a) -> Sublist ys zs -> Sublist xs ys -> Sublist xs zs
step xs xy yz = sublistTrans yz xy

qed : (xs : List a) -> Sublist xs xs
qed xs = sublistRefl

sandwich : (xs, ys, zs : List a) -> Sublist (xs ++ zs) (xs ++ ys ++ zs)
sandwich [] [] zs = sublistRefl
sandwich [] (y :: ys) zs = Drop (sandwich [] ys zs)
sandwich (x :: xs) ys zs = Keep (sandwich xs ys zs)

take : {xs : List a} -> (n : Nat) -> Sublist (take n xs) xs
take Z = Vacuous
take {xs = []} (S k) = Vacuous
take {xs = (x :: xs)} (S k) = Keep (take k)

drop : {xs : List a} -> (n : Nat) -> Sublist (drop n xs) xs
drop Z = sublistRefl
drop {xs = []} (S k) = Vacuous
drop {xs = (x :: xs)} (S k) = Drop (drop k)

keep : (n : Nat) -> Sublist (drop n xs) ys -> Sublist xs (take n xs ++ ys)
keep Z p = p
keep {xs = []} {ys = ys} (S k) p = Vacuous
keep {xs = (y :: xs)} {ys = ys} (S k) p = Keep (keep k p)

p : Sublist [2,4] [1,2,3,4,5,6,7]
p = [1,2,3,4,5,6,7] ={ take 4 }=
    [1,2,3,4]       ={ drop 1 }=
    [2,3,4]         ={ keep 1 (drop 1) }=
    [2,4]           QED

triple : List a -> List a
triple [] = []
triple (x::xs) = x::x::x::triple xs

q : (xs:List a) -> Sublist xs (triple xs)
q [] = sublistRefl
q (x::xs) = 
  (x::x::x::triple xs) ={ drop 2 }=
  (x::triple xs)       ={ keep 1 (q xs) }=
  (x::xs)              QED

ZeroElem.idr

module ZeroElem
import Data.List
import Syntax.PreorderReasoning

product : List Nat -> Nat
product [] = 1
product (x::xs) = x * product xs


zeroConsZeroProduct : (xs : List Nat) -> ZeroElem.product (0 :: xs) = 0
zeroConsZeroProduct xs = Refl


zeroElemZeroProduct : Elem Z xs -> ZeroElem.product xs = 0
zeroElemZeroProduct {xs = Z :: xs'} Here = zeroConsZeroProduct xs'
zeroElemZeroProduct {xs = left :: xs'} (There p) =
  (product (left :: xs')) ={ Refl }= 
  (left * product xs')    ={ cong (zeroElemZeroProduct p) }=
  (left * Z)              ={ multZeroRightZero left }=
  Z QED
--  rewrite zeroElemZeroProduct p in multZeroRightZero left