Simple boolean predicate

[spearman]

As an exercise I'm trying to define a safe subtraction function for natural numbers in a few different ways (subsorts, props, or boolean predicates) but I am having trouble figuring out the boolean predicate case:

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

// safe subtract subsort
fun mysub { m,n:nat | n <= m } (x:int m, y:int n) : int = x - y

// safe subtract prop
dataprop safesub_p (int, int)
= { m,n:nat | n <= m } mk_safesub_p (m,n)

fun mysub_p { m,n:int }
  (pf : safesub_p (m,n) | x:int m, y:int n) : int
= x - y

// safe subtract pred
stacst safesub_b : (int, int) -> bool

extern praxi lemma_safesub_b { m,n:nat | n <= m }
  () : [safesub_b (m,n)] unit_p

fun mysub_b { m,n:nat | safesub_b(m,n) }
  (x:int m, y:int n) : int
= let prval () = $solver_assert (lemma_safesub_b) in
  x - y
end

implement main0 () = (
  println!("mysub (5,4): ", mysub (5,4));
  println!("mysub_p (mk_safesub_p | 5,4): ",
    mysub_p (mk_safesub_p | 5,4));
  //println!("mysub_b (5,4): ", mysub_b (5,4)); // error: unresolved constraint
)

The above should compile but un-commenting the last function call gives an unresolved constraint.

There are a couple examples in the documentation around ATS that include examples of the boolean predicate style for fibonacci and factorial functions, but so far I haven't succeeded in translating that style to this function. fib and fact functions are defined inductively, and the predicate relates the input and output integers, so you have some existential quantification on the output, and no restriction on the input (defined for all naturals). This case (safesub) seems to be the opposite: the predicate relates only the inputs to each other. Really it looks almost the same as the first subsort implementation, but if I try this:

stadef safesub_b = lte_int_int

fun mysub_b { m,n:nat | safesub_b(m,n) } (x:int m, y:int n) : int = x - y

the unresolved constraint remains.

[gmhwxi]

>>stadef safesub_b = lte_int_int

Should it be

stadef safesub_b = gte_int_int

?

For typechecking mysub_b, you need to use Z3 to solve the
generated constraints.


[spearman]

Ah thank you for catching that, I have a habit of always writing my inequalities with LT, forgot that the arguments were the other way around!

So having $solver_assertion (lemma_safesub_b) isn't going to work in this case? Must reach for an external solver?

[gmhwxi]

Yes, $solver_assert is only supported when Z3 is used for solving constraints.

[spearman]

Thank you, this works with Z3:

// safe subtract pred
stacst safesub_b : (int, int) -> bool

extern praxi lemma_safesub_b { m,n:nat | n <= m }
  () : [safesub_b (m,n)]

unit_p

fun mysub_b { m,n:nat | n <= m }
  (x:int m, y:int n) : [safesub_b (m,n)] int

= let prval () = $solver_assert (lemma_safesub_b) in
  x - y
end

b.t.w., the SF repository at git://git.code.sf.net/p/ats2-lang/code is missing a few ./contrib/ sub directories:

- 'atscntrb-smt-z3'
- 'atscntrb-sdstring'
- 'ats2cpp'

and in the GitHub repository https://github.com/githwxi/ATS-Postiats is missing ./install-sh required by the ./configure script.

[gmhwxi]

>>b.t.w., the SF repository at git://git.code.sf.net/p/ats2-lang/code is missing a few ./contrib/ sub directories:
- 'atscntrb-smt-z3'
- 'atscntrb-sdstring'
- 'ats2cpp'

Thanks for reporting it. They will be included in the next release (ATS2-0.3.5).

>>and in the GitHub repository https://github.com/githwxi/ATS-Postiats is missing ./install-sh required by the ./configure script.

install_sh is shipped with Linux; it is supposed to be linked to the version available on the computer one is using.