Way to provide "hints" for existentials

[byorgey]

For example, consider the following function definition + accompanying claim that the function is onto:

!!! ∀ n:N. ∃ m:N. f3(m) == n
f3 : N -> N
f3(n) = n // 2

The test fails, however, because for some n that it tries Disco doesn't randomly hit upon the right value of m that makes the property true. However, as humans, we know that given n, one should use m = 2n. It would be neat if there was a way to give Disco this hint so that it could just verify it rather than randomly searching for examples.

Of course one could also just rewrite the test as

!!! ∀ n:N. f3(2n) == n

but this just seems like a workaround.

[byorgey]

It's not even clear to me what the right scope for this feature would be, what syntax we would use, etc. Ideally we would come up with something that somehow fits well into things we already have, rather than creating an entirely new language feature + syntax from scratch, but I don't yet know what that might look like. This would definitely require some nontrivial design work.

[byorgey]

What if there was a simple way to give "proof terms"? For example, we could define a proof term for ∀ n:N. ∃ m:N. f3(m) == n as something like \n. (2n, refl) which could then be checked with random inputs. This seems like a pretty bad idea but maybe there's some good idea buried inside it.

[byorgey]

I'm going to close this issue since it seems like it is both too abstract (students aren't really going to use/need this feature much) and too specific (if we're going to do something like this we may as way go all the way to dependent types / integration with a proof assistant / etc).