Ltac: obtenir le type de l'hypotesis du nom

Question

Je cherche un moyen d'obtenir une hypotèse par son nom afin de le faire correspondre. Comme ceci:

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

qui serait utilisé comme ceci:

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

Coq < mytactic H0. 

Merci.

Answer 1

Je ne suis pas sûr de comprendre complètement votre question, mais je vais essayer. Vous pouvez utiliser la construction type of <term> comme suit:

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.