The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

I do not see the point in this flag. Of course, I do not know your particular case, so I won’t say that it is useless. If you need some fix to your problem, and use equation to track in what case you are, you can try:

intro n.
generalize (eq_refl n); generalize n at 1; induction n; intros m EQN.

2014-02-11 10:22 GMT+01:00 Alain Lichnewsky <alain.lichnewsky AT gmail.com>:

 In the following example, adding the eqn: flag renders the generated
   induction hypothesis useless. This seems related but different
   from bugs id=2712 and  id=2741; also this syntax is rejected in
   version 8.3pl4.

   Found this quite confusing in a larger proof (where the eqn: flags seems
   useful !) .

   Best regards.

   Alain


Lemma test: forall n, n + n = 2 * n.
Proof.
    intro n.
    induction n eqn:EQN.  reflexivity.
(*  1 subgoals
n : nat
n0 : nat
EQN : n = S n0
IHn0 : n = n0 -> n0 + n0 = 2 * n0
______________________________________(1/1)
S n0 + S n0 = 2 * S n0
*)
    (* comment: is (n = n0) in IHn0 a trace of the informal
       reasoning "here is the case n=n0 (induction hypothesis)" ?
    *)
    subst.
(*
  1 subgoals
n0 : nat
IHn0 : S n0 = n0 -> n0 + n0 = 2 * n0
______________________________________(1/1)
S n0 + S n0 = 2 * S n0

*)

(* Version information
-------------------
The Coq Proof Assistant, version 8.4pl2 (May 2013)
Architecture Linux running Unix operating system
Gtk version is 2.24.10
This is coqide.opt (opt is the best one for this architecture and OS)
*)

--
.../Sedrikov\...