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?

  • 1
    $\begingroup$ Please post a working piece of code. It is not clear whether A, B, foo, rang` etc. are concrete types or variables. As written, without knowing more about them, you cannot prove the desired equalities. There is information that you are not communicating. $\endgroup$ May 22 at 12:49

1 Answer 1


Maybe use an explicit cast?

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

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.
  • $\begingroup$ "The term "id" has type "ID" while it is expected to have type "A X -> A Y" (cannot unify "Top.A X" and "Type")." $\endgroup$ Apr 22 at 3:23
  • $\begingroup$ Since you didn't post a full working file, I don't know exactly what you did. Here is my file, in which it works: gist.github.com/davidjao/b6209fa5242368b80d77c996d7273600 $\endgroup$
    – djao
    Apr 22 at 3:51
  • $\begingroup$ Probably erefl is being seen as a variable name, rather than the alias from SSReflect. eq_refl in its place should work. $\endgroup$
    – mudri
    Apr 22 at 14:46
  • $\begingroup$ @djao Yes, I can write the theorem now, but I can't prove it:) The function cast need eq_refl to be simplified. Is each proof e: X=Y equal to eq_refl? $\endgroup$ Apr 22 at 18:38
  • $\begingroup$ In general you need Streicher's axiom K to show that all proofs of equality are equal. When equality is decidable (which is the case for nat), you can prove the result directly without axioms. See coq.inria.fr/library/Coq.Logic.Eqdep_dec.html $\endgroup$
    – djao
    Apr 23 at 4:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.