The Coq mailing list

[S3 <scubed2 AT gmail.com>]

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

I was working on the attached proof file.
(I've cut out unnecessary proofs, so it should just have the main line.)

Then I tried this:

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

(Note: leb needs "Require Import Arith.".)
But, destruct gives me the error:
Error: The correctness of the conclusion relies on the body of b

What does that mean?
If I try a different order:

Theorem permutation_12 n r: permutation n r = permutation2 n r.
  destruct (leb r n) as [] _eqn.
  unfold permutation.
  rewrite Heqb.
"fun b : bool =>
 (if b as l return (b = l -> nat)
...
which is ill-typed.

How do I do case analysis here?
Is there an easy way to rewrite it to avoid this problem?
Or is there a tactic to address this?
I looked around a bit and one place recommended defining
a Scheme for the case, then destruct using that.
(But, unfortunately, I don't have enough of an understanding
of the formalisms to know what that actually means.)

Does it have to do with how I have an extra lambda to
pass the eq_refl in to reason about which case of
the match expression I'm in?

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

iEYEARECAAYFAk5IcngACgkQxzVgPqtIcftNQwCfZLCYDV98oCjtP9ReTdgdXBGK
U50An2tjb0VOl6AbnrpzU/y08j0CS2A9
=qaqG
-----END PGP SIGNATURE-----
Require Import Arith.
Require Import Recdef.
Require Import Setoid.

Theorem le_inc_both n m: n <= m -> S n <= S m.
  simpl_relation.
Qed.

Function divmod (n m: nat) (p: m > 0) {measure id n}: nat * nat :=
  if leb m n
  then
    let x := divmod (n - m) m p in
    (S (fst x), snd x)
  else (0, n).

  intros.
  unfold id.
  destruct m.
    inversion p.

  destruct n.
    discriminate teq.

  unfold lt.
  simpl.
  clear p teq.
  apply le_inc_both.
  apply le_minus.
Defined.

Inductive divides n: nat -> Prop :=
  | divides_0: divides n 0
  | divides_n m: divides n m -> divides n (m + n)
.

Definition exactdiv n m p (q: divides m n) := fst (divmod n m p).

Theorem divides_mult n m: divides n (n * m).
  induction m.
    rewrite mult_0_r.
    apply divides_0.

  rewrite mult_succ_r.
  apply divides_n.
  apply IHm.
Qed.

Theorem divides_exists n m: divides n m -> exists p, m = n * p.
  intros.
  induction H.
    exists 0.
    rewrite mult_0_r.
    tauto.

  inversion_clear IHdivides.
  rewrite H0.
  clear H0 m H.
  exists (S x).
  rewrite mult_succ_r.
  tauto.
Qed.

Definition permutation (n r: nat): nat.
  refine (
    (if leb r n as l return (leb r n = l -> nat)
     then fun _ => exactdiv (fact n) (fact (n - r)) _ _
     else fun _ => 0
    ) (eq_refl (leb r n))
  ).

    apply lt_O_fact.

  apply leb_complete in _H.
  apply le_plus_minus in _H.
  pattern n at 2.
  rewrite _H.
  clear _H.
  assert (exists a : _, n - r = a).
    exists (n - r).
    tauto.

  inversion_clear H.
  rewrite H0.
  clear H0 n.
  induction r.
    simpl.
    rewrite plus_n_O.
    rewrite plus_comm.
    apply divides_n.
    apply divides_0.

  simpl.
  pattern (fact (r + x)) at 1.
  rewrite <- mult_1_l.
  rewrite <- mult_plus_distr_r.
  rewrite mult_comm.
  apply divides_exists in IHr.
  inversion_clear IHr.
  rewrite H.
  clear H.
  rewrite <- mult_assoc.
  apply divides_mult.
Defined.

Fixpoint permutation2l n i p :=
  match i with
  | 0 => p
  | S q => permutation2l n q ((n - q) * p)
  end
.

Definition permutation2 n r :=
  if leb r n
  then permutation2l n r 1
  else 0
.

(* This part fails

Theorem permutation_12 n r: permutation n r = permutation2 n r.
  unfold permutation.
  unfold permutation2.
  destruct (leb r n) as [] _eqn.

*)

Attachment: perm.v.sig
Description: PGP signature