The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi,

  It is very difficult to help you:
We do not have the definitions used in your example, nor the command or tactic
that raised the error. Moreover, it seems that st1 and st2 as you wrote them
cannot be equal, if the function "update" is consistent with the intuition
given by its name.

  Questions like "I can't solve this goal" should give us access to the
smallest reproducible situation as possible, in a very small file
obtained by deleting all unnecessary details.

  When you get such "strange" error messages, it is often useful to try to
print full qualified names and terms by switching printing options and/or
using the Locate command. Perhaps it is only a clash between two identifiers
of different modules that share the same base name.


Best regards,

Pierre







Quoting fengsheng 
<fsheng1990 AT 163.com>:

> Error:
> In environment
> H : forall st st' : state, pXY / st || st' <-> pYX / st || st'
> st : state
> Heqst : st = empty_state
> st1 : state
> Heqst1 : st1 = update (update empty_state X 0) Y 2
> H1 : pYX / st || st1
> st2 : state
> Heqst2 : st2 = update (update empty_state Y 0) X 0
> H2 : pYX / st || st2
> The term "pYX" has type "com" while it is expected to have type "Imp.com".
>
> When I try to proof that st1 = st2, it just didnt do that and give the error
> information above. What does that mean and how to solve it ?