bug.v

From iris.algebra Require Export ofe stepindex_finite.

CoInductive stream := SCons {
  head : nat;
  tail : stream;
}.
Add Printing Constructor stream.

Fixpoint nth (s : stream) (n : nat) : nat :=
  match n with
  | 0 => head s
  | S n => nth (tail s) n
  end.

CoFixpoint fun2stream (f : nat → nat) : stream :=
  SCons (f 0) (fun2stream (f ∘ S)).

Section ofe.

Local Instance stream_equiv_instance : Equiv stream := λ s1 s2,
  ∀ n, nth s1 n = nth s2 n.

Local Instance stream_dist_instance : Dist stream := λ n s1 s2,
  ∀ i, i ≤ n → nth s1 i = nth s2 i.

Lemma stream_ofe_mixin : OfeMixin stream.
Proof.
  split.
  (* exercise *)
  - intros x y.
    split.
    + intros Hxy n i Hin.
      trivial.
    + intros Hdist m.
      apply (Hdist m).
      trivial.
  - intro n.
    split.
    + intros x i Hin.
      trivial.
    + intros x y Hxy i Hin.
      symmetry.
      apply (Hxy i Hin).
    + intros x y z Hxy Hyz i Hin.
      rewrite (Hxy i Hin).
      rewrite (Hyz i Hin).
      reflexivity.
  - intros n m x y Hxy Hmn i Him.
    simpl in Hmn.
    apply (Hxy i).
    exact (transitivity Him Hmn).
Qed.

Canonical Structure streamO := Ofe stream stream_ofe_mixin.

End ofe.

From Stdlib Require Export Classes.DecidableClass.
From Coq Require Export Init.Datatypes.


(******************************************************************************)
(* non-working examples *******************************************************)
(******************************************************************************)

Global Program Instance stream_cofe_3 : Cofe streamO
  := {| compl := λ c : chain streamO, fun2stream (λ i : nat, nth (c i) i)
      ; lbcompl
          := λ (n : natSI) (_ : SIdx.limit n) (c : bchain streamO n)
             , (λ (n : natSI) (c : bchain streamO n)
                , fun2stream (λ i : nat, let r := Nat.ltb_spec0 i n in
                                         let b := i <? n in
                                         match r with
                                         | ReflectT _ l => nth (c i l) i
                                         | ReflectF _ _ => 0
                                         end)
               ) n c;
     |}.

Global Program Instance stream_cofe_4 : Cofe streamO
 := {| lbcompl n _ c
         := fun2stream (λ i : nat, match Nat.ltb_spec0 i n with
                                   | ReflectT _ Hi => nth (c i Hi) i
                                   | ReflectF _ _ => 0
                                   end)
    |}.