Skip to Main content Skip to Navigation
New interface
Conference papers

Proof Trick: Small Inversions

Jean-François Monin 1, 2 
1 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
Abstract : 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [8 references]  Display  Hide  Download
Contributor : Service Ist Inria Sophia Antipolis-Méditerranée / I3s Connect in order to contact the contributor
Submitted on : Tuesday, July 27, 2010 - 3:59:48 PM
Last modification on : Friday, February 4, 2022 - 3:10:17 AM
Long-term archiving on: : Thursday, December 1, 2016 - 12:32:26 PM


Files produced by the author(s)


  • HAL Id : inria-00489412, version 2



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



Record views


Files downloads