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

Is there a way to write an equality decision function `dec (x y : X) : {x=y} + {x<>y}` for some type `X`, that reduces `dec x x` to `left eq_refl` no matter what `x : X` is?

An example: let’s define `my_bool` type and it’s default decision function:

``````Inductive my_bool := true | false.

Definition dec (b b': my_bool) : {b=b'} + {b<>b'}.
decide equality.
Defined.
``````

Introduce two opaque parameters

``````Parameter x x' : my_bool.
``````

The `Compute (dec x x')` can not be obviously reduced and definition of `dec` is just displayed.

However, I would really like to have `Compute (dec x x)` to reduce to `left eq_refl`.

Also, is there a way to show the following lemma?

``````Lemma id_dec : forall (b : my_bool), dec b b = (left eq_refl).
Proof.

You can prove a more general case of your lemma first:

``````From Coq Require Import Eqdep_dec.

Lemma eq_dec_refl A (eq_dec : forall x y : A, {x = y} + {x <> y}) x :
eq_dec x x = left eq_refl.
Proof.
destruct (eq_dec x x) as [|[]]; trivial.
f_equal.
now apply K_dec_type with (P := fun prf => prf = eq_refl).
Qed.
``````

Then the rest is easy:

``````Lemma id_dec b : dec b b = (left eq_refl).
Proof.
now rewrite eq_dec_refl.
Qed.
``````

Nice solution!

And what about the first part of the question?

How can I get `Compute (dec x x)` to reduce to `left eq_refl`?

I don’t think one can define a function like that in standard Coq. `dec` still has to inspect its inputs meaning that reduction of `dec x x` would be blocked on a `match`-expression.

In the definitional UIP branch https://github.com/coq/coq/pull/10390 this is possible.
However that branch has issues with infinite reductions (see discussion in the PR) so it’s unclear if any of it will get in a Coq release.

2 Likes

Actually computing to refl is possible in that branch but computing to left of refl probably isn’t.

I guess that would be possible when (if) user-defined rewrite rules land in Coq.

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?*)
``````

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

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

This `inversion eq` is the reason why you later need the equality proof to be `eq_refl`. Can you drop it?

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

Hedberg’s Theorem is probably what you are looking for. It was suggested to you by @anton-trunov earlier in this thread (the `K_dec_type` lemma in `Eqdep_dec`).

I can probably rewrite it into a dependent patter matching, but I think that is exactly what inversion is doing for me automatically. Thus, it probably cannot be done.

I guess I have to do some reading … I have never heard of Heberd’s Theorem … my background is in pdes and numerical analysis

Great! I have managed to prove `Lemma pair_identity` exactly as @anton-trunov suggested, and also thanks to @rafoo to nudge me to read his answer properly.