Add property checks for BinNat #1176
Conversation
| def div2(b: BinNat) -> BinNat: | ||
| match b: | ||
| case Zero: Zero | ||
| case Odd(n): n | ||
| case Even(n): prev(n) |
There was a problem hiding this comment.
this was a bug! yay for property checks!
test_workspace/BinNat.bosatsu
Outdated
| diff = sub_BinNat(left, right) | ||
| match diff: | ||
| case Zero: | ||
| match cmp_BinNat(left, right): |
There was a problem hiding this comment.
this seems bad to do internally, seems like we should be able to do this once outside the loop... should think some more.
Codecov ReportAll modified and coverable lines are covered by tests ✅
❗ Your organization needs to install the Codecov GitHub app to enable full functionality. Additional details and impacted files@@ Coverage Diff @@
## main #1176 +/- ##
==========================================
+ Coverage 91.32% 91.58% +0.26%
==========================================
Files 96 96
Lines 11846 12010 +164
Branches 2675 2778 +103
==========================================
+ Hits 10818 10999 +181
+ Misses 1028 1011 -17 ☔ View full report in Codecov by Sentry. |
test_workspace/BinNat.bosatsu
Outdated
| case Odd(right): | ||
| # (2n + 2) - (2m + 1) | ||
| # if n >= m: 2(n - m) + 1 | ||
| # if (2n + 2) > (2m + 1), then n > m |
There was a problem hiding this comment.
this is wrong... if (2n + 2) > (2m + 1) then n >= m. So, that means the invariant must actually be left >= right. So that means we only know that (2n + 2) >= (2m + 1), but that's okay, because we know an odd number can't equal an even number, so we recover n >= m.
test_workspace/BinNat.bosatsu
Outdated
| # (2n + 2) - (2m + 2) = 2(n - m) | ||
| times2(loop(left, right)) | ||
| case Zero: | ||
| # this is last because it is actually unreachable |
There was a problem hiding this comment.
this isn't true. The invariant is left >= right
test_workspace/BinNat.bosatsu
Outdated
| @@ -97,11 +142,51 @@ def times2(b: BinNat) -> BinNat: | |||
| #2(2(n + 1)) = 2((2n + 1) + 1) | |||
| Even(Odd(n)) | |||
|
|
|||
| def sub_BinNat(left: BinNat, right: BinNat) -> BinNat: | |||
| # invariant: left > right | |||
There was a problem hiding this comment.
see below: invariant: left >= right, so the comment below is wrong, we can return Zero.
add the same tests for BinNat as Nat.