The Coq mailing list

[S3 <scubed2 AT gmail.com>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

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

Thank you for the proof!  I haven't done much fancier things
like eapply yet.  I've been fidgeting around just trying
to get a feel for it.  I adapted your proof like this:

  intros.
  induction H.
  pattern b.
  apply (JMeq_ind (x:=a)).
    apply JMeq_refl.

  apply H0.

Though, eapply is useful to get around specifying x at the time.
I have some more questions around this subject,
but I'll play with it more before asking.

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

- -- 
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/

iEYEARECAAYFAlCh3pcACgkQxzVgPqtIcfvQPwCfcgZQDFHwL0zj7mJCO9HxiGvj
k8UAnihroE4jwSOXmf3+GhYWfd0qbXcv
=uoaj
-----END PGP SIGNATURE-----