gistfile1.v

Set Implicit Arguments.

CoInductive stream (A : Type) :=
| Cons : A -> stream A -> stream A
.

CoFixpoint nth_power_stream_aux
 : nat -> nat -> stream nat
 := fun n cur => Cons cur
      (nth_power_stream_aux n (cur * n))
.

Definition nth_power_stream
 : nat -> stream nat
 := fun n => nth_power_stream_aux n 1
.

CoFixpoint factorials_aux
 : nat -> nat -> stream nat
 := fun n cur => Cons cur
      (factorials_aux (n + 1) (cur * n))
.

Definition factorials
 : stream nat
 := factorials_aux 2 1
.

Inductive ord : Set :=
  | LT
  | EQ
  | GT
.

Fixpoint nat_cmp a b : ord
 :=
   match (a, b) with
   | (O, O) => EQ
   | (S _, O) => GT
   | (O, S_ ) => LT
   | (S a', S b') => nat_cmp a' b'
   end
.


CoFixpoint merge_uniq
 : forall {A : Type},
   (A -> A -> ord) ->
   stream A -> stream A -> stream A
 := fun _ cmp a b =>
      match (a, b) with
      | (Cons ha ta, Cons hb tb) =>
          match cmp ha hb with
          | EQ => Cons ha (merge_uniq cmp ta tb)
          | LT => Cons ha (merge_uniq cmp ta b)
          | GT => Cons hb (merge_uniq cmp a tb)
          end
      end
.


Require Import List.

Fixpoint take (A : Type) (left : nat) (s : stream A)
 : list A
 :=
   match left with
   | O => nil
   | S left' =>
       match s with
       | Cons h t => h :: take left' t
       end
   end
.

Notation "a ++ b" := (merge_uniq nat_cmp a b).


Definition res : stream nat
 :=
   factorials
   ++ nth_power_stream 2
   ++ nth_power_stream 3
.


Fixpoint nth {A : Type} (n : nat) (s : stream A) : A
 :=
   match (n, s) with
   | (O, Cons h _) => h
   | (S n', Cons _ t) => nth n' t
   end
.

Definition nth_res n := nth n res.

Extraction "/tmp/w.ml" nth_res.