The Coq mailing list

[roconnor AT theorem.ca]

On Tue, 13 Sep 2005, Conor McBride wrote:

> roconnor AT theorem.ca
>  wrote:
>
> > Welcome to the nightmare that is programming with dependent types. ;-)
> >
>
> Would you care to clarify, refine or qualify this remark?

Whenever I use dependent types defined by inductive families (is this the
righ terminology?), things that look easy turn out to be actually very
hard to do.  I think that Adam's case is a resonable example of this.

This maybe just because these things are hard to do, and their ease is
either an illusion. Maybe they are easy given some hard lemmas. Maybe I
just don't know what I am doing.

For example Pierre's solution to Adams' problem relies on his ``decomp''
theorem, which is obviously true, yet somewhat difficult to prove.  So
perhaps with better library support to get these hard lemmas out of the
way, programming with dependent types would be easier.

I should say ``reasoning about dependent programs'', because defining
BVand is not as difficult as proving properites about BVand.

Maybe it is worth a closer look at what I find to be a difficult about
this problem.  In Adam's problem it's not to hard to get as far as:

    even : forall n : nat, Bvector n -> bool
    y : Bvector 32
    ______________________________________(1/1)
    forall (a : bool) (v : vector bool 31),
    even 32 (Vcons bool a 31 v) || even 32 y =
    even 32 (BVand 32 (Vcons bool a 31 v) y)

if you know to use dependent inversion.

But now we cannot use dependent inversion to decontruct y.  Why not?
This is the error:

    The term "even" of type "forall n : nat, Bvector n -> bool"
    cannot be applied to the terms
     "n" : "nat"
     "Vcons bool a 31 v" : "vector bool 32"
    The 2nd term has type "vector bool 32" which should be
    coercible to "Bvector n"

So dependent inversion is trying to create a proof term that looks
something like:

    match y as y in (Bvector n)
    return (...(BVand n ??? y)...)
    ...

The fact that y occurs in the goal (making this very dependent) forces
BVand to take m as it's parameter.  So whetever ??? is it must be of type
(Bvector n).  But (Vcons ...) can never have type (Bvector n).  It is
always of type (Bvector (S ...)).  I am inclined to abstract out this
(Vcons ...) term and make it a variable.

So I try:

    even : forall n : nat, Bvector n -> bool
    y : Bvector 32
    ______________________________________(1/1)
    forall (a : bool) (v : vector bool 31) (s : vector bool 32),
    Vcons bool a 31 v = s -> even 32 s || even 32 y = even 32 (BVand 32 s y)

But again this doesn't work because (Vcons bool a 31 v) = s forces s and
(Vcons bool a 31 v) to have the same type.  So s must still be
(Bvector (S ...)) and we haven't got anywhere.

Upon reflection one notices that the problem isn't with the term
(Vcons bool a 31 v) but that its type isn't flexible enough.  We can
make the type more flexible by replacing the term with
(eq_rect 32 Bvector (Vcons bool a 31 v) 32 (refl_equal 32)), and then
generalizing (refl_equal 32).  With some coxing we can get coq to

    even : forall n : nat, Bvector n -> bool
    a : bool
    v : vector bool 31
    y : Bvector 32
    t := 32 : nat
    ______________________________________(1/1)
    forall e : t = 32,
    even 32 (eq_rect t Bvector (Vcons bool a 31 v) 32 e) || even 32 y =
    even 32 (BVand 32 (eq_rect t Bvector (Vcons bool a 31 v) 32 e) y)

and now apply dependent inversion y, leading to

    even : forall n : nat, Bvector n -> bool
    a : bool
    v : vector bool 31
    y : Bvector 32
    a0 : bool
    v0 : vector bool 31
    e : 32 = 32
    ______________________________________(1/1)
    even 32 (eq_rect 32 Bvector (Vcons bool a 31 v) 32 e)
    || even 32 (Vcons bool a0 31 v0) =
    even 32
      (BVand 32 (eq_rect 32 Bvector (Vcons bool a 31 v) 32 e)
         (Vcons bool a0 31 v0))

Now we need to get rid of the eq_rect we added.  This can be done with the
K_dec_set lemma found in the Eqdep_dec library.

Finally we end up at our desired place.

    even : forall n : nat, Bvector n -> bool
    a : bool
    v : vector bool 31
    a0 : bool
    v0 : vector bool 31
    ______________________________________(1/1)
    even 32 (Vcons bool a 31 v) || even 32 (Vcons bool a0 31 v0) =
    even 32 (BVand 32 (Vcons bool a 31 v) (Vcons bool a0 31 v0))

The resulting proof script is:

Require Import Bvector.
Require Import Eqdep_dec.
Require Import Peano_dec.

    Goal forall (even: forall n, (Bvector n) -> bool) (x y:Bvector 32), (even
    32 x) || (even 32 y) = (even 32 (BVand 32 x y)).
    intro.
    dependent inversion x.
    clear x n H0.
    intro y.
    change (Vcons bool a 31 v) with
    (eq_rect 32 Bvector (Vcons bool a 31 v) 32 (refl_equal 32)).
    generalize (refl_equal 32).
    set (t:=32).
    unfold t at 2 3 5 6 7 8 10.
    dependent inversion y.
    unfold t.
    clear y t H0 n.
    intro.
    pattern e.
    apply K_dec_set.
    apply eq_nat_dec.
    clear e.
    unfold eq_rect.

when you think it ought to be

    Goal forall (even: forall n, (Bvector n) -> bool) (x y:Bvector 32),
    (even 32 x) || (even 32 y) = (even 32 (BVand 32 x y)).
    intro; dependent inversion x.
    intro; dependent inversion y.

That is what I call a nightmare.  But perhaps I am only ignorant, and
there is some clear methodology to reason about dependent types that I
don't know.  I'd love to hear it (or have someone post it to the coq wiki
;-).

That being said I love dependent types.  I find it satisfying to write
code that doesn't return default values in absurd cases and instead prove
the absurd cases are impossible.

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''