Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Dependently-typed binary operators

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Dependently-typed binary operators


chronological Thread 
  • From: Conor McBride <ctm AT cs.nott.ac.uk>
  • To: roconnor AT theorem.ca
  • Cc: Coq Club <coq-club AT pauillac.inria.fr>
  • Subject: Re: [Coq-Club] Dependently-typed binary operators
  • Date: Tue, 13 Sep 2005 21:12:47 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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




Archive powered by MhonArc 2.6.16.

Top of Page