text:
> module Nat.OperationsProperties

> import Syntax.PreorderReasoning

> -- import NatPredicates
> import Nat.Operations
> import Nat.BasicProperties
> import Nat.LTEProperties
> import Nat.LTProperties
> import Basic.Operations
> import Functor.Predicates

> %default total
> %access public export
> %auto_implicits on

Properties of |pred|:

> |||
> predLemma : (n : Nat) -> (prf : Z `LT` n) -> S (pred n prf) = n
> predLemma  Z    prf = absurd prf
> predLemma (S m) _   = Refl
> %freeze predLemma

Properties of |=|:

> ||| EQ is contained in LTE
> eqInLTE : (m : Nat) -> (n : Nat) -> m = n -> m `LTE` n
> eqInLTE  Z     n    prf = LTEZero
> eqInLTE (S m)  Z    prf = absurd prf
> eqInLTE (S m) (S n) prf = LTESucc (eqInLTE m n (succInjective m n prf))
> %freeze eqInLTE

Properties of |plus|:

> |||
> plusPlusElimLeft : {m1, n1, m2, n2 : Nat} -> m1 + n1 = m2 + n2 -> m1 = m2 -> n1 = n2
> plusPlusElimLeft {m1 = Z} {n1} {m2 = Z} {n2} p1 Refl = s2 where
>   s1 : n1 = Z + n2
>   s1 = replace {x = Z + n1}
>                {y = n1}
>                {P = \ ZUZU => ZUZU = Z + n2}
>                (plusZeroLeftNeutral n1)
>                p1
>   s2 : n1 = n2
>   s2 = replace {x = Z + n2}
>                {y = n2}
>                {P = \ ZUZU => n1 = ZUZU}
>                (plusZeroLeftNeutral n2)
>                s1
> plusPlusElimLeft {m1 = Z}    {n1} {m2 = S m2} {n2} p1 Refl impossible
> plusPlusElimLeft {m1 = S m1} {n1} {m2 = Z}    {n2} p1 Refl impossible
> plusPlusElimLeft {m1 = S m1} {n1} {m2 = S m2} {n2} p1 p2 = plusPlusElimLeft p1' p2' where
>   p1' : m1 + n1 = m2 + n2
>   p1' = succInjective (m1 + n1) (m2 + n2) p1
>   p2' : m1 = m2
>   p2' = succInjective m1 m2 p2
> %freeze plusPlusElimLeft

> |||
> plusElimLeft : (m1 : Nat) -> (n : Nat) -> (m2 : Nat) -> m1 + n = m2 -> m1 = m2 -> n = Z
> plusElimLeft m n m p Refl = plusLeftLeftRightZero m n p
> %freeze plusElimLeft

> {-

> |||
> idPlusAnyPreservesLT : (m : Nat) -> (n : Nat) -> m `LT` n -> (p : Nat) -> m `LT` (n + p)

> |||
> idAnyPlusPreservesLT : (m : Nat) -> (n : Nat) -> m `LT` n -> (p : Nat) -> m `LT` (p + n)

> |||
> plusPreservesLT : (m : Nat) -> (n : Nat) -> m `LT` n ->
>                   (p : Nat) -> (q : Nat) -> p `LT` q ->
>                   (m + p) `LT` (n + q)
> plusPreservesLT  Z     Z     zLTz  _ _ _    = absurd  zLTz
> plusPreservesLT  Z    (S n)  zLTsn p q pLTq = idAnyPlusPreservesLT p q pLTq (S n)
> plusPreservesLT (S m)  Z    smLTz  _ _ _    = absurd smLTz
> plusPreservesLT (S m) (S n) smLTsn p q pLTq = LTESucc (plusPreservesLT m n (fromLteSucc smLTsn) p q pLTq)

> -}

Properties of |minus|:

> ||| The difference of equal numbers is zero
> minusLemma0 : m = n -> m - n = Z
> minusLemma0 {m = Z}    {n = Z}    Refl = Refl
> minusLemma0 {m = Z}    {n = S n'} prf  = absurd prf
> minusLemma0 {m = S m'} {n = Z}    prf  = absurd prf
> minusLemma0 {m = S m'} {n = S n'} prf  = trans s1 s2 where
>   s1 : S m' - S n' = m' - n'
>   s1 = Refl
>   s2 : m' - n' = Z
>   s2 = minusLemma0 (succInjective m' n' prf)
> %freeze minusLemma0

> |||
> minusLemma1 : n - m = S l -> l = n - (S m)
> minusLemma1 {l} {m = Z}    {n = Z}    p = absurd p
> minusLemma1 {l} {m = Z}    {n = S n'} p = s5 where
>   s1 : S n' = S l
>   s1 = p
>   s2 : l = n'
>   s2 = sym (succInjective n' l s1)
>   s3 : n' = n' - Z
>   s3 = sym (minusZeroRight n')
>   s4 : n' - Z = S n' - S Z
>   s4 = Refl
>   s5 : l = S n' - S Z
>   s5 = trans s2 (trans s3 s4)
> minusLemma1 {l} {m = S m'} {n = Z}    p = absurd p
> minusLemma1 {l} {m = S m'} {n = S n'} p = s3 where
>   s1 : n' - m' = S l
>   s1 = p
>   s2 : l = n' - (S m')
>   s2 = minusLemma1 s1
>   s3 : l = S n' - S (S m')
>   s3 = trans s2 Refl
> %freeze minusLemma1

> |||
> minusLemma2 : LTE m n -> n - m = S l -> LTE (S m) n
> minusLemma2 {m = Z}    {n = Z}    p q = absurd q
> minusLemma2 {m = Z}    {n = S n'} p q = LTESucc LTEZero
> minusLemma2 {m = S m'} {n = Z}    p q = absurd p
> minusLemma2 {m = S m'} {n = S n'} (LTESucc p') q = LTESucc (minusLemma2 p' q)
> %freeze minusLemma2

> |||
> minusLemma3 : LTE m n -> Z = n - m -> m = n
> minusLemma3 {m = Z}    {n = Z}    p q = Refl
> minusLemma3 {m = Z}    {n = S n'} p q = absurd q
> minusLemma3 {m = S m'} {n = Z}    p q = absurd p
> minusLemma3 {m = S m'} {n = S n'} (LTESucc p') q =
>   eqSucc m' n' (minusLemma3 {m = m'} {n = n'} p' q') where
>     q' : Z = n' - m'
>     q' = trans q Refl
> %freeze minusLemma3

> |||
> minusLemma4 : LTE (S m) n -> S (n - S m) = n - m
> minusLemma4 {m = Z} {n = Z}    p = absurd p
> minusLemma4 {m = Z} {n = S n'} (LTESucc p') =
>     ( S (S n' - S Z) )
>   ={ Refl }=
>     ( S (n' - Z)     )
>   ={ cong (minusZeroRight n') }=
>     ( S n'           )
>   ={ Refl }=
>     ( S n' - Z       )
>   QED
> minusLemma4 {m = S m'} {n = Z} p = absurd p
> minusLemma4 {m = S m'} {n = S n'} (LTESucc p') =
>     ( S (S n' - S (S m')) )
>   ={ Refl }=
>     ( S (n' - S m')       )
>   ={ minusLemma4 p' }=
>     ( n' - m'             )
>   ={ Refl }=
>     ( S n' - S m'         )
>   QED
> %freeze minusLemma4

Properties of |plus| and |minus|:

> |||
> plusZeroLeftZero : (m : Nat) -> (n : Nat) -> m + n = Z -> m = Z
> plusZeroLeftZero  Z     Z    _   = Refl
> plusZeroLeftZero  Z    (S n) prf = absurd prf
> plusZeroLeftZero (S m)  Z    prf = absurd prf
> plusZeroLeftZero (S m) (S n) prf = absurd prf
> %freeze plusZeroLeftZero

> |||
> plusZeroRightZero : (m : Nat) -> (n : Nat) -> m + n = Z -> n = Z
> plusZeroRightZero  Z     Z    _   = Refl
> plusZeroRightZero  Z    (S n) prf = absurd prf
> plusZeroRightZero (S m)  Z    prf = absurd prf
> plusZeroRightZero (S m) (S n) prf = absurd prf
> %freeze plusZeroRightZero

> -- plusOneEither : (m : Nat) -> (n : Nat) -> m + n = S Z -> Either (m = Z) (n = Z)

> plusRightInverseMinus : (m : Nat) -> (n : Nat) -> m `LTE` n -> (n - m) + m = n
> plusRightInverseMinus  Z    n _ =
>     ( (n - Z) + Z )
>   ={ plusZeroRightNeutral (n - Z) }=
>     ( n - Z )
>   ={ minusZeroRight n }=
>     ( n )
>   QED
> plusRightInverseMinus (S m) n p =
>     ( (n - S m) + S m )
>   ={ plusCommutative (n - S m) (S m) }=
>     ( S m + (n - S m) )
>   ={ plusSuccRightSucc m (n - S m) }=
>     ( m + S (n - S m) )
>   ={ replace {x = S (n - S m)}
>              {y = n - m}
>              {P = \ ZUZU => m + S (n - S m) = m + ZUZU }
>              (minusLemma4 p) Refl}=
>     ( m + (n - m) )
>   ={ plusCommutative m (n - m) }=
>     ( (n - m) + m )
>   ={ plusRightInverseMinus m n (lteLemma1 m n p) }=
>     ( n )
>   QED
> %freeze plusRightInverseMinus

Properties of |mult|:

> ||| Multiplication of successors is not zero
> multSuccNotZero : (m : Nat) -> (n : Nat) -> Not ((S m) * (S n) = Z)
> multSuccNotZero m  n  p = absurd p
> %freeze multSuccNotZero

> ||| Multiplication of non-zeros is not zero
> multNotZeroNotZero : (m : Nat) -> (n : Nat) -> Not (m = Z) -> Not (n = Z) -> Not (m * n = Z)
> multNotZeroNotZero  Z     n    p q = void (p Refl)
> multNotZeroNotZero (S m)  Z    p q = void (q Refl)
> multNotZeroNotZero (S m) (S n) p q = multSuccNotZero m n
> %freeze multNotZeroNotZero

> ||| Multiplication not zero implies non-zero left
> multNotZeroNotZeroLeft : (m : Nat) -> (n : Nat) -> Not (m * n = Z) -> Not (m = Z)
> multNotZeroNotZeroLeft  Z     n    p = void (p (multZeroLeftZero n))
> multNotZeroNotZeroLeft (S m)  _    _ = SIsNotZ
> %freeze multNotZeroNotZeroLeft

> ||| Multiplication not zero implies non-zero right
> multNotZeroNotZeroRight : (m : Nat) -> (n : Nat) -> Not (m * n = Z) -> Not (n = Z)
> multNotZeroNotZeroRight m  Z     p = void (p (multZeroRightZero m))
> multNotZeroNotZeroRight _ (S n)  _ = SIsNotZ
> %freeze multNotZeroNotZeroRight

> ||| Multiplication of greater-than-zeros is greater than zero
> multZeroLTZeroLT : (m : Nat) -> (n : Nat) -> Z `LT` m -> Z `LT` n -> Z `LT` (m * n)
> multZeroLTZeroLT  Z     n    p _ = absurd p
> multZeroLTZeroLT (S m)  Z    _ q = absurd q
> multZeroLTZeroLT (S m) (S n) _ _ = ltZS (n + m * (S n))
> %freeze multZeroLTZeroLT

> ||| Multiplication greater than zero implies greater than zero left
> multLTZeroLeftLTZero : (m : Nat) -> (n : Nat) -> Z `LT` (m * n) -> Z `LT` m
> multLTZeroLeftLTZero Z n p = absurd p' where
>   p' : Z `LT` Z
>   p' = replace {x = Z * n}
>                {y = Z}
>                {P = \ ZUZU => Z `LT` ZUZU}
>                (multZeroLeftZero n) p
> multLTZeroLeftLTZero (S m) n _ = ltZS m
> %freeze multLTZeroLeftLTZero

> ||| Multiplication greater than zero implies greater than zero right
> multLTZeroRightLTZero : (m : Nat) -> (n : Nat) -> Z `LT` (m * n) -> Z `LT` n
> multLTZeroRightLTZero m Z p = absurd p' where
>   p' : Z `LT` Z
>   p' = replace {x = m * Z}
>                {y = Z}
>                {P = \ ZUZU => Z `LT` ZUZU}
>                (multZeroRightZero m) p
> multLTZeroRightLTZero m (S n) _ = ltZS n
> %freeze multLTZeroRightLTZero

> |||
> multZeroRightOneLeftZero : (m : Nat) -> (n : Nat) -> m * (S n) = Z -> m = Z
> multZeroRightOneLeftZero m n prf = plusZeroLeftZero m (n * m) prf' where
>   prf' : (S n) * m = Z
>   prf' = replace {x = m * (S n)} {y = (S n) * m} {P = \ ZUZU => ZUZU = Z} (multCommutative m (S n)) prf
> %freeze multZeroRightOneLeftZero

> |||
> multZeroLeftOneRightZero : (m : Nat) -> (n : Nat) -> (S m) * n = Z -> n = Z
> multZeroLeftOneRightZero m n prf = plusZeroLeftZero n (m * n) prf
> %freeze multZeroLeftOneRightZero

> |||
> multOneLeftOne : (m : Nat) -> (n : Nat) -> m * n = S Z -> m = S Z
> multOneLeftOne  Z     n    prf = absurd prf
> multOneLeftOne (S m)  Z    prf = absurd prf' where
>   prf' : Z = S Z
>   prf' = replace {x = (S m) * Z}
>                  {y = Z}
>                  {P = \ ZUZU => ZUZU = S Z}
>                  (multZeroRightZero (S m)) prf
> multOneLeftOne (S m) (S n) prf = eqSucc m Z s5 where
>   s1 : S (n + m * (S n)) = S Z
>   s1 = prf
>   s2 : n + m * (S n) = Z
>   s2 = succInjective (n + m * (S n)) Z s1
>   s3 : n = Z
>   s3 = plusZeroLeftZero n (m * (S n)) s2
>   s4 : m * (S n) = Z
>   s4 = plusZeroRightZero n (m * (S n)) s2
>   s5 : m = Z
>   s5 = multZeroRightOneLeftZero m n s4
> %freeze multOneLeftOne

> |||
> multOneRightOne : (m : Nat) -> (n : Nat) -> m * n = S Z -> n = S Z
> multOneRightOne m n prf = multOneLeftOne n m prf' where
>   prf' : n * m = S Z
>   prf' = replace {x = m * n} {y = n * m} {P = \ ZUZU => ZUZU = S Z} (multCommutative m n) prf
> %freeze multOneRightOne

> |||
> multPreservesEq : (m1 : Nat) -> (m2 : Nat) -> (n1 : Nat) -> (n2 : Nat) ->
>                   m1 = m2 -> n1 = n2 -> m1 * n1 = m2 * n2
> multPreservesEq m m n n Refl Refl = Refl
> %freeze multPreservesEq

> |||
> multMultElimLeft : (m1 : Nat) -> (m2 : Nat) -> (n1 : Nat) -> (n2 : Nat) ->
>                    m1 = m2 -> Not (m1 = Z) -> m1 * n1 = m2 * n2 ->
>                    n1 = n2
> multMultElimLeft _  _   Z      Z     _      _      _            = Refl
> multMultElimLeft m1 m2  Z     (S n2) m1EQm2 nm1EQZ m1ZEQm2sn2   =
>   void (nm1EQZ s4) where
>     s0  :  m1 * Z = m2 * (S n2)
>     s0  =  m1ZEQm2sn2
>     s1  :  Z = m2 * (S n2)
>     s1  =  replace {x = m1 * Z} {y = Z} {P = \ ZUZU => ZUZU = m2 * (S n2)} (multZeroRightZero m1) s0
>     s2  :  Z = m2
>     s2  =  sym (multZeroRightOneLeftZero m2 n2 (sym s1))
>     s3  :  m2 = Z
>     s3  =  sym s2
>     s4  :  m1 = Z
>     s4  =  replace (sym m1EQm2) s3
> multMultElimLeft m1 m2 (S n1)  Z     m1EQm2 nm1EQZ m1sn1EQm2Z   =
>   void (nm1EQZ s2) where
>     s0  :  m1 * (S n1) = m2 * Z
>     s0  =  m1sn1EQm2Z
>     s1  :  m1 * (S n1) = Z
>     s1  =  replace {x = m2 * Z} {y = Z} {P = \ ZUZU => m1 * (S n1) = ZUZU} (multZeroRightZero m2) s0
>     s2  :  m1 = Z
>     s2  =  multZeroRightOneLeftZero m1 n1 s1
> multMultElimLeft m1 m2 (S n1) (S n2) m1EQm2 nm1EQZ m1sn1EQm2sn2 =
>   eqSucc n1 n2 s5 where
>     s0  :  m1 * (S n1) = m2 * (S n2)
>     s0  =  m1sn1EQm2sn2
>     s1  :  (S n1) * m1 = (S n2) * m2
>     s1  =  replace2 {a = Nat} {a1 = m1 * (S n1)} {a2 = (S n1) * m1}
>                     {b = Nat} {b1 = m2 * (S n2)} {b2 = (S n2) * m2}
>                     {P = \ ZUZU => \ ZAZA => ZUZU = ZAZA}
>                     (multCommutative m1 (S n1)) (multCommutative m2 (S n2)) s0
>     s2  :  m1 + n1 * m1 = m2 + n2 * m2
>     s2  =  s1
>     s3  :  n1 * m1 = n2 * m2
>     s3  =  plusPlusElimLeft s2 m1EQm2
>     s4  :  m1 * n1 = m2 * n2
>     s4  =  replace2 {a = Nat} {a1 = n1 * m1} {a2 = m1 * n1}
>                     {b = Nat} {b1 = n2 * m2} {b2 = m2 * n2}
>                     {P = \ ZUZU => \ ZAZA => ZUZU = ZAZA}
>                     (multCommutative n1 m1) (multCommutative n2 m2) s3
>     s5  :  n1 = n2
>     s5  =  multMultElimLeft m1 m2 n1 n2 m1EQm2 nm1EQZ s4
> %freeze multMultElimLeft --

> |||
> multMultElimRight : (m1 : Nat) -> (m2 : Nat) -> (n1 : Nat) -> (n2 : Nat) ->
>                     n1 = n2 -> Not (n1 = Z) -> m1 * n1 = m2 * n2 ->
>                     m1 = m2
> multMultElimRight m1 m2 n1 n2 n1EQn2 nn1EQZ prf =
>   multMultElimLeft n1 n2 m1 m2 n1EQn2 nn1EQZ prf' where
>     prf' : n1 * m1 = n2 * m2
>     prf' = replace2 (multCommutative m1 n1) (multCommutative m2 n2) prf
> %freeze multMultElimRight --

> |||
> multElim1 : (m : Nat) -> (n : Nat) -> (S m) * n = S m -> n = S Z
> multElim1 m    Z  p = absurd s1 where
>   s1 : Z = S m
>   s1 = replace {x = (S m) * Z} {y = Z} {P = \ ZUZU => ZUZU = S m} (multZeroRightZero (S m)) p
> multElim1 m (S Z) _ = Refl
> multElim1 m (S (S n)) p = void (multSuccNotZero n m s5) where
>   s1 : (S (S n)) * (S m) = S m
>   s1 = replace {x = (S m) * (S (S n))}
>                {y = (S (S n)) * (S m)}
>                {P = \ ZUZU => ZUZU = S m}
>                (multCommutative (S m) (S (S n))) p
>   s2 : S m + (S n) * (S m) = S m
>   s2 = replace {x = (S (S n)) * (S m)}
>                {y = S m + (S n) * (S m)}
>                {P = \ ZUZU => ZUZU = S m}
>                Refl s1
>   s5 : (S n) * (S m) = Z
>   s5 = plusLeftLeftRightZero (S m) ((S n) * (S m)) s2
> %freeze multElim1

> |||
> multSwapLeft : (a, b, c : Nat) -> a * b * c = b * a * c
> multSwapLeft a b c = ( a * b * c )
>                    ={ Refl }=
>                      ( (a * b) * c )
>                    ={ cong {f = \ ZUZU => ZUZU * c} (multCommutative a b) }=
>                      ( (b * a) * c )
>                    ={ Refl }=
>                      ( b * a * c )
>                    QED
> %freeze multSwapLeft

> |||
> multSwapRight : (a, b, c : Nat) -> a * b * c = a * c * b
> multSwapRight a b c = ( a * b * c )
>                     ={ Refl }=
>                       ( (a * b) * c )
>                     ={ sym (multAssociative a b c) }=
>                       ( a * (b * c) )
>                     ={ cong (multCommutative b c) }=
>                       ( a * (c * b) )
>                     ={ multAssociative a c b }=
>                       ( (a * c) * b )
>                     ={ Refl }=
>                       ( a * c * b )
>                     QED
> %freeze multSwapRight

> |||
> multSwap23 : (a, b, c, d : Nat) -> (a * b) * (c * d) = (a * c) * (b * d)
> multSwap23 a b c d = ( (a * b) * (c * d) )
>                    ={ Refl }=
>                      ( a * b * (c * d) )
>                    ={ sym (multAssociative a b (c * d)) }=
>                      ( a * (b * (c * d)) )
>                    ={ cong {f = \ ZUZU => a * ZUZU} (multAssociative b c d) }=
>                      ( a * ((b * c) * d) )
>                    ={ cong {f = \ ZUZU => a * ZUZU} (multSwapLeft b c d) }=
>                      ( a * ((c * b) * d) )
>                    ={ cong {f = \ ZUZU => a * ZUZU} (sym (multAssociative c b d)) }=
>                      ( a * (c * (b * d)) )
>                    ={ multAssociative a c (b * d) }=
>                      ( a * c * (b * d) )
>                    ={ Refl }=
>                      ( (a * c) * (b * d) )
>                    QED
> %freeze multSwap23

> |||
> multSwap24 : (a, b, c, d : Nat) -> (a * b) * (c * d) = (a * d) * (c * b)
> multSwap24 a b c d = ( (a * b) * (c * d) )
>                    ={ cong {f = \ ZUZU => (a * b) * ZUZU} (multCommutative c d) }=
>                      ( (a * b) * (d * c) )
>                    ={ multSwap23 a b d c }=
>                      ( (a * d) * (b * c) )
>                    ={ cong {f = \ ZUZU => (a * d) * ZUZU} (multCommutative b c) }=
>                      ( (a * d) * (c * b) )
>                    QED
> %freeze multSwap24

> |||
> multFlipCentre : (m1 : Nat) -> (m2 : Nat) -> (n1 : Nat) -> (n2 : Nat) ->
>                  (m1 * m2) * (n1 * n2) = (m1 * n1) * (m2 * n2)
> multFlipCentre = multSwap23
> %freeze multFlipCentre

> |||
> multOneRightNeutralPlusMultZeroLeftZero : (m : Nat) -> (n : Nat) -> m * 1 + 0 * n = m
> multOneRightNeutralPlusMultZeroLeftZero m n =
>     ( m * 1 + 0 * n )
>   ={ cong (multZeroLeftZero n) }=
>     ( m * 1 + 0 )
>   ={ cong {f = \ ZUZU => ZUZU + 0} (multOneRightNeutral m) }=
>     ( m + 0 )
>   ={ plusZeroRightNeutral m }=
>     ( m )
>   QED
> %freeze multOneRightNeutralPlusMultZeroLeftZero

Properties of |sum|:

> ||| |sum| is monotone
> -- sumMon : Monotone {B = Nat} {C = Nat} {F = List} LTE LTE sum
> sumMon : {A : Type} ->
>          (f : A -> Nat) -> (g : A -> Nat) ->
>          (p : (a : A) -> f a `LTE` g a) ->
>          (as : List A) ->
>          sum (map f as) `LTE` sum (map g as)
> sumMon {A} f g p Nil = LTEZero
> sumMon {A} f g p (a :: as) = s5 where
>   s1 : sum (map f (a :: as)) = f a + sum (map f as)
>   s1 = Refl
>   s2 : sum (map g (a :: as)) = g a + sum (map g as)
>   s2 = Refl
>   s3 : f a `LTE` g a
>   s3 = p a
>   s4 : sum (map f as) `LTE` sum (map g as)
>   s4 = sumMon f g p as
>   s5 : sum (map f (a :: as)) `LTE` sum (map g (a :: as))
>   s5 = monotoneNatPlusLTE s3 s4
> %freeze sumMon

> {-

Test:

> CLTtoLT : {m, n : Nat} -> compare m n = LT -> m `LT` n

> LTtoCLT : {m, n : Nat} -> m `LT` n -> compare m n = LT

> CEQtoEQ : {m, n : Nat} -> compare m n = EQ -> m = n

> EQtoCEQ : {m, n : Nat} -> m = n -> compare m n = EQ

> anyPlusPreservesOrd : {x, y, z : Nat} -> {ORD : Ordering} ->
>                       compare x y = ORD -> compare (z + x) (z + y) = ORD

> plusAnyPreservesOrd : {x, y, z : Nat} -> {ORD : Ordering} ->
>                       compare x y = ORD -> compare (z + x) (z + y) = ORD

> LTinLTE : {m, n : Nat} -> LT m n -> LTE m n

> pLTpEQpLTE : (LT x1 x2 -> LT y1 y2) -> (x1 = x2 -> y1 = y2) -> (LTE x1 x2 -> LTE y1 y2)

> anyPlusPreservesLT : LT x y -> LT (z + x) (z + y)
> anyPlusPreservesLT {x} {y} {z} prf = s3 where
>   s1  :  compare x y = LT
>   s1  =  LTtoCLT prf
>   s2  :  compare (z + x) (z + y) = LT
>   s2  =  anyPlusPreservesOrd s1
>   s3  :  (z + x) `LT` (z + y)
>   s3  =  CLTtoLT s2

> anyPlusPreservesEQ : {x, y, z : Nat} -> x = y -> (z + x) = (z + y)
> anyPlusPreservesEQ {x} {y} {z} prf = s3 where
>   s1  :  compare x y = EQ
>   s1  =  EQtoCEQ prf
>   s2  :  compare (z + x) (z + y) = EQ
>   s2  =  anyPlusPreservesOrd s1
>   s3  :  (z + x) = (z + y)
>   s3  =  CEQtoEQ s2

> anyPlusPreservesLTE : LTE x y -> LTE (z + x) (z + y)
> anyPlusPreservesLTE = pLTpEQpLTE anyPlusPreservesLT anyPlusPreservesEQ

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module IO
import Cam.FFI

||| print native(idris side) object
public export
%inline
println : a -> IO ()
println s = believe_me $ fcall FFun1 (Builtin "println") $ believe_me s

||| print any foreign object
public export
%inline
fprintln : Boxed a -> IO ()
fprintln boxed = believe_me $ fcall FFun1 (Builtin "println") $ believe_me boxed

||| print any object
public export
%inline
putStrLn : String -> IO ()
putStrLn boxed = believe_me $ fcall FFun1 (Builtin "println") $ believe_me boxed

public export
%inline
toText : a -> Boxed String
toText a = believe_me . unsafePerformIO $ fcall FFun1 (Builtin "to_text") $ believe_me a

ext: idr

max_stars_repo_name: thautwarm/idris-cam

max_issues_repo_name: thautwarm/idris-cam

max_forks_repo_name: thautwarm/idris-cam


text:
module AppendVec

import Data.Nat
import Data.Vect

%default total

-- this works since the order of `n` and `m` follow the definition of `plus`
{-
append : Vect n elem -> Vect m elem -> Vect (n + m) elem
append [] ys = ys
append (x :: xs) ys = x :: append xs ys
-}

-- if we change up the order of `n` and `m`, the we have to prove that the
-- addition still holds

append_nil : Vect m elem -> Vect (plus m 0) elem
append_nil {m} xs = rewrite plusZeroRightNeutral m in xs

append_xs : Vect (S (m + k)) elem -> Vect (plus m (S k)) elem
append_xs {m} {k} xs = rewrite sym (plusSuccRightSucc m k) in xs

append : Vect n elem -> Vect m elem -> Vect (m + n) elem
append [] ys = append_nil ys
append (x :: xs) ys = append_xs (x :: append xs ys)

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
module Main

import Effects
import Effect.StdIO

import IdrisNet.Packet
import IdrisNet.PacketLang
import Network.Socket
import IdrisNet.TCP.TCPServer

import PacketStruct

printSimpleStruct : (mkTy simpleStruct) -> { [STDIO] } Eff IO ()
printSimpleStruct (s1 ## s2 ## (Left b_int) ## xs ## b1 ## b2 ## prf) = do
  putStr $ "S1: " ++ s1 ++ "\n"
  putStr $ "S2: " ++ s2 ++ "\n"
  putStr $ "b_int: " ++ (show b_int) ++ "\n"
  putStr $ "xs: " ++ (show xs) ++ "\n"
  putStr $ "b1: " ++ (show b1) ++ "\n"
  putStr $ "b2: " ++ (show b2) ++ "\n"
printSimpleStruct (s1 ## s2 ## (Right s3) ## xs ## b1 ## b2 ## prf) = do
  putStr $ "S1: " ++ s1 ++ "\n"
  putStr $ "S2: " ++ s2 ++ "\n"
  putStr $ "S3: " ++ s2 ++ "\n"
  putStr $ "xs: " ++ (show xs) ++ "\n"
  putStr $ "b1: " ++ (show b1) ++ "\n"
  putStr $ "b2: " ++ (show b2) ++ "\n"

sendResponse : { [STDIO, TCPSERVERCLIENT (ClientConnected)] ==>
                 [STDIO, TCPSERVERCLIENT ()] } Eff IO ()
sendResponse = do
  OperationSuccess _ <- tcpWritePacket simpleResponse simpleResponseInstance
    | RecoverableError _ => sendResponse
    | FatalError err => do putStr ("Fatal error: " ++ (show err))
                           tcpFinalise
    | ConnectionClosed => return ()
  putStr "Sent response!\n"
  tcpClose

clientTask' : { [STDIO, TCPSERVERCLIENT (ClientConnected)] ==>
                [STDIO, TCPSERVERCLIENT ()] } Eff IO ()
clientTask' = do
  OperationSuccess m_packet <- tcpReadPacket simpleStruct 1024
    | RecoverableError err => clientTask'
    | FatalError err => do putStr ("Fatal error: " ++ (show err) ++ "\n")
                           tcpFinalise
    | ConnectionClosed => return ()
  case m_packet of
       Just (packet, len) => do
         printSimpleStruct packet
         sendResponse
       Nothing => do
         putStr "Error decoding packet"
         tcpClose

clientTask : ClientProgram ()
clientTask = new clientTask'

packetServer : Port -> { [TCPSERVER (), STDIO] } Eff IO ()
packetServer p = do
  OperationSuccess _ <- bind Nothing p
    | RecoverableError err => return ()
    | FatalError err => do (putStr $ "Error binding: " ++ (show err))
                           return ()
    | ConnectionClosed => return ()
  OperationSuccess _ <- listen
    | RecoverableError _ => closeBound
    | FatalError err => do
        putStr ("Error listening: " ++ (show err))
        finaliseServer
    | ConnectionClosed => return ()
  OperationSuccess _ <- accept clientTask
    | RecoverableError _ => closeListening
    | FatalError err => do
        putStr ("Error accepting client: " ++ (show err))
        finaliseServer
  closeListening

main : IO ()
main = run (packetServer 1234)


text:
> module EscardoOliva.Operations

> import Data.List

> import EscardoOliva.SelectionFunction
> import EscardoOliva.Quantifier

> %default total
> %access public export
> %auto_implicits off

> |||
> overline : {X, R : Type} -> J R X -> K R X
> overline e p = p (e p)

> |||
> otimes : {X : Type} -> {R : Type} ->
>          J R X -> (X -> J R (List X)) -> J R (List X)
> otimes e f p = x :: xs where
>   x   =    e (\ x' => overline (f x') (\ xs' => p (x' :: xs')))
>   xs  =  f x (\ xs' => p (x :: xs'))

> |||
> partial
> bigotimes : {X, R : Type} -> List (List X -> J R X) -> J R (List X)
> bigotimes       []   =  \ p => []
> -- bigotimes (e :: es)  =  (e []) `otimes` (\x => bigotimes [\ xs => d (x :: xs) | d <- es])
> {-
> bigotimes {X} {R} (e :: es)  =  (e []) `otimes` f where
>   partial
>   f : X -> J R (List X)
>   f x = bigotimes (map h es) where
>     h : (List X -> J R X) -> List X -> J R X
>     h d = \ xs => d (x :: xs)
> -}
> bigotimes {X} {R} (e :: es)  =  let f = \ x => bigotimes (map (\ d => \ xs => d (x :: xs) ) es) in
>                                 (e []) `otimes` f

> {-

> ---}


text:
module ExerciseOne

import Data.Vect

%default total

-- | Ex1
-- | Write a function:
-- | > repeat : (n : Nat) -> a -> Vect n a
-- | which constructs a vector of n copies of an item.

repeat : (n : Nat) -> a -> Vect n a
repeat Z     _ = []
repeat (S k) e = e :: repeat k e

--------------------------------------------------------------------------------
-- 2. Consider the following functions over Lists:
--     take : Nat -> List a -> List a
--     drop : Nat -> List a -> List a
-- (a) What are the types of the corresponding functions for Vect, vtake and vdrop?
-- Hint: What are the invariants? i.e. how many items need to be in the vector in each case?
-- (b) Implement vtake and vdrop

-- | A. Types for Vect, vtake and vdrop
vtake : (n : Nat) -> Vect (n + m) t -> Vect n t
vtake Z     _         = []
vtake (S k) (x :: xs) = x :: vtake k xs

vdrop : (n : Nat) -> Vect (n + m) t -> Vect m t
vdrop Z     xs        = xs
vdrop (S k) (x :: xs) = vdrop k xs

--------------------------------------------------------------------------------
-- 3. A matrix is a 2-dimensional vector, and could be defined as follows:
Matrix : Nat -> Nat -> Type -> Type
Matrix n m a = Vect n (Vect m a)

-- (a) Using repeat, above, and Vect.zipWith, write a function which transposes a matrix.
-- Hints: Remember to think carefully about its type first! zipWith for vectors is defined as follows:
--         zipWith : (a -> b -> c) -> Vect a n -> Vect b n -> Vect c n
--         zipWith f []      []      = []
--         zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
transpose' : Matrix x y t -> Matrix y x t
transpose' {x = Z} []      = repeat _ []
transpose'         (x::xs) = zipWith (::) x (transpose' xs)

-- (b) Write a function to multiply two matrices.
matX : Num t => Matrix x y t -> Matrix y z t -> Matrix x z t
matX []    _  = []
matX (x::xs) ys = (map (sum . zipWith (*) x) $ transpose' ys) :: (matX xs ys)

--------------------------------------------------------------------------------
-- 4. The following view describes a pair of numbers as a difference:
data Cmp : Nat -> Nat -> Type where
  cmpLT : (y : _) -> Cmp x (x + S y)
  cmpEQ : Cmp x x
  cmpGT : (x : _) -> Cmp (y + S x) y

-- (a) Write the function cmp : (n : Nat) -> (m : Nat) -> Cmp n m
--   which proves that every pair of numbers can be expressed in this way.
-- Hint: recall parity from the lecture. You will find the with construct very useful!
cmp' : (n : Nat) -> (m : Nat) -> Cmp n m
cmp'  Z     Z    = cmpEQ {x = Z}
cmp'  Z    (S k) = cmpLT k
cmp' (S k)  Z    = cmpGT k
cmp' (S k) (S j) with (cmp' k j)
  cmp' (S k) (S k) | cmpEQ = cmpEQ {x = S k}
  cmp' (S k) (S (k + S h)) | cmpLT h = cmpLT h
  cmp' (S (j + S h)) (S j) | cmpGT h = cmpGT h

-- (b) Assume you have a vector xs : Vect a n, where n is unknown.
--   How could you use cmp to construct a suitable input to vtake and vdrop from xs?

-- >>> Huh? What is this even asking?

--------------------------------------------------------------------------------
-- 5. Implement the following functions:
--   plus_nSm : (n : Nat) -> (m : Nat) -> n + S m = S (n + m)
--   plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
--   plus_assoc : (n : Nat) -> (m : Nat) -> (p : Nat) ->
--                n + (m + p) = (n + m) + p

--------------------------------------------------------------------------------
-- 6. One way to define a reverse function for lists is as follows:
--   reverse : List a -> List a
--   reverse xs = revAcc [] xs where
--     revAcc : List a -> List a -> List a
--     revAcc acc [] = acc
--     revAcc acc (x :: xs) = revAcc (x :: acc) xs
-- Write the equivalent function for vectors, vect reverse : Vect a
-- n ->
-- Hint: You can use the same structure as the definition for List, but you will need to think carefully
-- Vect a n
-- about the type for revAcc, and may need to do some theorem proving.

--------------------------------------------------------------------------------
-- 7. You are given the following definition of binary trees:
-- data Tree a = Leaf | Node (Tree a) a (Tree a)
-- Define a membership predicate ElemTree and a function elemInTree which calculates whether a
-- value in in the tree, and a corresponding proof.
--     data ElemTree  : a -> Tree a -> Type where ...
--     elemInTree : DecEq a =>
--                  (x : a) -> (t : Tree a) -> Maybe (ElemTree x t)

max_stars_repo_name: expede/idris-exercises

max_issues_repo_name: expede/idris-exercises

max_forks_repo_name: expede/idris-exercises


text:
module Language.LSP.Message.Rename

import Language.JSON
import Language.LSP.Message.Derive
import Language.LSP.Message.Location
import Language.LSP.Message.Progress
import Language.LSP.Message.TextDocument
import Language.LSP.Message.Utils
import Language.Reflection

%language ElabReflection
%default total

namespace PrepareSupportDefaultBehaviour
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_rename
  public export
  data PrepareSupportDefaultBehaviour = Identifier

export
ToJSON PrepareSupportDefaultBehaviour where
  toJSON Identifier = JNumber 1

export
FromJSON PrepareSupportDefaultBehaviour where
  fromJSON (JNumber 1) = pure Identifier
  fromJSON _ = neutral

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_rename
public export
record RenameClientCapabilities where
  constructor MkRenameClientCapabilities
  dynamicRegistration            : Maybe Bool
  prepareSupport                 : Maybe Bool
  prepareSupportDefaultBehaviour : Maybe PrepareSupportDefaultBehaviour
  honorsChangeAnnotation         : Maybe Bool
%runElab deriveJSON defaultOpts `{{RenameClientCapabilities}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_rename
public export
record RenameOptions where
  constructor MkRenameOptions
  workDoneProgress : Maybe Bool
  prepareProvider  : Maybe Bool
%runElab deriveJSON defaultOpts `{{RenameOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_rename
public export
record RenameRegistrationOptions where
  constructor MkRenameRegistrationOptions
  workDoneProgress : Maybe Bool
  prepareProvider  : Maybe Bool
  documentSelector : OneOf [DocumentSelector, Null]
%runElab deriveJSON defaultOpts `{{RenameRegistrationOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_rename
public export
record RenameParams where
  constructor MkRenameParams
  workDoneToken : Maybe ProgressToken
  textDocument  : TextDocumentIdentifier
  newName       : String
%runElab deriveJSON defaultOpts `{{RenameParams}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_prepareRename
public export
record PrepareRenameParams where
  constructor MkPrepareRenameParams
  textDocument : TextDocumentIdentifier
  position     : Position
%runElab deriveJSON defaultOpts `{{PrepareRenameParams}}

namespace PrepareRenameResponse
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_prepareRename
  public export
  record PrepareRenameDefaultResponse where
    constructor MkPrepareRenameDefaultResponse
    defaultBehaviour : Bool
  %runElab deriveJSON defaultOpts `{{PrepareRenameDefaultResponse}}

  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_prepareRename
  public export
  record PrepareRenamePlaceholderResponse where
    constructor MkPrepareRenamePlaceholderResponse
    range       : Range
    placeholder : String
  %runElab deriveJSON defaultOpts `{{PrepareRenamePlaceholderResponse}}


text:
module Control.App.Terminal

import Data.Maybe
import Control.App.Console
import System.IO.Terminal as T

-- ---------------------------------------------------------------------------

export
[terminal] PrimIO e => Console e where
  putChar c = primIO $ T.putChar c
  putStr str = primIO $ T.putStr str
  getChar = primIO $ T.getChar >>= pure . fromMaybe (cast (the Int (-1)))
  getLine = primIO $ T.getLine >>= pure . fromMaybe ""

-- ---------------------------------------------------------------------------
-- vim: tw=80 sw=2 expandtab :


text:
module Quantities.Information

import Quantities.Core

%default total
%access public export

Information : Dimension
Information = MkDimension "Information"

Bit : ElemUnit Information
Bit = MkElemUnit "bit" 1

Byte : ElemUnit Information
Byte = < one "byte" equals 8 Bit >

-- Binary prefixes for multiples of bits/bytes
-- Based on http://en.wikipedia.org/wiki/Binary_prefix

twoToTheTen : String -> Nat -> ElemUnit q -> ElemUnit q
twoToTheTen pre power (MkElemUnit name f) =
  < one (pre ++ name) equals (pow 1024.0 power) (MkElemUnit name f) >

kibi : ElemUnit q -> ElemUnit q
kibi = twoToTheTen "kibi" 1
ki : ElemUnit q -> ElemUnit q
ki = kibi

mebi : ElemUnit q -> ElemUnit q
mebi = twoToTheTen "mebi" 2
mi : ElemUnit q -> ElemUnit q
mi = mebi

gibi : ElemUnit q -> ElemUnit q
gibi = twoToTheTen "gibi" 3
gi : ElemUnit q -> ElemUnit q
gi = gibi

tebi : ElemUnit q -> ElemUnit q
tebi = twoToTheTen "tebi" 4
ti : ElemUnit q -> ElemUnit q
ti = tebi

pebi : ElemUnit q -> ElemUnit q
pebi = twoToTheTen "pebi" 5
pi : ElemUnit q -> ElemUnit q
pi = pebi

exbi : ElemUnit q -> ElemUnit q
exbi = twoToTheTen "exbi" 6
ei : ElemUnit q -> ElemUnit q
ei = exbi

zebi : ElemUnit q -> ElemUnit q
zebi = twoToTheTen "zebi" 7
zi : ElemUnit q -> ElemUnit q
zi = zebi

yobi : ElemUnit q -> ElemUnit q
yobi = twoToTheTen "yobi" 8
yi : ElemUnit q -> ElemUnit q
yi = yobi

-- Please Note: kibi byte /= kilo byte

max_stars_repo_name: timjb/quantities

max_issues_repo_name: timjb/quantities

max_forks_repo_name: timjb/quantities


text:
module ErlPrelude

%access export

data ErlFn : Type -> Type where
  MkErlFun : (x : t) -> ErlFn t
%used MkErlFun x

public export
data ErlRaw : Type -> Type where
  MkERaw : (x:t) -> ErlRaw t
%used MkERaw x

data Atom : Type

data Erl_NumTypes: Type -> Type where
  Erl_IntChar    : Erl_NumTypes Char
  Erl_IntNative  : Erl_NumTypes Int
  Erl_Double     : Erl_NumTypes Double

mutual
  data Erl_FunTypes : Type -> Type where
    Erl_Fun     : Erl_Types s -> Erl_FunTypes t -> Erl_FunTypes (s -> t)
    Erl_FunIO   : Erl_Types t -> Erl_FunTypes (EIO t)
    Erl_FunBase : Erl_Types t -> Erl_FunTypes t

  public export
  data Erl_Types : Type -> Type where
    Erl_Str  : Erl_Types String
    Erl_Atom : Erl_Types Atom
    Erl_Ptr  : Erl_Types Ptr
    Erl_Unit : Erl_Types ()
    Erl_List : Erl_Types a -> Erl_Types (List a)
    Erl_FunT : Erl_FunTypes a -> Erl_Types (ErlFn a)
    Erl_NumT : Erl_NumTypes t -> Erl_Types t
    Erl_Raw  : Erl_Types (ErlRaw a)

  public export
  FFI_Erl : FFI
  FFI_Erl = MkFFI Erl_Types String String

  public export
  -- Make your "Old MacDonald" jokes here please
  EIO : Type -> Type
  EIO = IO' FFI_Erl

%inline
public export
erlcall : (fname : String) -> (ty : Type) -> {auto fty : FTy FFI_Erl [] ty} -> ty
erlcall fname ty = foreign FFI_Erl fname ty

%inline
public export
Erl_Export : Type
Erl_Export = FFI_Export FFI_Erl "" []

ErlPid : Type
ErlPid = Ptr

-- Annoyingly, the File struct is abstract so we can't use it. I guess
-- this helps prevent people mixing the two kinds of files... not that
-- it would even be possible.
data EFile = EHandle Ptr

namespace Erl
  stdin : EFile
  stdin = EHandle prim__stdin

  stdout : EFile
  stdout = EHandle prim__stdout

  stderr : EFile
  stderr = EHandle prim__stderr

  openFile : String -> Mode -> EIO EFile
  openFile filename mode = do p <- open filename (modeStr mode)
                              pure (EHandle p)
    where modeStr : Mode -> String
          modeStr Read = "r"
          modeStr Write = "w"
          modeStr ReadWrite = "rw"

          open : String -> String -> EIO Ptr
          open = foreign FFI_Erl "idris_erlang_rts:file_open" (String -> String -> EIO Ptr)

  closeFile : EFile -> EIO ()
  closeFile (EHandle p) = do x <- close p
                             pure ()
    where close : Ptr -> EIO Int
          close = foreign FFI_Erl "idris_erlang_rts:file_close" (Ptr -> EIO Int)

  fgetc' : EFile -> EIO (Maybe Char)
  fgetc' (EHandle h) = do c <- getChar h
                          pure $ if (c < 0)
                                 then Nothing
                                 else (Just (cast c))
    where getChar : Ptr -> EIO Int
          getChar = foreign FFI_Erl "idris_erlang_rts:read_chr" (Ptr -> EIO Int)

  fgetc : EFile -> EIO Char
  fgetc (EHandle h) = do c <- getChar h
                         pure (cast c)
    where getChar : Ptr -> EIO Int
          getChar = foreign FFI_Erl "idris_erlang_rts:read_chr" (Ptr -> EIO Int)

  fread : EFile -> EIO String
  fread (EHandle h) = prim_fread h

  fwrite : EFile -> String -> EIO ()
  fwrite (EHandle h) s = do writeFile h s
                            pure ()
    where writeFile : Ptr -> String -> EIO Int
          writeFile = foreign FFI_Erl "idris_erlang_rts:write_file" (Ptr -> String -> EIO Int)

  feof : EFile -> EIO Bool
  feof (EHandle h) = do res <- fileEOF h
                        pure (res /= 0)
    where fileEOF : Ptr -> EIO Int
          fileEOF = foreign FFI_Erl "idris_erlang_rts:file_eof" (Ptr -> EIO Int)

  fflush : EFile -> EIO ()
  fflush (EHandle h) = do fileFlush h
                          pure ()
    where fileFlush : Ptr -> EIO Int
          fileFlush = foreign FFI_Erl "idris_erlang_rts:file_flush" (Ptr -> EIO Int)

  putChar : Char -> EIO ()
  putChar c = putStr' (singleton c)

  getChar : EIO Char
  getChar = fgetc stdin

  nullStr : String -> EIO Bool
  nullStr s = do res <- strIsNull s
                 pure (res /= 0)
    where strIsNull : String -> EIO Int
          strIsNull = foreign FFI_Erl "idris_erlang_rts:str_null" (String -> EIO Int)

  nullPtr : Ptr -> EIO Bool
  nullPtr p = do res <- isNull p
                 pure (res /= 0)
    where isNull : Ptr -> EIO Int
          isNull = foreign FFI_Erl "idris_erlang_rts:ptr_null" (Ptr -> EIO Int)

  eqPtr : Ptr -> Ptr -> EIO Bool
  eqPtr x y = do res <- ptrIsEq x y
                 pure (res /= 0)
    where ptrIsEq : Ptr -> Ptr -> EIO Int
          ptrIsEq = foreign FFI_Erl "idris_erlang_rts:ptr_eq" (Ptr -> Ptr -> EIO Int)

  validFile : EFile -> EIO Bool
  validFile (EHandle h) = do res <- nullPtr h
                             pure (not res)

  partial
  readFile : String -> EIO String
  readFile fn = do f <- openFile fn Read
                   c <- readFile' f ""
                   closeFile f
                   pure c
    where
      partial
      readFile' : EFile -> String -> EIO String
      readFile' f contents = do res <- feof f
                                if (not res)
                                then do l <- fread f
                                        readFile' f (contents ++ l)
                                else pure contents

atom : String -> EIO Atom
atom = foreign FFI_Erl "list_to_atom" (String -> EIO Atom)

max_stars_repo_name: lenary/idris-erlang

max_issues_repo_name: yurrriq/idris-erlang

max_forks_repo_name: yurrriq/idris-erlang


text:
> module Pairs.Operations

> import Sigma.Sigma

> %default total
> %access public export
> %auto_implicits on

> -- %hide getWitness
> -- %hide getProof

> {-

> namespace Exists
>   getWitness : {P : a -> Type} -> Exists {a} P -> a
>   getWitness (Evidence x pf) = x
>   getProof : {P : a -> Type} -> (x : Exists {a} P) -> P (getWitness x)
>   getProof (Evidence x pf) = pf

> namespace Subset
>   getWitness : {P : a -> Type} -> Subset a P -> a
>   getWitness (Element x pf) = x
>   getProof : {P : a -> Type} -> (x : Subset a P) -> P (getWitness x)
>   getProof (Element x pf) = pf

> ---}

> namespace Sigma
>   getWitness : {P : a -> Type} -> Sigma a P -> a
>   getWitness (MkSigma x pf) = x
>   getProof : {P : a -> Type} -> (x : Sigma a P) -> P (getWitness x)
>   getProof (MkSigma x pf) = pf


text:
module Client.Skeleton.BaseWithTest.InigoTOML

import Fmt

export
name : (String, String) -> List String
name = const ["Inigo.toml"]

export
build : (String, String) -> String
build (packageNS, packageName) = fmt """
ns=\"%s\"
package=\"%s\"
version=\"0.0.1\"

description=\"\"
link=\"\"
readme=\"\"
modules=[\"%s\"]
depends=[]
license=\"\"
main=\"%s\"
executable=\"%s\"

[deps]

[dev-deps]
Base.IdrTest=\"~0.0.1\"
""" packageNS packageName packageName packageName packageName

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module System.File.Buffer

import public System.File.Error
import System.File.Handle
import System.File.Meta
import System.File.Mode
import System.File.ReadWrite
import System.File.Support
import public System.File.Types

import Data.Buffer

%default total

%foreign support "idris2_readBufferData"
         "node:lambda:(f,b,l,m) => require('fs').readSync(f.fd,b,l,m)"
prim__readBufferData : FilePtr -> Buffer -> (offset : Int) -> (maxbytes : Int) -> PrimIO Int

%foreign support "idris2_writeBufferData"
         "node:lambda:(f,b,l,m) => require('fs').writeSync(f.fd,b,l,m)"
prim__writeBufferData : FilePtr -> Buffer -> (offset : Int) -> (maxbytes : Int) -> PrimIO Int

||| Read the data from the file into the given buffer.
|||
||| @ fh       the file handle to read from
||| @ buf      the buffer to read the data into
||| @ offset   the position in buffer to start adding
||| @ maxbytes the maximum size to read; must not exceed buffer length
export
readBufferData : HasIO io => (fh : File) -> (buf : Buffer) ->
                 (offset : Int) ->
                 (maxbytes : Int) ->
                 io (Either FileError ())
readBufferData (FHandle h) buf offset max
    = do read <- primIO (prim__readBufferData h buf offset max)
         if read >= 0
            then pure (Right ())
            else pure (Left FileReadError)

||| Write the data from the buffer to the given `File`.
||| (If you do not have a `File` and just want to write to a file at a known
||| path, you probably want to use `writeBufferToFile`.)
|||
||| @ fh       the file handle to write to
||| @ buf      the buffer from which to get the data to write
||| @ offset   the position in buffer to write from
||| @ maxbytes the maximum size to write; must not exceed buffer length
export
writeBufferData : HasIO io => (fh : File) -> (buf : Buffer) ->
                  (offset : Int) ->
                  (maxbytes : Int) ->
                  io (Either FileError ())
writeBufferData (FHandle h) buf offset max
    = do written <- primIO (prim__writeBufferData h buf offset max)
         if written >= 0
            then pure (Right ())
            else pure (Left FileWriteError)

||| Attempt to write the data from the buffer to the file at the specified file
||| name.
|||
||| @ fn   the file name to write to
||| @ buf  the buffer from which to get the data to write
||| @ max the maximum size to write; must not exceed buffer length
export
writeBufferToFile : HasIO io => (fn : String) -> (buf : Buffer) -> (max : Int) ->
                                io (Either FileError ())
writeBufferToFile fn buf max
    = do Right f <- openFile fn WriteTruncate
             | Left err => pure (Left err)
         Right ok <- writeBufferData f buf 0 max
             | Left err => pure (Left err)
         closeFile f
         pure (Right ok)

||| Create a new buffer by opening a file and reading its contents into a new
||| buffer whose size matches the file size.
|||
||| @ fn the name of the file to read
export
createBufferFromFile : HasIO io => (fn : String) -> io (Either FileError Buffer)
createBufferFromFile fn
    = do Right f <- openFile fn Read
             | Left err => pure (Left err)
         Right size <- fileSize f
             | Left err => pure (Left err)
         Just buf <- newBuffer size
             | Nothing => pure (Left FileReadError)
         Right ok <- readBufferData f buf 0 size
             | Left err => pure (Left err)
         closeFile f
         pure (Right buf)


text:
module Test.Assert

import Crayons

%access export

success : String -> String
success s = green ("✔ " <+> s)

failure : String -> String
failure s = red ("✖ " <+> s)

assertEq : Eq a => (desc : String) -> (given : a) -> (expected : a) -> IO ()
assertEq desc g e = if g == e
  then putStrLn (success desc)
  else putStrLn (failure desc)

assertNotEq : Eq a => (desc : String) -> (given : a) -> (expected : a) -> IO ()
assertNotEq desc g e = if not (g == e)
  then putStrLn (success desc)
  else putStrLn (failure desc)

assertTrue : (desc : String) -> Bool -> IO ()
assertTrue desc p = if p
  then putStrLn (success desc)
  else putStrLn (failure desc)

assertFalse : (desc : String) -> Bool -> IO ()
assertFalse desc p = if (not p)
  then putStrLn (success desc)
  else putStrLn (failure desc)

max_stars_repo_name: Risto-Stevcev/idris-assert

max_issues_repo_name: Risto-Stevcev/idris-assert

max_forks_repo_name: Risto-Stevcev/idris-assert


text:
module Gen.Abs

import Gen.Env
import Data.SortedMap
import Control.Monad.Identity
import Control.Monad.Trans
import Control.Monad.Reader

public export
Abstracted : Type -> Type -> Type -> Type
Abstracted i e a = Reader (Environment i e) a

public export
interface Ord i => Abstract i e a where
	abstr : a -> Abstracted i e a

export
implementation Abstract i e a => Abstract i e (List a) where
	abstr xs = for xs abstr

export
abstractOver : Abstract i e a => List i -> a -> List e -> a
abstractOver [] m _  = m
abstractOver xs m vs = runIdentity $ runReaderT (abstr m) (fromList $ zip xs vs)

max_stars_repo_name: totalscript/totalscript

max_issues_repo_name: totalscript/totalscript

max_forks_repo_name: totalscript/totalscript


text:
||| Implementation of a Idris2 LSP Server.
|||
||| (C) The Idris Community, 2021
module Server.Main

import Core.Context
import Core.Core
import Core.InitPrimitives
import Core.Metadata
import Core.UnifyState
import Compiler.Common
import Data.List1
import Data.String
import Idris.CommandLine
import Idris.Env
import Idris.REPL.Opts
import Idris.REPL.Common
import Idris.Package.Types
import Idris.SetOptions
import Idris.Syntax
import Idris.Version
import IdrisPaths
import Language.JSON
import Language.LSP.Message
import Libraries.Utils.Path
import Server.Configuration
import Server.Log
import Server.ProcessMessage
import Server.Response
import Server.Utils
import System
import System.Directory
import System.File

data Header = ContentLength Int | ContentType String | StartContent

Show Header where
  show (ContentLength l) = "Content-Length: " ++ show l
  show (ContentType s) = "Content-Type: " ++ s
  show StartContent = "stop"

headerPart : List Header -> String
headerPart [] = ""
headerPart (ContentLength l :: xs) = "Content-Length: " ++ show l ++ "\r\n" ++ headerPart xs
headerPart (ContentType s :: xs) = "Content-Type: " ++ s ++ "\r\n" ++ headerPart xs
headerPart (StartContent :: _) = "\r\n"

parseHeader : String -> Maybe Header
parseHeader "\r\n" = Just StartContent
parseHeader str =
  if "Content-Length:" `isPrefixOf` str
     then let (_ ::: xs) = split (== ':') str in
              ContentLength <$> parseInteger (fastAppend xs)
     else if "Content-Type:" `isPrefixOf` str
             then let (_ ::: xs) = split (== ':') str in
                      Just $ ContentType (fastAppend xs)
             else Nothing

parseHeaderPart : (h : File) -> Core (Either FileError (Maybe Int))
parseHeaderPart h = do
  Right line <- fGetHeader h
    | Left err => pure $ Left err
  case parseHeader line of
    Just (ContentLength l) => parseHeaderPart h *> pure (Right (Just l))
    Just (ContentType s) => parseHeaderPart h
    Just StartContent => pure $ Right Nothing
    Nothing => pure $ Right Nothing

handleMessage : Ref LSPConf LSPConfiguration
            => Ref Ctxt Defs
            => Ref UST UState
            => Ref Syn SyntaxInfo
            => Ref MD Metadata
            => Ref ROpts REPLOpts
            => Core ()
handleMessage = do
  inputHandle <- gets LSPConf inputHandle
  Right (Just l) <- parseHeaderPart inputHandle
    | _ => sendUnknownResponseMessage parseError
  Right msg <- coreLift $ fGetChars inputHandle l
    | Left err => do
      logShow Error (show err)
      sendUnknownResponseMessage (internalError "Error while recovering the content part of a message")
  logString Debug msg
  let Just msg = parse msg
    | _ => sendUnknownResponseMessage parseError
  let JObject fields = msg
    | _ => sendUnknownResponseMessage (invalidRequest "Message is not object")
  let Just (JString "2.0") = lookup "jsonrpc" fields
    | _ => sendUnknownResponseMessage (invalidRequest "jsonrpc is not \"2.0\"")
  case lookup "method" fields of
    Just methodJSON => do -- request or notification
      case lookup "id" fields of
        Just idJSON => do -- request
          let Just id = fromJSON {a=OneOf [Int, String]} idJSON
            | _ => sendUnknownResponseMessage (invalidRequest "id is not int or string")
          let Just method = fromJSON {a=Method Client Request} methodJSON
            | _ => sendResponseMessage Initialize $ Failure (extend id) methodNotFound
          logString Info $ "Received request for method " ++ show (toJSON method)
          let Just params = fromMaybeJSONParameters method (lookup "params" fields)
            | _ => sendResponseMessage method $ Failure (extend id) (invalidParams "Invalid params for send \{show methodJSON}")
          -- handleRequest can be modified to use a callback if needed
          result <- catch (handleRequest method params) $ \err => do
            logString Error (show err)
            resetContext (Virtual Interactive)
            pure $ Left (MkResponseError (Custom 4) (show err) JNull)
          sendResponseMessage method $ case result of
            Left error => Failure (extend id) error
            Right result => Success (extend id) result

        Nothing => do -- notification
          let Just method = fromJSON {a=Method Client Notification} methodJSON
            | _ => sendUnknownResponseMessage methodNotFound
          logString Info $ "Received notification for method " ++ show (toJSON method)
          let Just params = fromMaybeJSONParameters method (lookup "params" fields)
            | _ => sendUnknownResponseMessage (invalidParams "Invalid params for send \{show methodJSON}")
          catch (handleNotification method params) $ \err => do
            logString Error (show err)
            resetContext (Virtual Interactive)

    Nothing => do -- response
      let Just idJSON = lookup "id" fields
        | _ => sendUnknownResponseMessage (invalidRequest "Message does not have method or id")
      logString Warning "Ignoring response with id \{show idJSON}"

runServer : Ref LSPConf LSPConfiguration
         => Ref Ctxt Defs
         => Ref UST UState
         => Ref Syn SyntaxInfo
         => Ref MD Metadata
         => Ref ROpts REPLOpts
         => Core ()
runServer = do
  handleMessage
  runServer

main : IO ()
main = do
  coreRun (do l <- newRef LSPConf defaultConfig
              defs <- initDefs
              c <- newRef Ctxt defs
              s <- newRef Syn initSyntax
              addPrimitives
              bprefix <- coreLift $ idrisGetEnv "IDRIS2_PREFIX"
              the (Core ()) $ case bprefix of
                   Just p => setPrefix p
                   Nothing => setPrefix yprefix
              bpath <- coreLift $ idrisGetEnv "IDRIS2_PATH"
              the (Core ()) $ case bpath of
                   Just path => do traverseList1_ addExtraDir (map trim (split (==pathSeparator) path))
                   Nothing => pure ()
              bdata <- coreLift $ idrisGetEnv "IDRIS2_DATA"
              the (Core ()) $ case bdata of
                   Just path => do traverseList1_ addDataDir (map trim (split (==pathSeparator) path))
                   Nothing => pure ()
              blibs <- coreLift $ idrisGetEnv "IDRIS2_LIBS"
              the (Core ()) $ case blibs of
                   Just path => do traverseList1_ addLibDir (map trim (split (==pathSeparator) path))
                   Nothing => pure ()
              pdirs <- coreLift $ idrisGetEnv "IDRIS2_PACKAGE_PATH"
              the (Core ()) $ case pdirs of
                   Just path => do traverseList1_ addPackageDir (map trim (split (==pathSeparator) path))
                   Nothing => pure ()
              cg <- coreLift $ idrisGetEnv "IDRIS2_CG"
              the (Core ()) $ case cg of
                   Just e => case getCG (options defs) e of
                                  Just cg => setCG cg
                                  Nothing => throw (InternalError ("Unknown code generator " ++ show e))
                   Nothing => pure ()
              addPkgDir "prelude" anyBounds
              addPkgDir "base" anyBounds
              addDataDir (prefix_dir (dirs (options defs)) </> ("idris2-" ++ showVersion False version) </> "support")
              addLibDir (prefix_dir (dirs (options defs)) </> ("idris2-" ++ showVersion False version) </> "lib")
              Just cwd <- coreLift $ currentDir
                | Nothing => throw (InternalError "Can't get current directory")
              addLibDir cwd
              o <- newRef ROpts (Opts.defaultOpts Nothing (REPL False) [])
              u <- newRef UST initUState
              m <- newRef MD (initMetadata (Virtual Interactive))
              runServer)
    (\err => fPutStrLn stderr ("CRITICAL UNCAUGHT ERROR " ++ show err) *> exitWith (ExitFailure 1))
    (\res => pure ())


text:
module Sub12Apply108x90

import ProofColDivSeqBase
import ProofColDivSeqPostulate

%default total
-- %language ElabReflection

-- 3(36x+30) --F[5,-2]->B[1,-2]--> 3(16x+13)
fb108x90To48x39 :
  (o:Nat) -> P (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                              (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))
                                        (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))) (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))  (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                 (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))))))))))) 2
    -> P (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))))))))))))))) 2
fb108x90To48x39 o prf =
  let prf2 = lvDown (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                              (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))
                                        (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))) (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))  (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                 (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))))))))))) 2
                    prf in
    let prf3 = fb108x90To48x39' o prf2 in lvDown (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))))))))))))))) 3 prf3

export
apply108x90 : P (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                              (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))
                                        (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))) (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))  (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                 (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))))))))))) 2
  -> (m : Nat **
        (LTE (S m)
             (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                 (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))
                                           (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                          (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))
                                     (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                    (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))))))))))),
         P m 2))
apply108x90 {o} col = let col2 = fb108x90To48x39 o col in ((S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))))))))))))))
                                                           ** (lte108x90 o, col2)) where
  lte108x90 : (o:Nat) -> LTE (S (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))
                                                          (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))))))))))))))))
          (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                              (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))
                                        (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))) (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))                                  (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                 (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))))))))
  lte108x90 Z = (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc) LTEZero
  lte108x90 (S o) = let lemma = lte108x90 o in
    rewrite (sym (plusSuccRightSucc o o)) in
    rewrite (sym (plusSuccRightSucc (plus o o)  (S (plus o o)))) in
    rewrite (sym (plusSuccRightSucc (plus o o)  (plus o o))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) (plus o o))  (S (S (S (plus (plus o o) (plus o o))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) (plus o o))  (S (S (plus (plus o o) (plus o o)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) (plus o o))  (S (plus (plus o o) (plus o o))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) (plus o o))  (plus (plus o o) (plus o o)))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (S (S (S (S (S (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (S (S (S (S (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (S (S (S (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (S (S (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (S (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o)))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o))))) in

    rewrite (sym (plusSuccRightSucc (plus o o)  o)) in

    rewrite (sym (plusSuccRightSucc (plus (plus o o) o)  (S (S (S (S (plus (plus o o) o))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) o)  (S (S (S (plus (plus o o) o)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) o)  (S (S (plus (plus o o) o))))) in

    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))  (S (S (S (S (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))  (S (S (S (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))  (S (S (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))  (S (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))  (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))  (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))) in

    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))
                                    (S (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o)
                                            o))))))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))
                                    (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o)
                                            o)))))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))
                                    (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o)
                                            o))))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))
                                    (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o)
                                            o)))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))
                                    (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o)
                                            o))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))
                                    (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o)
                                            o)))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))
                                    (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o)
                                            o))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))
                                    (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o)
                                            o)))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))
                                    (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o)
                                            o))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))
                                    (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o)
                                            o)))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))
                                    (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o)
                                            o))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))
                                    (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o)
                                            o)))))))))))) in

    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))
                                                                                (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))))))
                                    (S (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o
                                                                                o) o)
                                                                                (S (S (plus (plus o o)
                                                                                o))))
                                                                                (S (S (plus (plus (plus o o)
                                                                                o) (S (S (plus (plus o o)
    o))))))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))
                                                                                (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))))))
                                    (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o
                                                                                o) o)
                                                                                (S (S (plus (plus o o)
                                                                                o))))
                                                                                (S (S (plus (plus (plus o o)
                                                                                o) (S (S (plus (plus o o)
    o)))))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))
                                                                                (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))))))
                                    (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o
                                                                                o) o)
                                                                                (S (S (plus (plus o o)
                                                                                o))))
                                                                                (S (S (plus (plus (plus o o)
                                                                                o) (S (S (plus (plus o o)
    o))))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))
                                                                                (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))))))
                                    (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o
                                                                                o) o)
                                                                                (S (S (plus (plus o o)
                                                                                o))))
                                                                                (S (S (plus (plus (plus o o)
                                                                                o) (S (S (plus (plus o o)
    o)))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))
                                                                                (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))))))
                                    (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o
                                                                                o) o)
                                                                                (S (S (plus (plus o o)
                                                                                o))))
                                                                                (S (S (plus (plus (plus o o)
                                                                                o) (S (S (plus (plus o o)
    o))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))
                                                                                (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))))))
                                    (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o
                                                                                o) o)
                                                                                (S (S (plus (plus o o)
                                                                                o))))
                                                                                (S (S (plus (plus (plus o o)
                                                                                o) (S (S (plus (plus o o)
    o)))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))
                                                                                (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))))))
                                    (S (S (S (S (S (S (S (S (plus (plus (plus (plus o
                                                                                o) o)
                                                                                (S (S (plus (plus o o)
                                                                                o))))
                                                                                (S (S (plus (plus (plus o o)
                                                                                o) (S (S (plus (plus o o)
    o))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))
                                                                                (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))))))
                                    (S (S (S (S (S (S (S (plus (plus (plus (plus o
                                                                                o) o)
                                                                                (S (S (plus (plus o o)
                                                                                o))))
                                                                                (S (S (plus (plus (plus o o)
                                                                                o) (S (S (plus (plus o o)
    o)))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))
                                                                                (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))))))
                                    (S (S (S (S (S (S (plus (plus (plus (plus o
                                                                                o) o)
                                                                                (S (S (plus (plus o o)
                                                                                o))))
                                                                                (S (S (plus (plus (plus o o)
                                                                                o) (S (S (plus (plus o o)
    o))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))
                                                                                (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))))))
                                    (S (S (S (S (S (plus (plus (plus (plus o
                                                                                o) o)
                                                                                (S (S (plus (plus o o)
                                                                                o))))
                                                                                (S (S (plus (plus (plus o o)
                                                                                o) (S (S (plus (plus o o)
    o)))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))
                                                                                (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))))))
                                    (S (S (S (S (plus (plus (plus (plus o
                                                                                o) o)
                                                                                (S (S (plus (plus o o)
                                                                                o))))
                                                                                (S (S (plus (plus (plus o o)
                                                                                o) (S (S (plus (plus o o)
    o))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))
                                                                                (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (S (plus (plus o o) o)))))))))))
                                    (S (S (S (plus (plus (plus (plus o
                                                                                o) o)
                                                                                (S (S (plus (plus o o)
                                                                                o))))
                                                                                (S (S (plus (plus (plus o o)
                                                                                o) (S (S (plus (plus o o)
    o)))))))))))) in
      (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc) lemma