Stream: Coq users

Topic: Ltac hypothesis label as argument

João Mendes (Jun 26 2023 at 20:02):

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

Gaëtan Gilbert (Jun 26 2023 at 20:11):

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

this bindslabel 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: Oct 13 2024 at 01:02 UTC