Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] bug (or feature?) in induction .. eqn:.. version 8.4pl2

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] bug (or feature?) in induction .. eqn:.. version 8.4pl2


Chronological Thread 
  • From: Cedric Auger <sedrikov AT gmail.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] bug (or feature?) in induction .. eqn:.. version 8.4pl2
  • Date: Tue, 11 Feb 2014 15:25:03 +0100

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



Archive powered by MHonArc 2.6.18.

Top of Page