1

我在 ATP 的世界里还是个新手，但肯定很有动力。我开始处理依赖类型。我参与了一个项目，我在其中定义了（有限和无限）序列的类型。

Inductive sequence {X : Type} : Type :=
    | FinSeq (x : list X)
    | InfSeq (f : nat -> X).

现在我想定义一个非空序列的头部。

Lemma aux_hd : forall {A : Type} (l : list A),
    0 < Datatypes.length l  -> @hd_error A l = None -> False.
Proof. destruct l.
 + simpl. lia. 
 + simpl. intros S. discriminate.
Qed.

Definition Hd {A : Type} (l : list A) : 0 < Datatypes.length l -> A :=
    match (hd_error l) with
    | Some a => (fun _ => a)
    | None => fun pf => match (aux_hd l pf ??) with end
    end.
     
Definition Head {A : Type} (s :sequence) (H : 0 << length s),
     match s with 
     | FinSeq x => Hd x H 
     | InfSeq f => f 0 end.

我的问题在于 Hd 的定义：我不知道如何证明@hd_error A l = None，因为我们已经在这样的匹配分支中。我相信这应该很容易。

我在最后一个定义中有一个类似的问题，因为我不知道如何转换 H，对于第一个匹配分支的特殊情况，我知道这一点length s = Datatypes.length x，因此0 << length s -> 0 < Datatypes.length x.

最后，我省略了关于 << 和长度序列的细节，因为我认为它与问题无关，但基本上我已经用 Inf 提升了 nat 来表示无限序列的长度，而 << 是 nat 的 < 和编号。

我已经学习了软件基础课程，我目前正在学习更多使用“具有依赖类型的认证编程”，这也非常好。在此先感谢，米格尔

4

1 回答 1

2

当您match处理某事时，所有额外的证据都必须作为参数传递给匹配项（这是 CPDT 中描述的“护航模式”）。

在Hd你想记住这一点hd_error l = None时，将它作为参数传递。这有点棘手，因为您必须match使用return子句显式注释（在更简单的情况下为您推断）：

Definition Hd {A : Type} (l : list A) : 0 < Datatypes.length l -> A :=
    match (hd_error l) as X return hd_error l = X -> 0 < Datatypes.length l -> A with
    | Some a => (fun _ _ => a)
    | None => fun pf1 pf2 => match (aux_hd l pf2 pf1) with end
    end eq_refl.

类似地Head，在模式匹配之后s你想简化0 << length s；将其作为参数传递：

Definition Head {A : Type} (s :sequence) (H : 0 << length s) :=
     match s return (0 << length s) -> _ with 
     | FinSeq x => fun H => Hd x H 
     | InfSeq f => fun _ => f 0
     end H.
于 2020-11-19T15:55:47.607 回答