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.