Coq Call 2023 09 05

• September 5th 4pm UTC+2 (Paris time zone offset)
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

Looking for feedback about a few experiments made during summer (Hugo):

• CEP #72 and PR #17888 on discharging on the fly
• support for extruding uniform parameters (the standard failure with map not in a section, PR #17986) and for dynamically recomputed recursive structure in guard condition (the standard asymmetry between recursing on tree or on list tree, PR #17950)
• an analysis of the treatment of associativity in gramlib (CEP #71)
• a short proposal, CEP #73, to resolve the conflict between expanding (for typing) or not (for guard checking) aliases in pattern-matching
• a refinement of the criterion propagating the size through a match with applicability to small inversion and definitional UIP, PR #14359

Notes

Participants: Gaëtan, Guillaume, Hugo, Matthieu, Pierre, Pierre-Marie

Only gramlib point discussed

• agreement on the fact that we should get rid of the recovery mechanism
  • would break things like _ /\ forall _ -> moving forall at level 10 seem a reasonable solution
  • other issue with unary minus: have to experiment
• PM: while at it, should get rid of the numbered level and use strings
  • more modular
  • then no more total order, we could let user add constraints (and rebuild the grammar each time) like we do for universes, asking for a lattice?, what to do when no order specified, do something arbitrary like is already the case?
  • PM: no need for any change in (our fork of) camlp5
• Guillaume: somehow, unary minus should have its argument at the level where the preceding operator is, that is, in a + - b, a * - b, a ^ - b, b should be respectively parsed at the level of +, *, and ^
• further discussion on minus with only Guillaume, Hugo and Pierre
  • move forall at level 10 (has to be below /\ at level 80 but also fun/let)
  • while at it move unary minus from level 35 to level 48 (would fix - a * b being parsed (- a) * b instead of - (a * b)), orthogonal, will likely break things but backward compatible fix by adding parentheses
  • test removing recovery mechanism on stdlib (Hugo) and mathcomp (Pierre)
  • if it helps we can add hack notations like _ ^ - _