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.