Equality between inductively defined relations

Using Coq
1

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.

2

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