Ltac: bekommen Hypotesis Typ von Name

Question

Ich bin auf der Suche nach einer Möglichkeit, eine Hypotesis durch seinen Namen zu bekommen, um es zu entsprechen. Wie folgt aus:

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

, die wie folgt verwendet werden würde:

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

Coq < mytactic H0. 

Dank.

Answer 1

Ich bin mir nicht sicher, ob ich Ihre Frage vollständig verstehe, aber ich werde es versuchen. Sie können die type of <term> Konstruktion wie folgt verwenden:

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.