coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
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\...
- [Coq-Club] bug (or feature?) in induction .. eqn:.. version 8.4pl2, Alain Lichnewsky, 02/11/2014
- Re: [Coq-Club] bug (or feature?) in induction .. eqn:.. version 8.4pl2, Cedric Auger, 02/11/2014
Archive powered by MHonArc 2.6.18.