Can I introduce sound constructor equivalence?

Question

Say I've got an Inductive type like

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

but what I really want is to "identify" b with c - that is, I want to be able to treat them as two different ways of writing the same thing - and be able to rewrite one into the other.

I could introduce it as an axiom:

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

But that's pretty clearly unsound:

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

Is there another way to do this, or something like it? I suspect the answer is no, because it would contradict Inductive constructors being injective.

Current workaround

I have a relation

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.

which then lets me define whether or not a proposition is well-defined with respect to it.

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

But this is unpleasant. It means that, for my own inductively-defined propositions, I need to add an additional constructor taking an equiv_foo to be able to prove the well-definedness property. (I suspect that just asserting the above property for some proposition would be unsound.)

Can I not tell Coq "this thing, and anything constructed using it, may not be injective"?

Answer 1

Your current workaround using an equivalence relation seems like the best solution, at least from what you described.

This looks like a use case for quotient types or homotopy type theory, but I don't know what work there is in integrating such systems with Coq.