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.
Type de document :
Communication dans un congrès
Yves Bertot. Second Coq Workshop, Jul 2010, Edinburgh, United Kingdom. 2010
Liste complète des métadonnées

Littérature citée [8 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00489412
Contributeur : Service Ist Inria Sophia Antipolis-Méditerranée / I3s <>
Soumis le : mardi 27 juillet 2010 - 15:59:48
Dernière modification le : jeudi 11 janvier 2018 - 06:22:29
Document(s) archivé(s) le : jeudi 1 décembre 2016 - 12:32:26

Fichier

coq2.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

1005

Téléchargements de fichiers

225