2

说我有一个Inductive类型

Inductive foo :=
  | a : foo
  | b : foo
  | c : foo.

但我真正想要的是“认同” b——c也就是说，我希望能够将它们视为编写同一事物的两种不同方式——并且能够将一种重写为另一种。

我可以把它作为一个公理来介绍：

Axiom b_equiv_c : forall P : foo -> Prop, P b <-> P c.

但这显然是不合理的：

Theorem whoops : False.
Proof.
  assert (b <> c) as H. { discriminate. }
  apply (b_equiv_c (fun x => x <> c)) in H.
  contradiction H.
  reflexivity.
  Qed.

有没有其他方法可以做到这一点，或者类似的东西？我怀疑答案是否定的，因为它与Inductive构造函数的内射相矛盾。

当前的解决方法

我有关系

Inductive equiv_foo : foo -> foo -> Prop :=
  | equiv_foo_refl (f : foo) : equiv_foo f f
  | equiv_foo_sym (f f' : foo) : equiv_foo f f' -> equiv_foo f' f
  | equiv_foo_b_c : equiv_foo b c.

然后让我定义一个命题是否是关于它的明确定义的。

Definition wd_wrt_equiv_foo (P : foo -> Prop) : Prop :=
  forall f f' : foo, equiv_foo f f' -> (P f <-> P f').

但这是不愉快的。这意味着，对于我自己的归纳定义命题，我需要添加一个额外的构造函数，equiv_foo以便能够证明明确定义的属性。（我怀疑仅仅为某个命题断言上述属性是不合理的。）

我能不能告诉 Coq“这个东西，以及使用它构建的任何东西，可能不是单射的”？

4

1 回答 1

2

您当前使用等价关系的解决方法似乎是最好的解决方案，至少从您的描述来看。

这看起来像是商类型或同伦类型理论的用例，但我不知道将此类系统与 Coq 集成有什么工作。

于 2020-03-31T15:17:28.553 回答