4

我有一个conat可以表示有限值和无限值的定义、从 的转换nat、无穷大的定义和互模拟关系：

CoInductive conat : Set := O' | S' (n : conat).

Fixpoint toCo (n : nat) : conat := match n with
  | O => O'
  | S n' => S' (toCo n') end.

CoFixpoint inf : conat := S' inf.

CoInductive bisim : conat -> conat -> Prop :=
  | OO : bisim O' O'
  | SS : forall n m : conat, bisim n m -> bisim (S' n) (S' m).

Notation "x == y" := (bisim x y) (at level 70).

我想证明它conat是有限的还是无限的（我不是 100% 确定这是正确的公式）：

(* This is the goal *)
Theorem fin_or_inf : forall n : conat, (exists m : nat, toCo m == n) \/ (n == inf).

到目前为止我无法证明它，但我可以证明另一个陈述，如果 aconat不是有限的，它是无限的（同样，不是 100% 确定公式）：

(* I have a proof for this *)
Theorem not_fin_then_inf : forall n : conat, ~ (exists m : nat, toCo m == n) -> (n == inf).

我不知道如何从not_fin_then_inf到fin_or_inf。

  1. 我的定义fin_or_inf正确吗？

  2. 我可以证明fin_or_inf使用not_fin_then_inf或不使用它吗？

此外，我发现弥合这两个定理之间的差距涉及双模拟（或其扩展）的可判定性。我认为可判定性定理可以表述为

Lemma bisim_dec : forall n m : conat, n == m \/ ~ (n == m).
  1. 我可以证明bisim_dec或任何类似的关于双模拟的陈述吗？

编辑

证明“有限或无限”的最初动机是证明 的交换性和结合性coplus：

CoFixpoint coplus (n m : conat) := match n with
  | O' => m
  | S' n' => S' (coplus n' m)
end.
Notation "x ~+ y" := (coplus x y) (at level 50, left associativity).

Theorem coplus_comm : forall n m, n ~+ m == m ~+ n.
Theorem coplus_assoc : forall n m p, n ~+ m ~+ p == n ~+ (m ~+ p).

nat采用与's相同的方式+不起作用，因为它需要==具有类似于 的引理的传递性plus_n_Sm，这使得 cofix 调用不受保护。否则，我必须同时破坏nand m，然后我就卡在了目标上n ~+ S' m == m ~+ S' n。

如果我选择另一种定义coplus：

CoFixpoint coplus (n m : conat) := match n, m with
  | O', O' => O'
  | O', S' m' => S' m'
  | S' n', O' => S' n'
  | S' n', S' m' => S' (S' (coplus n' m'))
end.

然后coplus_comm很容易，但反而coplus_assoc变得几乎不可能证明。

  1. 我真的可以coplus_comm用 的第一个定义coplus或coplus_assoc第二个定义来证明吗？
4

0 回答 0