Weird use of equality in Coq

Question

I have a situation that is kind of like this:

Parameter I : Type.
Parameter V : I -> Type.

Definition convert {k i} (A : V k) (eq : k = i) : V i.
    destruct eq.
    exact A.
Defined.

Theorem convert_eq : forall (i : I) (u : V i) (eq : i = i), convert u eq = u.
Proof.
    intros i u eq.
    unfold convert.
    (* Now what? *)

Usually, when working with convert, you can call destruct on the equality being used. However, in this case, trying to use destruct eq gives an error:

Abstracting over the terms "i" and "eq" leads to a term
fun (i0 : I) (eq0 : i0 = i0) => match eq0 in (_ = a) return (V a) with
                                | eq_refl => u
                                end = u
which is ill-typed.
Reason is: In pattern-matching on term "eq0" the branch for constructor "eq_refl" has type "V i" which should be 
"V i0".

I'll be honest that I've never really been good with these weird uses of equality in definitions, so maybe my whole approach is just wrong. But I feel like convert_eq should be provable somehow. Is there any way to do it?

Answer 1

This kind of thing is possible if equality on I is decidable.

From Coq Require Import Eqdep_dec.

Parameter I : Type.
Parameter V : I -> Type.

Definition convert {k i} (A : V k) (eq : k = i) : V i.
Proof.
  destruct eq.
  exact A.
Defined.

Axiom eq_dec_I : forall i j : I, i = j \/ i <> j.

Theorem convert_eq : forall (i : I) (u : V i) (eq : i = i), convert u eq = u.
Proof.
  intros i u eq.
  replace eq with (eq_refl i).
  - now simpl.
  - apply eq_proofs_unicity, eq_dec_I.
Qed.

(* alternate proof *)

Theorem convert_eq_2 : forall (i : I) (u : V i) (eq : i = i), convert u eq = u.
Proof.
  intros i u.
  apply K_dec.
  - apply eq_dec_I.
  - now simpl.
Qed.

If you can prove that equality on I is decidable, then great! Replace the axiom above with a theorem, prove the theorem, and you're all set.

If you can't prove that equality on I is decidable, then you could of course assume the law of the excluded middle. Or you could assume/prove a weaker property such as proof irrelevance, or Streicher's Axiom K. See Coq and Axioms.

Answer 2

Welcome to homotopy type theory. What if eq : i = i in convert_eq is not refl? Then conversion along eq could do something nontrivial to u.

The lemma convert_eq can be proved under the additional assumption that I is a set (in the sense of homotopy type theory). (In fact, it is equivalent ot the assumption that I is a set, but I am too lazy to formalize that.)

Parameter I : Type.
Parameter V : I -> Type.

Definition convert {k i} (A : V k) (eq : k = i) : V i.
    destruct eq.
    exact A.
Defined.

(** A set is a type whose identity types are propositions (have at most one element). *)
Definition is_set (B : Type) := forall (x y : B) (p q : x = y), p = q.

(** Note: a type with decidable equality is a set, see HoTT book 7.2.5. *)

(** Now can prove the lemma under the additional assumption. *)
Theorem convert_eq : is_set I -> forall (i : I) (u : V i) (eq : i = i), convert u eq = u.
Proof.
  intros setI i u eq.
  rewrite (setI i i eq eq_refl).
  reflexivity.
Qed.

An example of a type which is a set but its equality cannot be shown to be decidable is nat -> nat.