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.
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.