The Coq mailing list

[Dmitry Grebeniuk <gdsfh1 AT gmail.com>]

Hello.

  I've asked this question on #coq irc, but without any success,
so I'm writing here.

  Suppose I have some term I wish to build it partially with
refine tactic, partially with specific tactics.  refine can generate
many goals, one per "hole".  Some goals are better/faster solved
with one tactic, others with another tactic.

  So I want to apply specific tactic for each goal I've
"marked"/"named" somehow in the refine's body, and solve
other goals manually.  Also I don't want to rely on the order
of goals generated by refine, since it will require frequent
modifications of my tactic during developement.

  One of solutions is to try to apply complete set of possible
tactics to each goal (solve [ tac1 | tac2 | ... ]), but the
developement has grown, and some tactics consume few
seconds to solve/fail, and I don't want to spend time applying
tactic to the goal when this tactic will surely fail.  (suppose
I know which goals can't be solved by some tactic.)


  For example, in this code there can't be any fixed sequence
of tactics to solve goals generated by refine:


Record myrec :=
  { n : nat
  ; n_lt_10 : n < 10
  ; b : bool
  ; b_tf : b = true \/ b = false
  }
.

Require Import Omega.

Lemma bool_tf : forall b, b = true \/ b = false.
intro b; destruct b; auto.
Qed.

Goal myrec.
refine ( {| n := 7 ; b := true |} ).
omega.
apply bool_tf.
Qed.

Goal myrec.
refine ( {| n := 7 |} ).
omega.
instantiate (1 := true) (* ! *).
apply bool_tf.
Qed.

  So I want something like this pseudocode:

Goal myrec.
refine ( {| n := 7 ; n_lt_10 := ?goal_nat? ; b := true ; b_tf :=
?goal_bool? |} ).
for ?goal_nat? : omega.
for ?goal_bool? : apply bool_tf.
Qed.

(of course I understand that solution may be not so pretty as
the pseudocode, but aesthetics is not a my target.)