Static pythagorean triples

Google Group
1

dataprop isPythTrip (int, int, int) =
| {a,b,c:nat | aa + bb == c*c} Trip(a, b, c)
| {a,b,c:int} NotTrip(a, b, c)

// Write prfun to take 3 integers (a, b, c) and return
// a proof that a^2 + b^2 = c^2 (or not)

prfn
is_trip {l, m, n: int} (): isPythTrip(l, m, n) =
sif ll + mm == n*n then Trip(l, m, n)
else NotTrip(l,m,n)

The highlighted symbols no longer see to refer to the static variables. I’m
probably doing several things wrong here; my main objective is to get a
feel for creating proofs for certain states (conditions).

2

Thanks - the syntax makes sense.

The example looks like it will be a fun puzzle to fill in as well.On Sat, Nov 1, 2014 at 2:04 PM, gmhwxi gmh...@gmail.com wrote:

FYI.

I did an informal proof involving Pythagorean triples several years ago:

Home Page for ATS-example

On Saturday, November 1, 2014 1:57:43 PM UTC-4, gmhwxi wrote:

This is the right way to do what you wanted:

prfn
is_trip {l, m, n: nat} (): isPythTrip(l, m, n) =
sif ll + mm == n*n then Trip{l,m,n}() else NotTrip{l,m,n}()

On Saturday, November 1, 2014 11:54:09 AM UTC-4, Brandon Barker wrote:

dataprop isPythTrip (int, int, int) =
| {a,b,c:nat | aa + bb == c*c} Trip(a, b, c)
| {a,b,c:int} NotTrip(a, b, c)

// Write prfun to take 3 integers (a, b, c) and return
// a proof that a^2 + b^2 = c^2 (or not)

prfn
is_trip {l, m, n: int} (): isPythTrip(l, m, n) =
sif ll + mm == n*n then Trip(l, m, n)
else NotTrip(l,m,n)

The highlighted symbols no longer see to refer to the static variables.
I’m probably doing several things wrong here; my main objective is to get a
feel for creating proofs for certain states (conditions).

–
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.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/8c16842f-64d8-4b93-8319-0026e75348f5%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/8c16842f-64d8-4b93-8319-0026e75348f5%40googlegroups.com?utm_medium=email&utm_source=footer
.

Brandon Barker
brandon...@gmail.com

3

FYI.

I did an informal proof involving Pythagorean triples several years ago:

http://ats-lang.sourceforge.net/htdocs-old/EXAMPLE/example_new.htmlOn Saturday, November 1, 2014 1:57:43 PM UTC-4, gmhwxi wrote:

This is the right way to do what you wanted:

prfn
is_trip {l, m, n: nat} (): isPythTrip(l, m, n) =
sif ll + mm == n*n then Trip{l,m,n}() else NotTrip{l,m,n}()

On Saturday, November 1, 2014 11:54:09 AM UTC-4, Brandon Barker wrote:

dataprop isPythTrip (int, int, int) =
| {a,b,c:nat | aa + bb == c*c} Trip(a, b, c)
| {a,b,c:int} NotTrip(a, b, c)

// Write prfun to take 3 integers (a, b, c) and return
// a proof that a^2 + b^2 = c^2 (or not)

prfn
is_trip {l, m, n: int} (): isPythTrip(l, m, n) =
sif ll + mm == n*n then Trip(l, m, n)
else NotTrip(l,m,n)

The highlighted symbols no longer see to refer to the static variables.
I’m probably doing several things wrong here; my main objective is to get a
feel for creating proofs for certain states (conditions).

4

This is the right way to do what you wanted:

prfn
is_trip {l, m, n: nat} (): isPythTrip(l, m, n) =
sif ll + mm == n*n then Trip{l,m,n}() else NotTrip{l,m,n}()On Saturday, November 1, 2014 11:54:09 AM UTC-4, Brandon Barker wrote:

dataprop isPythTrip (int, int, int) =
| {a,b,c:nat | aa + bb == c*c} Trip(a, b, c)
| {a,b,c:int} NotTrip(a, b, c)

// Write prfun to take 3 integers (a, b, c) and return
// a proof that a^2 + b^2 = c^2 (or not)

prfn
is_trip {l, m, n: int} (): isPythTrip(l, m, n) =
sif ll + mm == n*n then Trip(l, m, n)
else NotTrip(l,m,n)

The highlighted symbols no longer see to refer to the static variables.
I’m probably doing several things wrong here; my main objective is to get a
feel for creating proofs for certain states (conditions).

5

One issue with the below code is that I’m not using linear functions over
static variables, but quadratic, so I don’t think this version will really
work in the end.On Saturday, November 1, 2014 11:54:09 AM UTC-4, Brandon Barker wrote:

dataprop isPythTrip (int, int, int) =
| {a,b,c:nat | aa + bb == c*c} Trip(a, b, c)
| {a,b,c:int} NotTrip(a, b, c)

// Write prfun to take 3 integers (a, b, c) and return
// a proof that a^2 + b^2 = c^2 (or not)

prfn
is_trip {l, m, n: int} (): isPythTrip(l, m, n) =
sif ll + mm == n*n then Trip(l, m, n)
else NotTrip(l,m,n)

The highlighted symbols no longer see to refer to the static variables.
I’m probably doing several things wrong here; my main objective is to get a
feel for creating proofs for certain states (conditions).