Proof Trick: Small Inversions
Résumé
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.
Domaines
Logique en informatique [cs.LO]
Origine : Fichiers produits par l'(les) auteur(s)