Hello Ramana. On 05/10/17 19:18, Ramana Kumar wrote: > 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.
Thanks for your comments. I do not think that those caveats will give problems. At most, one needs to introduce the side condition as a lemma before calling “simp” (or similar), so that it can apply use the conditional rewrite. > 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, […] At least I see it, the justification for partial definitions is a pragmatic one: To avoid some misleading results. For example, consider the hypothetical situation where one has proved a seemingly contradictory about the function; and at close inspection, one realizes that the function is being applied outside the intended domain, hence that one was able to prove the unexpected result in the first place. Regards. -- Do not eat animals; respect them as you respect people. https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ 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
