BooleanAlgebrasIntro2 - News
M$ SSreflect is Ass Backwards (and M$ changed my files to DOS format!)
Item posted by Daniel Wyckoff <deluger> on Mon 24 May 2021 03:27:02 AM UTC.
The exciting thing in developing a suitable finite type library is realizing that one suitable change to a specific finite type solution carries big consequences as you can develop intricate web-works of inductive types and predicates that relay between [Prop] and [Set] in such a way that keeps the big parameters out of the way. The only way to really test a finite type theory is to see how transparent it is in your target application. On the one hand group theory is very natural. Subnormal series don't take too much sweat to hold in your head, but try defining it inductively, and you'll suddenly see why a better solution than M$ SSreflect is necessary -- not only do you have to have a common universal primitive type for any solution, but you have to induct between successive terms correctly, and for normal series and central series preserve an inductive relation as well as set-theoretic containment. So, the first little step in [FinS] was to construct from a list, rather than the successive [Props] [~In A x]. Then we mod out equivalent set analogues. That one little hitch must have had consequences of several thousand lines, as not only a natural structure and specification system emerges elegantly and elfishly, but the excitement of realizing that a couple other weird little things like that will probably emerge to be noticed, and together the common code and specification can easily be transformed into something as arbitrarily computational and powerful as anything else in the [Set] sort. Let's not forget that [SSreflect]'s brilliance is that it's fundamental inductive relation hinges on a strange potent little thing, and of the voluminous finite type theories that exist, there's a surprising amount of room for eccentric patterns that are more about noticing than crunching! There are 2 other layers of B$ in M$ SSreflect, not the usual one for the mercurial cult.
One is that all the tactics are done in reverse order, A$$ Backwards, and the other is just speculation (and specification) for idle reflection!
Oh, don't use the same flash drive to transfer between online Ubooboo and your offline Debian and anything with your dad's Window$s machines, because EVERY flash drive "needs" to be repaired by Window$, and one such repair is changing source code files to DOS format! Haha! An extra layer of manual B$, and I'm proud of the people who coded that _man_ually! But, then again SSreflect proved the Odd Order Theorem, probably the most complicated formalization of ALL TIME, and it'll be a long time before any free software solution can offer a proof script THAT all-conquering! For now, I'll just aim towards Universal Frattini Extensions. The big flaw in SSreflect is that it can't interface well with Vanilla Coq (automorphism groups of arbitrary algebras have to be put through the M$ filter) and turned into eggos and chary sweeps of some conductor with a slow strategic smile! And with that, life is good, Happy Hacking! More [FinS] and group theory, the final final steps of Recursion Theorem, and Embedded!
Powered by Savane 3.15-e6e5.
Corresponding source code