Скажем, у меня есть 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 "эта вещь, и все, что сконструировано с ее использованием, не может быть инъективным"?