通過Coq列表中的索引執行安全元素檢索

Question

我試圖證明Coq提取機制和Aglon中的MAlonzo編譯器之間代碼生成的區別。我想出了在阿格達這個簡單的例子：

data Nat : Set where 
    zero : Nat 
    succ : Nat → Nat 

data List (A : Set) : Set where 
    nil : List A 
    cons : A → List A → List A 

length : ∀ {A} → List A → Nat 
length nil = zero 
length (cons _ xs) = succ (length xs) 

data Fin : Nat → Set where 
    finzero : ∀ {n} → Fin (succ n) 
    finsucc : ∀ {n} → Fin n → Fin (succ n) 

elemAt : ∀ {A} (xs : List A) → Fin (length xs) → A 
elemAt nil() 
elemAt (cons x _) finzero = x 
elemAt (cons _ xs) (finsucc n) = elemAt xs n 

直接翻譯勒柯克（與absurd pattern emulation）產量：

Inductive Nat : Set := 
| zero : Nat 
| succ : Nat -> Nat. 

Inductive List (A : Type) : Type := 
| nil : List A 
| cons : A -> List A -> List A. 

Fixpoint length (A : Type) (xs : List A) {struct xs} : Nat := 
    match xs with 
    | nil => zero 
    | cons _ xs' => succ (length _ xs') 
    end. 

Inductive Fin : Nat -> Set := 
| finzero : forall n : Nat, Fin (succ n) 
| finsucc : forall n : Nat, Fin n -> Fin (succ n). 

Lemma finofzero : forall f : Fin zero, False. 
Proof. intros a; inversion a. Qed. 

Fixpoint elemAt (A : Type) (xs : List A) (n : Fin (length _ xs)) : A := 
    match xs, n with 
    | nil, _ => match finofzero n with end 
    | cons x _, finzero _ => x 
    | cons _ xs', finsucc m n' => elemAt _ xs' n' (* fails *) 
    end. 

但elemAt最後一種情況下失敗：

File "./Main.v", line 26, characters 46-48: 
Error: 
In environment 
elemAt : forall (A : Type) (xs : List A), Fin (length A xs) -> A 
A : Type 
xs : List A 
n : Fin (length A xs) 
a : A 
xs' : List A 
n0 : Fin (length A (cons A a xs')) 
m : Nat 
n' : Fin m 
The term "n'" has type "Fin m" while it is expected to have type 
"Fin (length A xs')". 

看起來Coq並不推斷succ m = length A (cons A a xs')。我應該怎麼告訴Coq，因此它會使用這些信息？還是我在做一些完全沒有意義的事情？

Answer 1

做模式匹配相當於使用destruct策略。 您將無法直接使用destruct來證明finofzero。

inversion策略在執行destruct之前會自動生成一些等式。 然後它試圖做什麼discriminate。結果非常混亂。

Print finofzero. 

• 爲了證明像fin zero -> P您應將其更改爲fin n -> n = zero -> P第一。
• 爲了證明類似list nat -> P（更常見的是forall l : list nat, P l），您不需要將其更改爲list A -> A = nat -> P，因爲list的唯一參數是其定義中的參數。
• 要證明與S n <= 0 -> False類似的內容，首先應將其更改爲S n1 <= n2 -> n2 = 0 -> False，因爲<=的第一個參數是參數，而第二個參數不是。
• 在目標f x = f y -> P (f y)，你首先需要將目標更改爲f x = z -> f y = z -> P z，只有這樣，你可以使用感應假說改寫假設改寫，因爲=第一個參數（實際上是第二個）是一個參數定義爲=。

嘗試定義不帶參數的<=以查看歸納原理是如何變化的。 一般來說，在謂詞上使用歸納之前，應確保它的參數是變量。否則信息可能會丟失。

Conjecture zero_succ : forall n1, zero = succ n1 -> False. 
Conjecture succ_succ : forall n1 n2, succ n1 = succ n2 -> n1 = n2. 

Lemma finofzero : forall n1, Fin n1 -> n1 = zero -> False. 
Proof. 
intros n1 f1. 
destruct f1. 
intros e1. 
eapply zero_succ. 
eapply eq_sym. 
eapply e1. 
admit. 
Qed. 

(* Use the Show Proof command to see how the tactics manipulate the proof term. *) 
Definition elemAt' : forall (A : Type) (xs : List A) (n : Nat), Fin n -> n = length A xs -> A. 
Proof. 
fix elemAt 2. 
intros A xs. 
destruct xs as [| x xs']. 
intros n f e. 
destruct (finofzero f e). 
destruct 1. 
intros e. 
eapply x. 
intros e. 
eapply elemAt. 
eapply H. 
eapply succ_succ. 
eapply e. 
Defined. 

Print elemAt'. 

Definition elemAt : forall (A : Type) (xs : List A), Fin (length A xs) -> A := 
    fun A xs f => elemAt' A xs (length A xs) f eq_refl. 

CPDT對此有更多瞭解。

如果在證明Coq執行eta縮減和beta/zeta縮減（無論哪個變量在範圍內最多隻出現一次），那麼可能事情會更清楚。

Answer 2

我認爲你的問題類似於Dependent pattern matching in coq。 Coq的match不會推斷太多，所以你必須通過手動提供相等的方式來幫助它。