Skip to content

Latest commit

 

History

History
8 lines (6 loc) · 302 Bytes

README.md

File metadata and controls

8 lines (6 loc) · 302 Bytes

Duality Tactic for Lattice Theory

This new Coq tactic duality allows you to prove a lattice theory (in)equality if its dual has already been proven.

For a demo:

  1. Compile with make clean; make.
  2. Run Duality.v either from the command line, or from the Coq IDE.

Tested on Coq version 8.9.0.