fabian/veribase-idr2 - Change 37M6U67BGGKCHBINRKRCKR6QFBZQH7JAB6ZDYBAOQ7Q3XMFM5GWAC

Split Data.Natural

Created by fabian on June 19, 2021

37M6U67BGGKCHBINRKRCKR6QFBZQH7JAB6ZDYBAOQ7Q3XMFM5GWAC

Dependencies

In channels

main

Change contents

Insertion in veribase.ipkg at line 37 [6.6174]
[4.118]
[5.1299]

Insertion in veribase.ipkg at line 40 [6.6174]

[7.2061]

[8.0]


	, Data.Natural.Basic
	, Data.Natural.Equivalence
	, Data.Natural.ExtraOperations
	, Data.Natural.Group
	, Data.Natural.Order
	, Data.Natural.Semiring
	, Data.Natural.Show
	, Data.Natural.SupportPrimIntegerLiteral

Deletion in src/Data/Natural.idr at line 2 [8.31]

B:BD[8.52] → [8.52:68]

B:BD[8.68] → [9.106:193]

∅:D[9.193] → [8.68:105]

B:BD[8.68] → [8.68:105]

B:BD[8.105] → [10.0:33]

B:BD[10.33] → [11.0:30]

∅:D[11.30] → [8.105:106]

∅:D[10.33] → [8.105:106]

B:BD[8.105] → [8.105:106]

B:BD[8.106] → [9.194:223]

∅:D[9.223] → [12.823:824]

B:BD[13.86] → [12.823:824]

B:BD[12.824] → [3.489:548]

∅:D[3.548] → [13.86:87]

∅:D[12.848] → [13.86:87]

B:BD[13.86] → [13.86:87]

∅:D[13.87] → [8.106:201]

B:BD[8.106] → [8.106:201]

B:BD[8.201] → [14.0:24]

B:BD[14.24] → [12.849:863]

∅:D[12.863] → [14.24:179]

B:BD[14.24] → [14.24:179]

∅:D[14.179] → [8.201:389]

B:BD[8.201] → [8.201:389]

B:BD[8.389] → [10.34:48]

∅:D[10.48] → [8.389:518]

B:BD[8.389] → [8.389:518]

B:BD[8.518] → [10.49:63]

∅:D[10.63] → [8.518:647]

B:BD[8.518] → [8.518:647]

B:BD[8.647] → [12.864:871]

∅:D[12.871] → [8.661:923]

B:BD[8.661] → [8.661:923]

B:BD[8.923] → [12.872:886]

∅:D[12.886] → [8.923:1192]

B:BD[8.923] → [8.923:1192]

B:BD[8.1192] → [15.58:116]

∅:D[15.116] → [10.64:130]

B:BD[8.1249] → [10.64:130]

B:BD[10.130] → [15.117:225]

∅:D[15.225] → [10.234:375]

B:BD[10.234] → [10.234:375]

B:BD[10.375] → [11.31:32]

B:BD[11.32] → [2.0:7]

∅:D[2.7] → [11.46:116]

B:BD[11.46] → [11.46:116]

B:BD[11.116] → [15.226:279]

∅:D[15.279] → [11.173:255]

B:BD[11.173] → [11.173:255]

∅:D[11.255] → [10.375:376]

B:BD[10.375] → [10.375:376]

B:BD[10.376] → [2.8:15]

∅:D[2.15] → [10.390:606]

B:BD[10.390] → [10.390:606]


import Builtin
import Algebra.Group.Magma
import Algebra.Group.Semigroup
import Algebra.Group.Monoid
import Algebra.Relation.Equivalence
import Algebra.Relation.Preorder
import Algebra.Relation.Order
import Algebra.Ring.Semiring
import public Control.Show
import public Data.PrimInteger
%default total
public export
data Natural = Zero | Succesor Natural
%builtin Natural Natural
--
-- Restrictions
--
public export
data NotZero : Natural -> Type where
  IsNotZero : NotZero (Succesor _)
public export
Uninhabited (NotZero Zero) where
  uninhabited IsNotZero impossible
--
-- Equivalence
--
data NaturalEquiv : (x, y : Natural) -> Type where
  BothZero : NaturalEquiv Zero Zero
  SuccesorEquiv : NaturalEquiv x y -> NaturalEquiv (Succesor x) (Succesor y)
public export
Uninhabited (NaturalEquiv Zero (Succesor y)) where
  uninhabited BothZero impossible
  uninhabited (SuccesorEquiv _) impossible
public export
Uninhabited (NaturalEquiv (Succesor y) Zero) where
  uninhabited BothZero impossible
  uninhabited (SuccesorEquiv _) impossible
export
proofNotEquivThenNotSuccesorEquiv : {x, y : Natural}
                                  -> Not (NaturalEquiv x y)
                                  -> Not (NaturalEquiv (Succesor x) (Succesor y))
proofNotEquivThenNotSuccesorEquiv h (SuccesorEquiv ctra) = h ctra
public export
Equivalence Natural where
  Equiv = NaturalEquiv
  decEquiv Zero Zero = Yes BothZero
  decEquiv Zero (Succesor _) = No absurd
  decEquiv (Succesor _) Zero = No absurd
  decEquiv (Succesor x) (Succesor y) =
    case decEquiv x y of
      Yes p => Yes $ SuccesorEquiv p
      No cp => No  $ proofNotEquivThenNotSuccesorEquiv cp
--
-- Order
--
data NaturalLTE : (x, y : Natural) -> Type where
  ZeroLTEAny  : NaturalLTE Zero y
  SuccesorLTE : NaturalLTE x    y -> NaturalLTE (Succesor x) (Succesor y)
public export
Uninhabited (NaturalLTE (Succesor y) Zero) where
  uninhabited ZeroLTEAny impossible
  uninhabited (SuccesorLTE _) impossible
export
proofLTEThenLTESuccesor : NaturalLTE x y -> NaturalLTE x (Succesor y)
proofLTEThenLTESuccesor ZeroLTEAny      = ZeroLTEAny
proofLTEThenLTESuccesor (SuccesorLTE p) = SuccesorLTE $ proofLTEThenLTESuccesor p
export
proofNotLTEThenNotSuccesorLTE : Not (NaturalLTE x y) -> Not (NaturalLTE (Succesor x) (Succesor y))
proofNotLTEThenNotSuccesorLTE h (SuccesorLTE ctra) = h ctra
public export
Preorder Natural where
  LTE = NaturalLTE

Replacement in src/Data/Natural.idr at line 3 [8.31]

B:BD[10.607] → [10.607:774]

B:BD[10.774] → [15.280:334]

  decLTE Zero y = Yes ZeroLTEAny
  decLTE (Succesor _) Zero = No absurd
  decLTE (Succesor x) (Succesor y) =
    case decLTE x y of
      Yes p => Yes $ SuccesorLTE p
      No cp => No  $ proofNotLTEThenNotSuccesorLTE cp

[10.607]

[10.827]

import public Data.Natural.Basic
import public Data.Natural.ExtraOperations

Replacement in src/Data/Natural.idr at line 6 [8.31]

B:BD[10.828] → [10.828:932]

  proofReflexivity Zero = ZeroLTEAny
  proofReflexivity (Succesor x) = SuccesorLTE $ proofReflexivity x

[10.828]

[10.932]

import public Data.Natural.Equivalence
import public Data.Natural.Order

Replacement in src/Data/Natural.idr at line 9 [8.31]

B:BD[10.933] → [2.16:174]

∅:D[2.174] → [10.1115:1258]

B:BD[10.1115] → [10.1115:1258]

  proofTransitivity Zero Zero _ ZeroLTEAny ZeroLTEAny = ZeroLTEAny
  proofTransitivity Zero (Succesor _) (Succesor _) ZeroLTEAny (SuccesorLTE _) = ZeroLTEAny
  proofTransitivity (Succesor x) (Succesor y) (Succesor z) (SuccesorLTE p1) (SuccesorLTE p2) =
    SuccesorLTE $ proofTransitivity x y z p1 p2

[10.933]

[11.256]

import public Data.Natural.Group
import public Data.Natural.Semiring

Replacement in src/Data/Natural.idr at line 12 [8.31]

B:BD[11.257] → [11.257:355]

B:BD[11.355] → [2.175:232]

∅:D[2.232] → [11.412:545]

B:BD[11.412] → [11.412:545]

B:BD[11.545] → [15.335:390]

∅:D[15.390] → [11.599:915]

B:BD[11.599] → [11.599:915]

B:BD[11.915] → [2.233:318]

∅:D[2.318] → [11.1000:1108]

B:BD[11.1000] → [11.1000:1108]

B:BD[11.1108] → [15.391:432]

∅:D[15.432] → [11.1145:1186]

B:BD[11.1145] → [11.1145:1186]

B:BD[11.1186] → [13.88:92]

B:BD[13.92] → [12.887:905]

B:BD[12.905] → [3.549:1031]

∅:D[3.1031] → [12.905:906]

B:BD[12.905] → [12.905:906]

B:BD[12.906] → [3.1032:1076]

∅:D[3.1076] → [12.906:920]

B:BD[12.906] → [12.906:920]

B:BD[12.920] → [3.1077:1232]

∅:D[3.1232] → [12.1169:1170]

B:BD[12.1169] → [12.1169:1170]

B:BD[12.1170] → [3.1233:1296]

∅:D[3.1296] → [12.1194:1198]

B:BD[12.1194] → [12.1194:1198]

∅:D[12.1198] → [13.92:218]

B:BD[13.92] → [13.92:218]

B:BD[13.218] → [16.0:7]

∅:D[16.7] → [13.232:400]

B:BD[13.232] → [13.232:400]

B:BD[13.400] → [17.0:8]

B:BD[17.8] → [2.319:429]

∅:D[2.429] → [17.95:132]

B:BD[17.95] → [17.95:132]

B:BD[17.132] → [18.0:86]

B:BD[18.94] → [18.94:365]

B:BD[18.365] → [2.430:572]

∅:D[2.572] → [18.486:571]

B:BD[18.486] → [18.486:571]

∅:D[17.330] → [13.400:482]

∅:D[18.571] → [13.400:482]

B:BD[13.400] → [13.400:482]

B:BD[13.482] → [9.224:363]

∅:D[9.363] → [13.482:550]

B:BD[13.482] → [13.482:550]

B:BD[13.550] → [9.364:542]

∅:D[9.542] → [13.672:810]

∅:D[18.616] → [13.672:810]

B:BD[13.672] → [13.672:810]

B:BD[13.810] → [2.573:603]

∅:D[2.603] → [17.331:346]

B:BD[13.840] → [17.331:346]

B:BD[17.346] → [9.543:674]

∅:D[9.674] → [17.346:825]

B:BD[17.346] → [17.346:825]

B:BD[17.825] → [2.604:648]

∅:D[2.648] → [17.867:977]

B:BD[17.867] → [17.867:977]

B:BD[17.977] → [2.649:736]

∅:D[2.736] → [17.1062:1174]

B:BD[17.1062] → [17.1062:1174]

B:BD[17.1174] → [2.737:826]

∅:D[2.826] → [18.617:726]

B:BD[17.1261] → [18.617:726]

B:BD[18.726] → [2.827:1001]

∅:D[2.1001] → [18.896:1344]

B:BD[18.896] → [18.896:1344]

∅:D[18.1344] → [17.1261:1262]

B:BD[17.1261] → [17.1261:1262]

B:BD[17.1262] → [18.1345:1352]

B:BD[18.1352] → [2.1002:1110]

∅:D[2.1110] → [18.1445:1576]

B:BD[18.1445] → [18.1445:1576]

B:BD[18.1576] → [2.1111:1241]

∅:D[2.1241] → [18.1685:2374]

B:BD[18.1685] → [18.1685:2374]

B:BD[18.2374] → [9.675:1023]

∅:D[9.1023] → [18.2374:2375]

B:BD[18.2374] → [18.2374:2375]

∅:D[18.2375] → [17.1262:1330]

B:BD[17.1262] → [17.1262:1330]

B:BD[17.1330] → [15.433:447]

∅:D[15.447] → [17.1338:1408]

B:BD[17.1338] → [17.1338:1408]

B:BD[17.1408] → [9.1024:1097]

∅:D[9.1097] → [18.2376:2435]

B:BD[17.1485] → [18.2376:2435]

B:BD[18.2435] → [9.1098:1136]

∅:D[9.1136] → [18.2475:2484]

B:BD[18.2475] → [18.2475:2484]

B:BD[18.2484] → [14.180:769]

B:BD[14.769] → [9.1137:1837]

public export
Order Natural where
  LT x = NaturalLTE (Succesor x)
  decLT Zero Zero = No absurd
  decLT Zero (Succesor _) = Yes $ SuccesorLTE ZeroLTEAny
  decLT (Succesor _) Zero = No absurd
  decLT (Succesor x) (Succesor y) =
     case decLT x y of
       Yes p => Yes $ SuccesorLTE p
       No cp => No  $ proofNotLTEThenNotSuccesorLTE cp
  proofAntisymetry Zero Zero ZeroLTEAny ZeroLTEAny = BothZero
  proofAntisymetry (Succesor x) (Succesor y) (SuccesorLTE p1) (SuccesorLTE p2) =
    SuccesorEquiv $ proofAntisymetry x y p1 p2
  proofLTThenLTE (SuccesorLTE p) = proofLTEThenLTESuccesor p
  proofLTEThenLTOrEquiv Zero Zero ZeroLTEAny = Right BothZero
  proofLTEThenLTOrEquiv Zero (Succesor _) ZeroLTEAny = Left $ SuccesorLTE ZeroLTEAny
  proofLTEThenLTOrEquiv (Succesor x) (Succesor y) (SuccesorLTE p) =
    case proofLTEThenLTOrEquiv x y p of
      Left  l => Left  $ SuccesorLTE   l
      Right e => Right $ SuccesorEquiv e
--
-- FromInteger
--
natFromPrimInteger : (x : Integer) -> {auto ok : x `GTE` 0} -> Natural
natFromPrimInteger 0 = Zero
natFromPrimInteger x = case (decGTE (prim__sub_Integer x 1) 0) of
  Yes p => Succesor $ assert_total $ natFromPrimInteger $ prim__sub_Integer x 1
  No cp => void $ believe_me () -- TODO: impossible
%builtin IntegerToNatural natFromPrimInteger
natToPrimInteger : Natural -> Integer
natToPrimInteger Zero = 0
natToPrimInteger (Succesor x) = prim__add_Integer 1 $ natToPrimInteger x
%builtin NaturalToInteger natToPrimInteger
public export
SupportPrimIntegerLiteral Natural where
  PrimIntegerRestriction x = x `GTE` 0
  fromPrimInteger = natFromPrimInteger
  toPrimInteger   = natToPrimInteger
public export
Show Natural where
  show = show . toPrimInteger
--
-- Operations
--
public export
plus : (x, y : Natural) -> Natural
plus x Zero = x
plus x (Succesor y) = Succesor $ plus x y
export
proofPlusLeftIdentity : (x : Natural) -> plus Zero x = x
proofPlusLeftIdentity Zero = Refl
proofPlusLeftIdentity (Succesor x) = rewrite proofPlusLeftIdentity x in Refl
export
proofPlusLeftReduction : (x, y : Natural)
                       -> plus (Succesor x) y = Succesor (plus x y)
proofPlusLeftReduction x Zero = Refl
proofPlusLeftReduction x (Succesor y) =
  rewrite proofPlusLeftReduction x y in Refl
export
proofPlusCommutative : (x, y : Natural) -> plus x y = plus y x
proofPlusCommutative x Zero = rewrite proofPlusLeftIdentity x in Refl
proofPlusCommutative x (Succesor y) =
  rewrite proofPlusCommutative x y in
  rewrite proofPlusLeftReduction y x in
  Refl
export
proofPlusAssociative : (x, y, z : Natural)
                     -> plus x (plus y z) = plus (plus x y) z
proofPlusAssociative _ _ Zero = Refl
proofPlusAssociative x y (Succesor z) =
  rewrite proofPlusAssociative x y z in Refl
public export
[NaturalSumMagma] Magma Natural where
  (<>) = plus
public export
[NaturalSumCommutativeMagma] CommutativeMagma Natural using NaturalSumMagma where
  proofCommutative = proofPlusCommutative
public export
[NaturalSumSemigroup] Semigroup Natural using NaturalSumMagma where
  proofAssociative = proofPlusAssociative
public export
[NaturalSumCommutativeSemigroup] CommutativeSemigroup Natural using NaturalSumCommutativeMagma NaturalSumSemigroup where
public export
[NaturalSumMonoid] Monoid Natural using NaturalSumSemigroup where
  id = Zero
  proofLeftIdentity = proofPlusLeftIdentity
  proofRightIdentity _ = Refl
public export
[NaturalSumCommutativeMonoid] CommutativeMonoid Natural using NaturalSumCommutativeSemigroup NaturalSumMonoid where
public export
minus : (x, y : Natural) -> {auto ok : x `GTE` y} -> Natural
minus x Zero = x
minus (Succesor x) (Succesor y) {ok=(SuccesorLTE p)} = minus x y
public export
mult : (x, y : Natural) -> Natural
mult _ Zero = Zero
mult x (Succesor y) = x `plus` mult x y
export
proofMultLeftIdentity : (x : Natural) -> mult (Succesor Zero) x = x
proofMultLeftIdentity Zero = Refl
proofMultLeftIdentity (Succesor x) =
  rewrite proofMultLeftIdentity x in
  rewrite proofPlusLeftReduction Zero x in
  rewrite proofPlusLeftIdentity x in
  Refl
export
proofMultLeftAnnihilation : (x : Natural) -> mult Zero x = Zero
proofMultLeftAnnihilation Zero = Refl
proofMultLeftAnnihilation (Succesor x) =
  rewrite proofMultLeftAnnihilation x in Refl
export
proofMultRightAnnihilation : (x : Natural) -> mult x Zero = Zero
proofMultRightAnnihilation Zero = Refl
proofMultRightAnnihilation (Succesor x) =
  rewrite proofMultRightAnnihilation x in Refl
export
proofMultCommutative : (x, y : Natural) -> mult x y = mult y x
proofMultCommutative Zero Zero = Refl
proofMultCommutative Zero (Succesor y) =
  rewrite proofMultCommutative Zero y in Refl
proofMultCommutative (Succesor x) Zero =
  rewrite proofMultCommutative Zero x in Refl
proofMultCommutative (Succesor x) (Succesor y) =
  rewrite proofPlusLeftReduction x (mult (Succesor x) y) in
  rewrite proofPlusLeftReduction y (mult (Succesor y) x) in
  rewrite proofMultCommutative (Succesor x) y in
  rewrite proofMultCommutative (Succesor y) x in
  rewrite proofMultCommutative x y in
  rewrite proofPlusAssociative x y (mult y x) in
  rewrite proofPlusAssociative y x (mult y x) in
  rewrite proofPlusCommutative x y in
  Refl
export
proofMultLeftReduction : (x, y : Natural)
                       -> mult (Succesor x) y = plus y (mult x y)
proofMultLeftReduction x y =
  rewrite proofMultCommutative (Succesor x) y in
  rewrite proofMultCommutative x y in
  Refl
export
proofMultLeftDistributesPlus : (x, y, z : Natural)
                             -> mult x (plus y z) = plus (mult x y) (mult x z)
proofMultLeftDistributesPlus Zero y z =
  rewrite proofMultLeftAnnihilation y in
  rewrite proofMultLeftAnnihilation z in
  rewrite proofMultLeftAnnihilation (plus y z) in
  Refl
proofMultLeftDistributesPlus (Succesor x) y z =
  rewrite proofMultLeftReduction x y in
  rewrite proofMultLeftReduction x z in
  rewrite proofMultLeftReduction x (plus y z) in
  rewrite proofMultLeftDistributesPlus x y z in
  rewrite proofPlusAssociative (plus y (mult x y)) z (mult x z) in
  rewrite proofPlusCommutative (plus y (mult x y)) z in
  rewrite proofPlusAssociative z y (mult x y) in
  rewrite proofPlusCommutative z y in
  rewrite proofPlusAssociative (plus y z) (mult x y) (mult x z) in
  Refl
proofMultRightDistributesPlus : (x, y, z : Natural)
                              -> mult (plus x y) z = plus (mult x z) (mult y z)
proofMultRightDistributesPlus x y z =
  rewrite proofMultCommutative (plus x y) z in
  rewrite proofMultLeftDistributesPlus z x y in
  rewrite proofMultCommutative z x in
  rewrite proofMultCommutative z y in
  Refl
public export
[NaturalMultMagma] Magma Natural where
  (<>) = mult
public export
[NaturalMultSemigroup] Semigroup Natural using NaturalMultMagma where
  proofAssociative x y Zero = Refl
  proofAssociative x y (Succesor z) =
    rewrite proofMultLeftDistributesPlus x y (mult y z) in
    rewrite proofAssociative x y z in
    Refl
public export
[NaturalMultMonoid] Monoid Natural using NaturalMultSemigroup where
  id = Succesor Zero
  proofLeftIdentity = proofMultLeftIdentity
  proofRightIdentity _ = Refl
public export
divRem : (x, y : Natural) -> {auto ok : NotZero y} -> (Natural, Natural)
divRem x y = case decLTE y x of
  Yes _ => let (d, r) := divRem (x `minus` y) y in (Succesor d, r)
  No  _ => (Zero, x)
public export
div : (x, y : Natural) -> {auto ok : NotZero y} -> Natural
div x y = fst $ divRem x y
public export
rem : (x, y : Natural) -> {auto ok : NotZero y} -> Natural
rem x y = snd $ divRem x y
public export
Semiring Natural where
  (+) = plus
  (*) = mult
  zero = 0
  one  = 1
  proofSumZero = proofRightIdentity @{NaturalSumMonoid}
  proofSumCommutative = proofCommutative @{NaturalSumCommutativeMagma}
  proofSumAssociative = proofAssociative @{NaturalSumSemigroup}
  proofMultOneLeft  = proofLeftIdentity  @{NaturalMultMonoid}
  proofMultOneRight = proofRightIdentity @{NaturalMultMonoid}
  proofMultAssociative = proofAssociative @{NaturalMultSemigroup}
  proofMultDistributesSumLeft  = proofMultLeftDistributesPlus
  proofMultDistributesSumRight = proofMultRightDistributesPlus
  zeroAnnihilatorLeft  = proofMultLeftAnnihilation
  zeroAnnihilatorRight = proofMultRightAnnihilation

[11.257]

import public Data.Natural.SupportPrimIntegerLiteral
import public Data.Natural.Show

File addition: Natural (d--x------)
[6.14]

File addition: SupportPrimIntegerLiteral.idr (----------)

[0.535]

module Data.Natural.SupportPrimIntegerLiteral
import Builtin
import Algebra.Relation.Preorder
import Data.PrimInteger
import public Data.Natural.Basic
%default total
public export
natFromPrimInteger : (x : Integer) -> {auto ok : x `GTE` 0} -> Natural
natFromPrimInteger 0 = Zero
natFromPrimInteger x = case (decGTE (prim__sub_Integer x 1) 0) of
  Yes p => Succesor $ assert_total $ natFromPrimInteger $ prim__sub_Integer x 1
  No cp => void $ believe_me () -- TODO: impossible
-- TODO: Compiler not happy
-- %builtin IntegerToNatural natFromPrimInteger
public export
natToPrimInteger : Natural -> Integer
natToPrimInteger Zero = 0
natToPrimInteger (Succesor x) = prim__add_Integer 1 $ natToPrimInteger x
-- TODO: Compiler not happy
-- %builtin NaturalToInteger natToPrimInteger
public export
SupportPrimIntegerLiteral Natural where
  PrimIntegerRestriction x = x `GTE` 0
  fromPrimInteger = natFromPrimInteger
  toPrimInteger   = natToPrimInteger

File addition: Show.idr (----------)

[0.535]

module Data.Natural.Show
import Builtin
import Control.Show
import Data.PrimInteger
import public Data.Natural.SupportPrimIntegerLiteral
public export
Show Natural where
  show = show . toPrimInteger

File addition: Semiring.idr (----------)

[0.535]

module Data.Natural.Semiring
import Builtin
import Algebra.Group.Magma
import Algebra.Group.Semigroup
import Algebra.Group.Monoid
import Algebra.Ring.Semiring
import public Data.Natural.Basic
import public Data.Natural.Group
%default total
public export
Semiring Natural where
  (+) = add
  (*) = mult
  zero = Zero
  one  = (Succesor Zero)
  proofSumZero = proofRightIdentity @{NaturalSumMonoid}
  proofSumCommutative = proofCommutative @{NaturalSumCommutativeMagma}
  proofSumAssociative = proofAssociative @{NaturalSumSemigroup}
  proofMultOneLeft  = proofLeftIdentity  @{NaturalMultMonoid}
  proofMultOneRight = proofRightIdentity @{NaturalMultMonoid}
  proofMultAssociative = proofAssociative @{NaturalMultSemigroup}
  proofMultDistributesSumLeft  = proofMultLeftDistributesAdd
  proofMultDistributesSumRight = proofMultRightDistributesAdd
  zeroAnnihilatorLeft  = proofMultLeftAnnihilation
  zeroAnnihilatorRight = proofMultRightAnnihilation

File addition: Order.idr (----------)

[0.535]

module Data.Natural.Order
import Builtin
import Algebra.Relation.Equivalence
import Algebra.Relation.Preorder
import Algebra.Relation.Order
import public Data.Natural.Basic
import public Data.Natural.Equivalence
%default total
public export
data NaturalLTE : (x, y : Natural) -> Type where
  ZeroLTEAny  : NaturalLTE Zero y
  SuccesorLTE : NaturalLTE x    y -> NaturalLTE (Succesor x) (Succesor y)
public export
Uninhabited (NaturalLTE (Succesor y) Zero) where
  uninhabited ZeroLTEAny impossible
  uninhabited (SuccesorLTE _) impossible
export
proofLTEThenLTESuccesor : NaturalLTE x y -> NaturalLTE x (Succesor y)
proofLTEThenLTESuccesor ZeroLTEAny      = ZeroLTEAny
proofLTEThenLTESuccesor (SuccesorLTE p) = SuccesorLTE $ proofLTEThenLTESuccesor p
export
proofNotLTEThenNotSuccesorLTE : Not (NaturalLTE x y) -> Not (NaturalLTE (Succesor x) (Succesor y))
proofNotLTEThenNotSuccesorLTE h (SuccesorLTE ctra) = h ctra
public export
Preorder Natural where
  LTE = NaturalLTE
  decLTE Zero y = Yes ZeroLTEAny
  decLTE (Succesor _) Zero = No absurd
  decLTE (Succesor x) (Succesor y) =
    case decLTE x y of
      Yes p => Yes $ SuccesorLTE p
      No cp => No  $ proofNotLTEThenNotSuccesorLTE cp
  proofReflexivity Zero = ZeroLTEAny
  proofReflexivity (Succesor x) = SuccesorLTE $ proofReflexivity x
  proofTransitivity Zero Zero _ ZeroLTEAny ZeroLTEAny = ZeroLTEAny
  proofTransitivity Zero (Succesor _) (Succesor _) ZeroLTEAny (SuccesorLTE _) = ZeroLTEAny
  proofTransitivity (Succesor x) (Succesor y) (Succesor z) (SuccesorLTE p1) (SuccesorLTE p2) =
    SuccesorLTE $ proofTransitivity x y z p1 p2
public export
Order Natural where
  LT x = NaturalLTE (Succesor x)
  decLT Zero Zero = No absurd
  decLT Zero (Succesor _) = Yes $ SuccesorLTE ZeroLTEAny
  decLT (Succesor _) Zero = No absurd
  decLT (Succesor x) (Succesor y) =
     case decLT x y of
       Yes p => Yes $ SuccesorLTE p
       No cp => No  $ proofNotLTEThenNotSuccesorLTE cp
  proofAntisymetry Zero Zero ZeroLTEAny ZeroLTEAny = BothZero
  proofAntisymetry (Succesor x) (Succesor y) (SuccesorLTE p1) (SuccesorLTE p2) =
    SuccesorEquiv $ proofAntisymetry x y p1 p2
  proofLTThenLTE (SuccesorLTE p) = proofLTEThenLTESuccesor p
  proofLTEThenLTOrEquiv Zero Zero ZeroLTEAny = Right BothZero
  proofLTEThenLTOrEquiv Zero (Succesor _) ZeroLTEAny = Left $ SuccesorLTE ZeroLTEAny
  proofLTEThenLTOrEquiv (Succesor x) (Succesor y) (SuccesorLTE p) =
    case proofLTEThenLTOrEquiv x y p of
      Left  l => Left  $ SuccesorLTE   l
      Right e => Right $ SuccesorEquiv e

File addition: Group.idr (----------)

[0.535]

module Data.Natural.Group
import Builtin
import Algebra.Group.Magma
import Algebra.Group.Semigroup
import Algebra.Group.Monoid
import public Data.Natural.Basic
public export
[NaturalSumMagma] Magma Natural where
  (<>) = add
public export
[NaturalSumCommutativeMagma] CommutativeMagma Natural using NaturalSumMagma where
  proofCommutative = proofAddCommutative
public export
[NaturalSumSemigroup] Semigroup Natural using NaturalSumMagma where
  proofAssociative = proofAddAssociative
public export
[NaturalSumCommutativeSemigroup] CommutativeSemigroup Natural using NaturalSumCommutativeMagma NaturalSumSemigroup where
public export
[NaturalSumMonoid] Monoid Natural using NaturalSumSemigroup where
  id = Zero
  proofLeftIdentity = proofAddLeftIdentity
  proofRightIdentity _ = Refl
public export
[NaturalSumCommutativeMonoid] CommutativeMonoid Natural using NaturalSumCommutativeSemigroup NaturalSumMonoid where
public export
[NaturalMultMagma] Magma Natural where
  (<>) = mult
public export
[NaturalMultSemigroup] Semigroup Natural using NaturalMultMagma where
  proofAssociative x y Zero = Refl
  proofAssociative x y (Succesor z) =
    rewrite proofMultLeftDistributesAdd x y (mult y z) in
    rewrite proofAssociative x y z in
    Refl
public export
[NaturalMultMonoid] Monoid Natural using NaturalMultSemigroup where
  id = Succesor Zero
  proofLeftIdentity = proofMultLeftIdentity
  proofRightIdentity _ = Refl

File addition: ExtraOperations.idr (----------)

[0.535]

module Data.Natural.ExtraOperations
import Builtin
import Algebra.Relation.Preorder
import public Data.Natural.Basic
import public Data.Natural.Order
%default total
public export
minus : (x, y : Natural) -> {auto ok : x `GTE` y} -> Natural
minus x Zero = x
minus (Succesor x) (Succesor y) {ok=(SuccesorLTE p)} = minus x y
public export
divRem : (x, y : Natural) -> {auto ok : NotZero y} -> (Natural, Natural)
divRem x y = case decLTE y x of
  Yes _ => let (d, r) := divRem (x `minus` y) y in (Succesor d, r)
  No  _ => (Zero, x)
public export
div : (x, y : Natural) -> {auto ok : NotZero y} -> Natural
div x y = fst $ divRem x y
public export
rem : (x, y : Natural) -> {auto ok : NotZero y} -> Natural
rem x y = snd $ divRem x y

File addition: Equivalence.idr (----------)

[0.535]

module Data.Natural.Equivalence
import Builtin
import Algebra.Relation.Equivalence
import public Data.Natural.Basic
public export
data NaturalEquiv : (x, y : Natural) -> Type where
  BothZero : NaturalEquiv Zero Zero
  SuccesorEquiv : NaturalEquiv x y -> NaturalEquiv (Succesor x) (Succesor y)
public export
Uninhabited (NaturalEquiv Zero (Succesor y)) where
  uninhabited BothZero impossible
  uninhabited (SuccesorEquiv _) impossible
public export
Uninhabited (NaturalEquiv (Succesor y) Zero) where
  uninhabited BothZero impossible
  uninhabited (SuccesorEquiv _) impossible
export
proofNotEquivThenNotSuccesorEquiv : {x, y : Natural}
                                  -> Not (NaturalEquiv x y)
                                  -> Not (NaturalEquiv (Succesor x) (Succesor y))
proofNotEquivThenNotSuccesorEquiv h (SuccesorEquiv ctra) = h ctra
public export
Equivalence Natural where
  Equiv = NaturalEquiv
  decEquiv Zero Zero = Yes BothZero
  decEquiv Zero (Succesor _) = No absurd
  decEquiv (Succesor _) Zero = No absurd
  decEquiv (Succesor x) (Succesor y) =
    case decEquiv x y of
      Yes p => Yes $ SuccesorEquiv p
      No cp => No  $ proofNotEquivThenNotSuccesorEquiv cp

File addition: Basic.idr (----------)

[0.535]

module Data.Natural.Basic
import Builtin
%default total
public export
data Natural = Zero | Succesor Natural
%builtin Natural Natural
--
-- Restrictions
--
public export
data NotZero : Natural -> Type where
  IsNotZero : NotZero (Succesor _)
public export
Uninhabited (NotZero Zero) where
  uninhabited IsNotZero impossible
--
-- Operations
--
-- Addition
public export
add : (x, y : Natural) -> Natural
add x Zero = x
add x (Succesor y) = Succesor $ add x y
export
proofAddLeftIdentity : (x : Natural) -> add Zero x = x
proofAddLeftIdentity Zero = Refl
proofAddLeftIdentity (Succesor x) = rewrite proofAddLeftIdentity x in Refl
export
proofAddLeftReduction : (x, y : Natural)
                       -> add (Succesor x) y = Succesor (add x y)
proofAddLeftReduction x Zero = Refl
proofAddLeftReduction x (Succesor y) =
  rewrite proofAddLeftReduction x y in Refl
export
proofAddCommutative : (x, y : Natural) -> add x y = add y x
proofAddCommutative x Zero = rewrite proofAddLeftIdentity x in Refl
proofAddCommutative x (Succesor y) =
  rewrite proofAddCommutative x y in
  rewrite proofAddLeftReduction y x in
  Refl
export
proofAddAssociative : (x, y, z : Natural)
                     -> add x (add y z) = add (add x y) z
proofAddAssociative _ _ Zero = Refl
proofAddAssociative x y (Succesor z) =
  rewrite proofAddAssociative x y z in Refl
-- Diff
public export
diff : (x, y : Natural) -> Natural
diff Zero y = y
diff x Zero = x
diff (Succesor x) (Succesor y) = diff x y
-- Mult
public export
mult : (x, y : Natural) -> Natural
mult _ Zero = Zero
mult x (Succesor y) = x `add` mult x y
export
proofMultLeftIdentity : (x : Natural) -> mult (Succesor Zero) x = x
proofMultLeftIdentity Zero = Refl
proofMultLeftIdentity (Succesor x) =
  rewrite proofMultLeftIdentity x in
  rewrite proofAddLeftReduction Zero x in
  rewrite proofAddLeftIdentity x in
  Refl
export
proofMultLeftAnnihilation : (x : Natural) -> mult Zero x = Zero
proofMultLeftAnnihilation Zero = Refl
proofMultLeftAnnihilation (Succesor x) =
  rewrite proofMultLeftAnnihilation x in Refl
export
proofMultRightAnnihilation : (x : Natural) -> mult x Zero = Zero
proofMultRightAnnihilation Zero = Refl
proofMultRightAnnihilation (Succesor x) =
  rewrite proofMultRightAnnihilation x in Refl
export
proofMultCommutative : (x, y : Natural) -> mult x y = mult y x
proofMultCommutative Zero Zero = Refl
proofMultCommutative Zero (Succesor y) =
  rewrite proofMultCommutative Zero y in Refl
proofMultCommutative (Succesor x) Zero =
  rewrite proofMultCommutative Zero x in Refl
proofMultCommutative (Succesor x) (Succesor y) =
  rewrite proofAddLeftReduction x (mult (Succesor x) y) in
  rewrite proofAddLeftReduction y (mult (Succesor y) x) in
  rewrite proofMultCommutative (Succesor x) y in
  rewrite proofMultCommutative (Succesor y) x in
  rewrite proofMultCommutative x y in
  rewrite proofAddAssociative x y (mult y x) in
  rewrite proofAddAssociative y x (mult y x) in
  rewrite proofAddCommutative x y in
  Refl
export
proofMultLeftReduction : (x, y : Natural)
                       -> mult (Succesor x) y = add y (mult x y)
proofMultLeftReduction x y =
  rewrite proofMultCommutative (Succesor x) y in
  rewrite proofMultCommutative x y in
  Refl
export
proofMultLeftDistributesAdd : (x, y, z : Natural)
                             -> mult x (add y z) = add (mult x y) (mult x z)
proofMultLeftDistributesAdd Zero y z =
  rewrite proofMultLeftAnnihilation y in
  rewrite proofMultLeftAnnihilation z in
  rewrite proofMultLeftAnnihilation (add y z) in
  Refl
proofMultLeftDistributesAdd (Succesor x) y z =
  rewrite proofMultLeftReduction x y in
  rewrite proofMultLeftReduction x z in
  rewrite proofMultLeftReduction x (add y z) in
  rewrite proofMultLeftDistributesAdd x y z in
  rewrite proofAddAssociative (add y (mult x y)) z (mult x z) in
  rewrite proofAddCommutative (add y (mult x y)) z in
  rewrite proofAddAssociative z y (mult x y) in
  rewrite proofAddCommutative z y in
  rewrite proofAddAssociative (add y z) (mult x y) (mult x z) in
  Refl
export
proofMultRightDistributesAdd : (x, y, z : Natural)
                              -> mult (add x y) z = add (mult x z) (mult y z)
proofMultRightDistributesAdd x y z =
  rewrite proofMultCommutative (add x y) z in
  rewrite proofMultLeftDistributesAdd z x y in
  rewrite proofMultCommutative z x in
  rewrite proofMultCommutative z y in
  Refl

Split Data.Natural

Dependencies

In channels

Change contents

Insertion in veribase.ipkg at line 37 [6.6174]

Insertion in veribase.ipkg at line 40 [6.6174]

Deletion in src/Data/Natural.idr at line 2 [8.31]

Replacement in src/Data/Natural.idr at line 3 [8.31]

Replacement in src/Data/Natural.idr at line 6 [8.31]

Replacement in src/Data/Natural.idr at line 9 [8.31]

Replacement in src/Data/Natural.idr at line 12 [8.31]

File addition: Natural (d--x------)

File addition: SupportPrimIntegerLiteral.idr (----------)

File addition: Show.idr (----------)

File addition: Semiring.idr (----------)

File addition: Order.idr (----------)

File addition: Group.idr (----------)

File addition: ExtraOperations.idr (----------)

File addition: Equivalence.idr (----------)

File addition: Basic.idr (----------)