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.
```

instead of

```
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 `replace`

, no?

Last updated: Jun 15 2024 at 05:01 UTC