通过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不会推断太多，所以你必须通过手动提供相等的方式来帮助它。