Ltac：从名称中获取hypotesis的类型

Question

我正在寻找一种通过名称获得假设以匹配它的方法。像这样：

Ltac mytactic h_name :=
let h := hyp_from_name h_name in
    match h with
    | _ /\ _ => do_something
    | _ => print_error_message
    end
.

可以这样使用：

H0 : A /\ B
==================
A

Coq < mytactic H0.

谢谢。

Answer 1

我不确定我是否完全理解你的问题，但我会尝试。您可以像这样使用 type of <term> 结构：

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.

Ltac：从名称中获取hypotesis的类型

Ltac: get hypotesis' type from name

pattern-matching

coq

ltac