Ltac Matching on evars and instantiation

Using Coq
1

Hi,
I am trying to construct custom tactic, where I have the requirement that the same term occurs at twice. If one of the two terms is an evar it fails (instead of instantiating the evar). The following toy example shows what I want:

Parameter (A : Type) (X : Prop) (P Q : A -> Prop).
Parameter H0 : forall a : A, X -> P a.
Parameter H1 : forall a : A, P a -> Q a.

Ltac tac :=
  match goal with
  | [H : P ?a  |- Q ?a ] => eapply H1;eauto
  end.

Goal forall (a : A), X -> Q a.
  intros.
  eapply H0 in H. (* This introduces evar ?a *)
  Fail tac. (* How can I make this work ? *)

  Fail instantiate (1 := a). (* additional question: Why does this fail? *)
  Fail instantiate (a := a). (* how is this variant used appropriately ? *)
  Unshelve. 2: exact a.
  tac.
Qed.

Also I would like to know if there is some other way to instantiate evars – in the documentation there is also a variant of instantiate with an identifier, but I can’t figure out how this is supposed to work. In fact the “num” variant is strongly discouraged, but I don’t know what else I could do.

2

what’s your intention? If you want to apply H1 and potentially instantiate evars, simply applying would work. your tactic doesn’t work, because a and ?a are not the same (but they can be unified).

3

There’s the unify tactic, which might do what you want:

Ltac tac :=
  match goal with
  | [H : P ?a  |- Q ?b ] => unify a b; eapply H1;eauto
  end.

Goal forall (a : A), X -> Q a.
  intros.
  eapply H0 in H. 
  tac.
Qed.

is_evar or has_evar together with tryif might also be of help.

Not instantiating in matches on the goal is more flexible I think, otherwise there wouldn’t be a way to distinguish evars from concrete terms.

1 Like