Apply a lemma under binders

There are some cases where apply lem will fail, but intros; apply lem will succeed. The tactic binder apply is like intros; apply lem, but it cleans up after itself by reverting the things it introduced. The tactic binder apply lem in H is to binder apply lem, as apply lem in H is to apply lem. Note, however, that the implementation of binder apply lem in H is completely different and significantly more complicated.

The tactic eval_under_binders tac H is equivalent to tac H if H is not a product (lambda-abstraction), and roughly equivalent to the constr fun x ⇒ eval_under_binders tac (H x) if H is a product.

Bind a convenient name for the recursive call

If the hypothesis is a product (∀), we want to recurse under binders; if not, we're in the base case, and we simply compute the new term. We use match rather than lazymatch so that if the tactic fails to apply under all of the binders, we try again under fewer binders. We want to try first under as many binders as possible, in case the tactic, e.g., instantiates extra binders with evars.

Standard pattern for recursing under binders. We zeta-expand to work around https://coq.inria.fr/bugs/show_bug.cgi?id=3248 and https://coq.inria.fr/bugs/show_bug.cgi?id=3458; we'd otherwise need globally unique name for x. We zeta-reduce afterwards so the user doesn't see our zeta-expansion. We use x in both the pattern and the returned constructor so that we preserve the given name for the binder.

Base case - simply return tac H

The tactic make_tac_under_binders_using_in tac using_tac H uses tac to transform a term H, solving side-conditions (e.g., if tac uses apply) with using_tac. It returns the updated version of H as a constr; if H is a hypothesis in the context, it does not modify it. Conceptually, make_tac_under_binders_using_in tac idtac H is the composition of two tactics: a transform_under_binders : (constr → constr) → (constr → constr) that runs a tactic under the binders of the constr it's given, and what would be an eval tac in H, except for the fact that, e.g., eval rewrite in H doesn't actually work because it predates tactics in terms (we use eval_in_using tac using_tac H instead). The arguments are:

• tac - should take the name of a hypothesis, and modify that hypothesis in place. It could, for example, be fun H ⇒ rewrite lem in H to do the rewrite H under binders.
• using_tac - used to solve any side-conditions that tac generates. Not strictly necessary, since tac can always solve its own side-conditions, but it's sometimes convenient to instantiate tac with fun H ⇒ eapply lem in H or something, and solve the side-conditions with eassumption.
• H - the name of the hypothesis to start from.

N.B. We do not require Funext to use this tactic; Funext would only required to relate the term returned by this tactic and the original term. Note also that we only rewrite under top-level binders (e.g., under the x in a hypothesis of type ∀ x, P x, but not under the x in a hypothesis of type (fun x y ⇒ x + y) = (fun x y ⇒ y + x)).

If we try to apply HB, wanting to replace C with B, we get an error about being unable to unify B ? with A.

The tactic binder apply fixes this shortcoming.

We Abort, so that we don't get an extra constant floating around.

If we try to apply HB in HA, wanting to replace B with C, we get an error about being unable to instantiate the argument of type A: "Error: Unable to find an instance for the variable x."

The tactic binder apply fixes this shortcoming.

We Abort, so that we don't get an extra constant floating around.

We need to apply path_forall under binders five times in H'. We use a different variant each time to demonstrate the various ways of using this tactic. In a normal proof, you'd probably just do do 4 binder apply (@path_forall _) in H' or just repeat binder apply (@path_forall _) in H'. If we do binder apply path_forall in H', we are told that Coq can't infer the argument A to path_forall. Instead, we can binder eapply it, to tell Coq to defer inference and use an evar for now.

Alternatively, we can make A explicit. But then we get an error about not being able to resolve the instance of Funext. We can either tell Coq to solve the side condition using the assumption tactic (or typeclasses eauto, for that matter), or we can have typeclass inference run when we construct the lemma to apply. Some versions of Proof General are bad about noticing Fail within a tactic; see http://proofgeneral.inf.ed.ac.uk/trac/ticket/494. So we comment this one out.

  Fail binder apply @path_forall in H'.

Error: Tactic failure: Cannot use <tactic> to solve side-condition goal Funext . Extended goal with context: (Funext -> forall (A : Type) (f g : A -> A -> A -> A -> A) (H' : forall x' x'0 x'1 : A, f x' x'0 x'1 = g x' x'0 x'1), let H0 := H' in Funext).

Now we have removed all arguments to f and g in H'.

We Abort, so that we don't get an extra constant floating around.

N.B. constrbinder apply is like binder apply, except that it constructs a new term and returns it, rather than applying a lemma in-place to a hypothesis. It's primarily useful as plumbing for higher-level tactics.