Ltac：从名称

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.