A reflection-based proof tactic for lattices in Coq

Daniel W. H. James and Ralf Hinze

Trends in Functional Programming, June 2–4, 2009, Komárno, Slovakia
PDF † | BibTEX
Source Code
.tar.gz

Abstract

This paper presents a new proof tactic that decides equalities and in­equalities between terms over lattices. It uses a decision proce­dure that is a variation on Whitman’s algorithm and is imple­mented using a technique known as proof by reflection. We will paint the essence of the approach in broad strokes and discuss the use of certified functional programs to aid the automation of formal reasoning.

Keywords

proof by reflection, Coq, lattice theory, Whitman's algorithm

† Copyright © 2011 Intellect Ltd
All rights reserved. No part of this publication may be reproduced, store in a retrieval system, or transmitted, in any form or by any means, electronic, mechanical, photocopying, recording, or otherwise, without written permission.