sym for arbitrary type

[phlegmaticprogrammer]

I am wondering, did you try to program sym for an arbitrary type, ideally with sym not needing to take an extra argument for the type? Is that possible with current ProofScript?

[ghost]

I'm not sure there is a way to do it without having to redo the proof of symThm for each type.

[phlegmaticprogrammer]

I am pretty sure you have to redo the proof everytime. Still, if you are prepared to do so, is it easily possible to have a polymorphicSym?

[ghost]

I think it should be easy enough. It might still be worth keeping specialised versions around, since "sym" is likely to be used frequently.

[phlegmaticprogrammer]

We should definitely keep it around. For cases like this we should have a standard way of going about this, like symThm for the theorem you get without writing any type annotations, i.e.

'∀ x y. x = y → y = x'

would be symThm, then for the prop case '∀ x:ℙ, y. x = y → y = x', that would be propSymThm, with corresponding functions sym and propSym. Finally, for the generic version something like genericSym or polySym.

[ghost]

With a means to obtain the type of a term, I think I could implement the generic version, and have it use specialised versions for the most common cases, and reproving the theorem otherwise. This can be replaced later, if necessary, with mechanisms for defining and extending generic functions (protocols, multimethods, etc...)

[phlegmaticprogrammer]

So there are two different points here mangled together:

1. Given what we currently have, with no additions, can we do polySym? We should resolve that question first.
2. How would we actually like to do it, giving ourselves the possibility to add new features to the language. I would also be interested in looking here at caching mechanisms, for example a keyword theorem! in addition to theorem which first checks if the theorem to be proven has already been proven, and otherwise executes the proof. Or just make that the default behaviour of theorem, although this might lead to confusion, as something that is written as a proof after theorem might actually not be a proof, but this is never noticed because the cache is always hit!

[ghost]

1. I've pushed a new version of equal.thy with sym now polymorphic.
2. Caching would do in this case, I think.

[phlegmaticprogrammer]

Very cool commit (1d5cbd2b7b1acc426bc0982c2be604c2c8d50e3d). I especially like how the special case is easily transformed into the generic proof procedure!

As for caching, I think your solution is an example where caching would not be a good idea, because many different (and potentially huge) theorems would be cached. It would be better to go back to your original solution and dispatch on the type if more speed is desired. But I am not sure that a speed-up is really necessary here, the code looks pretty fast to me as is. Probably it would be better to put work into making the internal ProofScript implementation optimal in the sense that the current code executes quickly even when x and y are huge terms.

[phlegmaticprogrammer]

By the way, as for indentation: if you have a single def case, you can write

def name pattern = 
   block

instead of

def 
  name pattern =
    block 

In the first case, block has to be indented relative to def, in the second case block has to be indented relative to name.

[ghost]

If you're not too worried about efficiency with sym, you might consider dropping transitive from the kernel. I've pushed a derivation of transitive as trans and included it in equal.thy

[phlegmaticprogrammer]

Sweet! I'll keep transitive in the kernel for now, though, and might also add a function symmetric, because I suspect that for the current non-optimized implementation of ProofScript this will make a huge difference in performance. But you can keep using trans and sym: if these turn out to be too slow, we just add

val trans = transitive
val sym = symmetric

in equal.thy.