如何命名記憶表達式時的假設？

Coq的文檔包含一般警告而不是依賴於內置命名機制，但選擇自己的名稱，以免命名機制中的更改渲染過去的證明無效。如何命名記憶表達式時的假設？

當考慮表達式remember Expr as v時，我們將變量v設置爲表達式Expr。但是，假設的名字被自動選擇，並且是一樣的東西Heqv，所以我們有：

Heqv: v = Expr

如何選擇自己的名字，而不是Heqv？我總是可以使用rename命令將其重命名爲任何我喜歡的內容，但這並不能保證我的證明獨立於Coq中內置命名機制的假設性未來更改。

2012-07-16 Mayer Goldberg

如果您可能擺脫單獨的平等，請嘗試set (name := val)。使用unfold而不是rewrite將值返回原位。

如果你需要的平等超過rewrite <-，我知道沒有內置的戰術，這樣做。儘管如此，你可以手動完成，或者建立一個戰術/符號。我只是把它扔在一起。（注：我不是專家，這可能是更容易做到。）

Tactic Notation "remember_as_eq" constr(expr) ident(vname) ident(eqname) := 
    let v  := fresh in 
    let HHelp := fresh in 
    set (v := expr); 
    (assert (HHelp : sigT (fun x => x = v)) by (apply (existT _ v); reflexivity)); 
    inversion HHelp as [vname eqname]; 
    unfold v in *; clear v HHelp; 
    rewrite <- eqname in *.

用作remember_as_eq (2+2) four Heqfour得到相同的結果與remember (2+2) as four。

注意：已更新以處理更多情況，舊版本在值和目標類型的某些組合上失敗。如果您發現另一個可與rewrite一起使用的案例，請留下評論，但不要使用此案例。

來源

2012-07-17 01:09:28 nobody

請注意，如果您更喜歡使用它作爲記憶（2 + 2），您也可以將它定義爲'Tactic Notation「記住」constr（expr）「爲」ident（vname）「四個與Eq Heqfour'，但是這將會解析器並且影響內建的'remember _ as _.'。如果你使用'Tactic Notation'記住「ident（eqname）」的「constr（expr）」爲「ident（vname）'（或'withEq'而不是'with'或...），那麼排序很奇怪，但是老'記'仍然可以訪問。 – nobody 2012-07-22 17:16:22

如何命名記憶表達式時的假設？

回答

相關問題