The Coq mailing list

[Conor McBride <ctm AT cs.nott.ac.uk>]

Hi

Thank you for your clarification.

roconnor AT theorem.ca
 wrote:

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

I'm inclined to agree with you. I think you're right to imagine that 
these things should be easy. Given good tools, they are as easy as they 
look. I also think you're right to observe that these things turn out to 
be very hard in Coq, but this is for largely ephemeral reasons.

My worry is that people might jump to the conclusion that programming 
with dependent types is a nightmare inherently, rather than locally, 
because of poor support in one particular tool. This kind of 
misapprehension is dangerous, for me, if not for you.

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

There's an entirely systematic way to eliminate 'dependent 
subfamilies'---inductive families whose indices have been partially 
instantiated (nonempty vectors being everyone's favourite example). Its 
roots lie (perhaps unsurprisingly) in Cristina Cornes's development of 
inversion tactics for Coq. I wrote about it in my thesis, but also in my 
TYPES 2000 paper, `Elimination with a Motive', and it reappears at the 
heart of the Epigram language design in the paper (with James McKinna), 
`The view from the left'.

If you take this systematic approach, even without tool support, you at 
least reduce the amount of thought required, if not the amount of work. 
But it's highly automatable. Most of it relies on one elimination tactic 
which not only performs a suitable loading of the goal with equations, 
much the way you do by hand, but also simplifies the subgoals by 
eliminating their equational hypotheses, dismissing impossible cases 
etc. None of this is news.

> 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'm glad that there are good libraries around to help people work with 
vectors, at least. However, these are a workaround at best. It should 
not be necessary to develop a library of decomposition lemmas and such, 
just to get to a basic level of functionality with a new dependent family.

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

Fair enough. Not only that, closely related to reasoning about dependent 
programs is programming with types which themselves depend on values in 
dependent types (types indexed by vectors, for example). Fortunately, 
this also is possible with the very same technology.

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

[..]

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

You're on the right lines here...

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

This is ='s fault, not yours, and exactly the situation for which JMeq 
was invented. It gets rid of the eq_rect plumbing.

[..]

>    ______________________________________(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
>
>  
[..]

> 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 good news is, this is more or less the process which the 
`Elimination with a Motive' tactic automates, with a bit less frustrated 
experimentation.

The technique is a bit annoying to apply by hand, but mechanical. 
Whatever goal

 forall (v : Bvector 32), ...

is readily provable from

 forall (n : nat) (v' : Bvector n) (v : Bvector 32), (JMeq n 32) -> 
(JMeq v' v) -> ...

or, if you insist,

 forall (n : nat) (v' : Bvector n) (v : Bvector 32)
    (e1 : n = 32) (e2 : eq_rect n Bvector v' 32 e = v),
        ...

and then you can do whatever induction/inversion you like on v', because 
it's an arbitrary vector of an arbitrary length (which just happens to 
be equal to the one you first thought of). Notice, there's no crafty 
abstraction, nothing changes type; all you need is a suitably general 
element of the inductive family you're working with, plus some 
constraints equating the general element with your more specific original.

Of course, you'll need to simplify the more specific versions of these 
equations which show up in the subgoals. Necessarily that will involve 
Peano-style lemmas, substitutivity of equality, and possibly 
K-axioms/lemmas, in a proof-relevant and transparent form if you're 
using dependent telescopes of =-types with eq_rect coercions. However, 
the procedure for deploying these results is unremarkable: it's just 
first-order unification. Back in 1998, I was enough of a masochist to 
implement the whole gory thing in the Lego system.

It all gets a lot less gory if you use non-dependent sequences of 
JMeq-types. JMeq makes it easier to state the equations, and you only 
need its substitution principle in the simplification process. The 
Peano-lemmas for inductive families are also easily and systematically 
proven, in a form which is suited to eliminating equational hypotheses, 
given JMeq. James McKinna, Healf Goguen and I cooked up the technique in 
1998, and I simplified it for JMeq in my thesis. It somehow always got 
squeezed out of papers until this year's `A Few Constructions on 
Constructors'. It's a bit tedious by hand, although much less tedious 
than the standard method, and again it's readily automated.

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

I guess what I'm saying is that your instinct about how it ought to be 
is good and can be realised. Indeed it was realised in 1998 and persists 
to this day, but only in experimental systems without the many other 
conveniences and libraries of Coq. I know I haven't done a good enough 
job of exporting that technology, and it would be good to find a way to 
rectify that situation.

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

I'm biased, of course, but also very fortunate to be having the fun of 
programming with dependent types, without the nightmare.

All the best

Conor