On Sat, Oct 5, 2019 at 6:16 PM Norman Megill <[email protected]> wrote:
> On Saturday, October 5, 2019 at 6:53:27 AM UTC-4, Benoit wrote:
>
* I just noticed that it appears in Mario's latest slides, among the first
>> definitions in peano.mm0.
>>
>
> Mario, do you use it much, and in what situations?
>
Here's an example from peano.mm0:
theorem elwrite:
$ x <> y e. write F a b <-> ifp (x = a) (y = b) (x <> y e. F) $ =
In metamath notation that would be something like:
|- ( <. X , Y >. e. write F A B <-> ifp ( X = A , Y = B , <. X , Y >. e. F
) )
This modifies the value of the function or relation F at a particular point
a, setting the value to b, and the theorem says that if x = a then it is
true exactly at y = b, otherwise it is true where F is defined. (The
nearest equivalent set.mm function is sSet.)
Personally, I think it's a good idea to have a notation, and for that
notation to be as near to identical to "if" as possible, because it's
basically circumventing a restriction of the type system that we can't just
write if ( ph , foo , bar ) whenever foo and bar live in the same sort S to
give something in sort S. You will not be mislead by thinking they are one
and the same operation.
It can also be used together with bitwise type logical operations, such as
df-cad and df-had.
In any case, I wouldn't like to see the present df-if defined in terms of
> it. I find bj-df-ifc somewhat confusing at first, at least for me,
> requiring that I unwrap a couple of layers of abstraction in my head to
> understand the otherwise simple idea. At a minimum it requires
> unnecessarily learning an extra definition that the reader probably won't
> encounter otherwise.
>
I think that if df-ifp exists, it is a given that df-if will be rewritten
in terms of it. It would be totally in keeping with other similar
definitions that define a class operation in terms of the logical analogue,
e.g. df-un, df-in, df-v etc. (Actually df-v is an exception; it should
probably read { x | T. } and I guess the use of x = x is a historical
accident?) If df-ifp exists but df-if doesn't use it, then that means
people will have to go through the mental gymnastics of understanding
df-ifp twice (with the attendant worry that somehow it can't be reused and
maybe this use is different). df-if is basically mixing two concerns, the
lifting to classes and the logical operation, and if df-ifp exists then
these concerns are cleanly separated.
My understanding has been that the reason df-ifp doesn't exist is because
it isn't used often enough to warrant definition. I think I anticipated
that it would show up more in MM0 due to the more computer science bent,
but we will see; currently the only uses are in the "write" function and in
the definition of "if" for nat (which basically serves the same purpose as
set.mm's if for classes).
Mario
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAFXXJSsjcXZW38tqhSWLyLXtxDWXQOW6VmLjRrA9XZM%2BjYd8aw%40mail.gmail.com.
