The Coq mailing list

[AUGER Cédric <sedrikov 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.

> I have this suggestion.
> Here, the tactics are marked directly in the 'refine'.
> Also note, that this is note very extensible, you have to know in
> advance what tactics to use.
>
> Well you can still do a
>
> Ltac new_solve :=
> match goal with
> | |- new_hole_ _ => split; new_tac
> | _ => old_solve
> end.

*)

(*
> Registering "marks"
*)
Inductive omega_hole_ (T:Type) := Omega_hole : T -> omega_hole_ T.
Notation "'omega_hole'" := (match _ with Omega_hole t => t end).
Inductive tf_hole_ (T:Type) := Tf_hole : T -> tf_hole_ T.
Notation "'tf_hole'" := (match _ with Tf_hole t => t end).

(*
> binding tactics to marks
*)
Ltac solve_marked :=
  match goal with
  | |- omega_hole_ _ => split; omega
  | |- tf_hole_ _ => split; apply bool_tf
  | _ => idtac
  end.

Goal myrec.
refine ( {| n := 7 ;
            n_lt_10 := omega_hole ;
            b := true ;
            b_tf := tf_hole
         |} );
solve_marked.
Qed.

Ltac extend_solve old_solve new_hole new_tac :=
  match goal with
  | |- new_hole _ => split; new_tac
  | _ => old_solve
  end.

(*
> This variant is nearer of what you wanted
> [Note: you still have to define the Inductives like I did before
>  but you do not have to bind marks to tactics anymore]
*)

Tactic Notation "for" constr(x) "use" tactic(y) := extend_solve idtac x
y. Tactic Notation "for" constr(x) "use" tactic(y) tactic(z)
:= extend_solve z x y.

Goal myrec.
refine ( {| n := 7 ;
            n_lt_10 := omega_hole ;
            b := true ;
            b_tf := tf_hole
         |} );
for tf_hole_ use (apply bool_tf)
for omega_hole_ use omega.
Qed.

(*
> I think you can add '?' to the marks like you did in your example
> it is not a bad idea, as it marks as obvious the holes to fill
> I am not used to Hint databases, so there may also be some interesting
> ideas with it.
*)

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