Proof Trick: Small Inversions

Jean-François Monin (1, 2)

1 FORMES - Formal Methods for Embedded Systems
2 UJF - Université Joseph Fourier - Grenoble 1

We show how an inductive hypothesis can be inverted with small proof terms, using just dependent elimination with a diagonal predicate. The technique works without any auxiliary type such as True, False, eq. It can also be used to discriminate, in some sense, the constructors of an inductive type of sort Prop in Coq.

Domaines: Logique en informatique [cs.LO]

Jean-François Monin. Proof Trick: Small Inversions. Second Coq Workshop, Yves Bertot, Jul 2010, Edinburgh, United Kingdom. ⟨inria-00489412v2⟩