Gagallium

The second OCaml-Paris meetup took place on May 21 at IRILL; I think it was a very interesting event, with good presentations on surprisingly diverse and interesting topics.

With Pierre Boutillier, we have been working on a new Coq tactic lately, called invert. From my point of view, it started as a quest to build a replacement to the inversion tactic. inversion is a pain to use, as it generates sub-goals with many (dependent) equalities that must be substituted, which force the use of subst, which in turns also has its quirks, making the mantra inversion H; clear H; subst quite fragile. Furthermore, inversion has efficiency problems, being quite slow and generating big proof terms. From Pierre’s point of view, this work was a good way to implement a better destruct tactic, based on what he did during an internship (report in French (PDF)).