Могу ли я ввести эквивалентность звукового конструктора?

Question

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

Answer 1

Ваш текущий обходной путь с использованием отношения эквивалентности кажется лучшим решением, по крайней мере, из того, что вы описали.

Это похоже на вариант использования факторных типов или теории гомотопических типов, но я не знаю, как можно интегрировать такие системы с Coq.