如何拉RHS出平等的COQ

Question

如果我有以下幾點：

H : some complicated expression = some other complicated expression 

，我想抓住

u := some other complicated expression 

沒有硬編碼到我的證明（即使用pose ）

有沒有一種乾淨的方式在LTac中做到這一點？

Answer 1

我確信還有其他的ltac方式來做到這一點，在我的情況下，我更喜歡使用SSReflect的上下文模式語言來做到這一點。 （你需要安裝插件或使用勒柯克> = 8.7，其中包括SSReflect）：

(* ce_i = complicated expression i *) 
Lemma example T (ce_1 ce_2 : T) (H : ce_1 = ce_2) : False. 
set u := (X in _ = X) in H. 

導致目標：

T : Type 
    ce_1, ce_2 : T 
    u := ce_2 : T 
    H : ce_1 = u 
    ============================ 
    False 

通常直到你得到一個你可以細化模式越來越多相當穩定的比賽。

請注意，這恰好是SSReflect手冊中第8.3節「上下文模式」的第一個示例。

Answer 2

這裏是另一個版本，其使用LTAC和它的能力模式匹配上類型的使用條款：

Tactic Notation "assign" "rhs" "of" ident(H) "to" ident(u) "in" ident(H') := 
    match type of H with _ = ?rhs => set (u := rhs) in H' end. 

Tactic Notation "assign" "rhs" "of" ident(H) "to" ident(u) "in" "*" := 
    match type of H with _ = ?rhs => set (u := rhs) in * end. 

我們可以創建上述的多種變體（參見例如here）。這裏是如何使用它：

Lemma example {T} (ce1 ce2 ce3 : T) (H1 : ce1 = ce2) (H2 : ce2 = ce3) : ce1 = ce3. 
Proof. 
    assign rhs of H1 to u in *. 

證明狀態：

u := ce2 : T 
    H1 : ce1 = u 
    H2 : u = ce3 
    ============================ 
    ce1 = ce3 

再來一次：

Undo. 
    assign rhs of H1 to u in H1. 

證明狀態：

u := ce2 : T 
    H1 : ce1 = u 
    H2 : ce2 = ce3 
    ============================ 
    ce1 = ce3