The Coq mailing list

["St�phane Lescuyer" <lescuyer AT lri.fr>]

Hi,

If you look at the induction principle generated for your inductive
bit vectors, you see that it applies to a predicate P over bit vectors
of every possible size :

bits_ind
     : forall P : forall n : nat, bits n -> Prop,
       P 0 Bnil ->
       (forall (n : nat) (b : bool) (b0 : bits n),
        P n b0 -> P (S n) (Bcons n b b0)) ->
       forall (n : nat) (b : bits n), P n b

The thing here is you only want to prove something for bit vectors of
size 0, and Coq cannot infer a suitable predicate of type "forall (n :
nat) (b : bits n), P n b" such that P 0 b is precisely your goal. You
can help coq by filling in the missing cases (n <> 0) manually in the
following way :

Definition P : forall n, bits n -> Prop :=
  fun n =>
    match n return (bits n -> Prop) with
      | 0 => (fun b => b = Bnil)
      | _ => (fun b => True)
    end.

This defines a predicate P with the correct type such that P 0 is
precisely your lemma. Note that it is necessary to use dependent
matching since the equation b = Bnil only makes sense when n = 0. For
the other branch, we can use True : this makes it easily provable and
we are not interested in that branch anyway. Now, you can prove your
lemma this way :

Theorem only_one_bits0 : forall (bs:bits 0), bs = Bnil.
Proof.
  intro b; change (P O b).
  induction bs. (* this time, unification succeeds because we
explicited the suitable P *)
  simpl; reflexivity. (* the case you are interested in *)
  simpl; trivial. (* the trivial case for n <> 0 *)
Qed.

You dont have to use an auxiliary definition of P and an explicit
"change" tactic, you might as well use "apply bits_ind with P := ..."
directly when proving your lemma. If you end up doing this several
times, you can also define an inductive principle for bits 0 by
generalizing the predicate P above for any predicate of type bits 0 ->
Prop.

I dont know if there s a more elegant or quicker way to do this, but I
hope this helps.

Stephane L.
http://www.lri.fr/~lescuyer/

On Wed, Apr 9, 2008 at 1:58 PM, Michael Day 
<mikeday AT yeslogic.com>
 wrote:
> Hi,
>
>  Sorry to bother the list again, but I've been reading the manual and can't
> find any explanation of this error message:
>
>  User error: Cannot solve a second-order unification problem.
>
>  I get this error when attempting to prove the following theorem:
>
>  Inductive bits : nat -> Set :=
>     | Bnil : bits 0
>     | Bcons : forall n:nat, bool -> bits n -> bits (S n).
>
>  Theorem only_one_bits0 : forall (bs:bits 0), bs = Bnil.
>  Proof.
>  intro bs.
>  case bs. (* fails *)
>
>  It seems clear to me that a value of type "bits 0" has to be Bnil, as the
> other constructor has type "bits (S n)", but I can't figure out how to
> express this. Any help would be greatly appreciated.
>
>  Best regards,
>
>  Michael
>
>  --
>  Print XML with Prince!
>  http://www.princexml.com
>
>  --------------------------------------------------------
>  Bug reports: http://logical.futurs.inria.fr/coq-bugs
>  Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
>  Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>

-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06