natural numbers division

[chotu s]

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

[Brandon Barker]

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.com

> --
> 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.
> To post to this group, send email to 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.

[Brandon Barker]

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)

[chotu s]

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

[chotu s]

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

Thanks

[gmhwxi]

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)

[gmhwxi]

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.

[chotu s]

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

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

[gmhwxi]

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.