Assumptions generated from case statements?

[Yannick Duchêne]

Hi there,

Here is a sample which pass type‑checking:

fun loop {step: nat} .<step>. (n: int step): void =
  if n = 0 then () else loop(n - 1)

This one don't:

fun loop {step: nat} .<step>. (n: int step): void =
  case+ n of
  | 0 => ()
  | _ => loop(n - 1)

So I wanted to try to be explicit:

fun loop {step: nat} .<step>. (n: int step): void =
  case+ n of
  | 0 => ()
  | _ =>
    let prval () = prop_verify_and_add{step > 0}()
    in loop{step - 1}(n - 1)
    end

It seems not ovious to the checker, that `step` is greater than zero. It knows it when an `if` statement is used, and don't when a `case` statement is used.

This raises the question: what are the assumptions automatically generated by a case statement, if there are?

Or may be to be more general: what statements generates what assumptions?

A question aside: the “add” in `prop_verify_and_add` means “add to the store of available assumptions”, isn't it? (just to be sure)

[Hongwei Xi]

_ => ...

should be changed into

_ =>> ...

See:

https://groups.google.com/forum/?fromgroups#!searchin/ats-lang-users/sequentiality/ats-lang-users/g3A2fzeKM3A/2UYOjNLVZ5sJ

--
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/bbf20cec-7ce3-44a7-8be9-a9c079a1a3cf%40googlegroups.com.

[gmhwxi]

>>A question aside: the “add” in `prop_verify_and_add` means “add to the store of available assumptions”, isn't it? (just to be sure)

Yes, that is true.

If you really want to do it this way, you need to add the following line first:

val () = assertloc (n > 0)

[Yannick Duchêne]

Le mercredi 13 mai 2015 01:38:30 UTC+2, gmhwxi a écrit :

If you really want to do it this way, you need to add the following line first:

val () = assertloc (n > 0)

I don't know if “need”  means “should” or “must” here, as it seems to type-check without it and the `=>>` is enough. Or may that's because the sample is simple.

[gmhwxi]

Using =>> is the right way to address the issue here.

However, I want to make a point that I think is rather important in practice.

ATS has a lot of features. Compare it to C++. To use a feature, one has to
know it first. If one tries to do everything in ATS rigorously, then the learning
curve would be too steep to be acceptable. So my point is that one should be
ready to use features like $UN.cast and assertloc to bypass typechecking,
sometimes.

Being rigorous means very little if proofs/programs could not be effectively
constructed in the first place. So I keep emphasizing here on program-first
program verification.

[Yannick Duchêne]

Le mercredi 13 mai 2015 03:01:59 UTC+2, gmhwxi a écrit :

Using =>> is the right way to address the issue here.

However, I want to make a point that I think is rather important in practice.

ATS has a lot of features. Compare it to C++. To use a feature, one has to
know it first. If one tries to do everything in ATS rigorously, then the learning
curve would be too steep to be acceptable. So my point is that one should be
ready to use features like $UN.cast and assertloc to bypass typechecking,
sometimes.

I see: `assertloc` is a runtime check, **which adds an assumption**. I always though it was just like a debugging utility method as is `assert` or similar in other languages.

Indeed, that make it a good path to go toward check ahead without being blocked on an unsolvable case on the beginning. It happened I wished the languages with dynamic assertions (ex. Python), could make some assumptions based on the assertions statement. So ATS has this… very good to know.

[gmhwxi]

>>**which adds an assumption*

Yes!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! :)

This is the point. Trying to use run-time checks to establish
static assumptions is cheap and effectively. A lot of people
are kind of shy about using run-times checks; they prefer to prove
these assumptions. More likely than not, these people do not get
to write a lot of code at the end. Actually, more likely than not, they
do not get to write much functioning code at the end :(

[Yannick Duchêne]

Le mercredi 13 mai 2015 01:29:14 UTC+2, Yannick Duchêne a écrit :

Hi there,

Here is a sample which pass type‑checking:

fun loop {step: nat} .<step>. (n: int step): void =
  if n = 0 then () else loop(n - 1)

This one don't:

fun loop {step: nat} .<step>. (n: int step): void =
  case+ n of
  | 0 => ()
  | _ => loop(n - 1)

[…]

Something similar with conjunctions. Doing this:

if cond1 && cond2 then
  …

Conclusions from `cond1` are seen, but not conclusions from `cond2`, and this, has to be used instead:

if cond1 then
  if cond2 then
    …

(I don't mind, I'm noting this here for documentation)

[gmhwxi]

You could also write:

If cond1 * cond2 then ...

Note that '*' is a function; both cond1 and cond2 are evaluates even if cond1 is false.