在勒柯克（安全第n個功能）使用相關類型

Question

我努力學習勒柯克，但我發現很難讓從我在軟件基金會和與認證相關類型編程讀我自己的飛躍用例。

特別是，我想我會嘗試在列表上做一個驗證版本的nth函數。我設法寫：

Require Import Arith. 
Require Import List. 
Import ListNotations. 

Lemma zltz: 0 < 0 -> False. 
Proof. 
    intros. contradict H. apply Lt.lt_irrefl. 
Qed. 

Lemma nltz: forall n: nat, n < 0 -> False. 
Proof. 
    intros. contradict H. apply Lt.lt_n_0. 
Qed. 

Lemma predecessor_proof: forall {X: Type} (n: nat) (x: X) (xs: list X), 
    S n < length (x::xs) -> n < length xs. 
Proof. 
    intros. simpl in H. apply Lt.lt_S_n. assumption. 
Qed. 

Fixpoint safe_nth {X: Type} (n: nat) (xs: list X): n < length xs -> X := 
    match n, xs with 
    | 0, [] => fun pf: 0 < length [] => match zltz pf with end 
    | S n', [] => fun pf: S n' < length [] => match nltz (S n') pf with end 
    | 0, x::_ => fun _ => x 
    | S n', x::xs' => fun pf: S n' < length (x::xs') => safe_nth n' xs' (predecessor_proof n' x xs' pf) 
    end. 

這工作，但提出了兩個問題：

1. 將如何經歷勒柯克用戶寫的嗎？這三個引理是否真的有必要？這是{ | }類型的用例嗎？
2. 如何從其他代碼調用此函數，即如何提供所需的證明？

我嘗試這樣做：

Require Import NPeano. 
Eval compute in if ltb 2 (length [1; 2; 3]) then safe_nth 2 [1; 2; 3] ??? else 0. 

但是，當然，這是不行的，直到我弄清楚如何爲???部分寫。我試着把(2 < length [1; 2; 3])放在那裏，但是它的類型是Prop而不是2 < length [1; 2; 3]。我可以寫出並證明這個特定類型的引理，並且這是有效的。但是，通用解決方案是什麼？

Answer 1

zltz與nltz 0具有相同的類型。

Check zltz. 
Check nltz 0. 

使用帶有2和[1; 2; 3]你的函數從另一個函數中，你可以使用lt_dec。

Eval compute in match lt_dec 2 (length [1; 2; 3]) with 
    | left pf => safe_nth 2 [1; 2; 3] pf 
    | right _ => 0 
    end. 

如果提取lt_dec，你會發現它非常類似於ltb樣張被刪除後。如果您可以在調用safe_nth的函數中構建證明，則不需要使用lt_dec。

你可以縮短你的功能有點像這樣。

Fixpoint safe_nth' {X: Type} (xs: list X) (n: nat): n < length xs -> X := 
    match xs, n with 
    | [], _ => fun pf => match nltz n pf with end 
    | x::_, 0 => fun _ => x 
    | x::xs', S n' => fun pf => safe_nth' xs' n' (predecessor_proof n' x xs' pf) 
    end. 

我不知道什麼最好的做法，但如果你使用sig你整潔抽出代碼。

Answer 2

我不認爲對於做這種事情的最佳方式是一致的。

我相信通常Coq的發展傾向於贊成索引歸納類型來編寫這樣的代碼。這是Coq分配中的vector library之後的解決方案。在那裏，你可以爲矢量定義一個索引歸納類型，爲有界整數定義另一個（分別稱爲標準庫中的Vector.t和Fin.t）。例如nth等一些函數用這種風格寫起來要簡單得多，因爲例如，在去除矛盾的情況和執行遞歸調用時，向量和索引上的模式匹配最終爲您做了一點推理。缺點是Coq中的依賴模式匹配不是很直觀，有時你必須以奇怪的方式編寫你的函數才能使它們工作。這種方法的另一個問題是需要重新定義在列表上工作的許多函數來處理向量。

另一種解決方法是將有界整數定義爲nat的從屬對，並證明該索引是有界的，這實質上就是您在提到{ | }類型時所要做的。例如，這是ssreflect庫所遵循的方法（請參見ordinal類型）。要定義一個安全的函數nth，他們所做的是定義一個簡單的版本，當索引超出範圍時採用缺省元素返回，並使用n < length l提供該默認元素的證明（例如在tuple ssreflect庫，他們在那裏定義長度索引列表，並看他們如何定義tnth）。優點是將更多的信息類型和功能與更簡單的變體聯繫起來更容易。缺點是有些東西很難直接表達：例如，你不能直接在ssreflect元組上進行模式匹配。

另一點值得注意的是，通常使用布爾屬性而不是歸納定義的方法更容易，因爲計算和簡化避免了對某些引理的需要。因此，當使用布爾版本<時，Coq不會在0 < 0 = true和false = true的證明之間或S n < length (x :: l) = true的證明和n < length l = true的證明之間產生差異，這意味着您可以直接在這些證明中使用這些證明您的nth的定義，而不必用輔助引理進行按摩。不幸的是，Coq標準庫傾向於在布爾計算中使用歸納定義類型，而在很多情況下它們並不有用，比如定義<。另一方面，ssreflect庫更多地使用布爾計算來定義屬性，使其更適合於這種編程風格。