Polymorphism opportunities

[wdcraft01]

I was recently reviewing (admittedly at a fairly superficial level) polymorphism in Coq's Gallina language and just today was also reviewing the Max and Min classes in Prove-It where I began further developing a bit of the underlying Max and Min methods, such as the straightforward deduce_in_number_set() methods, and began wondering if we might implement some sort of polymorphism in Prove-It to help simplify or reduce a number of axioms.

It's not at all clear to me yet if it could be more generally useful (and it's not quite clear if my intuitive connection to polymorphism in Gallina is actually an appropriate comparison), but here's a very simple example. In the Max class, we have the deduce_in_number_set() method, which is bare-bones right now and limited to just being able to deduce that Max(a₁, ..., a_n) is Real if each of the arguments a₁, … a_n is real. This depends on a theorem and the Max operation that is specific to Reals. So I wrote another theorem specific to Integers and incorporated that into the deduce_in_number_set() method, and naturally began thinking about closure theorems, but began to wonder if can simply write a theorem that covers all desired specific standard sets, something like: I experimented with that and it seems to work fine. It's kind of a klunky way to achieve what I had in mind, however, where the theorem might be able to be written without the explicit listing of the meta-set K containing all the 'standard' sets to consider. It would also be nice to further include Intervals in the list of sets, but an Interval (or IntervalCC, intervalCO, etc) takes boundary arguments, so it's not clear how to include those in the theorem statement — the intervals would require another quantifier, but the standard set would not use the elements being quantified, so can we instantiate with something empty for the Interval bounds when it's not an Interval we're interested in?

[wwitzel]

We can take advantage of the fact that we are using set theory instead of type theory which offers some more flexibility. For example, a more general and simpler theorem would be Isn't this better?

[wdcraft01]

I think that looks beautiful, but a problem arises if we don't further constrain or characterize that subset S. For example, the real interval [0, 1] is a subset of the reals, but the arbitrary sum of elements from that subset is not guaranteed to produce an element in that subset. A similar problem arises for integer intervals as well. In fact, looking at my first attempt above, we run into problems with things like the non-zero Integer set as well …

[wwitzel]

But your example is "Max", not "Sum". Do you want to provide an example for "Sum" so I can better understand your point.

[wdcraft01]

Hah, I got distracted and forgot we were talking about Max. Yes, for Max this works nicely.