Dependent sum and equality with Coq

Question

I have types B and A n where n:nat. I want to prove that B is the sum of all A n. I have three functions

foo (n:nat) (a: A n) : B
rang (b:B) : nat
bar (b:B) : A (rang b)

I can prove

forall (b:B), foo (rang b) (bar b) = b
forall (n:nat) (a: A n),  rang (foo n a) = n

But when I write the theorem

forall (n:nat) (a: A n), bar (foo n a) = a

I get "The term bar (foo n a) has type A (rang (foo n a)) while it is expected to have type A n". What can I do?

Answer 1

One option is to use heterogeneous or "John-Majors" equality.

Essentially, the problem is that you are trying to say that two terms of syntactically different (but equal) types are the same. However, Coq and related systems require that terms are reducible to the same thing, rather than merely equal.

Heterogeneous equality solves this by allowing you to use two different types to set up your equality. You then must prove that both the types and the terms are equal in order to prove the equality.

In Coq, there's an implementation of heterogeneous equality in the standard library: https://coq.inria.fr/library/Coq.Logic.JMeq.html. You can then write

forall (n : nat) (a : A n), JMeq a (bar (foo n a))

just as you wanted. Working with JMeq is a little more difficult, see http://adam.chlipala.net/cpdt/html/Equality.html for examples.

Answer 2

Since the code snippet doesn't work I will assume that you are trying to construct an equality type on dependent types.

Hypothesis A: nat -> Type.
Hypothesis B: Type.

Definition foo (n: nat) (a: A n) : B.  Admitted.
Definition rang (b: B) : nat. Admitted.
Definition bar (b: B) : A (rang b). Admitted.

You now have

Theorem thm1: forall (b: B), foo (rang b) (bar b) = b.
Proof. Admitted.

Theorem thm2: forall (n: nat) (a: A n),  rang (foo n a) = n.
Proof. Admitted.

You have difficulty writing this:

Theorem thm3: forall (n:nat) (a: A n), bar (foo n a) = a.

which gives you the error:

In environment
n : nat
a : A n
The term "a" has type "A n" while it is expected to have type
"A (rang (foo n a))".

Is this what you want? Well, in that case, the root problem is that to construct a type = you have to let Coq know that the types of two terms must be the same, but since you have wrapped $n$ inside some functions, Coq has no idea whether rang (foo n a) = n. You can check how eq is constructed:

Check eq.
eq
     : ?A -> ?A -> Prop
where
?A : [ |- Type]

This is checked syntactically, which means propositional equality won't simply work in your case (even though you can prove that rang (foo n a) = n). This is also known as heterogenous equality. Also, by checking the recursion rule of eq you will know more about this:

Check eq_rect.
------------------------
eq_rect
     : forall (A : Type) (x : A) (P : A -> Type),
P x -> forall y : A, x = y -> P y

It says you will obtain a new term of type $ P y $ if you can provide a proof which states that $x = y$ holds (this is actually the Leibniz rule). So the trick to type check is using transport or type cast as suggested by @djao.

Answer 3

Maybe use an explicit cast?

Theorem rang_foo : ∀ (n:nat) (a: A n), rang (foo n a) = n.
Proof.
  admit.
Admitted.

Definition cast {X Y : nat} (e : X = Y) : A X → A Y :=
  match e with erefl => id end.

Goal ∀ (n:nat) (a: A n), cast (rang_foo n a) (bar (foo n a)) = a.