Coq：`Function ... with` syntax

Question

看來，由於w/Inductive和Fixpoint，您可以相互定義Function的w/with。你能給出這個的語法和/或例子嗎？我什麼都找不到。我想這跟Fixpoint 一樣（也沒有發現這個）。非工作（但半編譯 - 2分最後幾行以紅色突出顯示），例如：

Variable ARG:Type. 
Variable phy inf phyinf: ARG. 
Function Phy (x:ARG): ARG := match x with Inf x => phyinf | _ => phy end 
with Inf (x:ARG): ARG := match x with Phy x => phyinf | _ => inf end. (*Error: Unknown constructor: Inf.*) 

Answer 1

好吧，我想我終於明白你的問題。

確實有一種方法可以相互定義幾個Fixpoint。它（略）記錄在變體部分here中。

同樣，有一種方法可以相互定義幾個Inductive類型（記錄的here）。

還有一種方法可以相互定義幾個Function。但請注意，手動使有關此功能句話：

的Function建設也享有with擴展定義相互遞歸定義。但是，此功能對非結構遞歸函數不起作用。

您在半工作示例中遇到的錯誤與語法無關，但與Function ... with功能也沒有關係。錯誤是你只能在歸納類型上使用模式匹配，並且分支必須以構造函數開始。在你的例子中，ARG不是一個歸納類型，並且Inf不是一個構造函數。我不能真正「改正」你的榜樣，因爲我沒有看到你想表達的內容。這個例子僅僅是爲了這個問題嗎？在這種情況下，你將其剝離得太少。 PS：我不知道你是否試圖做induction-recursion（定義一個遞歸函數和一個歸納類型）。如果是這種情況，那就不要運氣了：Coq還沒有這個功能。