0

I'm try to run some simple examples on apply ... with ... tactic from Pierce's "Software Foundations".

It seems that examples from book doesn't work for me:

Theorem trans_eq: forall (X: Type) (n m o: Type),
                    n = m -> m = o -> n = o.
Proof.
  intros X n m o eq1 eq2. rewrite -> eq1. rewrite -> eq2. reflexivity.
Qed.

Example trans_eq_example' : forall (a b c d e f : nat),
     [a;b] = [c;d] ->
     [c;d] = [e;f] ->
     [a;b] = [e;f].
Proof.
  intros a b c d e f eq1 eq2.
  (* If we simply tell Coq apply trans_eq at this point,
     it can tell (by matching the goal against the
     conclusion of the lemma) that it should instantiate X
     with [nat], n with [a,b], and o with [e,f].
     However, the matching process doesn't determine an
     instantiation for m: we have to supply one explicitly
     by adding with (m:=[c,d]) to the invocation of
     apply. *)
  apply trans_eq with (m:=[c;d]). apply eq1. apply eq2. Qed.

trans_eq_example' failed with error:

trans_eq_example' < apply trans_eq with (m:=[c;d]).
Toplevel input, characters 6-30:
> apply trans_eq with (m:=[c;d]).
>       ^^^^^^^^^^^^^^^^^^^^^^^^
Error: Impossible to unify "?1707 = ?1709" with "[a; b] = [e; f]".

Additional information about Coq version:

coqtop -v
The Coq Proof Assistant, version 8.4pl4 (July 2014)
compiled on Jul 27 2014 23:12:44 with OCaml 4.01.0

How can I fix this error?

5
  • As I don't have the Software Foundation source code at hand, could you give us the notation for what [a;b] stands for ? Is it lists ?
    – Vinz
    Jan 21, 2016 at 9:10
  • 1
    The error seems to be quite trivial. In trans_eq, n, m and o must be of type X, not of type Type. Note that currently X is not used in your theorem.
    – eponier
    Jan 21, 2016 at 9:12
  • Damned @eponier, your beat me by 1min :) you should post answers in the Answer section.
    – Vinz
    Jan 21, 2016 at 9:15
  • @Vinz I hesitated, because it is a particular case. I post an answer when I have more interesting things to write. I am not sure if it is a question general enough to be kept on SO. At least, I would suggest to change the title to reflect the actual problem.
    – eponier
    Jan 21, 2016 at 9:24
  • I agree, the title should be corrected.
    – Vinz
    Jan 21, 2016 at 9:50

1 Answer 1

3

The issue is not the apply but a typo in your previous code. The definition of trans_eq should be:

Theorem trans_eq: forall (X:Type) (n m o: X), n = m -> m = o -> n = o.

Note that the type of n m o should be X, not Type.

Your Answer

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

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