A small Coq library for collecting side conditions and deferring their proof
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
attic
examples
manual
src
.gitignore
AUTHORS
CHANGES.md
LICENSE
Makefile
README.md
TacticsReference.md
_CoqProject
opam

README.md

coq-procrastination

A small Coq library for collecting side conditions and deferring their proof.

Goal exists x, <... complicated expression ...>.
  (* what might x be? *)
  begin defer assuming x. exists x.
    (* go on with the proof *)
    ...
    (* discover some side-conditions about x *)
    (* |- x <= 15 *)
    defer. (* keep that for later! *)
    ...
    (* |- x >= 2 /\ x / 2 = 1 *)
    defer.
    ...
  end defer.
  (* |- x <= 15 /\ x >= 2 /\ 3/2 = 1 *)
  (* Finding a valid instantiation is now easy/automatable *)
  exists 3. repeat split; auto; omega.
Qed.

Purpose & documentation

See the manual for a detailed introduction, and the Tactics reference.

Installation

Using opam:

opam install coq-procrastination

Examples

See examples/.