Add a clearer example of constructor backtracking

Fixes #17.

Author: tchajed

src/Constructors.v

@@ -3,6 +3,44 @@ Inductive foo :=
 | bar1
 | bar2.
 
+Definition ctornum f :=
+  match f with
+  | bar0 => 1
+  | bar1 => 2
+  | bar2 => 3
+  end.
+
+(* an illustration of constructor backtracking *)
+Goal { f:foo | ctornum f = 3 }.
+  unshelve eapply exist; [ constructor | match goal with
+                                          | |- ?g => idtac g
+                                          end; reflexivity ].
+Qed.
+
+(* same as above, but more directly *)
+Definition foo_by_ctornum : {f:foo | ctornum f = 3}.
+Proof.
+  (* the tactic after the ; works only because [constructor] backtracks until
+     [reflexivity] succeeds. *)
+  unshelve refine (exist _ _ _); [ constructor | reflexivity].
+Defined.
+
+Inductive NumIsGood (n:nat) : Prop :=
+| Good0 (H: n = 0)
+| Good3 (H: n = 3)
+| Good7 (H: n = 7)
+.
+
+Lemma three_is_good : NumIsGood 3.
+Proof.
+  (* [constructor] on its own would pick [Good0], resulting in an unprovable
+  goal. Adding [solve [ eauto ]] means the whole tactic backtracks on the choice
+  of constructor. *)
+  constructor; solve [ eauto ].
+Qed.
+
+(* a fun but not very useful thing we can do with constructor backtracking is to
+print them out: *)
 Ltac constructors t :=
   let make_constructors :=
       unshelve eapply exist;
@@ -15,20 +53,8 @@ Ltac constructors t :=
 
 Goal True.
   constructors foo.
-  (* bar0
+  (* output:
+     bar0
      bar1
      bar2 *)
 Abort.
-
-Definition ctornum f :=
-  match f with
-  | bar0 => 1
-  | bar1 => 2
-  | bar2 => 3
-  end.
-
-Goal { f:foo | ctornum f = 3 }.
-  unshelve eapply exist; [ econstructor | match goal with
-                                          | |- ?g => idtac g
-                                          end; reflexivity ].
-Qed.