The Coq mailing list

[Eric Tanter <etanter AT dcc.uchile.cl>]

Hi Evgeny,

> (Note that you can just say "rewrite H" instead of "rewrite -> H".) In
> any case, your insight that one can do "rewrite H. apply Em." instead
> of "rewrite <- H in Em. apply Em." is correct.

Thanks for confirming this! at least I'm not so confused ;)

> If you still have this problem, could you create a small standalone
> file and post it? Also, what version of Coq do you have? If you can
> use the command line and if you know where the program coqtop is, you
> can type "coqtop --version" to find out the version.

I have found what seems to be the problem. The SF files do some imports, 
which eventually import Basics.v. This file has a definition for plus/+ :

Fixpoint plus (n : nat) (m : nat) {struct n} : nat :=
  match n with
    | O => m
    | S n' => S (plus n' m)
  end.

Notation "x + y" := (plus x y)  (at level 50, left associativity).

Putting these definitions at the beginning of the following file:
-----------------------
(** imports, or definition of plus/+ **)

Inductive ev : nat -> Prop :=
  | ev_0 : ev O
  | ev_SS : forall n:nat, ev n -> ev (S (S n)).

Theorem ev_sum : forall n m,
   ev n -> ev m -> ev (n+m).
Proof.
  intros n m En.
  induction En as [|n' En'].
  simpl. intro Em. apply Em.
   intro Em. apply IHEn' in Em.
   assert (H: S (S n') + m = S (S (n' + m))).
   simpl. reflexivity.
   apply ev_SS in Em.  
   rewrite H.
(* rewrite <- H in Em. *)
   apply Em.
Qed.
-----------------------
fails on the rewrite H with 
"Error: Found no subterm matching "S (S n') + m" in the current goal."

If I remove the imports / remove the definition of plus/+, then it works!

So this seems to be a problem with the definition of plus/+. Any idea?

Thanks,

-- Éric