从Coq中流中提取有限的证据

Question

我正在努力实现Some Domain Theory and Denotational Semantics in Coq，但是遇到了一些技术问题。

首先，我定义了stream，定义为

CoInductive Stream (D : Type) := 
  Eps : Stream D -> Stream D |
  Val : D -> Stream D.

使用有限命题

Inductive Finite (D : Type) : Stream D -> Prop :=
  | Finite_Val : forall d, Finite D (Val D d)
  | Finite_Eps : forall d, Finite D (d) -> Finite D (Eps D d).

我的目标是找到一些有限流实际上是有限的证据，这是在下面的引理中构造返回n和d‘的函数。

Lemma finite_pred_nth (D : Type) :
  forall d, Finite D d -> exists n d', pred_nth d n = Val D d'.
Proof.
  intros. induction H.
  - exists 0. exists d. reflexivity.
  - destruct IHFinite as [n [d' IHF]].
    exists (S n). exists d'. simpl. apply IHF.
  Qed.

并且pred_nth被定义为

Fixpoint pred_nth {D : Type} (x : Stream D) (n : nat) : Stream D :=
  match x, n with
  | Eps _ x', S n' => pred_nth x' n'
  | Val _ d, _ => x
  | Eps _ x', 0 => x
  end.

这些是我的一些方法。

使用记录作为返回类型

Record fin_evid := mk_fin_evid 
  { 
    T :> Type;
    d : Stream T;
    n : nat;
    v : T;
    H : pred_nth d n = Val T d' }.

在这种情况下，我无法构造函数。

使用类型类作为返回类型

Class finite_evidence (D : cpo) (d : Stream D) := {pred_n : nat; pred_d' : D; pred : pred_nth d pred_n = Val D pred_d'}.

Fixpoint extract_evidence (D : cpo) (d : Stream D) (H : Finite D d) : finite_evidence D d.
Proof.
  destruct d.
- apply eps_finite_finite in H. apply extract_evidence in H.
  destruct H.
  exists (S pred_n0) (pred_d'0). simpl. apply pred0.
- exists 0 t. reflexivity.
Defined.

这个函数创建得很好，但是我找不到如何匹配类型类的方法，所以我可以在定义其他函数时提取pred_n，pred_d‘。

这些是最小的例子，完整的代码可以在here中查看，在598行(流的定义)和817行(使用类型类)附近。使用此技术可以创建最小上限(716行)，而不会破坏coq对停止的保证。更具体地说，给定流的单调递增序列并证明第一个元素是有限的(大于有限流的流也是有限的)，为每个元素提取封装元素，然后返回提取的封装元素的lub。

Answer 1

你的extract_evidence函数在我看来没问题。您可以直接使用类方法pred_n和pred_d'来提取这些见证者。例如：

Definition get_evidence (D : cpo) (d : Stream D) (H : Finite D d) :=
  @pred_n _ _ (extract_evidence D d H).

请注意@，它允许您指定您正在讨论的类实例。在这里，您可能不需要类型类解析机制，因此将finite_evidence声明为Record而不是Class是安全的。