能否以CoInductive为基础构建Inductive类型？

背景：Inductive表示CoInductive的示例 #

我们可以借助Inductive类型（如nat）来表示CoInductive类型，比如用函数nat -> A模拟无限流stream A，二者存在同构关系，示例代码如下：

CoInductive stream A :=
| SCons : A -> stream A -> stream A
. 
Arguments SCons {A}.

CoInductive streq {A} : stream A -> stream A -> Prop :=
| SRefl : forall h ta tb, streq ta tb -> streq (SCons h ta) (SCons h tb)
.

Definition shead {A} (s : stream A) := match s with
| SCons h _ => h
end.
    
Definition stail {A} (s : stream A) := match s with
| SCons _ t => t
end.

Definition stream_unfold {A} (s : stream A) : s = SCons (shead s) (stail s).
  destruct s; apply eq_refl.
Defined.

Definition stream_idx {A} := fix loop (s : stream A) n := match n with
| 0 => shead s  
| S n0 => loop (stail s) n0
end.

Definition stream_from_fn {A} :=
  cofix s (f : nat -> A) := SCons (f 0) (s (fun n => f (S n))).

Definition fneq {A B} (f g : A -> B) := forall a, f a = g a.

Theorem stream_from_fn_from_stream {A} (s : stream A) : streq s (stream_from_fn (stream_idx s)).
  revert s; cofix seq; intros.
  destruct s.
  rewrite (stream_unfold (stream_from_fn _)).
  apply SRefl, seq.
Qed.
  
Theorem fn_from_stream_from_fn {A} (f : nat -> A) : fneq f (stream_idx (stream_from_fn f)).
  intros n; revert f; induction n; intros; [ apply eq_refl | ].
  apply (IHn (fun n => f (S n))).
Qed.

核心问题：仅用CoInductive能否构建Inductive类型？ #

答案是可以部分模拟，但无法完全复刻标准Inductive类型的所有原生特性，具体细节如下：

可实现的部分：带终止标记的有限结构模拟 #

我们可以给CoInductive类型添加一个"终止构造子"，再配合谓词筛选出有限成员，以此模拟Inductive类型：

• 以自然数nat为例：

  CoInductive co_nat :=
  | CoS : co_nat -> co_nat  (* 对应后继 *)
  | CoZ : co_nat.           (* 对应终止的0 *)
  
  CoInductive is_finite : co_nat -> Prop :=
  | FinZ : is_finite CoZ
  | FinS : forall n, is_finite n -> is_finite (CoS n).
  

  此时{n : co_nat | is_finite n}这个依赖对类型，就对应标准nat的结构，我们可以基于它定义递归函数、证明归纳性质，只是需要手动通过is_finite的协归纳证明来保证操作的合法性。

• 以列表list A为例：

  CoInductive co_list A :=
  | CoCons : A -> co_list A -> co_list A
  | CoNil : co_list A.
  
  CoInductive is_finite_list {A} : co_list A -> Prop :=
  | FinNil : is_finite_list CoNil
  | FinCons : forall a l, is_finite_list l -> is_finite_list (CoCons a l).
  

  同样，{l : co_list A | is_finite_list l}可以模拟标准列表的有限结构。

无法匹配的原生特性 #

• 自动终止性检查：标准Inductive类型的构造子只能生成有限项，Coq会自动验证递归函数的终止性；而模拟的结构中，类型本身允许无限项存在，递归操作的终止性需要手动通过is_finite类的谓词证明，无法依赖类型检查器自动保证。
• 原生归纳原理：Inductive类型会自动生成对应的归纳原理，而模拟结构需要手动推导类似的原理，推导过程依赖协归纳证明，复杂度更高。
• 类型层面的有限性保证：Inductive类型从定义上就排除了无限项，而CoInductive模拟的结构只能通过谓词筛选有限成员，无法从类型本身限制无限项的存在。

实现边界 #

所有可以被"带终止标记的无限结构子集"刻画的Inductive类型，都可以用这种方式模拟。但对于嵌套归纳、互归纳等复杂Inductive类型，模拟的复杂度会急剧上升，且始终无法摆脱手动维护有限性谓词的额外负担。

内容的提问来源于stack exchange，提问作者scubed