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.See the manual for a detailed introduction, and the Tactics reference.
Using opam:
opam install coq-procrastination
See examples/.