# JMeq and dependent programming

I’m trying to wrap my brain around the essence of the problems with dependent programming and equality. Some proofs are more difficult or impossible to do without the `JMeq` axiom. I’ve been trying to formulate a minimal example that captures the essence of this problem:

``````Inductive inf : (unit -> Type) :=
| infc : inf tt -> inf tt.

Lemma match_eq (c : inf tt) (e : tt = tt) :
match e in _ = y return inf y with
| eq_refl => infc c
end = infc c.
``````

As far as I can see, this is not provable without axioms. Can anyone confirm this or give a counterexample? The closest I’ve gotten is:

``````refine (
match e as e0 in _ = f return
forall (c0 : inf f),
match e0 in _ = g return inf g with
| eq_refl => infc c
end = infc c0
with
| eq_refl => _
end c).
``````

The error message Coq gives here is very confusing by the way. It says that `c0` in `infc c0` has type `inf f` but should have type `inf ()`. If I then change it to `infc c`, Coq changes its mind and tells us it `c` has type `inf ()` but should have type `inf f`. This seems to be related to the usage of `unit`. If I change the argument of `inf` to `bool`, the error disappears (but the lemma is still not provable).

As far as I can see, this is not provable without axioms. Can anyone confirm this or give a counterexample?

Definitely provable:

``````Lemma match_eq (c : inf tt) (e : tt = tt) :
match e in _ = y return inf y with
| eq_refl => infc c
end = infc c.
Proof.
Require Import Coq.Logic.Eqdep_dec.
apply eq_sym.
apply Eqdep_dec.eq_rect_eq_dec.
decide equality.
Qed.

Print Assumptions match_eq.
(* Closed under the global context *)
``````

This works for any type with decidable equality, but for the case of unit the standard library actually includes a direct proof:

``````  (** Examples of short direct proofs of unicity of reflexivity proofs
on specific domains *)

Lemma UIP_refl_unit (x : tt = tt) : x = eq_refl tt.
Proof.
change (match tt as b return tt = b -> Prop with
| tt => fun x => x = eq_refl tt
end x).
destruct x; reflexivity.
Defined.
``````

Here is a way simpler handcrafted proof.

``````Lemma match_eq (c : inf tt) (e : tt = tt) :
match e in _ = y return inf y with
| eq_refl => infc c
end = infc c.
Proof.
refine (
match e as e0 in _ = f return
match e0 in _ = g return inf g with
| eq_refl => infc c
end = match f return inf tt -> inf f with tt => fun x => x end (infc c)
with
| eq_refl => eq_refl
end
).``````

Oh, I’m only now realizing that I never replied to this. It took me so long to try to understand what was going on that I forgot about it. But both of your replies were very helpful. I think that my conclusion is that it is very difficult to get Coq to do what you want when you have to supply a full ‘match as in return’. The error messages also seem to be a bit off sometimes. It’s good to know that the `Eqdep_dec` library exists, will help alleviate my problems

For once, the rules of what Coq are indeed documented, and there are some blog posts on the web, but this feature is definitely hard to use. A much more ergonomic interface is provided by the Equations plugin.