Relations with dependent types in Coq

user_10977061 0
Viewed 50

I want to define a relation over two type families in Coq and have come up with the following definition dep_rel and the identity relation dep_rel_id:

Require Import Coq.Logic.JMeq.
Require Import Coq.Program.Equality.
Require Import Classical_Prop.

Definition dep_rel (X Y: Type -> Type) :=
  forall i, X i -> forall j, Y j -> Prop.

Inductive dep_rel_id {X} : dep_rel X X :=
| dep_rel_id_intro i x: dep_rel_id i x i x.

However, I got stuck when I tried to prove the following lemma:

Lemma dep_rel_id_inv {E} i x j y:
  @dep_rel_id E i x j y -> existT _ i x = existT _ j y.
Proof.
  intros H. inversion H. subst.
Abort.

inversion H seems to ignore the fact that the two xs in dep_rel_id i x i x are the same. I end up with the proof state:

  E : Type -> Type
  j : Type
  x, y, x0 : E j
  H2 : existT (fun x : Type => E x) j x0 = existT (fun x : Type => E x) j x
  H : dep_rel_id j x j y
  x1 : E j
  H5 : existT (fun x : Type => E x) j x1 = existT (fun x : Type => E x) j y
  x2 : E j
  H4 : j = j
  ============================
  existT E j x = existT E j x1

I don't think the goal can be proved in this way. Are there any tactics for situation like this that I'm not aware of?

By the way, I was able to prove the lemma with a somehow tweaked definition like below:

Inductive dep_rel_id' {X} : dep_rel X X :=
| dep_rel_id_intro' i x j y:
  i = j -> x ~= y -> dep_rel_id' i x j y.

Lemma dep_rel_id_inv' {E} i x j y:
  @dep_rel_id' E i x j y -> existT _ i x = existT _ j y.
Proof.
  intros H. inversion H. subst.
  apply inj_pair2 in H0.
  apply inj_pair2 in H1. subst.
  reflexivity.
Qed.

But I'm still curious whether this can be done in a simpler way (without using JMeq probably?). I'd be grateful for your suggestions.

dependent-type coq
1 Answers

Not sure what the issue is with inversion, indeed it seems like it has lost track of an important equality. However, using case H instead of inversion H seems to work just fine:


Lemma dep_rel_id_inv {E} i x j y:
  @dep_rel_id E i x j y -> existT _ i x = existT _ j y.
Proof.
  intros H.
  case H.
  reflexivity.
Qed.

But having case or destruct do the job where inversion couldn’t is very suprising to me. I suspect some kind of bug/wrong simplification by inversion, as simple inversion also gives a hypothesis from which one can prove the goal.

user_153746210
Related