# Assumptions generated from case statements?

**URL:** <https://discourse.ats-lang.org/t/assumptions-generated-from-case-statements/709>\
**Category:** Google Group\
**Created:** [May 12, 2015, 11:29pm UTC](https://discourse.ats-lang.org/t/assumptions-generated-from-case-statements/709 "2015-05-12T23:29:14Z")\
**Posts on this page:** 9\
**Page:** 1

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [May 12, 2015, 11:29pm UTC](https://discourse.ats-lang.org/t/assumptions-generated-from-case-statements/709/1 "2015-05-12T23:29:14Z")

</div>

Hi there,

Here is a sample which pass type‑checking:

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

This one don’t:

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

So I wanted to try to be explicit:

fun loop {step: nat} .. (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)

---

<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:** [May 12, 2015, 11:35pm UTC](https://discourse.ats-lang.org/t/assumptions-generated-from-case-statements/709/2 "2015-05-12T23:35:34Z")

</div>

\_ =\> …

should be changed into

\_ =\>\> …

See:

[Redirecting to Google Groups](https://groups.google.com/forum/?fromgroups#!searchin/ats-lang-users/sequentiality/ats-lang-users/g3A2fzeKM3A/2UYOjNLVZ5sJOn) Tue, May 12, 2015 at 7:29 PM, ‘Yannick Duchêne’ via ats-lang-users \< [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com)\> wrote:

> Hi there,
> 
> Here is a sample which pass type‑checking:
> 
> fun loop {step: nat} .. (n: int step): void =  
> if n = 0 then () else loop(n - 1)
> 
> This one don’t:
> 
> fun loop {step: nat} .. (n: int step): void =  
> case+ n of  
> | 0 =\> ()  
> | \_ =\> loop(n - 1)
> 
> So I wanted to try to be explicit:
> 
> fun loop {step: nat} .. (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)
> 
> –  
> 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).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](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](https://groups.google.com/d/msgid/ats-lang-users/bbf20cec-7ce3-44a7-8be9-a9c079a1a3cf%40googlegroups.com)  
> [https://groups.google.com/d/msgid/ats-lang-users/bbf20cec-7ce3-44a7-8be9-a9c079a1a3cf%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/bbf20cec-7ce3-44a7-8be9-a9c079a1a3cf%40googlegroups.com?utm_medium=email&utm_source=footer)  
> .

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [May 13, 2015, 12:02am UTC](https://discourse.ats-lang.org/t/assumptions-generated-from-case-statements/709/3 "2015-05-13T00:02:27Z")

</div>

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

---

<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:** [May 12, 2015, 11:38pm UTC](https://discourse.ats-lang.org/t/assumptions-generated-from-case-statements/709/4 "2015-05-12T23:38:30Z")

</div>

> > 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)On Tuesday, May 12, 2015 at 7:29:14 PM UTC-4, Yannick Duchêne wrote:

> Hi there,
> 
> Here is a sample which pass type‑checking:
> 
> fun loop {step: nat} .. (n: int step): void =  
> if n = 0 then () else loop(n - 1)
> 
> This one don’t:
> 
> fun loop {step: nat} .. (n: int step): void =  
> case+ n of  
> | 0 =\> ()  
> | \_ =\> loop(n - 1)
> 
> So I wanted to try to be explicit:
> 
> fun loop {step: nat} .. (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)

---

<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:** [May 13, 2015, 1:01am UTC](https://discourse.ats-lang.org/t/assumptions-generated-from-case-statements/709/5 "2015-05-13T01:01:59Z")

</div>

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.On Tuesday, May 12, 2015 at 8:02:27 PM UTC-4, Yannick Duchêne wrote:

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

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [May 13, 2015, 3:25am UTC](https://discourse.ats-lang.org/t/assumptions-generated-from-case-statements/709/6 "2015-05-13T03:25:16Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [May 14, 2015, 5:25am UTC](https://discourse.ats-lang.org/t/assumptions-generated-from-case-statements/709/7 "2015-05-14T05:25:28Z")

</div>

> Hi there,
> 
> Here is a sample which pass type‑checking:
> 
> fun loop {step: nat} .. (n: int step): void =  
> if n = 0 then () else loop(n - 1)
> 
> This one don’t:
> 
> fun loop {step: nat} .. (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)

---

<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:** [May 13, 2015, 3:45am UTC](https://discourse.ats-lang.org/t/assumptions-generated-from-case-statements/709/8 "2015-05-13T03:45:43Z")

</div>

> > \*_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 :(On Tuesday, May 12, 2015 at 11:25:16 PM UTC-4, Yannick Duchêne wrote:

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

---

<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:** [May 14, 2015, 1:58pm UTC](https://discourse.ats-lang.org/t/assumptions-generated-from-case-statements/709/9 "2015-05-14T13:58:48Z")

</div>

You could also write:

If cond1 \* cond2 then …

Note that ‘\*’ is a function; both cond1 and cond2 are evaluates even if  
cond1 is false.On Thursday, May 14, 2015 at 1:25:29 AM UTC-4, Yannick Duchêne wrote:

> 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} .. (n: int step): void =  
> > if n = 0 then () else loop(n - 1)
> > 
> > This one don’t:
> > 
> > fun loop {step: nat} .. (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)