模式匹配沒有專門的類型

我在Coq玩耍，試圖創建一個排序列表。我只是想要一個函數，它需要一個列表[1,2,3,2,4]並返回類似Sorted [1,2,3,4]的東西 - 即取出壞部分，但不是實際排序整個列表。模式匹配沒有專門的類型

我想我會先定義一個函數lesseq的類型(m n : nat) -> option (m <= n)，然後我可以很容易地模式匹配。也許這是一個壞主意。

我在現在這個問題的關鍵是，（片段，在底部全功能）

Fixpoint lesseq (m n : nat) : option (m <= n) := 
    match m with 
     | 0 => match n with 
      | 0 => Some (le_n 0) 
      ...

沒有類型檢查;它表示它期望option (m <= n)，但Some (le_n 0)的類型爲option (0 <= 0)。我不明白，因爲顯然m和n在這種情況下是零，但我不知道如何告訴科克。

整個功能是：

Fixpoint lesseq (m n : nat) : option (m <= n) := 
    match m with 
    | 0 => match n with 
     | 0 => Some (le_n 0) 
     | S n_ => None 
     end 
    | S m_ => match n with 
     | 0 => None 
     | S _ => match lesseq m_ n with 
       | Some x=> le_S m n x 
       | None => None 
       end 
      end 
    end.

也許我自己走在前面的，只是需要繼續讀我解決這個之前。

來源

2011-05-23 Amos Robinson

你可能想定義以下功能（即使你將其標註爲正常，你[le_S MNX]沒有你想要的類型）：

 Fixpoint lesseq (m n : nat) : option (m <= n) := 
    match n with 
    | 0 => 
     match m with 
     | 0 => Some (le_n 0) 
     | S m0 => None 
     end 
    | S p => 
     match lesseq m p with 
     | Some l => Some (le_S m p l) 
     | None => None 
     end 
    end.

但正如你已經注意到，在typechecker是當你摧毀出現在結果類型中的變量時，不足以猜測新上下文。你必須標註下列方式匹配：

 Fixpoint lesseq (m n : nat) : option (m <= n) := 
    match n return (option (m <= n)) with 
    | 0 => 
     match m return (option (m <= 0)) with 
     | 0 => Some (le_n 0) 
     | S m0 => None 
     end 
    | S p => 
     match lesseq m p with 
     | Some l => Some (le_S m p l) 
     | None => None 
     end 
    end.

請參見參考手冊，如果你真的想了解模式匹配如何與相關類型的作品。如果你覺得沒有足夠的勇氣，你寧願使用戰術機制來建立你的證明（「精煉」戰術是一個偉大的工具）。

 Definition lesseq m n : option (m <= n). 
    refine (fix lesseq (m : nat) (n : nat) {struct n} := _). 

    destruct n. 
    destruct m. 
    apply Some; apply le_n. 
    apply None. 

    destruct (lesseq m n). 
    apply Some. 
    apply le_S. 
    assumption. 
    apply None. 
    Defined.

順便說一句，我不認爲你的功能將是真正的幫助（即使它是一個好主意），因爲你需要證明以下引理：引理 lesseq_complete： FORALL mn，lesseq mn <>無 - > m> n。

這就是爲什麼人們使用Coq.Arith.Compare_dec。玩得開心。

來源

2011-05-23 14:29:23 Marc

順便說一句，如果你遵循這種方法，我非常建議使用程序功能。它允許你按照第一列表的樣式編寫你的程序，但留下任何數量的「漏洞」（_），然後你可以使用戰術（第二列表的樣式）「填充」。因此，它可以讓你很好地分離編程和驗證。 – akoprowski 2011-05-23 16:42:23

謝謝你們的幫助。我有很多東西需要學習，沒有意識到你可以使用戰術來定義函數（儘管它很有意義）。我現在同意一個總和類型（一個<= b \/ a > b）會很好，因爲我設法通過返回None來實現錯誤的lesseq，當我想要一些;這對於更具體的類型是不可能的。我一定會再看看標準庫。 – 2011-05-24 08:56:36

你想寫這個函數作爲練習還是僅僅爲了實現更大的目標？在後一種情況下，您應該看看標準庫，該庫充滿決策功能，可以完成這裏的工作，Coq.Arith.Compare_dec;例如參見le_gt_dec。

另請注意，您建議的功能只會爲您提供信息是否。對於模式匹配，總和類型{ ... } + { ... }更有用，給你兩個可能的情況下處理。

來源

2011-05-23 14:09:31 akoprowski

模式匹配沒有專門的類型

回答

相關問題