Small inversions, 2022

This directory contains a number of .v files illustrating small inversion techniques, basically as developed in the sibling directory 2021 with improvements explained in a short paper accepted at TYPES22. The simplest example to start with is even_half.v. Two of the other examples mention the Braga method developed with D. Larchey-Wendling and reuse a number of definitions from this repository. The examples below contain places which seem out of reach of Coq standard inversion.

• files.tgz : all Coq files
• BoundedNat :
  • computing the half of an even natural number, using even as the termination certificate; probably the best introductory example;
  adaptation of finite_set.v from the paper at ITP 2013 + application to even bounded natural numbers in order to show that the technique scales up to higher dependent type. In particular we can compute the half of even bounded natural numbers.
• eqle : Yet another short proof of UIP on nat, and a proof of unicity of proofs of the standard ≤ inductive relation on nat (using UIP).
• eval_exp : adaptation of an example from the paper at ITP 2013; contains situations where 2 coupled arguments drive the hypothesis to be inverted.
• nb_steps : improvement of a very basic example from the chapter on the Braga method
• list_from_right : improvement of an example from the chapter on the Braga method; contains notable simplifications on the original developement