2

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

Isaac van Bakel
  • 1,772
  • 10
  • 22
  • Why not define `c` as a `Notation` or `Definition` for `b`? – Li-yao Xia Mar 31 '20 at 13:42
  • The actual problem is slightly more complex. I have an `Inductive` which is just an enum, and another `Inductive` with two constructors wrapping that enum. I want, for some of the enum values, that the two constructors are equivalent. – Isaac van Bakel Mar 31 '20 at 14:52

1 Answers1

2

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.

Li-yao Xia
  • 31,896
  • 2
  • 33
  • 56
  • This won't be the last word, since it seems like quotients and HoTT are both active development areas in Coq. Hopefully in a few months there will be a way to actually implement this without a setoid or equivalent construction. – Isaac van Bakel Apr 06 '20 at 16:10