Email Gateway (Aug 22 2022 at 18:29): Email Gateway (Aug 22 2022 at 18:29):From: Manfred Kerber <mnfrd.krbr@gmail.com>
Dear All,
I am not too familiar with option types and have a question of how to
best use them.
More concretely, we have defined a partial function using the option
type and the function is defined on a finite number of real numbers
inside the unit interval. Then we have proved a number of properties
of this function. Now we want to also use an extended version of the
function which is defined in two further points (in 0 and 1) and want
to reuse the original proofs as much as possible.
What is the best way to extend a partial function defined via an
option type so that as much of the structure of the definitions,
theorems, and proofs can be reused?
Many thanks
Manfred
Email Gateway (Aug 22 2022 at 18:29):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear Manfred,
I see at least two possibilities. Assume your current definition of the
function is:
f :: real => real
f = some_definition
1) You write your extended function like
g = f (0 ↦ 5, 1 ↦ 7)
and then try to prove properties of g by reusing the existing theorems for f.
2) You change the definition of f itself to
f = some_definition (0 ↦ 5, 1 ↦ 7)
and then add a case-anaylsis on x = 0, x = 1, x != 0,1 to your existing proofs.
I hope some of these approaches is applicable in your case.
Best regards,
René
Last updated: Apr 25 2024 at 12:23 UTC