The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/23/2014 11:07 AM, Jason Gross wrote:

Er, I think I meant [refine (_ /\ _)], not [refine (_ : _ /\ _)].  [assert
R] says "give me a goal whose type is R", which isn't actually what you
want if [R] might be unprovable.  I suppose you might be able to do
something like

  let T := type of R in
  let R' := fresh in
  refine (let R' : T := _ in _);
  [ refine (_ /\ _)
  | intro R'; unify R' R ]

Maybe?

Anyway, is this what you're looking for, to find deeply nested evars?

(** Test if a tactic succeeds, but always roll-back the results *)
Tactic Notation "test" tactic3(tac) :=
  try (first [ tac | fail 2 tac "does not succeed" ]; fail tac "succeeds";
[](* test for [t] solved all goals *)).

(** [not tac] is equivalent to [fail tac "succeeds"] if [tac] succeeds, and
is equivalent to [idtac] if [tac] fails *)
Tactic Notation "not" tactic3(tac) := try ((test tac); fail 1 tac
"succeeds").

(** Traverses down nested [_ /\ _] looking for the right-most evar clause
Ltac find_right_most_evar_in_and term :=
  match term with
    | ?L /\ ?R => let check := $(has_evar R; exact I)$ in
find_right_most_evar_in_and R
    | ?L /\ ?R => let check := $(not (has_evar R); has_evar L; exact I)$ in
find_right_most_evar_in_and L
    | _ => let check := $(is_evar term; exact I)$ in term
    | _ => fail 1 "No right-most evar clause in" term
  end.

(I haven't actually tested this.)

Oh - sorry - I meant deeply nested evars in arbitrary terms, not just disjunctions as is the case with prop smuggling.   The use of evars in prop smuggling is quite trivial compared to other cases - so what really scares me about the possible deprecation of instantiate are those other cases.

Consider a somewhat messy goal like ... |- foo (bar (forall x, baz ?42 x) 0) 1.

Without instantiate, it seems like we would have to descend into this goal to find the evar - which pretty much amounts to reflecting the entire goal, right?  Just to get at that one measly evar.

Oh - wait - context can be used for that:

Ltac name_evars :=
  repeat match goal with |- context[?V] => is_evar V; set V end.

Hey, I like that!  But now one has a bunch of hypotheses each with an evar as their value.  Nicer, since now instantiate's funky numbering is no longer needed.  But, is there a way to fill in the values of those evars without using instantiate?  Hmmm:

Ltac assign name term :=
  match goal with name := ?V : _ |- _ => unify V term end.

Cool!  These tactics need to be dressed up a bit using Tactic Notation.  But, now I think I can deal with the possible deprecation of instantiate.

-- Jonathan