Skip to content

2024 04 16 Meeting

Jump to bottom
affeldt-aist edited this page Jun 5, 2024 · 3 revisions

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:
  • 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
Clone this wiki locally