2024 04 16 Meeting

Participants: Pierre, Takafumi, Yves, Quentin, Reynald, Zachary

• announcements:
  • new documentation
    • report issues here: https://github.com/affeldt-aist/coq2html
    • TODO(rei): check about links to isMeasurableType and constructs generated by HB
    • pierre: use coq2html for MathComp?
      • better do it during the next months to benefit from support by Imai
  • next release 1.2.0 planned for May 15, prepare PRs accordingly
• separating pointed out of topological
  • related issue: splitting topology.v
  • goal: do not make pointed a requirement for topology
  • this is a breaking change
  • technical problem: mixins must be outside of the modules
  • zachary:
    • original plan: add everything outside of the module
  • pierre: what about putting the non-pointed structure outside of the module?
    1. add the new one with a long name
    2. deprecate the old one
    3. change the names back a few versions later Pbm: requires to change all the lemmas
  • zachary: ring has the same problem
    • the current change is an exercise towards solving the same problem with ring
  • Problems:
    • Hints do not work anymore (simple apply), needs to make the patterns more explicit
    • about the factories:
      • we want them to take the unpointed structures
      • to make it backward compatible we need to provide two versions with new notations for legacy/new modes
  • cyril:
    • what about imposing long names and explicit exports and provide as notations with a deprecation warning for the old behavior?
    • zachary: for a factory which nbhs should I use? we need two factories (the second one should call the unpointed one)
    • use the NES feature of HB instead of reexport by hand (https://github.com/LPCIC/coq-elpi/blob/master/apps/NES/examples/usage_NES.v)
    • zachary: wants to access the fields of mixin before declaring the structure, HB.reexport does not export notations by default
• new proof of Zorn's lemma
  • related PR: Zorn's variant
  • move the relation from Prop codomain to bool?
    • needs to put Prop to bool functions everywhere
    • zachary: btw, quotients cause the same problem, requiring pselect's
    • georges wants to use bool maximally, predicates in Prop and sets in bool (in this view definitions depend less on eqType and choiceType)
    • cyril prefers to have Prop everywhere and bool on demand with a meta function that translates from Prop to bool, this is implemented with a type class in Lean. We should use an HB structure, see also Peq in boolp.v
    • as a rule of thumb: use Prop rather than bool
    • wochoice.v is supposed to come before classical_sets.v, should be merged before boolp.v -> having duplicates may be tolerable
    • problems are upper_bound, lower_bound, maximum_of, nonempty because of quantifiers
    • universe consistency problem likely comes from Prop/bool conversions
    • zachary: introduce a Prop-like typeclass with field to_bool, from_bool? Prop is an instance, as well as bool
    • cyril: not sure of the implications (what is pred going to look like?)
• bernoulli, binomial, and uniform probability measures
  • implement generic semiring operations on measures?
    • see addition and multiplication for functions
  • pierre: keep only bernoulliT and get rid of bernoulli?
  • cyril:
    • suspects that bernoulliT could cause problem of inference
    • if p is out of bound, make it equal to 1
    • the definition of bernoulli would become a theorem
    • TODO(rei): to update the PR
• PR triaging:
  • lemmas about total_variation
    • TODO(zachary): review
  • moving mulr_rev
    • mulr_rev puts a new alias on the converse of the ring
    • shortcut: reimplement rev_mulr without mulr_rev
    • try to inline the definition
  • minor generalizations
    • TODO(zachary): review
• issue triaging:
  • naming notin_set issue 1190
    • notin_set -> notin_setE
  • about uniform_bigO.v issue 1141
    • add to the Mmakefile
    • rename misc to showcase
    • distinct makefile for it
    • TODO: add an all_analysis.v file