Writing equality decision that reduces `dec x x` for opaque `x`

Using Coq
8

Interesting, I will probably try it out.

Context:

Anyway, I will give a bit more context, since I can be potentially suffering from XY problem and solving an incorrect problem.

This question is connected to my previous question. Where I define an inductive type representing types and a type expr : type -> Type representing computations/programs.

Expressions are equivalent under a certain reduction. In the previous question I have asked how to implement this reduction. The part in the reduction is to reduce Pair[Proj1[p]][Proj2[q]] to just p : X×Y. Reduction implemented using Equations plugin:

Equations? reduce {E : type} (e : E) : E :=
  ...
  reduce (Pair[Proj1[p]][Proj2[q]]) := _;                                                           
  ...
  reduce e := e.

(* if p ≡ q then p else pair[proj1[p]][proj2[q]] *)
destruct (dec_expr p q) as [eq | neq].
- inversion eq.
  rewrite H0.
  apply q.
- apply (pair[proj1[p]][proj2[q]]).
Defined.

I define an equality on expression that have the same computational behavior i.e. are the same under reduction expr_eq_red, give the same result for all inputs expr_eq_ext and equal programs preserve this equality expr_eq_mor. (The symmetry and transitivity is there to make my life easier, I had trouble proving it, but that is a topic for another question)

Reserved Notation "x == y" (at level 70).

Inductive ExprEq : forall (X : type), X -> X -> Prop :=
| expr_eq_refl : forall {X : type}, forall (x : X), x == x
| expr_eq_sym : forall {X : type}, forall {x y : X}, x == y -> y == x
| expr_eq_tran : forall {X : type}, forall {x y z : X}, x == y -> y == z -> x == z
                                                                            
| expr_eq_ext : forall {X Y : type}, forall {f g : X --> Y}, (forall (x : X), f[x] == g[x]) -> f == g
| expr_eq_mor : forall {X Y : type} {f g : X --> Y} {x y : X}, f == g -> x == y -> f[x] == g[y]

| expr_eq_red : forall {X : type} (x : X), (reduce x) == x
where 
"x == y" := (ExprEq _ x y).

Under these definitions, I have trouble proving the following lemma:

 Lemma pair_identity : forall {X Y : type} (p : X × Y), pair[proj1[p]][proj2[p]] == p.
  Proof.
    intros.
    pose proof (expr_eq_red pair[proj1[p]][proj2[p]]) as p'.
    (* what now?*)
    admit.
  Admitted.

p' does not reduce to p because dec_expr p p cannot be reduced to left eq_refl in the definition of reduce