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

Using Coq
1

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.
  admit.
Admitted.
2

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.
3

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?

4

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.

5

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
6

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

7

I guess that would be possible when (if) user-defined rewrite rules land in 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

9 
(* 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).

10

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 :smiley:

11

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.