0
$\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

1 Answer 1

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$
    – 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$
    – 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

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.