FormaSys kick‐off meeting topics

Topics and people interested

Complex analysis

• Cyril
• Reynald

Drafting HB missing subject-change related commands

• Cyril
• Pierre
• Reynald
• Kazuhiko
• Enrico

Porting the inverted pendulum to mathcomp 2

• Cyril
• Reynald

Proving trajectories correct

• Yves

Important information is that the proof of correctness for the vertical cell decomposition algorithm is now complete. At this stage, it should be easy to show the two following facts:

• every segment where both extremities are strictly inside the same cell is safe
• every triangle with one point in one cell and one point in an adjacent cell, and the two segments intersecting with the same door is safe.

LRA without Stdlib

• Pierre

Parametricity and its consequences: free theorems, refinements, and induction principles

• Kazuhiko
  • I can describe the recent version of A bargain for mergesorts (NB: the publicly-available preprint is outdated), which exploits a case where parametricity implies naturality (which is also an instance of free theorems) and the fact that parametricity implies induction principles on Church-encoded datatypes (which is perhaps related to the derive plugin of Rocq-Elpi).
  • I plan to establish RocqEAL-style refinements for commutative and non-commutative polynomials in monalg.v of multinomials, derive a reflexive decision procedure for non-commutative (semi)algebras over commutative (semi)rings (by exploiting the fact that mixed commutative and non-commutative polynomials are isomorphic to non-commutative polynomials over commutative polynomials), and later extend it to non-square matrices over commutative (semi)rings using untyping theorems
• Enrico

Union-find based caching mechanism for conversion in reification in Rocq-Elpi

The idea is to reduce the calls of coq.unify-eq (and thus readback). It shouldn't be hard to implement, but the challenge would be not compromising the readability and maintainability of reification procedures, as we need to pass around the state. There is a related open issue of Algebra Tactics.

• Kazuhiko
• Enrico
  • how does this compare to tabling?
    • KS: The advantage of union-find is that it computes the symmetric and transitive closure of the set of known equations. Perhaps, we should try tabling first since it 1) looks like a lightweight yet very effective approach and 2) has the advantage that it automatically caches disequations.

Attending (please complete)

• Cyril (whole week)
• Pierre (Wed, Thu, Fri)
• Yves (?)
• Kazuhiko (whole week)
• Reynald (whole week)
• Holger (whole week)
• Enrico (mon, tue, wed)
• Jacques (whole week)
• Quentin (whole week)
• Takafumi (whole week)