JMeq and dependent programming

Using Coq
1

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

2

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

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
).
4

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

5

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.