Define a 'head' for coinductive type stream in Coq(without pattern matching)

1) I believe that it is possible to use inductive types without pattern matching. (using _rec,_rect,_ind only). It is opaque, complicated, but possible. 2) Is it possible to use coinductive types withous pattern matching?

There exist a function from coinductive type to union of constructors' domains of coinductive type. Does Coq generate it explicitly? If yes, how to rewrite 'hd' ?

Section stream.
  Variable A : Type.

  CoInductive stream : Type :=
  | Cons : A -> stream -> stream.
End stream.

Definition hd A (s : stream A) : A :=
  match s with
    | Cons x _ => x
  end.

Although it is possible to use inductive types without directly resorting to pattern matching, this is only superficially true: the _rec, _rect and _ind combinators generated by Coq are all defined in terms of match. For instance:

Print nat_rect.

nat_rect = 
fun (P : nat -> Type) (f : P 0) (f0 : forall n : nat, P n -> P (S n)) =>
fix F (n : nat) : P n :=
  match n as n0 return (P n0) with
  | 0 => f
  | S n0 => f0 n0 (F n0)
  end
     : forall P : nat -> Type,
       P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

Furthermore, there are many cases where replacing pattern matching by an eliminator would result in a term with different computational behavior. Consider the following function, which divides a nat by two:

Fixpoint div2 (n : nat) :=
  match n with
  | 0 | 1 => 0
  | S (S n') => S (div2 n')
  end.

It is possible to rewrite this function using nat_rec, but the recursive call on n - 2 makes it a bit complicated (try it!).

Now, back to your main question, Coq does not automatically generate similar elimination principles for coinductive types. The Paco library helps deriving more useful principles for reasoning about coinductive data. But as far as I am aware, there is nothing similar for writing plain functions.

It is worth pointing out that your proposed approach is different from what Coq does for inductive data types, in that nat_rect and friends allow writing recursive functions and proofs by induction. One of the reasons providing these combinators is that they are used by the induction tactic. Something of type nat -> unit + nat, which more or less corresponds to what you proposed, wouldn't suffice.