Minutes February 20 2020 - math-comp/math-comp GitHub Wiki

About lattices:

• for a formalization of polyhedral geometry Pierre Yves & Xavier needs many variants of lattices
  • inf meet
  • inf bot
  • sub
  • covering
• Seems a good test case for HB, but lattices have a "display" parameter
• Kazuhiko has an idea about dual lattices, but needs primitive record
  • atomic, co-atomic, co-co-*
  • they need (dual (dual l)) === l
  • trick combining primitive records (for eta) and canonical inference
  • currently eta breaks canonical inference (loop?)
  • Georges: maybe eta can be simulated via a default CS (see also the 3 projections used in hypermaps of 4CT)
  • Kazuhiko will open a proper bugreport for Coq about primproj + CS inference
• Pierre Yves will extract meaningful bits from polyhedral repo and add it on a order.v

About release:

• Pierre Yves says currently master drifted from 1.10 with renaming and there are no backward compatibility aliases. There is a compat module in ssrnum but is not opened by default. Pierre Yves will report some of these issues, but his library does not cover much of ssrnum.

About commutative in mini mathcomp and the hack of making them Notations:

• Coercion classes cannot be syndefs
• Makes sense to have these properties be actually definitions
• Conclusion: fix in Coq/SSR, attribute #[unfold in Search]
• Search could see that the query is on a CS instance and rephrase the query on the abstract form
• mini_bigop cannot find a place in MC, too different

Laurent is curating:

• https://github.com/math-comp/tutorial_material
• extra material is welcome

Next meeting is on: 12 March at 11AM