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
Yves Bertot. Second Coq Workshop, Jul 2010, Edinburgh, United Kingdom. 2010
Liste complète des métadonnées


https://hal.inria.fr/inria-00489412
Contributor : Service Ist Inria Sophia Antipolis-Méditerranée / I3s <>
Submitted on : Tuesday, July 27, 2010 - 3:59:48 PM
Last modification on : Tuesday, May 23, 2017 - 11:20:48 AM
Document(s) archivé(s) le : Thursday, December 1, 2016 - 12:32:26 PM

File

coq2.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00489412, version 2

Collections

Citation

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

Share

Metrics

Record views

658

Document downloads

180