Extracting evidence of finiteness from stream in Coq

Question

I'm working on implementing Some Domain Theory and Denotational Semantics in Coq, however stucked with some technical issue.

First, I defined stream, defined as

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

with finite proposition

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).

My goal is to find evidence that some finite stream is actually finite, which is constructing function returning n and d' in following lemma.

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.

and pred_nth is defined as

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.

These are some of my approaches.

Using record as return type

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

In this case, I failed to construct function.

Using typeclass as return type

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.

This function creation worked well, however I couldn't find how to pattern match typeclass, so I can extract pred_n, pred_d' in defining other function.

These are minimal example, and the full code can be viewed in here, around line 598(Definition of stream) and line 817(using typeclass). Using this technique is to create least upper bound(line 716) without destructing coq's assurance for halting. More specifically, given monotonically increasing sequence of stream and proof that first element is finite(stream larger than finite stream is also finite), extracting capsuled element for each element, then returning lub of extracted capsuled elements.

user_1633770 · Answer

Your extract_evidence function looks fine to me. You can use the class methods pred_n and pred_d' directly to extract those witnesses. For example:

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

Note the @, which allows you to specify which class instance you are talking about. Here, you probably do not need the type class resolution mechanism, so it is safe to declare finite_evidence as a Record instead of a Class.

Extracting evidence of finiteness from stream in Coq

1 Answers