能否针对共归纳类型证明对应共归纳原理？以Stream类型为例

你给出的这个是Stream类型共归纳原理的余代数实例，本身是成立的，在Agda和Coq中都可以通过原生的共递归机制直接证明，不需要引入额外公理。
首先需要补充说明一个你写的伪代码里的小疏漏：你目前列的三个前提（性质P、destruct_head、destruct_tail）不足以推出结论Σ y : Stream A. P y——比如取P为常值False，两个前提都是空洞成立的，但结论显然不成立。你需要额外补充一个初始前提：存在至少一个项s : Stream A满足P s，或者你可以把原理调整为“状态机到Stream的共递归存在性”版本，不需要依赖已有的Stream实例，只要给出状态到head的映射和状态转移函数，就能构造对应Stream。
下面分别给你两种语言下的实现参考：

Agda 实现 #

Agda原生支持共归纳类型的copattern匹配，只要构造满足保护式条件，类型检查器会直接接受：

-- 标准Stream定义
record Stream (A : Set) : Set where
  coinductive
  field
    head : A
    tail : Stream A
open Stream
-- 你要的共归纳原理版本（补全初始前提）
stream-coind : {A : Set} (P : Stream A → Set)
  → (destruct-head : ∀ x → P x → Σ A λ y → head x ≡ y)
  → (destruct-tail : ∀ x → P x → P (tail x))
  → (∃ λ x → P x) -- 补的初始前提：存在满足P的Stream
  → Σ (Stream A) λ s → P s
stream-coind P dh dt (x , px) = go x px
  where
  -- 共递归构造保持P的Stream
  go : ∀ x → P x → Σ (Stream A) λ s → P s
  go x px .fst .head = (dh x px) .fst
  go x px .fst .tail = (go (tail x) (dt x px)) .fst
  go x px .snd = px -- 这里可以根据你P的定义调整，保持性质成立

如果你要的是不需要初始Stream的状态机构造版本，写起来更简单：

unfold-stream : {A S : Set} → (S → A) → (S → S) → S → Stream A
unfold-stream h t s .head = h s
unfold-stream h t s .tail = unfold-stream h t (t s)

Coq 实现 #

Coq用CoInductive定义共归纳类型，用cofix策略做共递归，只要保证递归调用出现在共归纳构造子的 guarded 位置即可：

(* 标准Stream定义 *)
CoInductive Stream (A : Type) : Type := Cons : A -> Stream A -> Stream A.
Arguments Cons {A} _ _.
Definition head {A} (s : Stream A) := match s with Cons x _ => x end.
Definition tail {A} (s : Stream A) := match s with Cons _ tl => tl end.
(* 补全前提的共归纳原理 *)
Theorem stream_coind {A : Type} (P : Stream A -> Type) :
  (forall x, P x -> { y : A | head x = y }) ->
  (forall x, P x -> P (tail x)) ->
  (exists x, P x) ->
  exists s : Stream A, P s.
Proof.
  intros Hd Ht [x0 Px0].
  (* 启动共递归 *)
  cofix Cofix.
  exists (Cons (proj1_sig (Hd x0 Px0)) (proj1_sig Cofix)).
  (* 性质保持的证明根据你的P的具体定义补全即可 *)
Admitted.

你平时见的更多的Stream共归纳原理是互模拟蕴含相等的版本，本质也是同一个余代数原理的应用，一样可以用上述共递归机制直接证明。
内容的提问来源于stack exchange，提问作者Hexirp