The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Mon, 12 Nov 2012 07:53:11 -0800,
S3 
<scubed2 AT gmail.com>
 a écrit :

> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA1
> 
> I'm using Coq 8.3pl1, which I know is old.
> I don't have a newer version handy to check on.
> So, I'm posting this just-in-case.
> This triggers the anomaly error message.
> 
> 
> Require Import JMeq.
> 
> Inductive Even : nat -> Prop :=
> | e0 : Even 0
> | e2 : forall n, Even n -> Even (S (S n))
> .
> 
> Theorem split_e2 n0 n1 a b : n0 = n1 -> JMeq a b -> JMeq (e2 n0 a)
> (e2 n1 b). intros.
>   induction H0.
> (*
> Anomaly: Uncaught exception Option.IsNone. Please report.
> *)

That is easily explained, though once again coq error messages are
bad :(

The reason is that the "true" JMeq principle induction would be:
∀ A (x : A) (P : ∀ B y, Prop), (P A x) → ∀ B (y : B),
 JMeq A x B y → P B y

(You can see it by redefining JMeq the way it is defined,
 that is "Print JMeq." copy/paste definition, rename it into JMeq2 as
 well as its constructors, then "Print JMeq2_ind".)

But some people (maybe they are wrong, maybe they are not) thought it
would be better to have some apparently weaker induction principle:
∀ A (x : A) (P : A → Prop), (P A x) → ∀ (y : A),
 JMeq A x A y → P A y

So they probably have deactivated induction generation (Unset
Elimination Schemes. or something alike), then they manually defined
their own. As a result, the expected type of JMeq_{ind,rec,rec_t} does
not match what induction expects.

Theorem split_e2 n0 n1 a b : n0 = n1 -> JMeq a b -> JMeq (e2 n0 a) (e2
n1 b). intros.
  subst.
  change ((fun x => JMeq (e2 n1 a) (e2 n1 x)) b).
  eapply JMeq_ind.
   esplit.
  auto.
Qed.

I never use the induction tactic when there is no recursion. I prefer a
straight-forward "destruct" or "case" tactic. In fact, I even consider
generation of induction principles annoying for non recursive types, as
I never use them, but they tend to pollute the results of
SearchAbout&co. Plus they are extracted when doing an Extraction
Library (but I have found the Separate Extraction command, which is a
lot better for most developements IMHO).

> - -- 
> echo 'scale=2735;sqrt(57)' | BC_LINE_LENGTH=391 bc |
> tail -n 1 | tr 0-9 'ertiSSngl '
> -----BEGIN PGP SIGNATURE-----
> Version: GnuPG v2.0.17 (GNU/Linux)
> Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
> 
> iEYEARECAAYFAlChG2cACgkQxzVgPqtIcftZSQCfdE+8Spy1fMRvXrJ2x9wz/pU6
> tYoAn3T99WK22rNxL7b4iWKIeL1GIV60
> =WJxr
> -----END PGP SIGNATURE-----