Coq Call 2023 09 05 - coq/coq GitHub Wiki

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 _ ^ - _