I've been working on a formalization for a process calculus in Coq (repository here), and constantly find myself trying to apply a function which fails because of equivalent, but syntactically different, subterms. This often happens because of manipulation of de Bruijn variables. As unification fails, I'll usually just replace misbehaving subterms explictly beforehand and then apply the function I need. A simple code as an example of what I mean:
Require Import Lia.
Goal
forall P: nat -> Prop,
(forall a b c, P (a + (b + c))) ->
forall a b c, P (b + c + a).
Proof.
intros.
(* Unification fails here. *)
Fail apply H.
(* Replace misbehaving subterms explictly. *)
replace (b + c + a) with (a + (b + c)).
- (* Now application succeeds. *)
apply H.
- (* Show now they were the same thing. *)
lia.
Qed.
So, my question is: is there a tactic, or is it possible to write one with ltac, which is similar to apply, but turning unification errors into additional equality goals instead of failing?
applys_eq
from Programming Language Foundations' LibTactics will accomplish that. From the documentation (as of Version 6.1 of the book):
applys_eq H
helps proving a goal of the formP x1 .. xN
from an [sic] hypothesisH
that concludesP y1 .. yN
, where the argumentsxi
andyi
may or may not be convertible. Equalities are produced for all arguments that don't unify.The tactic invokes
equates
on all arguments, then callsapplys K
, and attempts reflexivity on the side equalities.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With