I am trying to implement an ltac passing as argument the label of a hypothesis as the following:

```
Ltac test label P :=
lazymatch goal with
| label : ?H |- ?G =>
let H0 := fresh "H0" in
assert (H0 : H \/ P);
[ left; auto | ]
end.
```

But it doesn't work as I wish. For example, when execute this:

```
Theorem test : forall (A B C D : Prop), A -> B.
Proof.
intros A B C D.
intro label.
test label C.
test label D.
```

The hypotheses are

```
A B C D : Prop
label : A
H0 : A ∨ C
H1 : (A ∨ C) ∨ D
```

Though, I wish it was

```
A B C D : Prop
label : A
H0 : A ∨ C
H1 : A ∨ D
```

```
lazymatch goal with
| label : ?H |- ?G =>
```

this binds`label`

to some hypothesi, shadowing the binding from applying `test`

I don't think there's a way to use match goal with an hypothesis of specific name

you can do `let H := type of label in ...`

to get the type of the hypothesis instead

Last updated: Jun 23 2024 at 03:02 UTC