# Natural numbers division

**URL:** <https://discourse.ats-lang.org/t/natural-numbers-division/78>\
**Category:** Google Group\
**Created:** [February 1, 2014, 12:07pm UTC](https://discourse.ats-lang.org/t/natural-numbers-division/78 "2014-02-01T12:07:41Z")\
**Posts on this page:** 9\
**Page:** 1

<div class="post-metadata">

**Author:** ![Chotu\_S](https://avatars.discourse-cdn.com/v4/letter/c/7cd45c/32.png) [@Chotu\_S](https://discourse.ats-lang.org/u/Chotu_S)\
**Post date:** [February 1, 2014, 12:07pm UTC](https://discourse.ats-lang.org/t/natural-numbers-division/78/1 "2014-02-01T12:07:41Z")

</div>

How does division of natural numbers work ?

For example I want a function that takes any natural number “n” and return  
a natural number “n / 2” (i.e positive integer quotient ) .

Thanks

---

<div class="post-metadata">

**Author:** ![Chotu\_S](https://avatars.discourse-cdn.com/v4/letter/c/7cd45c/32.png) [@Chotu\_S](https://discourse.ats-lang.org/u/Chotu_S)\
**Post date:** [February 1, 2014, 2:13pm UTC](https://discourse.ats-lang.org/t/natural-numbers-division/78/2 "2014-02-01T14:13:43Z")

</div>

Thanks Brandon,

I’ll take a look inside the integers,sats .

But how do you compile following function :

fun div\_by\_2 {n:nat} ( n : int (n) ) : [m : nat] int (m) = n/2

(\* or \*)

fun ddiv\_by\_2 {n:nat} ( n : int (n) ) : [m : nat | m == n/2] int (m) = n/2On Sat, Feb 1, 2014 at 7:37 PM, Brandon Barker [brandon...@gmail.com](mailto:brandon...@gmail.com)wrote:

> But it seems that, as in C, this is the default behavior (so my suggestion  
> above may not be necessary):
> 
> val n7 = 7  
> val n8 = 8
> 
> val n3 = n7/2  
> val () = println!(n3)  
> val () = assertloc (n3 = 3)  
> val n4 = n8/2  
> val () = println!(n4)  
> val () = assertloc (n4 = 4)
> 
> >

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [February 1, 2014, 3:25pm UTC](https://discourse.ats-lang.org/t/natural-numbers-division/78/3 "2014-02-01T15:25:49Z")

</div>

Or you can use ‘half’.

In practice, if I don’t know a function in the ATS library  
that does what ‘div\_by\_2’ is expected to do, then I will implement it:

fun div\_by\_2 {n:nat} (n: int n): int(n/2) = $UN.cast{int(n/2)}(n/2)On Saturday, February 1, 2014 9:19:53 AM UTC-5, chotu s wrote:

> This g1int\_ndiv(n,2) seems to work , it is defined in integers.sats file  
> .
> 
> Thanks
> 
> On Sat, Feb 1, 2014 at 7:43 PM, chotu s \<[cho...@gmail.com](mailto:cho...@gmail.com) \<javascript:\>\>wrote:
> 
> > Thanks Brandon,
> > 
> > I’ll take a look inside the integers,sats .
> > 
> > But how do you compile following function :
> > 
> > fun div\_by\_2 {n:nat} ( n : int (n) ) : [m : nat] int (m) = n/2
> > 
> > (\* or \*)
> > 
> > fun ddiv\_by\_2 {n:nat} ( n : int (n) ) : [m : nat | m == n/2] int (m) =  
> > n/2
> > 
> > On Sat, Feb 1, 2014 at 7:37 PM, Brandon Barker \<[brand...@gmail.com](mailto:brand...@gmail.com)\<javascript:\> wrote:
> > 
> > > But it seems that, as in C, this is the default behavior (so my  
> > > suggestion above may not be necessary):
> > > 
> > > val n7 = 7  
> > > val n8 = 8
> > > 
> > > val n3 = n7/2  
> > > val () = println!(n3)  
> > > val () = assertloc (n3 = 3)  
> > > val n4 = n8/2  
> > > val () = println!(n4)  
> > > val () = assertloc (n4 = 4)
> > > 
> > > >

---

<div class="post-metadata">

**Author:** ![Chotu\_S](https://avatars.discourse-cdn.com/v4/letter/c/7cd45c/32.png) [@Chotu\_S](https://discourse.ats-lang.org/u/Chotu_S)\
**Post date:** [February 1, 2014, 2:19pm UTC](https://discourse.ats-lang.org/t/natural-numbers-division/78/4 "2014-02-01T14:19:53Z")

</div>

This g1int\_ndiv(n,2) seems to work , it is defined in integers.sats file .

ThanksOn Sat, Feb 1, 2014 at 7:43 PM, chotu s [chot...@gmail.com](mailto:chot...@gmail.com) wrote:

> Thanks Brandon,
> 
> I’ll take a look inside the integers,sats .
> 
> But how do you compile following function :
> 
> fun div\_by\_2 {n:nat} ( n : int (n) ) : [m : nat] int (m) = n/2
> 
> (\* or \*)
> 
> fun ddiv\_by\_2 {n:nat} ( n : int (n) ) : [m : nat | m == n/2] int (m) = n/2
> 
> On Sat, Feb 1, 2014 at 7:37 PM, Brandon Barker [brandon...@gmail.com](mailto:brandon...@gmail.com)wrote:
> 
> > But it seems that, as in C, this is the default behavior (so my  
> > suggestion above may not be necessary):
> > 
> > val n7 = 7  
> > val n8 = 8
> > 
> > val n3 = n7/2  
> > val () = println!(n3)  
> > val () = assertloc (n3 = 3)  
> > val n4 = n8/2  
> > val () = println!(n4)  
> > val () = assertloc (n4 = 4)
> > 
> > >

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [February 1, 2014, 2:07pm UTC](https://discourse.ats-lang.org/t/natural-numbers-division/78/5 "2014-02-01T14:07:22Z")

</div>

But it seems that, as in C, this is the default behavior (so my suggestion  
above may not be necessary):

val n7 = 7  
val n8 = 8

val n3 = n7/2  
val () = println!(n3)  
val () = assertloc (n3 = 3)  
val n4 = n8/2  
val () = println!(n4)  
val () = assertloc (n4 = 4)

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [February 1, 2014, 1:52pm UTC](https://discourse.ats-lang.org/t/natural-numbers-division/78/6 "2014-02-01T13:52:47Z")

</div>

You may want to check out prelude/SATS/integer.sats for this sort of  
thing (search for “div”). prelude\_integer.dats has some related  
examples.  
Brandon Barker  
brandon…@gmail.comOn Sat, Feb 1, 2014 at 7:07 AM, chotu s [chot...@gmail.com](mailto:chot...@gmail.com) wrote:

> How does division of natural numbers work ?
> 
> For example I want a function that takes any natural number “n” and return  
> a natural number “n / 2” (i.e positive integer quotient ) .
> 
> Thanks
> 
> –  
> You received this message because you are subscribed to the Google Groups  
> “ats-lang-users” group.  
> To unsubscribe from this group and stop receiving emails from it, send an  
> email to [ats-lang-user...@googlegroups.com](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> To view this discussion on the web visit  
> [https://groups.google.com/d/msgid/ats-lang-users/03a04197-a32a-49eb-97fa-bd94509cbcfb%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/03a04197-a32a-49eb-97fa-bd94509cbcfb%40googlegroups.com).

---

<div class="post-metadata">

**Author:** ![Chotu\_S](https://avatars.discourse-cdn.com/v4/letter/c/7cd45c/32.png) [@Chotu\_S](https://discourse.ats-lang.org/u/Chotu_S)\
**Post date:** [February 2, 2014, 10:05am UTC](https://discourse.ats-lang.org/t/natural-numbers-division/78/7 "2014-02-02T10:05:08Z")

</div>

I agree with you , but I need to practice using such tool and I plan to do  
so for most part of this year for small set of code only.

Also I don’t start code with dependent types but later after I get a  
working code do I try convert to dependent types.

I just wanted to convert some contracts into ATS for quick sort algorithm ,  
it was just a mechanical process(not a pragmatic one). So I eventually  
managed to get some of it converted , the code is given here : qs.dats[https://bitbucket.org/chotu/ats-explore/src/0dce1c05b6007fc876e4703c4c1c7d42a7048f2d/r1d1qs/qs.dats?at=master](https://bitbucket.org/chotu/ats-explore/src/0dce1c05b6007fc876e4703c4c1c7d42a7048f2d/r1d1qs/qs.dats?at=master)

I’ll try to convert other contracts/invariants for this code to ATS as I  
get more familiar/practice with ATS .

I did _not_ struggle with ATS , but with my stupidity and silly mistakes  
(for example change in order of args . incorrect spec , etc).

I must say that I now starting to like ATS , most of the stuff is intuitive  
I believe 🙂

ThanksOn Saturday, February 1, 2014 9:11:34 PM UTC+5:30, gmhwxi wrote:

> I just want to add a note that reflects my current view of program  
> verification:
> 
> First and foremost, program verification is the thought process that  
> justifies to oneself why  
> one’s code is correct (in a general and broad sense). Using tools (e.g.,  
> typecheckers, theorem-provers)  
> to ensure the correctness of this thought process is a secondary issue.  
> This view is largely based  
> on the way in which people construct mathematical proofs.
> 
> On Saturday, February 1, 2014 10:25:49 AM UTC-5, gmhwxi wrote:
> 
> > Or you can use ‘half’.
> > 
> > In practice, if I don’t know a function in the ATS library  
> > that does what ‘div\_by\_2’ is expected to do, then I will implement it:
> > 
> > fun div\_by\_2 {n:nat} (n: int n): int(n/2) = $UN.cast{int(n/2)}(n/2)
> > 
> > On Saturday, February 1, 2014 9:19:53 AM UTC-5, chotu s wrote:
> > 
> > > This g1int\_ndiv(n,2) seems to work , it is defined in integers.sats file  
> > > .
> > > 
> > > Thanks
> > > 
> > > On Sat, Feb 1, 2014 at 7:43 PM, chotu s [cho...@gmail.com](mailto:cho...@gmail.com) wrote:
> > > 
> > > > Thanks Brandon,
> > > > 
> > > > I’ll take a look inside the integers,sats .
> > > > 
> > > > But how do you compile following function :
> > > > 
> > > > fun div\_by\_2 {n:nat} ( n : int (n) ) : [m : nat] int (m) = n/2
> > > > 
> > > > (\* or \*)
> > > > 
> > > > fun ddiv\_by\_2 {n:nat} ( n : int (n) ) : [m : nat | m == n/2] int (m) =  
> > > > n/2
> > > > 
> > > > On Sat, Feb 1, 2014 at 7:37 PM, Brandon Barker [brand...@gmail.com](mailto:brand...@gmail.com)wrote:
> > > > 
> > > > > But it seems that, as in C, this is the default behavior (so my  
> > > > > suggestion above may not be necessary):
> > > > > 
> > > > > val n7 = 7  
> > > > > val n8 = 8
> > > > > 
> > > > > val n3 = n7/2  
> > > > > val () = println!(n3)  
> > > > > val () = assertloc (n3 = 3)  
> > > > > val n4 = n8/2  
> > > > > val () = println!(n4)  
> > > > > val () = assertloc (n4 = 4)
> > > > > 
> > > > > >

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [February 1, 2014, 3:41pm UTC](https://discourse.ats-lang.org/t/natural-numbers-division/78/8 "2014-02-01T15:41:34Z")

</div>

I just want to add a note that reflects my current view of program  
verification:

First and foremost, program verification is the thought process that  
justifies to oneself why  
one’s code is correct (in a general and broad sense). Using tools (e.g.,  
typecheckers, theorem-provers)  
to ensure the correctness of this thought process is a secondary issue.  
This view is largely based  
on the way in which people construct mathematical proofs.On Saturday, February 1, 2014 10:25:49 AM UTC-5, gmhwxi wrote:

> Or you can use ‘half’.
> 
> In practice, if I don’t know a function in the ATS library  
> that does what ‘div\_by\_2’ is expected to do, then I will implement it:
> 
> fun div\_by\_2 {n:nat} (n: int n): int(n/2) = $UN.cast{int(n/2)}(n/2)
> 
> On Saturday, February 1, 2014 9:19:53 AM UTC-5, chotu s wrote:
> 
> > This g1int\_ndiv(n,2) seems to work , it is defined in integers.sats file  
> > .
> > 
> > Thanks
> > 
> > On Sat, Feb 1, 2014 at 7:43 PM, chotu s [cho...@gmail.com](mailto:cho...@gmail.com) wrote:
> > 
> > > Thanks Brandon,
> > > 
> > > I’ll take a look inside the integers,sats .
> > > 
> > > But how do you compile following function :
> > > 
> > > fun div\_by\_2 {n:nat} ( n : int (n) ) : [m : nat] int (m) = n/2
> > > 
> > > (\* or \*)
> > > 
> > > fun ddiv\_by\_2 {n:nat} ( n : int (n) ) : [m : nat | m == n/2] int (m) =  
> > > n/2
> > > 
> > > On Sat, Feb 1, 2014 at 7:37 PM, Brandon Barker [brand...@gmail.com](mailto:brand...@gmail.com)wrote:
> > > 
> > > > But it seems that, as in C, this is the default behavior (so my  
> > > > suggestion above may not be necessary):
> > > > 
> > > > val n7 = 7  
> > > > val n8 = 8
> > > > 
> > > > val n3 = n7/2  
> > > > val () = println!(n3)  
> > > > val () = assertloc (n3 = 3)  
> > > > val n4 = n8/2  
> > > > val () = println!(n4)  
> > > > val () = assertloc (n4 = 4)
> > > > 
> > > > >

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [February 2, 2014, 5:25pm UTC](https://discourse.ats-lang.org/t/natural-numbers-division/78/9 "2014-02-02T17:25:37Z")

</div>

Good to know that you like it 🙂

In my note, I mainly meant:

1. one should have a good understanding what kind of proof is expected when  
trying to construct it in ATS
2. Do not be shy away from using unsafe casting ($UN.cast…): Get a proof  
first and worry about casting later.On Sunday, February 2, 2014 5:05:08 AM UTC-5, chotu s wrote:

> I agree with you , but I need to practice using such tool and I plan to do  
> so for most part of this year for small set of code only.
> 
> Also I don’t start code with dependent types but later after I get a  
> working code do I try convert to dependent types.
> 
> I just wanted to convert some contracts into ATS for quick sort algorithm  
> , it was just a mechanical process(not a pragmatic one). So I eventually  
> managed to get some of it converted , the code is given here : qs.dats[https://bitbucket.org/chotu/ats-explore/src/0dce1c05b6007fc876e4703c4c1c7d42a7048f2d/r1d1qs/qs.dats?at=master](https://bitbucket.org/chotu/ats-explore/src/0dce1c05b6007fc876e4703c4c1c7d42a7048f2d/r1d1qs/qs.dats?at=master)
> 
> I’ll try to convert other contracts/invariants for this code to ATS as I  
> get more familiar/practice with ATS .
> 
> I did _not_ struggle with ATS , but with my stupidity and silly mistakes  
> (for example change in order of args . incorrect spec , etc).
> 
> I must say that I now starting to like ATS , most of the stuff is  
> intuitive I believe 🙂
> 
> Thanks
> 
> On Saturday, February 1, 2014 9:11:34 PM UTC+5:30, gmhwxi wrote:
> 
> > I just want to add a note that reflects my current view of program  
> > verification:
> > 
> > First and foremost, program verification is the thought process that  
> > justifies to oneself why  
> > one’s code is correct (in a general and broad sense). Using tools (e.g.,  
> > typecheckers, theorem-provers)  
> > to ensure the correctness of this thought process is a secondary issue.  
> > This view is largely based  
> > on the way in which people construct mathematical proofs.
> > 
> > On Saturday, February 1, 2014 10:25:49 AM UTC-5, gmhwxi wrote:
> > 
> > > Or you can use ‘half’.
> > > 
> > > In practice, if I don’t know a function in the ATS library  
> > > that does what ‘div\_by\_2’ is expected to do, then I will implement it:
> > > 
> > > fun div\_by\_2 {n:nat} (n: int n): int(n/2) = $UN.cast{int(n/2)}(n/2)
> > > 
> > > On Saturday, February 1, 2014 9:19:53 AM UTC-5, chotu s wrote:
> > > 
> > > > This g1int\_ndiv(n,2) seems to work , it is defined in integers.sats  
> > > > file .
> > > > 
> > > > Thanks
> > > > 
> > > > On Sat, Feb 1, 2014 at 7:43 PM, chotu s [cho...@gmail.com](mailto:cho...@gmail.com) wrote:
> > > > 
> > > > > Thanks Brandon,
> > > > > 
> > > > > I’ll take a look inside the integers,sats .
> > > > > 
> > > > > But how do you compile following function :
> > > > > 
> > > > > fun div\_by\_2 {n:nat} ( n : int (n) ) : [m : nat] int (m) = n/2
> > > > > 
> > > > > (\* or \*)
> > > > > 
> > > > > fun ddiv\_by\_2 {n:nat} ( n : int (n) ) : [m : nat | m == n/2] int (m)  
> > > > > = n/2
> > > > > 
> > > > > On Sat, Feb 1, 2014 at 7:37 PM, Brandon Barker [brand...@gmail.com](mailto:brand...@gmail.com)wrote:
> > > > > 
> > > > > > But it seems that, as in C, this is the default behavior (so my  
> > > > > > suggestion above may not be necessary):
> > > > > > 
> > > > > > val n7 = 7  
> > > > > > val n8 = 8
> > > > > > 
> > > > > > val n3 = n7/2  
> > > > > > val () = println!(n3)  
> > > > > > val () = assertloc (n3 = 3)  
> > > > > > val n4 = n8/2  
> > > > > > val () = println!(n4)  
> > > > > > val () = assertloc (n4 = 4)
> > > > > > 
> > > > > > >