Youtube
/
Idris2-ep0
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Define plus

This commit is contained in:
Nathan McCarty 2023-06-30 10:36:01 -04:00
parent 267fabf43e
commit 1760675a1e
Signed by: thatonelutenist
SSH Key Fingerprint: SHA256:hwQEcmak9E6sdU9bXc98RHw/Xd1AhpB5HZT7ZSVJkRM
1 changed files with 27 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
src/Naturals.idr
View File

@ -35,3 +35,30 @@ injection n n Reflexive = Reflexive
succNotZero : (n : Natural) -> Equality (S n) Zero -> Void succNotZero : (n : Natural) -> Equality (S n) Zero -> Void
succNotZero _ Reflexive impossible succNotZero _ Reflexive impossible
plus : (n, m : Natural) -> Natural
plus n Zero = n
plus n (S x) = S (n `plus` x)
zeroIdentityRight : (n : Natural) -> Equality n (n `plus` Zero)
zeroIdentityRight n = Reflexive
eqSucc : (n, m : Natural) -> Equality n m -> Equality (S n) (S m)
eqSucc n n Reflexive = Reflexive
zeroIdentityLeft : (n : Natural) -> Equality n (Zero `plus` n)
zeroIdentityLeft Zero = Reflexive
zeroIdentityLeft (S x) =
let rec = zeroIdentityLeft x
in eqSucc _ _ rec
commutativeHelper : (n, m : Natural) -> Equality (S (n `plus` m)) (S (m `plus` n))
-> Equality (S (n `plus` m)) ((S m) `plus` n)
commutative : (n, m : Natural) -> Equality (n `plus` m) (m `plus` n)
commutative n Zero = zeroIdentityLeft _
commutative n (S m) =
let rec = eqSucc _ _ $ commutative n m
in commutativeHelper _ _ rec
associative : (n, m, o : Natural) -> Equality (n `plus` (m `plus` o)) ((n `plus` m) `plus` o)