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

Question

我正在努力实现 Coq中的一些领域理论和DenotationalSemantics。但卡了一些技术问题。

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

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' }.

在这种情况下，我未能构造函数。

使用typeeclass作为返回类型

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.

这个函数的创建工作很好，但是我找不到如何匹配typeclass，所以我可以在定义其他函数时提取pred_n, pred_d'。

这些都是最小的例子，完整的代码可以在这里查看。此处在第598行(流的定义)和第817行(使用typeclass)附近，使用这种技术是为了在不破坏coq的保证的情况下创建最小上界(第716行)。更具体地说，给定单调递增的流序列，并证明第一个元素是有限的（大于有限流的流也是有限的），为每个元素提取胶囊元素，然后返回提取的胶囊元素的润滑。

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.