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 metadatas

Cited literature [8 references]  Display  Hide  Download

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 : Thursday, April 11, 2019 - 2:34:03 PM
Long-term archiving on: 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. Second Coq Workshop, Yves Bertot, Jul 2010, Edinburgh, United Kingdom. ⟨inria-00489412v2⟩

Share

Metrics

Record views

1604

Files downloads

503