In this meeting, the speaking time was mostly given to Jelle Wemmenhove from Eindhoven university, who used the slides provided here. In particular, these slides contain a wish list of features that the Waterproof developers would like to see in in Coq, so that they could exploit them in their proof environment. Here is a summary of this wish list.

- Mathematical library for education, possibly including tactics
- Waterproof can use this library with little interfacing
- Library plays together nicely with Waterproof style automation
- special care around rewrite
- combine
`lra`with inequality lemmas in hint databases - high-quality feedback from automation procedure, including when user specifies the lemma that is to be used

- Library uses common mathematical notation
- Subsets like in normal math, with usual inclusions (natural numbers in integers, in rational numbers, in real numbers)
- Avoid educationally probelmatic naming of dummy variables
- Native support for chains of (in)equalities
- Non-expert level documentation

In the STAMP team, researchers took the decision to modify parts of Coq to make the language evolve in the expected direction. One of the difficulties of "vanilla-unmodified" Coq comes from limitations in the way coercions can be added between types. Thanks to our extensions of Coq, users can add coercions that would not be accepted in Coq.

A demonstration of of the added capabilities was performed
by Quentin Vermande. This showed that a set could be defined by comprehension,
as a special instance of a generic construction. The set appeared as a
*subset* of an existing type, but it could also be used as a proposition,
thanks to a membership relation. This made the following lines possible
in a Coq script.

(* Define even as a subset of the type nat *) Definition even : set nat := [set n | exists m, n = 2 * m]. (* Thanks to the membership relation ... \in ... this can be used as a proposition, well typed if x is a natural number. *) Check (fun x : nat => x \in even). (* The set "even" can also be used as type, and its elements can automatically be used as natural numbers (members of the super-type) *) Check (fun x : even => x * 3). (* We can express that a multiple of an even number is even, but of course this does not constitute a proof. *) Check (fun x => x \in even -> x * 3 \in even). (* Because there is no proof, viewing (x * 3) as an even number provokes a typing error. *) Fail Check (fun x : even => (x * 3 : even)). (* But we can prove that a multiple of an even number is even. *) Lemma times_3_even (x : even): x * 3 \in even. Proof. move: (memP x). (* This adds the information "x \in even" in the goal. *) rewrite !setE. (* This expands the definition of even, exposing *) (* the existential statements. *) move=> [m ->]. (* These are plain proof steps, in the style of *) exists (3 * m). (* ssreflect. *) lia. Qed. (* Once the proof is performed, it can later be used to help the *) (* proof system construct even numbers *) HB.instance Definition _ (x : even) := times_3_even x. (* This command failed earlier, but is now accepted. *) Check (fun x : even => (x * 3 : even)).

researchers willing to reproduce this experiment can do so by executing the following commands.

opam switch create liberabaci-demo ocaml-base-compiler.4.13.1 opam repo add liberabaci-released https://www-sop.inria.fr/members/Yves.Bertot/tmp/liberabaci-released opam install coq-hierarchy-builder.20240229 eval $(opam env)

You should then download demo-liberabaci-feb-2024.zip, extract the archive, compile `sets.v` (with `coqc`), and execute `demo.v` and execute in your favorite working environment. The important lines are at numbers 136 to 180.