Ltac: get type of hypothesis from name
I am looking for a way to get a hypothesis by name to fit it. Like this:
Ltac mytactic h_name :=
let h := hyp_from_name h_name in
match h with
| _ /\ _ => do_something
| _ => print_error_message
end
.
Which will be used like this:
H0 : A /\ B
==================
A
Coq < mytactic H0.
Thank.
+3
source to share
1 answer
I'm not sure I fully understand your question, but I will try. You can use the construct type of <term>
like this:
Ltac mytactic H :=
match type of H with
| _ /\ _ =>
let H1 := fresh in
let H2 := fresh in
destruct H as [H1 H2]; try (inversion H1; inversion H2; subst)
| _ => fail "Algo salió mal, mi amigo"
end.
Example por_ejemplo x : x >= 0 /\ x <= 0 -> x = 0.
Proof.
intros H.
now mytactic H.
Qed.
+3
source to share