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

https://hal.inria.fr/inria-00489412
Contributor : Yves Bertot <>
Submitted on : Friday, June 4, 2010 - 4:09:30 PM
Last modification on : Thursday, April 11, 2019 - 2:34:03 PM
Long-term archiving on: Friday, October 19, 2012 - 3:36:05 PM

File

paper_1.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00489412, version 1

Collections

Citation

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

Share

Metrics

Record views

15

Files downloads

165