1
$\begingroup$

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?

Improve this question
$\endgroup$
1
  • 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$
    – Andrej Bauer
    May 22 at 12:49

2 Answers 2

Reset to default
0
$\begingroup$

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.
Improve this answer
$\endgroup$
6
  • $\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$
    – Pavel Shuhray
    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$
    – James Wood
    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$
    – Pavel Shuhray
    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
0
$\begingroup$

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.

Improve this answer
$\endgroup$

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.