Abstract Algebra

in F*

Alex Rozanov

Why would we need this in F*

• Uniform handling of different kinds of objects, as long as they possess certain structure
• Square Matrices
• Polynomials
• Vectors
• Strings (although the structure may differ depending on the task at hand)

​

• Getting functions and proofs for concrete properties that come for free from the corresponding abstract algebra structure axioms
• Unit matrix uniqueness lemma
• Euclidean division algorithm, but for polynomials

i.e. once you have shown that your objects form a ring, you get all the ring lemmas defined in the algebra framework for free. As simple as System.Collections.Generic.List<T> in .NET is, but {|ring t|} offers way more flexibility than <T>.

Prerequisites & prelims

I. Equivalence Relations

Pretty much obvious to any good first-year.

• reflexivity (x=x)
• symmetry ((x=y) ⇔ (y=x))
• transitivity (((x=y) /\ (y=z)) ⇒ (x=z))

Any equivalence relation can be used to construct sets of equivalence classes.

• We certainly want this as a mechanism in F*, but we’re not there yet :(

(a `eq` b) is the most typical goal in abstract algebra – but currently F* does not treat custom equivalence relations as anything special.

In my current implementation, equivalence relations are all t → t → bool (not prop!)

Prerequisites & prelims

II. Single Operation Algebraic Structures (S, · )

• We add congruence as an axiom: our custom equivalence relation should respect the set operation: ((a `eq` b) /\ (c `eq` d)) ⇔ ((a · c) `eq` (b · d))
• We add more and more structure to our set by adding axioms:
• Associativity is the requirement for semigroups ( (AB)C = A(BC) )
• Identity axioms are needed for monoids (∃e. ∀x. ((x e = x) /\ (e x = x)))
• Inverse elements for all set members make (S, · ) a group (∀x. ∃x⁻¹. ((x x⁻¹ = e) /\ (x¹ x = x)))
• Semigroups, monoids and groups have their commutative counterparts

We separately define typeclasses for (*) and (+), as (+) tends to be commutative almost always.�The only exception I know of is cardinal addition, and I doubt we’ll ever need that in F* anyway.

Prerequisites & prelims

III. Ringlikes (R, · , +)

​

• Ring definition is also first-year stuff:
• (R, +) is a commutative group
• (R, · ) is a monoid (if ( · ) is also commutative, the ring is called a commutative ring)
• (+) and ( · ) obey both distributivity laws
• the two distributivities are the same thing for commutative rings
• polynomials with addition and composition do NOT form a ring
• but linear polys, on the other hand…
• This is usually omitted in algebra textbooks, but we must keep it in mind
• The equivalence relation used in (R, +) must be the same as the one used in (R, · )
• Ring is a domain, if the cancellation law holds
• Domain is called integral domain, if it is commutative
• Domain is a skewfield (division ring), if (R\{0}, ·) is a group
• Skewfield is a field, if it is commutative.
• Fun fact: every finite domain is automatically a field.
• Yes, cancellation would imply both commutativity and existence of inverses

The Lean Way to do it

Now onto F*

Approach I. Records (F* demo is shown in parallel)

Downsides

• F* offers no record inheritance, so the definitions are ugly
• You will always make shortcuts like let ( * ) = ring.multiplication.op in
• Your formulas in pre/post-conditions would be ugly and barely human-readable
• As you make more and more structures, your basic record gains more and more fields that only get their meaning in the most advanced of successors
• The alternative is encapsulating stuff, and then you’re bound to have �field.domain.ring.multiplication.op, �field.domain.left_cancellation_law, �field.inverse_law,�but without all the coloring which I carefully chose to make stuff human-readable

Upsides

• Proofs are usually lightning fast – at least compared to typeclass-based implementations
• But I currently only have ~10 typeclasses — why is it already slow at this scale?

Key definitions in AlgebraTypes.fst

Typeclass-based implementation

(F* demo is shown in parallel)

• A typeclass equatable defined for some type with a custom equivalence relation would allow to redefine (=), making formulas human-readable again
• all eqtypes would get an equatable instance for free
• for the rest – and for eqtypes with overridden (=), we no longer have (a = b) ⇒ (a == b)
• Typeclasses has_mul and has_add offer the same for (+) and (*)
• Typeclass inheritance is emulated via special attribute usage that prevents projector generation
• Refinements ensure consistency in diamond inheritance scenarios
• e.g. child_class.base1.equatable == child_class.base2.equatable
• Manually generated instances propagate the projector definitions from base typeclasses to children
• Lemmas are way easier to read, but often slower to verify
• Perhaps, we need to cache more stuff when resolving typeclasses

Notable results so far

• Construction of fields of fractions for arbitrary integral domains
• Equivalence is properly induced from the parent ring, (a/b ~ c/d) ⇔ (ad = bc)
• Sums and products of fractions are defined as you would expect them to be
• All the lemmas are provided to ensure the resulting structure being a field
• Polynomials over a commutative ring R forming a commutative ring R[x]
• Quite non-trivial proofs for multiplication commutativity and associativity
• Notion of compact polys that would eliminate ambiguities like 0x+1 = 1
• Construction of FStar.Algebra.CommMonoid.Equiv.cm (comes for free)
• for example, for list/seq fold connectivity
• Matrices with coefficients from some commutative ring
• Already in FStar’s ulib, see FStar.Matrix module
• Quite non-trivial commutativity and (especially) associativity proofs

Good practices

• Keeping the context as clean as possible
• Sometimes it is tempting to just throw every basic lemma into Classical.forall_intro cauldron
• While rewarding in little stand-alone lemmas, this can easily get bigger proofs unstable due to lots of unwanted facts preventing the prover from seeing the forest for the trees
• Use of opaques
• Some properties and definitions use forall in their definitions, which leads to lots of facts being generated inevitably, which in turn increases the strain on verifier
• Marking heavy definitions with [@@”opaque_to_smt”] keeps the context clean and lightweight
• This is extremely well-shown in AlgebraTypes.fst, where absolute majority of definitions are opaque, and helper lemmas are used to obtain concrete facts about concrete objects, rather than drowning the verifier in a sea of facts about each variable in the context
• Some lemmas are instantly proved automatically with just a few carefully chosen reveal_opaque invocations
• Keeping the assertions
• Since I almost never touch SMTPats, assertions only serve the purpose of debugging my lemmas, as I often need to know whether at some point, some fact is proved already or not
• Still, one well-placed assertion is worth several lines of comments as it explains the thought process behind the proofs. Some proofs, while being fully valid from F*’s point of view, appear completely arcane to people with moderate F* exposure, and a few asserts turn them from arcane to obvious
• Until your proof isn’t finished, no assertion is obvious and safe to remove. Trust me on that.

Good practices

• calc proofs are sometimes just vital, especially in abstract algebra, in current F*
• well suited for custom equivalence relations due to calc accepting any custom relation func
• easier to read and understand, because the syntax exposes the sequential structure of the proof
• if you’re ever going to prove a formula, knowing how calc proofs work is a must
• usually you’ll need a Classical.forall_intro call on the transitivity lemma of the equivalence relation
• poor man’s calc is trans_lemma_4 and trans_lemma_5, as done in AlgebraTypes.fst:44
• 4-argument associativity lemma helps a lot see AlgebraTypes.fst:110
• bulky to write, but once written, would simplify lots of proofs
• 5-assoc is too rare and too bulky to bother writing
• probably one just needs tactics with this – but I don’t yet know how to write custom tactics :(
• Simple induction in recursive proofs see FStar.OrdSet.fst:22
• a generic utility could help proving lots of facts with minimal effort, as I’ve shown in FStar.OrdSet
• sometimes, custom decreases could help, e.g. (decreases length s1 + length s2)
• Complex proofs are always worth splitting in smaller auxiliary lemmas
• verification time will improve, almost always
• you might even get a chance to reuse these aux lemmas in other proofs

What to be aware of

• Some statements are surprisingly proven via assert_norm while demanding fuel increase otherwise, notably foldm_snoc cm (singleton x) == cm.mult cm.unit x.
• I’d rather avoid relying on the fact entirely, as this is clearly implementation detail, as silently changing the library func foldm_snoc to return x for any input (singleton x) would break the proof!
• And some other statements, notably (fun x -> … == fun y -> …), would also require assert_norm, which is completely confusing to an outsider :)
• Generally, it is best to stay away from reasoning about equality of functions, unless you feel experienced enough and brave enough at the same time
• Still, I did some proofs in this fashion, notably proofs on nested folds (now they’re part of F*)
• F* code formatting style can be easily misleading, as we tend to write� let x = smth in rather than let x = smth in� let y = smth in let y = smth in
• But once you know of this, you can use it to your advantage, eliminating quite a few of redundant begin .. ends in your code!

What often goes wrong

• Lots of forall facts in the proof context
• This just leads to increased rlimit requirements
• But certain simple facts are insta-proven automatically with this, so in these cases why not
• Especially if we forall_intro the associativity (or, god forbid, congruence) lemma
• Bigger proofs will either demand bigger rlimits, or just fail (unless we wait for minutes)
• Reasoning about lambdas, especially while adjusting domains
• All it takes is one recursive lemma with a lambda that has its domain depending on decreasing arg
• Functions on restricted domains
• notably partial inverse function that only works on some subset of a semigroup
• Complex record refinements (see Fractions.fst)
• This is relatively new regression; was also fast in older F* versions

What F* currently lacks

• inheritance
• partially emulated in typeclasses. Still requires manually constructed instances for all public parents to access lemmata declared in parent classes
• not available at all in records
• (a) declare all fields in the least advanced type, refine as needed
• (b) encapsulate less advanced record
• operator overload
• currently have to construct int and nat instances for has_mul and has_add
• sometimes have to write (x <: int) to invoke (=), (+), ( * )
• painfully slow typeclass resolution
• even when there are only few
• integer literal coercion
• natural numbers could be used in context of any semiring
• integers could be used in any ring
• would be great to have 1*x automatically understood as �(ring.multiplication.neutral * x)
• could come for free with operator overload (?)

Points of interest

• Tactics-driven proofs in user-defined grouplikes and ringlikes
• Real typeclass inheritance (as done in Lean)
• Operator Overloads
• Vector spaces and modules, both featuring S-multiplication
• (10*x) makes sense, but (y*x) also does!
• Maybe more fluent handling of equality
• Special Constants Coercion
• Imagine F* automatically accepting 1 and 0 as special constants for any generic ring!
• Profiling and improving verification performance
• Step-by-step debugging. Both with tactics and without. Please!
• Abstract Algebra API enrichment
• More structures and more clear distinctions
• Unique Factorization Domains! Principal Ideal Domains! Euclidean ones! ACC! DCC!
• More lemmas proving more delicate properties
• Which ring properties are preserved under polynomial ring construction?
• Links and maps between structures
• Constructions (Fractions, Polynomials, Factor Rings…)
• Documenting stuff (this is ironically last, but we all know this is not least)
• There is no point in the API if nothing is written on how to use it

My own motivation and roadmap

• Polynomials, field extensions
• what does ℝ[x]/(x²+1) really mean? Besides the loss of meaningful order I mean…
• how and why is ℚ[π] the same thing as ℚ[x], but an entirely different beast from ℚ[√2]
• The notion of algebraic closure and polynomial splitting field
• So good to start with ℂ, too bad we can’t use it in practice
• how does one compute the polynomial splitting field?
• Imagine PROVING the property in F*...
• Rings and Fields with derivation defined
• Extension of derivation onto (K[x])[t]
• Algebraic and transcendental extensions
• When is K[t] already also a field?
• How to construct the smallest field containing K[t]?
• Derivation in Quotient fields ℚ → ℚ[x|Dx=1] → ℚ[x][t|Dt=t] → …
• Antiderivatives, and what form do they naturally take
• Imagine them not being an example of warlock-grade chaos, comparing ��
• Liouville’s Theorem (proving it would mark a really huge milestone)
• This would finish the foundations necessary to (merely) start approaching Risch’s Integration Algorithm

Links

• All the F* stuff I’m working on is available on my github,�
• https://github.com/hacklex/CuteCAS
• https://github.com/hacklex/FStarBisect
• https://github.com/hacklex/AbstractMathTypes
• F#, but I’ll eventually prove things from there and introduce them to CuteCAS
• Real CAS stuff:
• K. Geddes, S. Czapor, G. Labahn – Algorithms for Computer Algebra
• M. Bronstein – Symbolic Integration Tutorial
• Mathlib in Lean (thankfully loads of documentation on this one)