The Coq mailing list

[Evgeny Makarov <emakarov AT gmail.com>]

Éric,

I am having trouble reproducing your result. Here is the complete
standalone file that works in Coq 8.3 as well as in more recent trunk
version.

Require String. Open Scope string_scope.

Ltac move_to_top x :=
  match reverse goal with
  | H : _ |- _ => try move x after H
  end.

Tactic Notation "assert_eq" ident(x) constr(v) :=
  let H := fresh in
  assert (x = v) as H by reflexivity;
  clear H.

Tactic Notation "Case_aux" ident(x) constr(name) :=
  first [
    set (x := name); move_to_top x
  | assert_eq x name; move_to_top x
  | fail 1 "because we are working on a different case" ].

Ltac Case name := Case_aux Case name.

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'].
 Case "E = ev_0". simpl. intro Em. apply Em.
 Case "E = ev_SS n' En'".
  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. apply Em.
  (*rewrite <- H in Em. apply Em.*)
Qed.

(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.

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.

Evgeny