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.
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"?
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.