Suppose I have an inductive type
Inductive T : nat -> nat -> Type := | T1 : T 0 1 .
Now I have a value
t : T x y. I'd like to have a tactic
tac T1, which like
apply tries to apply
T1, and leaves the goals
x = 0 and
y = 1. Does this exist?
That is plain
inversion, isn't it?
Ah no, sorry, misread the ordering.
I think the
apply tactic from CFML does that.
Otherwise you can write something by hand that can do the job in at least a few cases.
From Coq Require Import Utf8. Inductive T : nat → nat → Type := | T1 : T 0 1 . Inductive bar : nat → nat → Type := | C : bar 2 2 | D : ∀ x, bar x x . Ltac replace_args g := lazymatch g with | ?f ?x => let x' := fresh x in let t := type of x in evar (x' : t) ; replace x with x' ; [ replace_args f ; subst x' | subst x' ] | _ => idtac end. Ltac eqapply ff := lazymatch goal with | |- ?g => replace_args g ; [ eapply ff | try reflexivity .. ] end. Lemma foo : ∀ x y, T x y. Proof. intros x y. eqapply T1. Abort. Lemma foo : ∀ x y, bar x y. Proof. intros x y. Fail Fail eqapply D. (* Asks for x = y *) eqapply C. (* Asks for 2 = x and 2 = y *) Abort.
evar (x' : t) ; replace x with x' ; [ replace_args f ; subst x' | subst x' ]
I would do
let x' := open_constr:(_ : t) in replace x with x' ; [replace_args f |]
We used this as an example how to implement tactics using MetaCoq for last year's Coq WS: https://arxiv.org/abs/2006.15135 Usage example: https://github.com/uds-psl/metacoq-examples-coqws/blob/master/test.v
But for your use case, using MetaCoq for this might be overkill and Théo's solution is easier
Thanks for the responses, I don't completely understand how the ltac approach works yet (what actually introduces the equality types here?). The MetaCoq approach looks good, that's exactly what I've been doing by hand for now.
@spaceloop the equalities come from
Last updated: Oct 01 2023 at 18:01 UTC