Equality between inductively defined relations

Hi there,

I have a theorem stating that if a binary relation can be split as the union of two other relations (R = union R1 R2) than a certain property holds, where the union is defined inductively:

Definition Rel (A:Type) := A → A → Prop.

Inductive union {A} (red1 red2: Rel A) : Rel A :=
| union_left: forall a b, red1 a b → union red1 red2 a b
| union_right: forall a b, red2 a b → union red1 red2 a b.

Theorem mytheorem {A:Type}: forall (R :Rel A), exists (R1 R2: Rel A), R = (union R1 R2) /\ …

In other project, I defined the relation lx inductively as follows:

Inductive lx: Rel pterm :=
| b_ctx_rule : forall t u, b_ctx t u → lx t u
| x_ctx_rule : forall t u, x_ctx t u → lx t u.

Now I need to prove that lx = union b_ctx x_ctx in order to use my theorem:

1 subgoal (ID 333)

lx = union b_ctx x_ctx

Is it possible to do so? In other words, is an inductive defined relation “equal” to the union of its constructors?

Any comment suggestion is very much appreciated.

This is not possible in Coq without axioms, because equality of inductive types is nominal, not structural. One typical workaround is to strengthen mytheorem to apply when forall a b, R a b <-> union R1 R2 a b, though this may complicate the proof. Another is to change the definition of lx to be explicitly Definition lx := union b_ctx x_ctx.

The axioms of Propositional Extensionality plus Function Extensionality should make the goal lx = union b_ctx x_ctx provable.
You could also take a look at this discussion coq/coq#5293, which sort of expanded from the initial limited feature request to a discussion of the possibility of structural inductive types in Coq.

1 Like