The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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.)

On Wed, Jul 23, 2014 at 3:42 PM, Jonathan <jonikelee AT gmail.com> wrote:

On 07/23/2014 10:29 AM, Jason Gross wrote:

If you have your hands on an evar in Ltac, is there a way to get it as a
goal?  For example, could I do something like:

match type of H with
   | _ /\ ?R => is_evar R; R: refine (_ : _ /\ _)
end

That doesn't work for me at all - why not ...=> is_evar R; assert R?

Also, this doesn't answer my question of how to deal with evars buried deep inside of complex terms.

-- Jonathan