Séminaire Cambium, Inria Paris
                                     BJ09
                          Vendredi 3 octobre, 10h00

                               Yannick Zakowski
                                    Inria

                         Coinduction in Rocq in 2025

A user's first contact with proofs by coinduction in Rocq can be confusing, if
not disheartning. Seemingly valid proofs are mysteriously refused at "Qed-time",
leading to a particularly painful debugging experience---especially if one is
new to coinduction altogether and struggles to figure out if the proof is
morally wrong, or simply rubbing off the system the wrong way. Luckily, this
state of affair is vastly a thing of the past! Library support has been
introduced in the ecosystem to vastly alleviate these difficulty, leaving the
user with the noble half of the task: figuring out a sound proof.

In this talk, we will discuss the foundations and implementation of coinductive
proofs for coinductive relations in Rocq. We should skim through Knaster-Tarski
fixpoint theorem, Hur et al.'s parametric coinduction, Pous's companion, and
Schäfer and Smolka's tower induction.

The talk will contain no novel research material, but will rather be a sort of
tutorial, focusing on the use of Damien Pous's library `coq-coinduction`. It
will notably use material developped at other occasions with Damien Pous.

            Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct
                            via le lien ci-dessus.