My intuition says that working with total functions (and especially
predicates) will be easier.
Why? I don't know exactly, but here are some possible reasons:
you can just use plain rewriting rather than conditional rewriting,
and you don't need to state so many assumptions explicitly on your
theorems.
I also want to make a point against the supposed elegance of partial
definitions. My understanding is that it seems more elegant to not
specify a function on inputs that are supposed to be "invalid" for
that function, because then you know your proofs don't depend on how
the function behaves on those inputs. In theory you could substitute
any function which agrees only on the valid inputs. However,
practically, I've never seen this work out. Nobody takes a proof on
an underspecified function and transports it to another setting with
another function that's the same on valid inputs, at least not
without doing substantial work. But often people do run into annoying
problems due to underspecification.
On 6 October 2017 at 06:04, Mario Castelán Castro <marioxcc...@yandex.com>
wrote:
> Hello.
>
> What is the preferred way to define functions only for some values? For
> example, as in arithmetic$DIV in HOL?:
>
> ⊢ ∀n. 0 < n ⇒ ∀k. k = k DIV n * n + k MOD n ∧ k MOD n < n)
>
> Here nothing is asserted for the value of DIV for n = 0, thus it is
> “undefined” in some sense. I know that this can be done with
> “new_specification” but proving _trivial_ existence theorems seems like
> something that should be automatized.
>
> I am writing a formalization of elementary topology[1]. I have to define
> the concept of the interior, closure, etc. Currently I use total
> definitions. I am thinking that it may be more elegant to use a partial
> definition like the above.
>
> For example, currently I have the definition:
>
> interior To X r ⇔
> is_topo To ∧ X ⊆ space To ∧ r ∈ space To ∧
> ∃Y. r ∈ Y ∧ Y ⊆ X ∧ Y open_in To
>
> I want to change this to:
>
> is_topo To ∧ X ⊆ space To ⇒
> interior To X = ⋃ {Y | Y ⊆ X ∧ Y open_in To}
>
> Is there some expected difficulty with this under-specification?
>
> Thanks.
>
> [1] <https://puszcza.gnu.org.ua/projects/hol-proofs/> (work in progress).
>
> --
> Do not eat animals; respect them as you respect people.
> https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
>
>
> ------------------------------------------------------------
> ------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
