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/.