The Coq mailing list

[S3 <scubed2 AT gmail.com>]

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

> S3 wrote:
>> Theorem permutation_12 n r: permutation n r = permutation2 n r.
>>    unfold permutation.
>>    unfold permutation2.
>>    destruct (leb r n) as [] _eqn.
>> Error: The correctness of the conclusion relies on the body of b
>
> In situations like this, it is useful to break the operation of [destruct]
into stages.  Your example fails in the very first stage.
>
> To simulate that stage, run:
>     generalize (leb r n).
> This tactic just tries to replace all occurrences of the term with a fresh
variable.  The error message reveals that the result is ill-typed, due to a 
use
of [leb_complete], one of whose arguments is typed in terms of [leb].  Because
you replace a use of [leb], that argument assumes an improper type.
>
> The easiest solution I know is to run [generalize (leb_complete r n)] first.
Then your original strategy works.

Thanks!  I tried that and was able to prove the rest fairly directly.

- -- 
++++++++++++[->+++++++>+++++++++<<]>-.>[->+>+>+>+>+
<<<<<]>++++++++.>-------.<--.>>.---.>++.>-----.>+++
+++++[->++++<]>.<<<<<<<<.>>++.>.>.>.>>++++++++++.
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.17 (GNU/Linux)
Comment: Using GnuPG with Gentoo - http://enigmail.mozdev.org/

iEYEARECAAYFAk5KDpAACgkQxzVgPqtIcfvJ+QCeNhO0iia0X58pgY/OA6CTt2l0
gYgAn2NSKa7h4dUCyPIAfak7OblmFq/g
=upPZ
-----END PGP SIGNATURE-----