如何定義精益中的互感命題？

我嘗試使用感應數據類型的語法，但它得到一條錯誤消息「互感類型必須編譯爲具有相關消除的基本歸納類型」。如何定義精益中的互感命題？

下面是我嘗試的例子對自然數

mutual inductive even, odd 
with even: ℕ → Prop 
| z: even 0 
| n: ∀ n, odd n → even (n + 1) 
with odd: ℕ → Prop 
| z: odd 1 
| n: ∀ n, even n → odd (n + 1)

另外一個相關的問題定義命題even和odd：什麼是定義相互遞歸函數的語法？我似乎無法在任何地方找到它。

來源

2017-01-21 Phil

我認爲精益自動嘗試創建recursors even.rec和odd.rec與Type，不Prop工作。但是這不起作用，因爲精益將邏輯世界（Prop）和計算世界（Type）分開。換句話說，我們可以摧毀一個邏輯術語（證明）只是爲了產生一個邏輯術語。請注意，如果您製作ℕ → Type類型的even和odd，則您的示例可以正常工作。

的Coq的證明助手，這是一個相關的系統，處理這種情況通過創建兩個（相當弱的和不切實際）感應原理自動，但它不會產生過程的一般recursors。

有一種替代方法，在此Lean wiki article說明。它涉及寫很多樣板。讓我舉一個例子，說明如何爲這種情況做好準備。

首先，我們編譯了互感類型在感應家庭。我們添加一個布爾指數較均勻度：

inductive even_odd: bool → ℕ → Prop 
| ze: even_odd tt 0 
| ne: ∀ n, even_odd ff n → even_odd tt (n + 1) 
| zo: even_odd ff 1 
| no: ∀ n, even_odd tt n → even_odd ff (n + 1)

接下來，我們定義一些縮寫來模擬互感類型：

-- types 
def even := even_odd tt 
def odd := even_odd ff 

-- constructors 
def even.z : even 0 := even_odd.ze 
def even.n (n : ℕ) (o : odd n): even (n + 1) := even_odd.ne n o 
def odd.z : odd 1 := even_odd.zo 
def odd.n (n : ℕ) (e : even n): odd (n + 1) := even_odd.no n e

現在，我們推出我們自己的感應原理：

-- induction principles 
def even.induction_on {n : ℕ} (ev : even n) (Ce : ℕ → Prop) (Co : ℕ → Prop) 
         (ce0 : Ce 0) (stepe : ∀ n : ℕ, Co n → Ce (n + 1)) 
         (co1 : Co 1) (stepo : ∀ n : ℕ, Ce n → Co (n + 1)) : Ce n := 
    @even_odd.rec (λ (switch : bool), bool.rec_on switch Co Ce) 
       ce0 (λ n _ co, stepe n co) 
       co1 (λ n _ ce, stepo n ce) 
       tt n ev 

def odd.induction_on {n : ℕ} (od : odd n) (Co : ℕ → Prop) (Ce : ℕ → Prop) 
        (ce0 : Ce 0) (stepe : ∀ n : ℕ, Co n → Ce (n + 1)) 
        (co1 : Co 1) (stepo : ∀ n : ℕ, Ce n → Co (n + 1)) := 
    @even_odd.rec (λ (switch : bool), bool.rec_on switch Co Ce) 
       ce0 (λ n _ co, stepe n co) 
       co1 (λ n _ ce, stepo n ce) 
       ff n od

暗示Ce : ℕ → Prop參數even.induction_on會更好，但由於某些原因，精益無法推斷它（參見最後的引理， e我們必須明確地通過Ce，否則精益推斷Ce與我們的目標無關）。情況與odd.induction_on對稱。

什麼是定義相互遞歸函數的語法？

如本lean-user thread解釋的，對於相互遞歸函數的支持受到很大限制：

存在用於任意相互遞歸功能的支持，但對於一個非常簡單的情況下支持。在我們定義了一個相互遞歸的類型之後，我們可以定義相互遞歸的函數來「鏡像」這些類型的結構。

您可以在該線程的例子。但是，我們可以再次使用相同的add-a-switching-parameter方法來模擬相互遞歸函數。讓我們來模擬相互遞歸布爾謂詞evenb和oddb：

def even_oddb : bool → ℕ → bool 
| tt 0  := tt 
| tt (n + 1) := even_oddb ff n 
| ff 0  := ff 
| ff (n + 1) := even_oddb tt n 

def evenb := even_oddb tt 
def oddb := even_oddb ff

下面是如何上述所有可以使用的例子。讓我們證明一個簡單的引理：

lemma even_implies_evenb (n : ℕ) : even n -> evenb n = tt := 
    assume ev : even n, 
    even.induction_on ev (λ n, evenb n = tt) (λ n, oddb n = tt) 
    rfl 
    (λ (n : ℕ) (IH : oddb n = tt), IH) 
    rfl 
    (λ (n : ℕ) (IH : evenb n = tt), IH)

來源

2017-01-22 12:36:52

如何定義精益中的互感命題？

回答

相關問題