How do you work with dependent types where the function making the type differs?
I'm working on a problem where I have 2 dependent types where the types are indexed in different ways. I want to show a form of proof irrelevance. Basically, I want to prove
Theorem existT_eqrect_bool_irrel {A B} (P : A -> Type) p b (eq0 eq1 : b = true)
(Q := fun (b : bool) => if b then P p else B) Qb :
existT P p (eq_rect b Q Qb true eq0) =
existT P p (eq_rect b Q Qb true eq1).
destruct eq0.
Error: Abstracting over the terms "b0" and "eq0" leads to a term
fun (b1 : bool) (eq2 : b = b1) =>
forall eq3 : b = b1,
existT P p (eq_rect b Q Qb b1 eq2) = existT P p (eq_rect b Q Qb b1 eq3)
which is ill-typed.
Reason is: Illegal application:
The term "existT" of type
"forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}"
cannot be applied to the terms
"A" : "Type"
"P" : "A -> Type"
"p" : "A"
"eq_rect b Q Qb b1 eq2" : "Q b1"
The 4th term has type "Q b1" which should be coercible to
"P p".
But, any attempts I make to change it are ill-typed in that
it no longer knows that P p = Q true because it generalizes the true
and P p = Q b isn't generally true.
If I try smaller cases, they follow immediately, e.g.
Theorem existT_eqrect_irrel {A} (P : A -> Type) a b (eq0 eq1 : a = b) Pa :
existT P b (eq_rect a P Pa b eq0) =
existT P b (eq_rect a P Pa b eq1).
destruct eq0, eq1; apply eq_refl.
Qed.
Is it possible to prove existT_eqrect_bool_irrel without extra axioms?
Or, is there some similar form that is provable?
Additionally, working with types through eq_rect seems painful
in Coq. Is there general advice to make it more manageable?
Indeed, what you want is a consequence of proof irrelevance for equality. In general, this does not hold in Coq, ie. it is not provable that forall (A : Type) (x y : A) (p q : x = y), p = q. However, by Hedberg's theorem, any type with decidable equality has proof irrelevant equality. A consequence of this is that your identity is provable, albeit not through a simple destruct:
From Coq Require Import Logic.Eqdep_dec.
Theorem existT_eqrect_bool_irrel {A B} (P : A -> Type) p b (eq0 eq1 : b = true)
(Q := fun (b : bool) => if b then P p else B) Qb :
existT P p (eq_rect b Q Qb true eq0) =
existT P p (eq_rect b Q Qb true eq1).
Proof.
f_equal.
destruct eq0 ; cbn.
apply eq_rect_eq_dec.
intros [] [].
1,4: left ; easy.
all: right ; congruence.
Qed.